Limited tree size

IntersectMBO · Apr 23, 2024 · 1cc78b5 · 1cc78b5
1 parent 8109a16
commit 1cc78b5
Showing 1 changed file with 15 additions and 5 deletions.
diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway.hs
@@ -41,6 +41,7 @@ import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway (
  )
 import Test.Cardano.Ledger.Constrained.Conway (
   IsConwayUniv,
+  ProposalTree,
   govEnvSpec,
   govProceduresSpec,
   govProposalsSpec,
@@ -186,6 +187,10 @@ agdaCompatibleProposal prop =
       (branch $ \_ _ -> True)
       (branch $ const True)
 
+limitTreeSize :: IsConwayUniv fn => Term fn ProposalTree -> Pred fn
+limitTreeSize proptree = match proptree $ \_ trees ->
+  forAll trees $ \tree -> genHint (Just 3, 1) tree
+
 instance
   ( NFData (SpecRep (ConwayGovPredFailure Conway))
   , IsConwayUniv fn
@@ -199,11 +204,16 @@ instance
   stateSpec env = govProposalsSpec env <> constrained agdaConstraints
     where
       agdaConstraints :: Term fn (Proposals Conway) -> Pred fn
-      agdaConstraints props = match @fn props $ \ppups _ _ _ _ ->
-        match ppups $ \_ ppupForest ->
-          forAll ppupForest $ \ppupTree ->
-            forAll' ppupTree $ \gas _ ->
-              match gas $ \_ _ _ _ prop _ _ -> agdaCompatibleProposal prop
+      agdaConstraints props = match @fn props $
+        \ppups ppuTree hfTree committeeTree _ ->
+          [ match ppups $ \_ ppupForest ->
+              forAll ppupForest $ \ppupTree ->
+                forAll' ppupTree $ \gas _ ->
+                  match gas $ \_ _ _ _ prop _ _ -> agdaCompatibleProposal prop
+          , limitTreeSize ppuTree
+          , limitTreeSize hfTree
+          , limitTreeSize committeeTree
+          ]
 
   signalSpec env st = govProceduresSpec env st <> constrained agdaConstraints
     where