Add a balanced TxBody specification (#4728)

* Added TxBody example

* Changed type of MemberSpec to use (NonEmpty a) instead of [a]

libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Deleg.hs

@@ -38,10 +38,13 @@ import Test.Cardano.Ledger.Constrained.Conway.PParams (pparamsSpec)
 -- | Specify that some of the rewards in the RDPair's are zero.
 --   without this in the DState, it is hard to generate the ConwayUnRegCert
 --   certificate, since it requires a rewards balance of 0.
+--   We also specify that both reward and deposit are greater thn (Coin 0)
 someZeros :: forall fn. IsConwayUniv fn => Specification fn RDPair
 someZeros = constrained $ \ [var| someRdpair |] ->
-  match someRdpair $ \ [var| reward |] _deposit ->
-    satisfies reward (chooseSpec (1, constrained $ \ [var| x |] -> assert $ x ==. lit 0) (3, TrueSpec))
+  match someRdpair $ \ [var| reward |] [var|deposit|] ->
+    [ satisfies reward (chooseSpec (1, constrained $ \ [var| x |] -> assert $ x ==. lit 0) (3, gtSpec 0))
+    , satisfies deposit (geqSpec 0)
+    ]
 
 dStateSpec ::
   forall fn era. (IsConwayUniv fn, EraSpecDeleg era) => Specification fn (DState era)

libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances/Basic.hs

@@ -91,7 +91,7 @@ makeNonNegativeInterval i j = fromJust (boundRational (i % j))
 instance HasSimpleRep Coin where
   type SimpleRep Coin = Word64
   toSimpleRep (Coin i) = case integerToWord64 i of
-    Nothing -> error "The impossible happened in toSimpleRep for `Coin`"
+    Nothing -> error $ "The impossible happened in toSimpleRep for (Coin " ++ show i ++ ")"
     Just w -> w
   fromSimpleRep = word64ToCoin
 instance BaseUniverse fn => HasSpec fn Coin

libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Pool.hs

@@ -1,8 +1,10 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE ImportQualifiedPost #-}
+{-# LANGUAGE QuasiQuotes #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE ViewPatterns #-}
 
 -- | Specs necessary to generate, environment, state, and signal
 -- for the POOL rule
@@ -46,9 +48,8 @@ pStateSpec = constrained $ \ps ->
         dom_ retiring `subset_` dom_ stakePoolParams
     , assertExplain (pure "dom of deposits is dom of stakePoolParams") $
         dom_ deposits ==. dom_ stakePoolParams
-    , assertExplain (pure "no deposit is 0") $
-        not_ $
-          lit (Coin 0) `elem_` rng_ deposits
+    , forAll (rng_ deposits) $ \ [var|dep|] ->
+        assertExplain (pure "all deposits are greater then (Coin 0)") $ dep >=. lit (Coin 0)
     , assertExplain (pure "dom of stakePoolParams is disjoint from futureStakePoolParams") $
         dom_ stakePoolParams `disjoint_` dom_ futureStakePoolParams
     ]

libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/TxBodySpec.hs

@@ -16,7 +16,7 @@
 
 module Test.Cardano.Ledger.Constrained.Conway.TxBodySpec where
 
--- import Cardano.Ledger.BaseTypes
+import Cardano.Ledger.BaseTypes (Network (..))
 import Cardano.Ledger.Coin
 import Cardano.Ledger.Conway (Conway)
 import Cardano.Ledger.Conway.Rules (CertsEnv (..))
@@ -28,7 +28,7 @@ import Cardano.Ledger.TxIn (TxIn (..))
 import Cardano.Ledger.UTxO (UTxO (..), coinBalance)
 import Cardano.Ledger.Val
 import Constrained hiding (Value)
-import Constrained.Base (Pred (..), hasSize, rangeSize)
+import Constrained.Base
 import Data.Foldable (toList)
 import Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
@@ -52,13 +52,15 @@ import qualified Test.Cardano.Ledger.Generic.Proof as Proof
 import Test.QuickCheck hiding (forAll)
 import Prelude hiding (seq)
 
+import Cardano.Ledger.Address (Withdrawals (..))
 import Cardano.Ledger.Allegra (Allegra)
 import Cardano.Ledger.Alonzo (Alonzo)
 import Cardano.Ledger.Babbage (Babbage)
+import Cardano.Ledger.CertState (lookupDepositDState, lookupDepositVState)
 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 Cardano.Ledger.Shelley.LedgerState (CertState (..), PState (..))
 import Data.Text (pack)
 import Lens.Micro
 import Prettyprinter (sep, vsep)
@@ -122,126 +124,60 @@ subMapSuperDependsOnSub sub super =
         match kvpair $ \k v -> [onJust (lookup_ k super) (\a -> v ==. a)]
     ]
 
