Fix various issues in Dijkstra CddlSpec to make all the tests pass

cabal.project

@@ -27,7 +27,7 @@ source-repository-package
 -- NOTE: If you would like to update the above,
 -- see CONTRIBUTING.md#to-update-the-referenced-agda-ledger-spec
 index-state:
-  , hackage.haskell.org 2026-05-06T14:09:41Z
+  , hackage.haskell.org 2026-05-15T10:51:09Z
   , cardano-haskell-packages 2026-04-11T06:29:42Z
 
 packages:
@@ -104,8 +104,8 @@ source-repository-package
   type: git
   location: https://github.com/tweag/cardano-cls.git
   subdir: merkle-tree-incremental mempack-scls scls-cbor scls-cardano scls-format scls-core
-  --sha256: sha256-XY9e1iqr8Kc7PXNKw1KPyJpEOIqIll+1ZrTg6WWhcJU=
-  tag: 310a407f572fd227020b598db5926e44a7365a1b
+  --sha256: sha256-3rAc99T2/MZk7Rd2gb9zq7iUM9hMDOzNvehOq/8hpfs=
+  tag: 8e2bba9442cb388089f53d708cc4aedcb47726ea
 
 constraints:
   -- Happy version 2.2.1 fails to compile haskell-src-exts

eras/alonzo/impl/cardano-ledger-alonzo.cabal

@@ -133,6 +133,7 @@ library cddl
   build-depends:
     base,
     cardano-ledger-alonzo,
+    cardano-ledger-core:cddl,
     cardano-ledger-mary:cddl,
     heredoc,
 

eras/alonzo/impl/cddl/data/alonzo.cddl

@@ -436,7 +436,7 @@ plutus_data =
   / bounded_bytes
 
 constr<a0> =
-  #6.102([uint, [* a0]])
+  #6.101([uint, [* a0]])
   / #6.121([* a0])
   / #6.122([* a0])
   / #6.123([* a0])

eras/alonzo/impl/cddl/lib/Cardano/Ledger/Alonzo/HuddleSpec.hs

@@ -33,6 +33,18 @@ module Cardano.Ledger.Alonzo.HuddleSpec (
 ) where
 
 import Cardano.Ledger.Alonzo (AlonzoEra)
+import Cardano.Ledger.Huddle.Gen (
+  MonadGen (choose),
+  RuleTerm (..),
+  Term (..),
+  genArrayTerm,
+  generateFromGRef,
+  liftAntiGen,
+  listOf,
+  oneof,
+  scale,
+  (|!),
+ )
 import Cardano.Ledger.Mary.HuddleSpec
 import Data.Proxy (Proxy (..))
 import Data.Word (Word64)
