Merge pull request #1283 from input-output-hk/jc/fix-cddl-group-tests

fixing remaining CDDL tests

.buildkite/default.nix

@@ -1,8 +1,7 @@
 { pkgs ? import ../nix {}
-, commonLib ? pkgs.commonLib
 }:
 
-commonLib.haskellBuildUtils.stackRebuild {
+pkgs.haskellBuildUtils.stackRebuild {
   script = ./rebuild.hs;
   buildTools = [];
   libs = ps: [];

nix/haskell.nix

@@ -3,6 +3,7 @@
 ############################################################################
 { lib
 , stdenv
+, pkgs
 , haskell-nix
 , buildPackages
 , config ? {}
@@ -23,8 +24,9 @@ let
         packages.cs-blockchain.configureFlags = [ "--ghc-option=-Werror" ];
         packages.cs-ledger.configureFlags = [ "--ghc-option=-Werror" ];
         packages.delegation.configureFlags = [ "--ghc-option=-Werror" ];
-        packages.non-integer.configureFlags = [ "--ghc-option=-Werror" ];
+        packages.shelley-spec-non-integral.configureFlags = [ "--ghc-option=-Werror" ];
         packages.small-steps.configureFlags = [ "--ghc-option=-Werror" ];
+        packages.shelley-spec-ledger.components.tests.shelley-spec-ledger-test.build-tools = [pkgs.cddl pkgs.cbor-diag];
         enableLibraryProfiling = profiling;
         # Disable doctests for now (waiting for https://github.com/input-output-hk/haskell.nix/pull/427):
         packages.small-steps.components.tests.doctests.buildable = lib.mkForce false;

nix/pkgs.nix

@@ -4,6 +4,7 @@ pkgs: _: with pkgs; {
     inherit config
       lib
       stdenv
+      pkgs
       haskell-nix
       buildPackages
       ;

nix/sources.json

@@ -5,10 +5,10 @@
         "homepage": "https://input-output-hk.github.io/haskell.nix",
         "owner": "input-output-hk",
         "repo": "haskell.nix",
-        "rev": "6a2fe9ae07de5be7d3cf5410af556ce2f06a0a7d",
-        "sha256": "0bj7iivivjlfnhcag1dy0g6asyib8r1hsk1g3n51wpar4grgqyyq",
+        "rev": "8099da8fe035efe49e81a6eb974eea9e5656b9c6",
+        "sha256": "195rldxg6bmhxfrjz0bzqs0099wiq956wv49fz1i6h6rznaxy5y4",
         "type": "tarball",
-        "url": "https://github.com/input-output-hk/haskell.nix/archive/6a2fe9ae07de5be7d3cf5410af556ce2f06a0a7d.tar.gz",
+        "url": "https://github.com/input-output-hk/haskell.nix/archive/8099da8fe035efe49e81a6eb974eea9e5656b9c6.tar.gz",
         "url_template": "https://github.com/<owner>/<repo>/archive/<rev>.tar.gz"
     },
     "iohk-nix": {
@@ -17,10 +17,10 @@
         "homepage": null,
         "owner": "input-output-hk",
         "repo": "iohk-nix",
-        "rev": "083761953f5f74ec12e803aa735b460cde9985c8",
-        "sha256": "16xdndn57br83ayq9xj7f0f7milwqgr5c2sak3ps033n4ndxfsxg",
+        "rev": "30cf81c421d7fca198660e1e995038dd8b6f3d13",
+        "sha256": "0sy9gza5gsrbqfbizp0dd98njnymigchj0aszswkfzxndskknarj",
         "type": "tarball",
-        "url": "https://github.com/input-output-hk/iohk-nix/archive/083761953f5f74ec12e803aa735b460cde9985c8.tar.gz",
+        "url": "https://github.com/input-output-hk/iohk-nix/archive/30cf81c421d7fca198660e1e995038dd8b6f3d13.tar.gz",
         "url_template": "https://github.com/<owner>/<repo>/archive/<rev>.tar.gz"
     }
 }

shell.nix

@@ -18,9 +18,9 @@ let
     packages = ps: with ps; [
       cs-blockchain
       cs-ledger
-      non-integer
+      shelley-spec-non-integral
       small-steps
-      delegation
+      shelley-spec-ledger
     ];
 
     # These programs will be available inside the nix-shell.

shelley/chain-and-ledger/cddl-spec

@@ -0,0 +1 @@
+executable-spec/cddl-files/

shelley/chain-and-ledger/cddl-spec/shelley.cddl → shelley/chain-and-ledger/executable-spec/cddl-files/shelley.cddl

@@ -2,10 +2,12 @@
 
 block =
   [ header
-  , transaction_bodies         : [* transaction_body]  ; 19
-  , transaction_witness_sets   : [* transaction_witness_set] ; 20
+  , transaction_bodies         : [* transaction_body]
+  , transaction_witness_sets   : [* transaction_witness_set]
   , transaction_metadata_set   : { * transaction_index => transaction_metadata }
-  ]
+  ]; Valid blocks must also satisfy the following two constraints:
+   ; 1) the length of transaction_bodies and transaction_witness_sets must be the same
+   ; 2) every transaction_index must be strictly smaller than the length of transaction_bodies
 
 transaction = [transaction_body, transaction_witness_set, [?transaction_metadata]]
 