-putPretty :: PrettyA t => [Char] -> t -> IO ()
-putPretty nm x = putStrLn (nm ++ "\n" ++ show (prettyA x))
-
-test1 :: IO ()
-test1 = do
-  super <- generate $ genFromSpec @ConwayFn @(Map Int Int) (hasSize (rangeSize 5 7))
-  sub <-
-    generate $
-      genFromSpec @ConwayFn @(Map Int Int)
-        ( constrained $ \sub ->
-            [ assert $ sizeOf_ (dom_ sub) <. sizeOf_ (dom_ (lit super))
-            , subMapSubDependsOnSuper sub (lit super)
-            ]
-        )
-  putPretty "\nsuper" super
-  putPretty "sub" sub
+sumTxOut_ :: forall fn era. EraSpecTxOut era fn => Term fn [TxOut era] -> Term fn Coin
+sumTxOut_ x = foldMap_ (txOutCoin_ @era @fn) x
 
-test2 :: IO ()
-test2 = do
-  sub <- generate $ genFromSpec @ConwayFn @(Map Int Int) (hasSize (rangeSize 4 4))
-  super <-
-    generate $
-      genFromSpec @ConwayFn @(Map Int Int)
-        ( constrained $ \super ->
-            [ subMapSuperDependsOnSub (lit sub) super
-            , assert $ sizeOf_ (dom_ super) ==. 6
-            ]
-        )
-  putPretty "\nsuper" super
-  putPretty "sub" sub
+sumCoin_ :: forall fn. IsConwayUniv fn => Term fn [Coin] -> Term fn Coin
+sumCoin_ x = foldMap_ id x
 
-foo :: IO (Map Int Int, Map Int Int)
-foo = generate $ genFromSpec $ subMap @Int @Int @ConwayFn
+adjustTxOutCoin :: EraTxOut era => DeltaCoin -> TxOut era -> TxOut era
+adjustTxOutCoin (DeltaCoin n) x = x & coinTxOutL .~ ((x ^. coinTxOutL) <+> (Coin n))
 
--- ===================================================================
+-- | Extract the total deposits and refunds from a list of TxCerts.
+--   This a kind of AdaPot relative to the Certs in a Transaction body
+--   It depends on the PParams (deposit ammounts for registering a staking key, a ppol, and registering a Drep)
+--   and on the CertState (what deposits were made in the past)
+getDepositRefund ::
+  forall era. EraTxCert era => PParams era -> CertState era -> [TxCert era] -> (DeltaCoin, DeltaCoin)
+getDepositRefund pp (CertState vs ps ds) certs =
+  ( delta $ getTotalDepositsTxCerts pp (`Map.member` psStakePoolParams ps) certs
+  , delta $ getTotalRefundsTxCerts pp (lookupDepositDState ds) (lookupDepositVState vs) certs
+  )
+  where
+    delta (Coin n) = DeltaCoin n
 
