From 8020d12b42431f15f617c04ec67fc2a960a8019f Mon Sep 17 00:00:00 2001 From: Jack Hodgkinson <30505104+jhodgdev@users.noreply.github.com> Date: Tue, 12 Apr 2022 13:44:05 +0100 Subject: [PATCH] more work on treasury testing! --- agora-test/Spec.hs | 10 ++ agora-test/Spec/Model/Treasury.hs | 253 ++++++++++++++++++++++++------ agora/Agora/AuthorityToken.hs | 36 +++-- agora/Agora/Treasury.hs | 3 +- flake.lock | 8 +- flake.nix | 2 +- 6 files changed, 248 insertions(+), 64 deletions(-) diff --git a/agora-test/Spec.hs b/agora-test/Spec.hs index 6442ae8..37a6267 100644 --- a/agora-test/Spec.hs +++ b/agora-test/Spec.hs @@ -1,3 +1,5 @@ +{-# OPTIONS_GHC -Wwarn #-} + -------------------------------------------------------------------------------- import Prelude @@ -9,6 +11,7 @@ import Test.Tasty (defaultMain, testGroup) -------------------------------------------------------------------------------- import Spec.Model.MultiSig qualified as MultiSig +import Spec.Model.Treasury qualified as Treasury import Spec.Stake qualified as Stake -- | The Agora test suite. @@ -28,4 +31,11 @@ main = , MultiSig.genTests ] ] + , testGroup + "Treasury tests" + [ testGroup + "Treasury" + [ Treasury.genTests + ] + ] ] diff --git a/agora-test/Spec/Model/Treasury.hs b/agora-test/Spec/Model/Treasury.hs index d09a456..b9d81a5 100644 --- a/agora-test/Spec/Model/Treasury.hs +++ b/agora-test/Spec/Model/Treasury.hs @@ -1,64 +1,97 @@ {-# OPTIONS_GHC -Wwarn #-} -module Spec.Model.Treasury ( - ) where +{- | +Module: Spec.Model.Treasury +Description: `apropos-tx` tests for Treasury validator. +Maintainer: jack@mlabs.city +This module contains `apropos-tx` tests for ensuring that +the `Agora.Treasury` validator acts as desired. Notes on desired +behaviour and invluded in this description. + +A Treasury transaction should pass if: + + 1. A GAT is burned. + + 2. All GATs are valid. + + 3. The script purpose is Minting. + +If either of these things do /not/ hold, then the transaction +should fail. +-} +module Spec.Model.Treasury ( + plutarchTests, + genTests, +) where + +import Agora.Treasury ( + PTreasuryDatum (PTreasuryDatum), + PTreasuryRedeemer (PAlterTreasuryParams), + treasuryValidator, + ) import Apropos ( Apropos (Apropos), + Contract, Enumerable (enumerated), Formula ( - ExactlyOne, Not, + Some, Var, Yes, - (:&&:), - (:->:) + (:&&:) ), Gen, HasLogicalModel (satisfiesProperty), HasParameterisedGenerator (parameterisedGenerator), + HasPermutationGenerator (buildGen, generators), LogicalModel (logic), + Morphism (Morphism, contract, match, morphism, name), + add, runGeneratorTestsWhere, (:+), ) +import Apropos.Gen.Contexts (scriptContext, txInInfo) +import Apropos.Gen.Value (currencySymbol) import Apropos.Script (ScriptModel (expect, runScriptTestsWhere, script)) -import Data.Maybe (fromMaybe) import Data.Set (Set) +import Plutarch.Api.V1 (PCurrencySymbol, PScriptContext) +import Plutarch.Builtin (pforgetData) import Plutus.V1.Ledger.Address (Address (addressCredential)) import Plutus.V1.Ledger.Contexts ( ScriptContext (scriptContextPurpose, scriptContextTxInfo), ScriptPurpose (Minting), - TxInfo (txInfoMint, txInfoOutputs), + TxInInfo (txInInfoResolved), + TxInfo (txInfoInputs, txInfoMint, txInfoOutputs), TxOut (txOutAddress, txOutValue), ) import Plutus.V1.Ledger.Credential (Credential (PubKeyCredential, ScriptCredential)) -import Plutus.V1.Ledger.Scripts (ValidatorHash (ValidatorHash)) -import Plutus.V1.Ledger.Value (CurrencySymbol, TokenName (unTokenName), Value (getValue)) -import PlutusTx.AssocMap (Map, elems, keys) -import PlutusTx.AssocMap qualified as AssocMap (all, lookup) +import Plutus.V1.Ledger.Scripts (Script, ValidatorHash (ValidatorHash)) +import Plutus.V1.Ledger.Value ( + CurrencySymbol (CurrencySymbol), + TokenName (unTokenName), + Value (Value, getValue), + ) +import PlutusTx.AssocMap (Map, elems, fromList, keys, singleton, toList, unionWith) +import PlutusTx.AssocMap qualified as AssocMap (lookup) import Test.Tasty (TestTree, testGroup) import Test.Tasty.Hedgehog (fromGroup) -{- - -A Treasury transaction should pass if: - -1. A GAT is burned. -2. All GATs are valid. - -If either of these things do _not_ hold, then the transaction -should fail. - --} - data TreasuryTxProp = GATIsBurned - | GATIsNotBurned | AllGATsValid - | SomeGATsInvalid - | ScriptPurposeIsNotMinting + | ScriptPurposeIsMinting deriving stock (Show, Eq, Ord, Enum, Bounded) +instance LogicalModel TreasuryTxProp where + logic :: Formula TreasuryTxProp + logic = + Some + [ Var GATIsBurned + , Var AllGATsValid + , Var ScriptPurposeIsMinting + ] + data TreasuryTxModel = TreasuryTxModel { gatCs :: CurrencySymbol , ctx :: ScriptContext @@ -69,12 +102,6 @@ instance Enumerable TreasuryTxProp where enumerated :: [TreasuryTxProp] enumerated = [minBound .. maxBound] -instance LogicalModel TreasuryTxProp where - logic :: Formula TreasuryTxProp - logic = - ExactlyOne [Var GATIsBurned, Var GATIsNotBurned] - :&&: Var SomeGATsInvalid :->: Not (Var AllGATsValid) - isMinting :: ScriptPurpose -> Bool isMinting (Minting _) = True isMinting _ = False @@ -113,30 +140,158 @@ instance HasLogicalModel TreasuryTxProp TreasuryTxModel where Nothing -> 0 Just m -> sum $ elems m in case prop of - GATIsBurned -> csValueSum <= -1 - GATIsNotBurned -> csValueSum >= 0 + GATIsBurned -> csValueSum == -1 AllGATsValid -> all - (authorityTokensValidIn model.gatCs) - txInfo.txInfoOutputs - SomeGATsInvalid -> - any - (not . authorityTokensValidIn model.gatCs) - txInfo.txInfoOutputs - ScriptPurposeIsNotMinting -> not $ isMinting purpose + (authorityTokensValidIn model.gatCs . txInInfoResolved) + txInfo.txInfoInputs + ScriptPurposeIsMinting -> isMinting purpose instance HasParameterisedGenerator TreasuryTxProp TreasuryTxModel where parameterisedGenerator :: Set TreasuryTxProp -> Gen TreasuryTxModel - parameterisedGenerator propSet = do - purpose <- - if ScriptPurposeIsNotMinting `elem` propSet - then undefined - else undefined - undefined + parameterisedGenerator = buildGen baseGen + where + baseGen :: Gen TreasuryTxModel + baseGen = do + cs <- currencySymbol + ctx <- scriptContext + return $ TreasuryTxModel cs ctx + +{- | Updates the `Integer` and `TokenName` for a given + `CurrencySymbol` for a given value. +-} +replaceValue :: + -- | The value whose entry to update. + Value -> + -- | The currency symbol of the entry to update. + CurrencySymbol -> + -- | The token name of the entry to place in the new value. + TokenName -> + -- | The number of tokens to place in the new value. + Integer -> + -- | The updated value. + Value +replaceValue (Value v) cs tn n = Value $ unionWith (\_ x -> x) v v' + where + v' :: Map CurrencySymbol (Map TokenName Integer) + v' = singleton cs $ singleton tn n + +kmap :: (k -> k') -> Map k v -> Map k' v +kmap g = fromList . fmap (\(x, y) -> (g x, y)) . toList + +fixTokenNames :: TxInInfo -> TxInInfo +fixTokenNames inf = + let cred = inf.txInInfoResolved.txOutAddress.addressCredential + val = inf.txInInfoResolved.txOutValue + in case cred of + PubKeyCredential _ -> inf + ScriptCredential (ValidatorHash bs) -> undefined + +-- | TODO: Define. +instance HasPermutationGenerator TreasuryTxProp TreasuryTxModel where + generators :: [Morphism TreasuryTxProp TreasuryTxModel] + generators = + [ Morphism + { name = "Ensure GAT is burned" + , match = Not $ Var GATIsBurned + , contract = add GATIsBurned + , morphism = \m -> + let ctx' = m.ctx + txInfo = ctx'.scriptContextTxInfo + mint = txInfo.txInfoMint + newMint = replaceValue mint m.gatCs "gat" (-1) + in return + m + { ctx = + ctx' + { scriptContextTxInfo = + txInfo + { txInfoMint = newMint + } + } + } + } + , Morphism + { name = "Ensure all GATs are valid" + , match = Not $ Var AllGATsValid + , contract = add AllGATsValid + , {- For every GAT to be considered "valid", their + `TokenName`s have to be equal to the address + of their script. To represent this as a `Morphism`: + + - FOR every UTXO input in the transaction: + - FOR every value in the input: + - IF the currency symbol matches the recognised + GAT currency symbol: + - THEN: set the `TokenName` to be equal to + the UTXO's address. + - ELSE: ignore it. + -} + morphism = \m -> + let ctx' = m.ctx + txInfo = ctx'.scriptContextTxInfo + infoInputs :: [TxInInfo] = txInfo.txInfoInputs + in return $ + m + { ctx = + ctx' + { scriptContextTxInfo = + txInfo + { txInfoInputs = + fixTokenNames <$> infoInputs + } + } + } + } + , Morphism + { name = "Ensure script purpose is minting" + , match = Not $ Var ScriptPurposeIsMinting + , contract = add ScriptPurposeIsMinting + , morphism = \m -> + return + m + { ctx = + m.ctx + { scriptContextPurpose = Minting m.gatCs + } + } + } + ] instance ScriptModel TreasuryTxProp TreasuryTxModel where - expect = undefined - script = undefined + expect :: (TreasuryTxModel :+ TreasuryTxProp) -> Formula TreasuryTxProp + expect _ = + Var GATIsBurned + :&&: Var AllGATsValid + :&&: Var ScriptPurposeIsMinting + + script :: (TreasuryTxModel :+ TreasuryTxProp) -> TreasuryTxModel -> Script + script _ m = compile result + where + result :: Term s POpaque + result = + treasuryValidator cs + # (pforgetData $ pdata d) + # (pforgetData $ pdata r) + # ctx + + cs :: CurrencySymbol + cs = m.gatCs + + d :: Term s PTreasuryDatum + d = pcon $ PTreasuryDatum fields + where + adaStateThread :: Term _ PCurrencySymbol + adaStateThread = pconstant $ CurrencySymbol "" + + fields :: Term _ (PDataRecord '["stateThread" ':= PCurrencySymbol]) + fields = pdcons # (pdata adaStateThread) # pdnil + + r :: Term s PTreasuryRedeemer + r = pcon $ PAlterTreasuryParams pdnil + + ctx :: Term s PScriptContext + ctx = pconstant m.ctx genTests :: TestTree genTests = diff --git a/agora/Agora/AuthorityToken.hs b/agora/Agora/AuthorityToken.hs index dadabe4..70bbe3b 100644 --- a/agora/Agora/AuthorityToken.hs +++ b/agora/Agora/AuthorityToken.hs @@ -69,30 +69,48 @@ newtype AuthorityToken = AuthorityToken are tagged with a TokenName that matches where they live. -} authorityTokensValidIn :: Term s (PCurrencySymbol :--> PTxOut :--> PBool) -authorityTokensValidIn = phoistAcyclic $ +authorityTokensValidIn = phoistAcyclic $ -- /Lift/ the `Term`. plam $ \authorityTokenSym txOut'' -> P.do + -- Extract the desired fields: address and value, from the + -- transaction output info. PTxOut txOut' <- pmatch txOut'' txOut <- pletFields @'["address", "value"] $ txOut' PAddress address <- pmatch txOut.address PValue value' <- pmatch txOut.value PMap value <- pmatch value' + + -- Search the transaction output info's value for the + -- provided currency symbol for the authority token. pmatch (plookup # pdata authorityTokenSym # value) $ \case + -- In the case of `PNothing`, no GATs exist at this output + -- and ipso facto they are all valid. + PNothing -> pconstant True + -- This is the case wherein a TokenName/Integer map /has/ + -- been found for the given currency symbol. PJust (pfromData -> tokenMap') -> + -- Now we need to look at the transaction output's + -- address. pmatch (pfield @"credential" # address) $ \case - PPubKeyCredential _ -> - -- GATs should only be sent to Effect validators - pconstant False + -- GATs should only be sent to Effect validators, + -- therefore we consider this invalid and return False. + PPubKeyCredential _ -> pconstant False + -- This is a script address. We need to ensure that + -- the the `TokenName`s associated with the given + -- currency symbol are all equal to this script + -- address. PScriptCredential ((pfromData . (pfield @"_0" #)) -> cred) -> P.do + -- Unwrap the `TokenName`/`Integer` map. PMap tokenMap <- pmatch tokenMap' + + -- Check that the `TokenName` is equal to the validator + -- hash for all of the `TokenName` keys in the map. pall # plam - ( \pair -> - pforgetData (pfstBuiltin # pair) #== pforgetData (pdata cred) + ( \tnMap -> + pforgetData (pfstBuiltin # tnMap) + #== pforgetData (pdata cred) ) # tokenMap - PNothing -> - -- No GATs exist at this output! - pconstant True -- | Assert that a single authority token has been burned. singleAuthorityTokenBurned :: diff --git a/agora/Agora/Treasury.hs b/agora/Agora/Treasury.hs index 3f48a1f..8e12a07 100644 --- a/agora/Agora/Treasury.hs +++ b/agora/Agora/Treasury.hs @@ -57,7 +57,8 @@ treasuryValidator gatCs' = plam $ \datum redeemer ctx' -> P.do gatCs <- plet $ pconstant gatCs' - passert "A single authority token has been burned" $ singleAuthorityTokenBurned gatCs txInfo' mint + passert "A single authority token has been burned" $ + singleAuthorityTokenBurned gatCs txInfo' mint popaque $ pconstant () diff --git a/flake.lock b/flake.lock index de979be..bfdf259 100644 --- a/flake.lock +++ b/flake.lock @@ -103,17 +103,17 @@ "plutus": "plutus" }, "locked": { - "lastModified": 1649421738, - "narHash": "sha256-07LdyHykRDObI984W04lIXgvh6sWKDEW8enAGhIijQU=", + "lastModified": 1649673880, + "narHash": "sha256-LpR+F+fHB6Mh1NHI2O+3zeeSE+ZzyVBwuP9T12X3rek=", "owner": "mlabs-haskell", "repo": "apropos-tx", - "rev": "5257325e3dd2603d09c0ebe468eec676eeb233b8", + "rev": "dd292b49a29f8a259bdc3e35cf4ab1dbbc73582f", "type": "github" }, "original": { "owner": "mlabs-haskell", "repo": "apropos-tx", - "rev": "5257325e3dd2603d09c0ebe468eec676eeb233b8", + "rev": "dd292b49a29f8a259bdc3e35cf4ab1dbbc73582f", "type": "github" } }, diff --git a/flake.nix b/flake.nix index eae71ab..f3dacca 100644 --- a/flake.nix +++ b/flake.nix @@ -19,7 +19,7 @@ # inputs to follow a commit on those master branches. For more # info, see: https://github.com/mlabs-haskell/apropos-tx/pull/37 inputs.apropos-tx.url = - "github:mlabs-haskell/apropos-tx?rev=5257325e3dd2603d09c0ebe468eec676eeb233b8"; + "github:mlabs-haskell/apropos-tx?rev=dd292b49a29f8a259bdc3e35cf4ab1dbbc73582f"; inputs.apropos-tx.inputs.nixpkgs.follows = "plutarch/haskell-nix/nixpkgs-unstable"; inputs.apropos.url =