shelley/chain-and-ledger/executable-spec/shelley-spec-ledger.cabal

@@ -5,6 +5,10 @@ author:              IOHK Formal Methods Team
 maintainer:          formal.methods@iohk.io
 build-type:          Simple
 cabal-version:       >=1.8
+extra-source-files:
+  cddl-files/shelley.cddl
+  cddl-files/mock/crypto.cddl
+  cddl-files/mock/finset.cddl
 
 source-repository head
   type: git

shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/BlockChain.hs

@@ -7,6 +7,7 @@
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE NamedFieldPuns #-}
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE Rank2Types #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TypeApplications #-}
@@ -17,7 +18,7 @@ module Shelley.Spec.Ledger.BlockChain
   , BHBody(..)
   , BHeader(..)
   , Block(..)
-  , ProtVer(..)
+  , LaxBlock(..)
   , TxSeq(..)
   , bhHash
   , bbHash
@@ -54,8 +55,8 @@ import           GHC.Generics (Generic)
 import           Numeric.Natural (Natural)
 import           Shelley.Spec.Ledger.MetaData (MetaData)
 
-import           Cardano.Binary (FromCBOR (fromCBOR), ToCBOR (toCBOR), decodeListLen, encodeListLen,
-                     matchSize, serializeEncoding')
+import           Cardano.Binary (Decoder, FromCBOR (fromCBOR), ToCBOR (toCBOR), decodeListLen,
+                     encodeListLen, matchSize, serializeEncoding')
 import           Cardano.Crypto.Hash (SHA256)
 import qualified Cardano.Crypto.Hash.Class as Hash
 import qualified Cardano.Crypto.VRF.Class as VRF
@@ -69,7 +70,8 @@ import           Shelley.Spec.Ledger.EpochBoundary (BlocksMade (..))
 import           Shelley.Spec.Ledger.Keys (Hash, KESig, KeyHash, VKey, VRFValue (..), hash, hashKey,
                      hashKeyVRF)
 import           Shelley.Spec.Ledger.OCert (OCert (..))
-import           Shelley.Spec.Ledger.PParams (ActiveSlotCoeff, activeSlotLog, activeSlotVal)
+import           Shelley.Spec.Ledger.PParams (ActiveSlotCoeff, ProtVer (..), activeSlotLog,
+                     activeSlotVal)
 import           Shelley.Spec.Ledger.Serialization (CBORGroup (..), CBORMap (..), CborSeq (..),
                      FromCBORGroup (..), ToCBORGroup (..))
 import           Shelley.Spec.Ledger.Slot (BlockNo (..), SlotNo (..))
@@ -162,26 +164,6 @@ instance Crypto crypto
      sig <- fromCBOR
      pure $ BHeader bhb sig
 
-data ProtVer = ProtVer Natural Natural Natural
-  deriving (Show, Eq, Generic, Ord)
-  deriving ToCBOR via (CBORGroup ProtVer)
-
-instance NoUnexpectedThunks ProtVer
-
-instance ToCBORGroup ProtVer where
-  toCBORGroup (ProtVer x y z) =
-          toCBOR x
-       <> toCBOR y
-       <> toCBOR z
-  listLen _ = 3
-
-instance FromCBORGroup ProtVer where
-  fromCBORGroup = do
-    x <- fromCBOR
-    y <- fromCBOR
-    z <- fromCBOR
-    pure $ ProtVer x y z
-
 data BHBody crypto = BHBody
   { -- | Hash of the previous block header
     bheaderPrev           :: HashHeader crypto
@@ -285,33 +267,46 @@ instance Crypto crypto
         <> toCBORGroup h
         <> toCBORGroup txns
 
-instance Crypto crypto
-  => FromCBOR (Block crypto)
- where
-  fromCBOR = do
-    n <- decodeListLen
-    header <- fromCBORGroup
-    matchSize "Block" ((fromIntegral . toInteger . listLen) header + 3) n
-    bodies <- unwrapCborSeq <$> fromCBOR
-    wits <- unwrapCborSeq <$> fromCBOR
-    let b = length bodies
-        w = length wits
-
-    metadata <- constructMetaData b . unwrapCBORMap <$> fromCBOR
-    let m = length metadata
-
-    unless (b == w)
+blockDecoder :: Crypto crypto => Bool -> forall s. Decoder s (Block crypto)
+blockDecoder lax = do
+  n <- decodeListLen
+  header <- fromCBORGroup
+  matchSize "Block" ((fromIntegral . toInteger . listLen) header + 3) n
+  bodies <- unwrapCborSeq <$> fromCBOR
+  wits <- unwrapCborSeq <$> fromCBOR
+  let b = length bodies
+      w = length wits
+
+  metadata <- constructMetaData b . unwrapCBORMap <$> fromCBOR
+  let m = length metadata
+
+  unless (lax || b == w)
       (fail $ "different number of transaction bodies ("
         <> show b <> ") and witness sets ("
         <> show w <> ")"
       )
-    unless (b == m)
+  unless (lax || b == m)
       (fail $ "mismatch between transaction bodies ("
         <> show b <> ") and metadata ("
         <> show w <> ")"
       )
-    let txns = Seq.zipWith3 cborWitsToTx bodies wits metadata
-    pure $ Block header (TxSeq txns)
+  let txns = Seq.zipWith3 cborWitsToTx bodies wits metadata
+  pure $ Block header (TxSeq txns)
+
+instance Crypto crypto
+  => FromCBOR (Block crypto)
+ where
+  fromCBOR = blockDecoder False
+
+newtype LaxBlock crypto
+  = LaxBlock (Block crypto)
+  deriving (Show, Eq)
+  deriving ToCBOR via (Block crypto)
+
+instance Crypto crypto
+  => FromCBOR (LaxBlock crypto)
+ where
+  fromCBOR = LaxBlock <$> blockDecoder True
 
 bHeaderSize
   :: forall crypto. (Crypto crypto)

shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/PParams.hs

@@ -1,5 +1,7 @@
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE DerivingVia #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE TemplateHaskell #-}
 
@@ -32,6 +34,7 @@ module Shelley.Spec.Ledger.PParams
   , mkActiveSlotCoeff
   , activeSlotVal
   , activeSlotLog
+  , ProtVer(..)
   ) where
 
 import           Cardano.Binary (FromCBOR (..), ToCBOR (..), encodeListLen, enforceSize)
@@ -42,6 +45,8 @@ import           Numeric.Natural (Natural)
 import           Shelley.Spec.Ledger.BaseTypes (FixedPoint, Nonce (NeutralNonce), UnitInterval,
                      fpPrecision, interval0, intervalValue)
 import           Shelley.Spec.Ledger.Coin (Coin (..))
+import           Shelley.Spec.Ledger.Serialization (CBORGroup (..), FromCBORGroup (..),
+                     ToCBORGroup (..))
 import           Shelley.Spec.Ledger.Slot (EpochNo (..))
 
 import           Shelley.Spec.NonIntegral (ln')
@@ -89,7 +94,7 @@ data PParams = PParams
     -- | Extra entropy
   , _extraEntropy    :: Nonce
     -- | Protocol version
-  , _protocolVersion :: (Natural, Natural)
+  , _protocolVersion :: ProtVer
   } deriving (Show, Eq, Generic)
 
 data ActiveSlotCoeff =
@@ -133,6 +138,23 @@ activeSlotVal = unActiveSlotVal
 activeSlotLog :: ActiveSlotCoeff -> FixedPoint
 activeSlotLog f = (fromIntegral $ unActiveSlotLog f) / fpPrecision
 
+data ProtVer = ProtVer Natural Natural
+  deriving (Show, Eq, Generic, Ord)
+  deriving ToCBOR via (CBORGroup ProtVer)
+  deriving FromCBOR via (CBORGroup ProtVer)
+
+instance NoUnexpectedThunks ProtVer
+
+instance ToCBORGroup ProtVer where
+  toCBORGroup (ProtVer x y) = toCBOR x <> toCBOR y
+  listLen _ = 2
+
+instance FromCBORGroup ProtVer where
+  fromCBORGroup = do
+    x <- fromCBOR
+    y <- fromCBOR
+    pure $ ProtVer x y
+
 instance NoUnexpectedThunks PParams
 
 instance ToCBOR PParams
@@ -179,7 +201,7 @@ instance ToCBOR PParams
         <> toCBOR activeSlotCoeff'
         <> toCBOR d'
         <> toCBOR extraEntropy'
-        <> toCBOR protocolVersion'
+        <> toCBORGroup protocolVersion'
 
 instance FromCBOR PParams
  where
@@ -205,7 +227,7 @@ instance FromCBOR PParams
       <*> fromCBOR
       <*> fromCBOR
       <*> fromCBOR
-      <*> fromCBOR
+      <*> fromCBORGroup
 
 makeLenses ''PParams
 
@@ -232,5 +254,5 @@ emptyPParams =
      , _activeSlotCoeff = mkActiveSlotCoeff interval0
      , _d = interval0
      , _extraEntropy = NeutralNonce
-     , _protocolVersion = (0, 0)
+     , _protocolVersion = ProtVer 0 0
      }

shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Chain.hs

@@ -32,7 +32,8 @@ import           Shelley.Spec.Ledger.LedgerState (AccountState (..), DPState (..
                      EpochState (..), LedgerState (..), NewEpochState (..), PState (..),
                      UTxOState (..), emptyDState, emptyPState, getGKeys, updateNES, _genDelegs)
 import           Shelley.Spec.Ledger.OCert (KESPeriod)
-import           Shelley.Spec.Ledger.PParams (PParams, _maxBBSize, _maxBHSize, _protocolVersion)
+import           Shelley.Spec.Ledger.PParams (PParams, ProtVer (..), _maxBBSize, _maxBHSize,
+                     _protocolVersion)
 import           Shelley.Spec.Ledger.Slot (BlockNo, EpochNo, SlotNo)
 import           Shelley.Spec.Ledger.Tx (TxBody)
 import           Shelley.Spec.Ledger.Updates (AVUpdate (..), Applications, PPUpdate (..),
@@ -157,7 +158,7 @@ chainTransition = do
   let NewEpochState _ _ _ (EpochState _ _ _ pp) _ _ _ = nes
 
   maxpv <- liftSTS $ asks maxMajorPV
-  let (m, _) = _protocolVersion pp
+  let (ProtVer m _) = _protocolVersion pp
   m <= maxpv ?! ObsoleteNodeCHAIN m maxpv
 
   let bhb = bhbody bh

shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ppup.hs

@@ -24,7 +24,6 @@ import           Data.Typeable (Typeable)
 import           Data.Word (Word8)
 import           GHC.Generics (Generic)
 import           Ledger.Core (dom, (⊆), (⨃))
-import           Numeric.Natural (Natural)
 import           Shelley.Spec.Ledger.BaseTypes
 import           Shelley.Spec.Ledger.Keys
 import           Shelley.Spec.Ledger.PParams
@@ -104,8 +103,8 @@ instance
       5 -> matchSize "PVCannotFollowPPUP" 1 n >> pure PVCannotFollowPPUP
       k -> invalidKey k
 
-pvCanFollow :: (Natural, Natural) -> Ppm -> Bool
-pvCanFollow (m, n) (ProtocolVersion (m', n'))
+pvCanFollow :: ProtVer -> Ppm -> Bool
+pvCanFollow (ProtVer m n) (ProtocolVersion (ProtVer m' n'))
   = (m+1, 0) == (m', n') || (m, n+1) == (m', n')
 pvCanFollow _ _ = True