-bodyspec ::
-  forall era fn.
-  ( EraSpecTxOut era fn
-  , EraSpecCert era fn
+-- | This is exactly the same as reify, except it names the existential varaible for better error messages
+reifyX ::
+  ( HasSpec fn a
+  , HasSpec fn b
+  , IsPred p fn
   ) =>
-  UTxO era ->
-  CertsEnv era ->
-  CertState era ->
-  Specification
-    fn
-    ( ShelleyTxBody era
-    , Map (TxIn (EraCrypto era)) (TxOut era)
-    , TxIn (EraCrypto era)
-    )
-bodyspec utxo certsenv certstate =
-  constrained' $ \ [var|shelleyBody|] [var|inputUtxo|] [var|feeInput|] ->
-    match shelleyBody $
-      \ [var|inputs|] [var|outputs|] [var|certs|] [var|rewAcct|] [var|fee|] _ [var|update|] _ ->
-        [ dependsOn shelleyBody fee
-        , dependsOn shelleyBody inputs
-        , dependsOn shelleyBody outputs
-        , dependsOn feeInput inputUtxo
-        , dependsOn inputs inputUtxo
-        , dependsOn outputs inputUtxo
-        , dependsOn fee feeInput
-        , dependsOn outputs inputUtxo
-        , satisfies inputUtxo (hasSize (rangeSize 2 4))
-        , subMapSubDependsOnSuper inputUtxo (lit (unUTxO utxo))
-        , assert $ update ==. lit Nothing
-        , assert $ member_ feeInput (dom_ inputUtxo)
-        , assert $ onJust (lookup_ feeInput (lit (unUTxO utxo))) (\ [var|txout|] -> fee ==. txOutCoin_ txout)
-        , assert $ inputs ==. dom_ inputUtxo
-        , reify inputUtxo (map snd . Map.toList) $
-            \ [var|txouts|] ->
-              [ dependsOn outputs txouts
-              , assert $ (sumCoin_ @fn @era outputs) ==. sumCoin_ @fn @era txouts - fee
-              ]
-        , forAll certs $ \ [var|oneCert|] -> satisfies oneCert (txCertSpec (projectEnv certsenv) certstate)
-        , assert $ sizeOf_ certs <=. 4
-        , assert $ rewAcct ==. lit Map.empty
-        ]
-
-seqToList :: IsConwayUniv fn => HasSpec fn t => Specification fn (Data.Sequence.Internal.Seq t, [t])
-seqToList = constrained' $ \ [var|seq|] [var|list|] -> reify seq toList (\x -> list ==. x)
-
-testUTxO ::
-  forall era. (Era era, HasSpec ConwayFn (TxOut era)) => IO (Map (TxIn (EraCrypto era)) (TxOut era))
-testUTxO =
-  generate $
-    genFromSpec @ConwayFn @(Map (TxIn (EraCrypto era)) (TxOut era)) (hasSize (rangeSize 7 15))
-
--- | Exercise the 'bodyspec'
-go ::
-  forall era.
-  ( EraSpecTxOut era ConwayFn
-  , EraSpecCert era ConwayFn
-  , HasSpec ConwayFn (Tx era)
-  ) =>
-  IO ()
-go = do
-  utxo <- UTxO <$> testUTxO @era
-  certState <-
-    generate $
-      genFromSpec @ConwayFn @(CertState era)
-        (certStateSpec @ConwayFn @era) -- (lit (AccountState (Coin 1000) (Coin 100))) (lit (EpochNo 100)))
-        -- error "STOP"
-  certsEnv <- generate $ genFromSpec @ConwayFn @(CertsEnv era) certsEnvSpec
-
-  (basic, subutxo, feeinput) <-
-    generate $ genFromSpec (bodyspec @era @ConwayFn utxo certsEnv certState)
-
-  putStrLn
-    ("Input UTxO, total " ++ show (coinBalance @era utxo) ++ ", size = " ++ show (Map.size (unUTxO utxo)))
-  putPretty "\nSubMap of Utxo" (UTxO subutxo)
-  putStrLn ("SubMap of UTxO, total Coin " ++ show (coinBalance @era (UTxO subutxo)))
-  putPretty "\nfeeInput" feeinput
-  putPretty "\nTxBody" basic
-
-sumCoin_ :: forall fn era. EraSpecTxOut era fn => Term fn [TxOut era] -> Term fn Coin
-sumCoin_ x = foldMap_ (txOutCoin_ @era @fn) x
+  Term fn a ->
+  (a -> b) ->
+  (Term fn b -> p) ->
+  Pred fn
+reifyX t f body =
+  exists (\eval -> pure $ f (eval t)) $ \ [var|reifyvar|] ->
+    -- NOTE we name the existenital variable 'reifyvar'
+    [ reifies reifyvar t f
+    , toPredExplain (pure ("reifies " ++ show reifyvar)) $ body reifyvar
+    ]
 
--- ===============================================================
+-- =======================================================================
 
-bodyspec2 ::
+-- | This is the first step to generating balanced TxBodies. It illustrates several techniques
+--   1) Generate a tuple of related types. Previously we relied on generating one type and then
+--      passing the actual generated value as the input of the next generator. This is an alternative to that.
+--      But note we still rely partly on the old technique because we take CertsEnv and CertState values as input.
+--   2) Carefully using dependsOn, to make explicit the order the code writer thinks the the variables
+--      should be solved in. This makes failures less mysterious. Because variable ordering failures
+--      are mysterious and hard to solve
+--   3) The use of nested reify (here reifyX which just makes error messages better). This supports
+--      using complicated Haskell functions to extract one random value, from a previous solved variable
+--      using a pure function. Examples of this are 'getDepositRefund' and 'adjustTxOutCoin'
+--   4) How complicated balancing constraints can be solved declaratively, rather than algorithmically
+--      i.e.  toDelta_ (sumTxOut_ @fn @era outputs) ==. inputS + with + refund - deposit - f
+bodyspec ::
   forall era fn.
   ( EraSpecTxOut era fn
   , EraSpecCert era fn
@@ -254,49 +190,60 @@ bodyspec2 ::
     , Map (TxIn (EraCrypto era)) (TxOut era)
     , TxIn (EraCrypto era)
     )
