diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Deleg.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Deleg.hs index 5c359b185b4..e0b3bacdaa4 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Deleg.hs +++ b/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) diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances/Basic.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances/Basic.hs index 22f105b77ea..a7969cadaf0 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances/Basic.hs +++ b/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 diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Pool.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Pool.hs index 6d07b3232d7..e24b3cf7665 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Pool.hs +++ b/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 ] 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 index 548c594bf33..b10f0ff88e7 100644 --- 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 @@ -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 diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Generic/PrettyCore.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Generic/PrettyCore.hs index e46966dfad3..30b29d23713 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Generic/PrettyCore.hs +++ b/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 ) => diff --git a/libs/constrained-generators/src/Constrained/Base.hs b/libs/constrained-generators/src/Constrained/Base.hs index a7d39bfa157..50373c9705f 100644 --- a/libs/constrained-generators/src/Constrained/Base.hs +++ b/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