[#545] Extend the transaction generators to take fees into account

Closes #545

byron/ledger/executable-spec/src/Cardano/Ledger/Spec/STS/UTXOW.hs

@@ -50,6 +50,7 @@ import Ledger.UTxO
   , body
   , fromTxOuts
   , inputs
+  , pcMinFee
   )
 import qualified Ledger.UTxO.Generators as UTxOGen
 
@@ -117,8 +118,8 @@ instance HasTrace UTXOW where
         -- come from we use the hash of the address as transaction id.
         pure $ fromTxOuts txOuts
 
-  sigGen _e st = do
-    tx <- UTxOGen.genTxFromUTxO traceAddrs (utxo st)
+  sigGen UTxOEnv { pps } st = do
+    tx <- UTxOGen.genTxFromUTxO traceAddrs (pcMinFee pps) (utxo st)
     let wits = witnessForTxIn tx (utxo st) <$> inputs tx
     pure $ TxWits tx wits
 

byron/ledger/executable-spec/src/Ledger/UTxO.hs

@@ -50,6 +50,9 @@ data TxOut = TxOut { addr  :: Addr
                    , value :: Lovelace
                    } deriving (Show, Eq, Ord, Generic, Hashable)
 
+instance HasTypeReps TxOut where
+  typeReps o = typeOf o <| empty
+
 -- |The unspent transaction outputs.
 newtype UTxO = UTxO
   { unUTxO :: Map TxIn TxOut
@@ -68,11 +71,7 @@ fromTxOuts = UTxO . Map.fromList . fmap (\out -> (TxIn (mkId out) 0, out))
 data Tx = Tx
   { inputs  :: [TxIn]
   , outputs :: [TxOut]
-  } deriving (Eq, Show, Ord, Generic, Hashable)
-
-instance HasTypeReps Tx where
-  typeReps x@(Tx inputs outputs)
-    = typeOf x <| typeOf inputs <| typeOf outputs <| empty
+  } deriving (Eq, Show, Ord, Generic, Hashable, HasTypeReps)
 
 txid :: Tx -> TxId
 txid = TxId . hash
@@ -105,7 +104,7 @@ instance Ledger.Core.HasHash Tx where
 
 pcMinFee :: PParams -> Tx -> Lovelace
 pcMinFee PParams {_factorA = a, _factorB = b} tx
-  = fromIntegral $ a * txsize tx + b
+  = fromIntegral $ a + b * txsize tx
 
 txsize :: Tx -> Int
 txsize = abstractSize costs

byron/ledger/executable-spec/src/Ledger/UTxO/Generators.hs

@@ -17,7 +17,7 @@ import qualified Hedgehog.Gen as Gen
 import qualified Hedgehog.Range as Range
 
 import Hedgehog.Internal.Gen
-  (atLeast, ensure, mapGenT, runDiscardEffect, toTree, toTreeMaybeT)
+  (atLeast, ensure, mapGenT, runDiscardEffectT, toTree, toTreeMaybeT)
 import Hedgehog.Internal.Tree (NodeT(..), TreeT(..), treeValue)
 import qualified Hedgehog.Internal.Tree as Tree
 
@@ -63,20 +63,29 @@ genTxFromUTxO
   :: [Addr]
   -- ^ List of addresses to choose from as recipients of the transaction
   -- outputs.
+  -> (Tx -> Lovelace)
+  -- ^ Fee calculation
   -> UTxO
   -- ^ UTxO used to determine which unspent outputs can be used in the
   -- transaction.
   -> Gen Tx
-genTxFromUTxO addrs utxo =
-  uncurry Tx <$> Gen.filter
-    (not . null . fst)
-    (genInputOutput
-      (M.keys $ unUTxO utxo)
-      (maybe 0 (unLovelace . value) . flip M.lookup (unUTxO utxo))
-      (fmap (. Lovelace) $ TxOut <$> Gen.element addrs)
-      (unLovelace . value)
-      (\f out -> out { value = Lovelace . f . unLovelace $ value out })
-    )
+genTxFromUTxO addrs txfee utxo = subtractFees txfee $ uncurry Tx <$> Gen.filter
+  (not . null . fst)
+  (genInputOutput
+    (M.keys $ unUTxO utxo)
+    (maybe 0 (unLovelace . value) . flip M.lookup (unUTxO utxo))
+    (fmap (. Lovelace) $ TxOut <$> Gen.element addrs)
+    (unLovelace . value)
+    (\f out -> out { value = Lovelace . f . unLovelace $ value out })
+  )
+
+subtractFees :: (Tx -> Lovelace) -> Gen Tx -> Gen Tx
+subtractFees txfee = fmap subtractFees'
+  . Gen.filter (\tx -> sum (value <$> outputs tx) >= txfee tx)
+ where
+  subtractFees' tx =
+    tx { outputs = subFromList (txfee tx) value updateValue (outputs tx) }
+  updateValue f out = out { value = f (value out) }
 
 -- | A property to test that the entire shrink tree generated by
 --   'genInputOutput' maintains the invariant that the inputs and outputs have