-bodyspec2 certsenv certstate =
+bodyspec certsenv certstate =
   constrained' $ \ [var|shelleyBody|] [var|utxo|] [var|feeInput|] ->
     match shelleyBody $
-      \ [var|inputs|] [var|outputs|] [var|certs|] [var|rewAcct|] [var|fee|] _ [var|update|] _ ->
-        [ dependsOn shelleyBody fee
-        , dependsOn shelleyBody (inputs :: Term fn (Set (TxIn (EraCrypto era))))
-        , dependsOn shelleyBody outputs
-        , dependsOn shelleyBody certs
-        , dependsOn utxo inputs
-        , -- , exists (\eval -> undefined) $ \ [var|feeInput|] ->
-          exists (\eval -> pure (Map.restrictKeys (eval utxo) (eval inputs))) $ \ [var|utxosubset|] ->
-            exists (\_eval -> undefined) $ \ [var|tempUtxo|] ->
-              [ dependsOn inputs utxosubset
-              , dependsOn utxo utxosubset
-              , dependsOn feeInput inputs
-              , dependsOn fee utxosubset
-              , 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
-              , assert $ inputs ==. dom_ utxosubset
-              , assert $ onJust (lookup_ feeInput utxosubset) (\ [var|txout|] -> fee ==. txOutCoin_ @era @fn txout)
-              , satisfies (dom_ tempUtxo) (hasSize (rangeSize 8 10))
-              , subMapSuperDependsOnSub utxosubset tempUtxo
-              , assert $ (sumCoin_ @fn @era outputs) ==. sumCoin_ @fn @era (rng_ utxosubset) - fee
-              , forAll outputs $ \x -> txOutCoin_ @era @fn x >=. lit (Coin 0)
-              , reify
-                  (pair_ tempUtxo feeInput)
-                  (\(m, i) -> Map.adjust baz i m)
-                  (\u -> utxo ==. u)
-              ]
-        , assert $ update ==. lit Nothing
-        , forAll certs $ \ [var|oneCert|] -> satisfies oneCert (txCertSpec (projectEnv certsenv) certstate)
-        , assert $ sizeOf_ certs <=. 4
-        , assert $ rewAcct ==. lit Map.empty
-        , assert $ sizeOf_ outputs ==. 4
-        ]
+      \ [var|inputs|] [var|outputs|] [var|certs|] [var|withdrawals|] [var|fee|] _ [var|update|] _ ->
+        exists (\eval -> pure $ Map.restrictKeys (eval utxo) (eval inputs)) $ \ [var|utxosubset|] ->
+          exists (\eval -> pure $ Map.adjust (adjustTxOutCoin (DeltaCoin 0)) (eval feeInput) (eval utxo)) $ \ [var|tempUtxo|] ->
+            [ assert $ update ==. lit Nothing
+            , satisfies utxosubset (hasSize (rangeSize 3 4))
+            , forAll' utxosubset $ \_ [var|out|] -> assert $ txOutCoin_ @era @fn out >. lit (Coin 0)
+            , dependsOn feeInput utxosubset
+            , assert $ member_ feeInput (dom_ utxosubset)
+            , dependsOn fee feeInput
+            , onJust (lookup_ feeInput utxosubset) (\ [var|feeTxout|] -> fee ==. txOutCoin_ @era @fn feeTxout)
+            , dependsOn inputs utxosubset
+            , assert $ inputs ==. dom_ utxosubset
+            , assert $ member_ feeInput inputs
+            , dependsOn tempUtxo utxosubset
+            , satisfies (dom_ tempUtxo) (hasSize (rangeSize 8 10))
+            , subMapSuperDependsOnSub utxosubset tempUtxo
+            , forAll' tempUtxo $ \_ [var|out|] -> assert $ txOutCoin_ @era @fn out >. lit (Coin 0)
+            , -- Certs has no dependencies
+              forAll certs $ \ [var|oneCert|] -> satisfies oneCert (txCertSpec (projectEnv certsenv) certstate)
+            , assert $ sizeOf_ certs ==. 4
+            , -- withdrawals hs no dependencies
+              assert $ sizeOf_ withdrawals ==. lit 2
+            , forAll' withdrawals $ \ [var|acct|] [var|val|] ->
+                [ assert $ val <=. lit (Coin 10)
+                , assert $ val >. lit (Coin 0)
+                , match acct $ \ [var|network|] _ -> assert $ network ==. lit Testnet
+                ]
+            , dependsOn outputs certs
+            , dependsOn outputs fee
+            , dependsOn outputs withdrawals
+            , dependsOn outputs utxosubset
+            , assert $ sizeOf_ outputs ==. 4
+            , forAll outputs $ \ [var|oneoutput|] -> txOutCoin_ @era @fn oneoutput >=. lit (Coin 0)
+            , reifyX (toDelta_ fee) id $ \ [var|f|] ->
+                reifyX (toDelta_ (sumTxOut_ @fn @era (rng_ utxosubset))) id $ \ [var|inputS|] ->
+                  reifyX (toDelta_ (sumCoin_ @fn (rng_ withdrawals))) id $ \ [var|with|] ->
+                    reify' certs (getDepositRefund @era (certsPParams certsenv) certstate) $
+                      \ [var|deposit|] [var|refund|] ->
+                        toDelta_ (sumTxOut_ @fn @era outputs) ==. inputS + with + refund - deposit - f
+            , dependsOn utxo tempUtxo
+            , reifyX
+                (pair_ tempUtxo feeInput)
+                (\(m, i) -> Map.adjust (adjustTxOutCoin (DeltaCoin 0)) i m) -- mimics how we will adjust fee
+                (\ [var|u|] -> utxo ==. u)
+            ]
+
+-- ==============================================================================
+-- Some code to visualize what is happening, this code will disappear eventually
 
