(NonEmpty x) in MemberSpec (#4712)

* Changed type of MemberSpec to use (NonEmpty a) instead of [a]
IntersectMBO · Oct 26, 2024 · 0ae0b17 · 0ae0b17
1 parent d62d17d
commit 0ae0b17
Show file tree

Hide file tree

Showing 8 changed files with 271 additions and 132 deletions.
diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances/Ledger.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances/Ledger.hs
@@ -145,6 +145,7 @@ import Data.Coerce
 import Data.Foldable
 import Data.Int
 import Data.Kind
+import Data.List.NonEmpty qualified as NE
 import Data.Map (Map)
 import Data.Map.Strict qualified as Map
 import Data.Maybe
@@ -173,7 +174,7 @@ import Test.Cardano.Ledger.TreeDiff (ToExpr)
 import Test.Cardano.Slotting.Numeric ()
 import Test.QuickCheck hiding (Args, Fun, forAll)
 
--- EpochNo Num instance
+-- ==========================================================
 
 type ConwayUnivFns = CoinFn : CoerceFn : StringFn : MapFn : FunFn : TreeFn : BaseFns
 type ConwayFn = Fix (OneofL ConwayUnivFns)
@@ -1758,7 +1759,7 @@ instance (Typeable fn, Member (CoinFn fn) fn) => Functions (CoinFn fn) fn where
               (mapList (\(C.Value a) -> Lit a) pre)
               (x' :> mapList (\(C.Value a) -> Lit a) suf)
        in Let (App (injectFn fn) args) (x :-> p)
-  propagateSpecFun ToDelta (NilCtx HOLE) (MemberSpec xs) = MemberSpec (map deltaToCoin xs)
+  propagateSpecFun ToDelta (NilCtx HOLE) (MemberSpec xs) = MemberSpec (NE.map deltaToCoin xs)
   propagateSpecFun ToDelta (NilCtx HOLE) (TypeSpec (NumSpecInterval l h) cant) =
     ( TypeSpec
         (NumSpecInterval (fromIntegral <$> l) (fromIntegral <$> h))

diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/TxBodySpec.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/TxBodySpec.hs
@@ -57,6 +57,7 @@ import Cardano.Ledger.Alonzo (Alonzo)
 import Cardano.Ledger.Babbage (Babbage)
 import Cardano.Ledger.Mary (Mary)
 import Cardano.Ledger.Shelley (Shelley)
+import Cardano.Ledger.Shelley.AdaPots (Consumed (..), Produced (..), consumedTxBody, producedTxBody)
 import Cardano.Ledger.Shelley.LedgerState (CertState)
 import Data.Text (pack)
 import Lens.Micro
@@ -272,6 +273,7 @@ bodyspec2 certsenv certstate =
               , dependsOn fee feeInput
               , dependsOn outputs utxosubset
               , dependsOn outputs fee
+              , dependsOn outputs certs
               , dependsOn utxo tempUtxo
               , satisfies utxosubset (hasSize (rangeSize 3 4))
               , assert $ member_ feeInput inputs
@@ -314,9 +316,12 @@ go2 = do
   (body, utxomap, feeinput) <-
     generate $ genFromSpec (bodyspec2 @era @ConwayFn certsEnv certState)
   let utxo = UTxO utxomap
+      txbody = fromShelleyBody body
 
   putStrLn
     ("Input UTxO, total " ++ show (coinBalance @era utxo) ++ ", size = " ++ show (Map.size utxomap))
   putPretty "UTxO" utxo
   putPretty "\nfeeInput" feeinput
-  putStrLn (show (pcTxBodyWithUTxO utxo (fromShelleyBody body)))
+  putStrLn (show (pcTxBodyWithUTxO utxo txbody))
+  print (consumedTxBody txbody (certsPParams certsEnv) certState utxo)
+  print (producedTxBody txbody (certsPParams certsEnv) certState)