@@ -119,11 +128,11 @@ genInputOutput ins inValue genOut outValue modifyOutValue =
       )
     $ do
         insTree <- toTreeMaybeT (Gen.subsequence ins)
-        case runDiscardEffect insTree of
-          Nothing       -> empty
-          Just insTree' -> (,) <$> pure insTree <*> toTreeMaybeT
+        case treeValue (runDiscardEffectT insTree) of
+          Nothing -> empty
+          Just is -> (,) <$> pure insTree <*> toTreeMaybeT
             (genSplitValue
-              (sum . fmap inValue $ treeValue insTree')
+              (sum $ inValue <$> is)
               genOut
               outValue
               modifyOutValue
@@ -191,20 +200,26 @@ shrinkLeftPreserving inValue outValue modifyOutValue (xs1, ys1) = do
       lost = sum (inValue <$> nodeValue xs1) - sum (inValue <$> nodeValue xs3)
       ys2  = subFromList lost outValue modifyOutValue <$> ys1
     pure $ interleaveInputOutput inValue outValue modifyOutValue (xs3, ys2)
- where
-  subFromList
-    :: Integer
-    -> (a -> Integer)
-    -> ((Integer -> Integer) -> a -> a)
-    -> [a]
-    -> [a]
-  subFromList n getVal modifyVal = go n
-   where
-    go 0  x        = x
-    go _  []       = []
-    go n' (x : xs) = if getVal x > n'
-      then modifyVal (subtract n') x : xs
-      else go (n' - getVal x) xs
+
+-- | Remove total value from a list, removing from the front
+subFromList
+  :: (Num n, Ord n)
+  => n
+  -- The total value to remove from the list
+  -> (a -> n)
+  -- A view into the value contained in type @a@
+  -> ((n -> n) -> a -> a)
+  -- A modifier for the value contained in type @a@
+  -> [a]
+  -- The list of @a@s to remove value from
+  -> [a]
+subFromList n getVal modifyVal = go n
+  where
+  go 0  x        = x
+  go _  []       = []
+  go n' (x : xs) = if getVal x > n'
+    then modifyVal (subtract n') x : xs
+    else go (n' - getVal x) xs
 
 
 -- | A property to check that `genSplitValue` does indeed preserve the input
@@ -238,9 +253,9 @@ genSplitValue n genA getValue modifyValue =
   go 0    acc = pure acc
   go left acc = do
     mTree <- toTreeMaybeT (genA <*> Gen.integral (Range.constant 1 left))
-    case runDiscardEffect mTree of
-      Nothing   -> empty
-      Just tree -> go (left - getValue (treeValue tree)) (mTree : acc)
+    case treeValue (runDiscardEffectT mTree) of
+      Nothing -> empty
+      Just a  -> go (left - getValue a) (mTree : acc)
 
 -- | Used as part of 'genSplitValue', so see there for details of the arguments
 interleaveTreeTPreserving

byron/ledger/executable-spec/src/Ledger/Update/Generators.hs

@@ -70,8 +70,8 @@ pparamsGen =
     <*> Gen.integral (Range.linear (0 :: Natural) 1000) -- scriptVersion
     <*> Gen.integral (Range.linear 0 1000)              -- cfmThd
     <*> Gen.double (Range.constant 0 1)                 -- upAdptThd
-    <*> pure 0                                          -- factor @a@
-    <*> pure 0                                          -- factor @b@
+    <*> Gen.int (Range.linear 0 100)                    -- factor @a@
+    <*> Gen.int (Range.linear 0 10)                     -- factor @b@
  where
   -- | Generates maxBkSz, maxHdrSz, maxTxSz and maxPropSz
   szGen :: Gen (Natural, Natural, Natural, Natural)

byron/ledger/executable-spec/test/Ledger/UTxO/Properties.hs

@@ -3,6 +3,7 @@
 
 module Ledger.UTxO.Properties where
 
+import Control.Lens ((^.))
 import Control.Monad (when)
 import Hedgehog
   ( Property
@@ -18,13 +19,15 @@ import Control.State.Transition.Generator (classifyTraceLength, trace)
 import Control.State.Transition.Trace
   ( TraceOrder(OldestFirst)
   , firstAndLastState
+  , traceEnv
   , traceLength
   , traceSignals
   )
 
-import Cardano.Ledger.Spec.STS.UTXO (reserves, utxo)
+import Cardano.Ledger.Spec.STS.UTXO (pps, reserves, utxo)
 import Cardano.Ledger.Spec.STS.UTXOW (UTXOW)
-import Ledger.UTxO (balance, body, inputs, outputs)
+import Ledger.UTxO
+  (Tx(Tx), TxIn(TxIn), balance, body, inputs, outputs, pcMinFee)
 
 -- | Check that the money is constant in the system.
 moneyIsConstant :: Property
@@ -52,6 +55,20 @@ tracesAreClassified = withTests 200 . property $ do
   let (tl, step) = (500, 50)
   tr <- forAll (trace @UTXOW tl)
   classifyTraceLength tr tl step
+
+  let
+    pparams = pps (tr ^. traceEnv)
+    -- Transaction with one input and one output
+    unitTx = Tx [TxIn undefined undefined] [undefined]
+    unitTxFee = pcMinFee pparams unitTx
+  classify "Unit transaction cost == 0" $ unitTxFee == 0
+  classify "Unit transaction cost == 1" $ unitTxFee == 1
+  classify "Unit transaction cost [2, 5)" $ 2 <= unitTxFee && unitTxFee < 5
+  classify "Unit transaction cost [5, 10)" $ 5 <= unitTxFee && unitTxFee < 10
+  classify "Unit transaction cost [10, 25)" $ 10 <= unitTxFee && unitTxFee < 25
+  classify "Unit transaction cost [25, 100)" $ 25 <= unitTxFee && unitTxFee < 100
+  classify "Unit transaction cost >= 100" $ 100 <= unitTxFee
+
   -- Classify the average number of inputs and outputs. Note that the intervals
   -- were arbitrarily determined, since in order to have a good partition of
   -- the interval [0, maximum possible number of inputs/outputs] we'd need to

byron/ledger/formal-spec/utxo.tex

@@ -82,9 +82,9 @@ \section{UTxO}
       \fun{txbody} & \Tx \to \powerset{\TxIn} \times (\Ix \mapsto \TxOut)
                                   & \text{transaction body}\\
       %
-      \fun{a} & \PPMMap \to \mathbb{Z} & \text{minumum fee factor}\\
+      \fun{a} & \PPMMap \to \mathbb{Z} & \text{minimum fee constant}\\
       %
-      \fun{b} & \PPMMap \to \mathbb{Z} & \text{minumum fee constant}\\
+      \fun{b} & \PPMMap \to \mathbb{Z} & \text{minimum fee factor}\\
       %
       \fun{txSize} & \Tx \to \mathbb{Z} & \text{abstract size of a transaction}\\
       %
@@ -125,7 +125,7 @@ \section{UTxO}
    %
     & \fun{minfee} \in \PPMMap \to \Tx \to \mathbb{Z} & \text{minimum fee}\\
     & \fun{minfee}~\var{pps}~\var{tx} =
-      \fun{a}~\var{pps} * \fun{txSize}~\var{tx} + \fun{b}~\var{pps}
+      \fun{a}~\var{pps} + \fun{b}~\var{pps} * \fun{txSize}~\var{tx}
   \end{align*}
   \caption{Functions used in UTxO rules}
   \label{fig:derived-defs:utxo}

byron/semantics/executable-spec/src/Control/State/Transition/Generator.hs

@@ -146,7 +146,7 @@ genTrace ub env st0 aSigGen = do
         <- toTreeMaybeT $ aSigGen env sti
       let
         --  Take the root of the next-state signal tree.
-        mSig = treeValue <$> runDiscardEffect sigTree
+        mSig = treeValue $ runDiscardEffectT sigTree
       case mSig of
         Nothing ->
           loop (d - 1) sti acc