One property test is working, Fixed some awkward PParams values.

alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxo.hs

@@ -65,7 +65,7 @@ import Data.Coders
     (<!),
   )
 import Data.Coerce (coerce)
-import Data.Foldable (toList)
+import Data.Foldable (foldl', toList)
 import qualified Data.Map.Strict as Map
 import Data.Set (Set)
 import qualified Data.Set as Set
@@ -185,7 +185,7 @@ data UtxoPredicateFailure era
   | TriesToForgeADA
   | -- | list of supplied bad transaction outputs
     OutputTooBigUTxO
-      ![Core.TxOut era]
+      ![(Int, Int, Core.TxOut era)]
   | InsufficientCollateral
       !Coin
       -- ^ balance computed
@@ -370,13 +370,14 @@ utxoTransition = do
   -- use serialized length of Value because this Value size is being limited inside a serialized Tx
   let outputs = Map.elems $ unUTxO (txouts @era txb)
       maxValSize = getField @"_maxValSize" pp
-      outputsTooBig =
-        filter
-          ( \out ->
-              let v = getField @"value" out
-               in (fromIntegral . BSL.length . serialize) v > maxValSize
-          )
-          outputs
+      outputsTooBig = foldl' accum [] outputs
+        where
+          accum ans out =
+            let v = getField @"value" out
+                size = (fromIntegral . BSL.length . serialize) v
+             in if size > maxValSize
+                  then (fromIntegral size, fromIntegral maxValSize, out) : ans
+                  else ans
   null outputsTooBig ?! OutputTooBigUTxO outputsTooBig
 
   ni <- liftSTS $ asks networkId

alonzo/test/lib/Test/Cardano/Ledger/Alonzo/AlonzoEraGen.hs

@@ -138,10 +138,8 @@ genAlonzoTxBody _genenv pparams currentslot input txOuts certs wdrls fee updates
   validityInterval <- genValidityInterval currentslot
   return
     ( TxBody
-        -- non fee inputs
-        Set.empty -- TODO do something better here (use genenv ?)
-        -- inputs for fees
         input
+        Set.empty -- collaeral -- TODO do something better here (use genenv ?)
         txouts'
         certs
         wdrls
@@ -176,7 +174,7 @@ genAlonzoPParamsDelta constants pp = do
   price <- genM (Prices <$> (Coin <$> choose (100, 5000)) <*> (Coin <$> choose (100, 5000)))
   mxTx <- genM (ExUnits <$> (choose (100, 5000)) <*> (choose (100, 5000)))
   mxBl <- genM (ExUnits <$> (choose (100, 5000)) <*> (choose (100, 5000)))
-  mxV <- genM (genNatural 1 10000)
+  mxV <- genM (genNatural 4000 5000) -- Not too small
   let c = SJust 150
       mxC = SJust 10
   pure (Alonzo.extendPP shelleypp ada cost price mxTx mxBl mxV c mxC)
@@ -192,7 +190,7 @@ genAlonzoPParams constants = do
   price <- (Prices <$> (Coin <$> choose (100, 5000)) <*> (Coin <$> choose (100, 5000)))
   mxTx <- (ExUnits <$> (choose (100, 5000)) <*> (choose (100, 5000)))
   mxBl <- (ExUnits <$> (choose (100, 5000)) <*> (choose (100, 5000)))
-  mxV <- (genNatural 10000 50000) -- This can't be too small
+  mxV <- pure 10000 -- (genNatural 10000 50000) -- This can't be too small
   let c = 150
       mxC = 10
   pure (Alonzo.extendPP shelleypp ada cost price mxTx mxBl mxV c mxC)
@@ -205,8 +203,9 @@ instance Mock c => EraGen (AlonzoEra c) where
   genEraAuxiliaryData = genAux
   genGenesisValue = maryGenesisValue
   genEraTxBody = genAlonzoTxBody
-  updateEraTxBody txb coinx txin txout =
-    txb {inputs = txin, txfee = coinx, outputs = txout}
+  updateEraTxBody txb coinx txin txout = new
+    where
+      new = txb {inputs = txin, txfee = coinx, outputs = txout}
   genEraPParamsDelta = genAlonzoPParamsDelta
   genEraPParams = genAlonzoPParams
   genEraWitnesses setWitVKey mapScriptWit = TxWitness setWitVKey Set.empty mapScriptWit Map.empty (Redeemers Map.empty)

alonzo/test/test/Test/Cardano/Ledger/Alonzo/Trials.hs

@@ -31,6 +31,7 @@ import Control.State.Transition.Trace.Generator.QuickCheck (HasTrace, forAllTrac
 import Data.Default.Class (Default (def))
 import qualified Data.Map as Map
 import Data.Proxy (Proxy (..))
+import GHC.Natural
 import Shelley.Spec.Ledger.API (ApplyBlock)
 import Shelley.Spec.Ledger.API.Protocol (GetLedgerView)
 import Shelley.Spec.Ledger.API.Validation (ApplyBlock)
@@ -46,6 +47,7 @@ import qualified Test.Cardano.Ledger.Alonzo.Serialisation.Tripping as Tripping
 import qualified Test.Cardano.Ledger.Alonzo.Translation as Translation
 import Test.Cardano.Ledger.EraBuffet (TestCrypto)
 import Test.QuickCheck
+import Test.QuickCheck.Random (mkQCGen)
 import Test.Shelley.Spec.Ledger.ConcreteCryptoTypes (Mock)
 import Test.Shelley.Spec.Ledger.Generator.Block (genBlock)
 import Test.Shelley.Spec.Ledger.Generator.Constants (Constants (..))
@@ -96,6 +98,7 @@ import Test.Shelley.Spec.Ledger.Utils
     testGlobals,
   )
 import Test.Tasty
+import Test.Tasty.QuickCheck
 
 kps = take 10 $ keyPairs @TestCrypto (geConstants ag)
 
@@ -227,3 +230,21 @@ type T = TestCrypto
 
 main :: IO ()
 main = defaultMain tests
+
+cgen = mkQCGen 174256
+
+-- 174256 on 23 try
+-- 2 fails on 5 try
+-- 6 fails on 1st try
+
+go =
+  defaultMain
+    ( localOption
+        (QuickCheckReplay (Just 6))
+        (testProperty "ADA" $ adaPreservationChain @(AlonzoEra TestCrypto))
+    )
+
+maxvalsize :: Natural
+maxvalsize = 10000
+
+testPropertyAdaPreservation = (testProperty "Property test preserves ADA" $ adaPreservationChain @(AlonzoEra TestCrypto))

alonzo/test/test/Tests.hs

@@ -19,18 +19,36 @@ import Test.Cardano.Ledger.Alonzo.Golden as Golden
 import qualified Test.Cardano.Ledger.Alonzo.Serialisation.CDDL as CDDL
 import qualified Test.Cardano.Ledger.Alonzo.Serialisation.Tripping as Tripping
 import qualified Test.Cardano.Ledger.Alonzo.Translation as Translation
+import Test.Cardano.Ledger.Alonzo.Trials (testPropertyAdaPreservation)
 import Test.Cardano.Ledger.EraBuffet (TestCrypto)
 import Test.QuickCheck
 import Test.Shelley.Spec.Ledger.Generator.Constants (Constants (..))
+{-
+import GHC.Records(HasField(..))
+import Test.Shelley.Spec.Ledger.PropertyTests
+  ( adaPreservationChain,
+    -- propertyTests,
+  )
+import Cardano.Ledger.Alonzo.PParams(PParams' (..))
+import Test.Cardano.Ledger.Alonzo.AlonzoEraGen ()
+import Test.Shelley.Spec.Ledger.Generator.Trace.Chain
+import Test.Shelley.Spec.Ledger.Generator.Trace.Chain
+import Test.Shelley.Spec.Ledger.Generator.Trace.Ledger
+import Test.Shelley.Spec.Ledger.Generator.Utxo
+-}
+
 import Test.Tasty
+import Test.Tasty.QuickCheck
 
 -- ====================================================================================
 
 tests :: TestTree
 tests =
   testGroup
     "Alonzo tests"
-    [ Tripping.tests,
+    [ -- testProperty "Property test ada preserved" (adaPreservationChain @(AlonzoEra TestCrypto)),
+      testPropertyAdaPreservation,
+      Tripping.tests,
       Translation.tests,
       CDDL.tests 5,
       Golden.goldenUTxOEntryMinAda,

shelley/chain-and-ledger/shelley-spec-ledger-test/src/Test/Shelley/Spec/Ledger/Generator/EraGen.hs

@@ -189,7 +189,7 @@ type MinGenTxBody era =
     FromCBOR(Annotator (Core.TxBody era)) -- arises because some pattern Constructors deserialize
   )
 
-class MinGenTxout era where
+class Show (Core.TxOut era) => MinGenTxout era where
   calcEraMinUTxO :: Core.TxOut era -> Core.PParams era -> Coin
   addValToTxOut :: Core.Value era -> Core.TxOut era -> Core.TxOut era
   genEraTxOut :: Gen (Core.Value era) -> [Addr (Crypto era)] -> Gen [Core.TxOut era]

shelley/chain-and-ledger/shelley-spec-ledger-test/src/Test/Shelley/Spec/Ledger/Generator/Trace/Ledger.hs

@@ -71,7 +71,7 @@ import Test.Shelley.Spec.Ledger.Utils
     runShelleyBase,
   )
 import Cardano.Ledger.Era(SupportsSegWit(TxInBlock))
-
+import Debug.Trace
 -- ======================================================
 
 genAccountState :: Constants -> Gen AccountState
@@ -179,7 +179,7 @@ instance
                     (TRC (ledgerEnv, (u, dp), tx))
           pure $ case res of
             Left pf ->
-              error ("LEDGERS sigGen: " <> show pf)
+              trace ("\nPF = "++show pf) (error ("LEDGER sigGen: " <> show pf))
             Right (u', dp') ->
               (u', dp', tx : txs)
 

shelley/chain-and-ledger/shelley-spec-ledger-test/src/Test/Shelley/Spec/Ledger/Generator/Utxo.hs

@@ -12,6 +12,8 @@
 {-# LANGUAGE TypeSynonymInstances #-}
 {-# LANGUAGE UndecidableInstances #-}
 
+{-# OPTIONS_GHC -fno-warn-unused-imports #-}  -- TODO FIX ME
+
 module Test.Shelley.Spec.Ledger.Generator.Utxo
   ( genTx,
     Delta (..),
@@ -366,14 +368,16 @@ genNextDelta
         draftSize =
           sum
             [ 5 :: Integer, -- safety net in case the coin or a list prefix rolls over into a larger encoding
-              12 :: Integer, -- TODO the size calculation somehow needs extra buffer when minting tokens
+              --12 :: Integer, -- TODO the size calculation somehow needs extra buffer when minting tokens
+              20 :: Integer, -- TODO the size calculation somehow needs extra buffer when minting tokens  THIS IS NEW FIX ME
               encodedLen (max dfees (Coin 0)) - 1,
               foldr (\a b -> b + encodedLen a) 0 extraInputs,
               encodedLen change,
               encodedLen extraWitnesses
             ]
 
         deltaFee = draftSize <×> Coin (fromIntegral (getField @"_minfeeA" pparams))
+                   <+> Coin (fromIntegral (getField @"_minfeeB" pparams))  -- TODO THIS IS NEW FIX ME
         totalFee = baseTxFee <+> deltaFee :: Coin
         remainingFee = totalFee <-> dfees :: Coin
         changeAmount = getChangeAmount change
@@ -488,7 +492,7 @@ applyDelta
     --fix up the witnesses here?
     -- Adds extraInputs, extraWitnesses, and change from delta to tx
     let txBody = getField @"body" tx
-        outputs' = getField @"outputs" txBody StrictSeq.|> change
+        outputs' = (getField @"outputs" txBody) StrictSeq.|> change
         body2 =
           (updateEraTxBody @era)
             txBody