-baz :: EraTxOut era => TxOut era -> TxOut era
-baz x = x & coinTxOutL .~ ((x ^. coinTxOutL) <+> (Coin 100))
+putPretty :: PrettyA t => [Char] -> t -> IO ()
+putPretty nm x = putStrLn (nm ++ "\n" ++ show (prettyA x))
 
 go2 ::
   forall era.
@@ -314,7 +261,7 @@ go2 = do
   certsEnv <- generate $ genFromSpec @ConwayFn @(CertsEnv era) certsEnvSpec
 
   (body, utxomap, feeinput) <-
-    generate $ genFromSpec (bodyspec2 @era @ConwayFn certsEnv certState)
+    generate $ genFromSpec (bodyspec @era @ConwayFn certsEnv certState)
   let utxo = UTxO utxomap
       txbody = fromShelleyBody body
 

libs/cardano-ledger-test/src/Test/Cardano/Ledger/Generic/PrettyCore.hs

@@ -2634,7 +2634,7 @@ pcMultiSig h (RequireMOf m _) = ppSexp "MOf" [ppInt m, h]
 pcMultiSig _ _ = error "Impossible: All NativeScripts should have been accounted for"
 
 instance
-  ( AllegraEraScript era
+  ( ShelleyEraScript era
   , Reflect era
   , NativeScript era ~ MultiSig era
   ) =>

libs/constrained-generators/src/Constrained/Base.hs

@@ -1221,6 +1221,7 @@ flattenPred pIn = go (freeVarNames pIn) [pIn]
 
 computeDependencies :: Pred fn -> DependGraph fn
 computeDependencies = \case
+  x@(Exists _ (_v :-> Block [Reifies (V a) _b _, _c])) -> deleteNode (Name a) (computeDependencies x)
   Monitor {} -> mempty
   Subst x t p -> computeDependencies (substitutePred x t p)
   Assert _ t -> computeTermDependencies t
@@ -4794,9 +4795,9 @@ instance BaseUniverse fn => Functions (IntFn fn) fn where
             memberSpecList
               (nub $ mapMaybe (safeSubtract @fn i) (NE.toList es))
               ( NE.fromList
-                  [ "propagateSpecFn on Add"
-                  , "Spec is (MemberSpec is), such that can't safely subtract from any i in is"
-                  , "Leads to an empty MemberSpec, and hence this ErrorSpec"
+                  [ "propagateSpecFn on (" ++ show i ++ " +. HOLE)"
+                  , "The Spec is a MemberSpec = " ++ show spec
+                  , "We can't safely subtract " ++ show i ++ " from any choice in the MemberSpec."
                   ]
               )
   propagateSpecFun Negate (NilCtx HOLE) spec = case spec of