better TxOuts

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

@@ -28,7 +28,7 @@ import Cardano.Ledger.Conway.PParams
 import Cardano.Ledger.Conway.Rules
 import Cardano.Ledger.Conway.TxCert
 import Cardano.Ledger.Core
-import Cardano.Ledger.Credential (Credential, Ptr)
+import Cardano.Ledger.Credential (Credential, Ptr, StakeCredential, StakeReference (..))
 import Cardano.Ledger.Keys (GenDelegs (..), KeyHash, KeyRole (..))
 import Cardano.Ledger.Mary (MaryValue (..))
 import Cardano.Ledger.Mary.Value (AssetName (..), MultiAsset (..), PolicyID (..))
@@ -281,6 +281,40 @@ correctTxOutB txOut =
         )
     ]
 
+delegatedStakeReference ::
+  (IsConwayUniv fn, Crypto c) =>
+  Term fn (Map (Credential 'Staking c) (KeyHash 'StakePool c)) ->
+  Specification fn (StakeReference c)
+delegatedStakeReference delegs =
+  constrained $ \ref ->
+    caseOn
+      ref
+      (branch $ \base -> member_ base (dom_ delegs))
+      (branch $ \ptr -> TruePred)
+      (branch $ \null -> TruePred)
+
+betterTxOutS ::
+  (EraTxOut era, Value era ~ Coin, IsConwayUniv fn) =>
+  Term fn (Map (Credential 'Staking (EraCrypto era)) (KeyHash 'StakePool (EraCrypto era))) ->
+  Term fn (ShelleyTxOut era) ->
+  Pred fn
+betterTxOutS delegs txOut =
+  match txOut $ \addr v ->
+    [ match v $ \c -> [0 <. c, c <=. fromIntegral (maxBound :: Word64)]
+    , (caseOn addr)
+        ( branch $ \n _ r ->
+            [ assert $ n ==. lit Testnet
+            , satisfies r (delegatedStakeReference delegs)
+            ]
+        )
+        ( branch $ \bootstrapAddr ->
+            match bootstrapAddr $ \_ nm _ ->
+              (caseOn nm)
+                (branch $ \_ -> False)
+                (branch $ \_ -> True)
+        )
+    ]
+
 -- ====================================================================================
 -- The AcountState must have sufficient capacity to support the InstantaneousRewards
 -- So we pass a (Term fn AccountState) as input to 'instantaneousrewardsspec'