@@ -129,19 +141,40 @@ requiredSignersRule pname p = pname =.= huddleRule1 @"set" p (huddleRule @"addr_
 constr :: IsType0 a => Proxy "constr" -> a -> GRuleCall
 constr pname =
   binding $ \x ->
-    pname
-      =.=
-      -- We use 'unType0 . toType0' to convert each 'Tagged ArrayChoice' to 'Choice Type2',
-      -- making the list homogeneous so that 'foldl1 (/)' can be used.
-      -- Ideally, we should have used `toChoice`, but it's not exported by `cuddle`.
-      foldl1
-        (/)
-        ( fmap
-            (unType0 . toType0)
-            ( tag 102 (arr [a VUInt, a $ arr [0 <+ a x]])
-                : [tag t (arr [0 <+ a x]) | t <- [121 .. 127] ++ [1280 .. 1400]]
-            )
-        )
+    withCBORGen (generator x) $
+      pname
+        =.=
+        -- We use 'unType0 . toType0' to convert each 'Tagged ArrayChoice' to 'Choice Type2',
+        -- making the list homogeneous so that 'foldl1 (/)' can be used.
+        -- Ideally, we should have used `toChoice`, but it's not exported by `cuddle`.
+        foldl1
+          (/)
+          ( fmap
+              (unType0 . toType0)
+              ( tag 101 (arr [a VUInt, a $ arr [0 <+ a x]])
+                  : [tag t (arr [0 <+ a x]) | t <- [121 .. 127] ++ [1280 .. 1400]]
+              )
+          )
+  where
+    generator ref = do
+      t <-
+        liftAntiGen $
+          oneof [choose (121, 127), choose (1280, 1400)]
+            |! oneof [choose (0, 120), choose (128, 1279), choose (1401, 0xffffffffffffffff)]
+      let
+        unwrapElems = traverse $ \case
+          SingleTerm e -> pure e
+          _ -> error "Expected single term"
+      elems <-
+        scale (`div` 2) $
+          if t == 101
+            then do
+              uInt <- TInt <$> choose (0, 2 ^ (64 :: Int) - 1)
+              elems <- genArrayTerm =<< unwrapElems =<< listOf (generateFromGRef ref)
+              pure . SingleTerm <$> genArrayTerm [uInt, elems]
+            else listOf $ generateFromGRef ref
+      singleElems <- unwrapElems elems
+      SingleTerm . TTagged t <$> genArrayTerm singleElems
 
 instance HuddleGroup "operational_cert" AlonzoEra where
   huddleGroupNamed = shelleyOperationalCertGroup

eras/babbage/impl/cddl/data/babbage.cddl

@@ -168,7 +168,7 @@ plutus_data =
   / bounded_bytes
 
 constr<a0> =
-  #6.102([uint, [* a0]])
+  #6.101([uint, [* a0]])
   / #6.121([* a0])
   / #6.122([* a0])
   / #6.123([* a0])

eras/conway/impl/CHANGELOG.md

@@ -42,10 +42,13 @@
 
 ### cddl
 
+* Change `maybeTaggedNonemptySet` to take an extra argument for the projection function
+* Add `generateMaybeTaggedSet`
 * Extend `constr` CDDL rule to include tags 1280–1400 for Plutus `Data` constructor indexes
 
 ### `testlib`
 
+* Add `genNonEmptyVotingProcedures`
 * Add to `Test.Cardano.Ledger.Conway.Examples`:
   - `exampleConwayOnwardsEraPParams`
   - `exampleConwayOnwardsEraPParamsUpdate`

eras/conway/impl/cardano-ledger-conway.cabal

@@ -152,6 +152,7 @@ library cddl
     -Wunused-packages
 
   build-depends:
+    QuickCheck,
     base,
     cardano-ledger-babbage:cddl,
     cardano-ledger-conway,

eras/conway/impl/cddl/data/conway.cddl

@@ -213,7 +213,7 @@ plutus_data =
   / bounded_bytes
 
 constr<a0> =
-  #6.102([uint, [* a0]])
+  #6.101([uint, [* a0]])
   / #6.121([* a0])
   / #6.122([* a0])
   / #6.123([* a0])

eras/conway/impl/cddl/lib/Cardano/Ledger/Conway/HuddleSpec.hs

@@ -3,6 +3,7 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE ImportQualifiedPost #-}
+{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE MonoLocalBinds #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE OverloadedLists #-}
@@ -11,6 +12,7 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE ViewPatterns #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
 
 module Cardano.Ledger.Conway.HuddleSpec (
@@ -65,6 +67,7 @@ module Cardano.Ledger.Conway.HuddleSpec (
   maybeTaggedNonemptySet,
   maybeTaggedNonemptyOset,
   conwayCostModelsGenerator,
+  generateMaybeTaggedSet,
 ) where
 
 import Cardano.Ledger.Babbage.HuddleSpec hiding (
@@ -83,21 +86,35 @@ import Cardano.Ledger.Huddle.Gen (
   MonadGen (choose, resize),
   RuleTerm (..),
   Term (..),
+  antiChoose,
+  antiVectorOfUnique,
+  arbitrary,
+  faultyNum,
   genArrayTerm,
   genMapTerm,
   genRule,
+  generateFromGRef,
   liftAntiGen,
   oneof,
   replicateMNorm,
   shuffle,
+  unwrapSingle,
+  unwrapSingleOrError,
+  validateArrayTerm,
+  validateFromGRef,
   withAntiGen,
   (|!),
  )
 import Cardano.Ledger.Huddle.Gen qualified as Gen
+import Control.Monad (unless)
+import Data.Foldable (traverse_)
+import Data.List (nubBy)
+import Data.Maybe (fromMaybe)
 import Data.Proxy (Proxy (..))
 import Data.Traversable (forM)
 import Data.Word (Word64)
 import GHC.TypeLits (KnownSymbol)
+import Test.QuickCheck qualified as QC
 import Text.Heredoc
 import Prelude hiding ((/))
 
@@ -706,18 +723,51 @@ conwayRedeemer pname p =
       , "ex_units" ==> huddleRule @"ex_units" p
       ]
 
+generateMaybeTaggedSet :: Int -> CBORGen Term -> CBORGen Term
+generateMaybeTaggedSet nElems gen = do
+  elems <- fromMaybe QC.discard <$> withAntiGen (antiVectorOfUnique nElems) gen
+  elemsArr <- genArrayTerm elems
+  tagged <- arbitrary
+  if tagged
+    then do
+      t <- liftAntiGen $ faultyNum 258
+      pure $ TTagged t elemsArr
+    else pure elemsArr
+
 mkMaybeTaggedSet ::
-  forall name a. (KnownSymbol name, IsType0 a) => Proxy name -> Word64 -> a -> GRuleCall
-mkMaybeTaggedSet pname n = binding $ \x -> pname =.= tag 258 (arr [n <+ a x]) / sarr [n <+ a x]
+  forall name a.
+  (KnownSymbol name, IsType0 a) => Proxy name -> Int -> (Term -> Term -> Bool) -> a -> GRuleCall
+mkMaybeTaggedSet pname n eq = binding $ \x ->
+  withCBORGen (generator x)
+    . withValidator (validator x)
+    $ pname =.= tag 258 (arr [fromIntegral n <+ a x]) / sarr [fromIntegral n <+ a x]
+  where
+    generator :: GRef -> CBORGen RuleTerm
+    generator ref = do
+      nElems <- liftAntiGen . Gen.sized $ \sz ->
+        let sz' = max n sz in antiChoose (n, sz') (0, sz')
+      fmap SingleTerm . generateMaybeTaggedSet nElems $ unwrapSingleOrError <$> generateFromGRef ref
+    validator ref term = do
+      term_ <- unwrapSingle term
+      let
+        validateInner t = do
+          elems <- validateArrayTerm t
+          unless (length elems == length (nubBy eq elems)) $
+            fail "not all elements are unique"
+          traverse_ (validateFromGRef ref) elems
+      case term_ of
+        TTagged t x | t == 258 -> validateInner x
+        x -> validateInner x
 
 maybeTaggedSet :: IsType0 a => Proxy "set" -> a -> GRuleCall
-maybeTaggedSet pname = mkMaybeTaggedSet pname 0
+maybeTaggedSet pname = mkMaybeTaggedSet pname 0 (==)
 
 maybeTaggedNonemptySet :: IsType0 a => Proxy "nonempty_set" -> a -> GRuleCall
-maybeTaggedNonemptySet pname = mkMaybeTaggedSet pname 1
+maybeTaggedNonemptySet pname = mkMaybeTaggedSet pname 1 (==)
 
-maybeTaggedNonemptyOset :: IsType0 a => Proxy "nonempty_oset" -> a -> GRuleCall
-maybeTaggedNonemptyOset pname = mkMaybeTaggedSet pname 1
+maybeTaggedNonemptyOset ::
+  IsType0 a => Proxy "nonempty_oset" -> (Term -> Term -> Bool) -> a -> GRuleCall
+maybeTaggedNonemptyOset pname eq = mkMaybeTaggedSet pname 1 eq
 
 instance HuddleRule "bounded_bytes" ConwayEra where
   huddleRuleNamed pname _ = boundedBytesRule pname
@@ -1372,7 +1422,7 @@ instance HuddleRule1 "nonempty_set" ConwayEra where
   huddleRule1Named pname _ = maybeTaggedNonemptySet pname
 
 instance HuddleRule1 "nonempty_oset" ConwayEra where
-  huddleRule1Named pname _ = maybeTaggedNonemptyOset pname
+  huddleRule1Named pname _ = maybeTaggedNonemptyOset pname (==)
 
 instance HuddleRule1 "multiasset" ConwayEra where
   huddleRule1Named = conwayMultiasset

eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Arbitrary.hs

@@ -31,6 +31,7 @@ module Test.Cardano.Ledger.Conway.Arbitrary (
   genCommitteeGovAction,
   genConstitutionGovAction,
   genProposals,
+  genNonEmptyVotingProcedures,
   ProposalsNewActions (..),
   ProposalsForEnactment (..),
   ShuffledGovActionStates (..),
@@ -897,3 +898,8 @@ instance Arbitrary (TransitionConfig ConwayEra) where
 deriving newtype instance Arbitrary (Tx TopTx ConwayEra)
 
 deriving newtype instance Arbitrary (ApplyTxError ConwayEra)
+
+genNonEmptyVotingProcedures :: Era era => Gen (VotingProcedures era)
+genNonEmptyVotingProcedures =
+  VotingProcedures . Map.fromList <$> do
+    listOf1 $ (,) <$> arbitrary <*> (Map.fromList <$> listOf1 arbitrary)

eras/dijkstra/impl/CHANGELOG.md

@@ -71,6 +71,7 @@
 
 ### testlib
 
+* Add `genSmallDijkstraBlockBody`
 * Add to `Test.Cardano.Ledger.Dijkstra.Examples`:
   - `exampleDijkstraOnwardsEraPParams`
   - `exampleDijkstraOnwardsEraPParamsUpdate`

eras/dijkstra/impl/cardano-ledger-dijkstra.cabal

@@ -211,16 +211,13 @@ library cddl
     -Wunused-packages
 
   build-depends:
-    QuickCheck,
     antigen,
     base,
     cardano-ledger-conway:cddl,
     cardano-ledger-core:cddl,
     cardano-ledger-dijkstra,
     cborg,
-    cuddle,
     heredoc,
-    quickcheck-transformer,
     text,
 
 executable generate-cddl
@@ -266,6 +263,7 @@ test-suite tests
 
   build-depends:
     base,
+    cardano-data,
     cardano-ledger-alonzo:{cardano-ledger-alonzo, testlib},
     cardano-ledger-babbage:testlib,
     cardano-ledger-binary:testlib,

eras/dijkstra/impl/cddl/data/dijkstra.cddl

@@ -222,7 +222,7 @@ plutus_data =
   / bounded_bytes
 
 constr<a0> =
-  #6.102([uint, [* a0]])
+  #6.101([uint, [* a0]])
   / #6.121([* a0])
   / #6.122([* a0])
   / #6.123([* a0])