agora-spec made independent from agora-test

agora-spec/Spec/AuthorityToken.hs

@@ -0,0 +1,158 @@
+{-# LANGUAGE QuasiQuotes #-}
+
+{- |
+Module     : Spec.AuthorityToken
+Maintainer : emi@haskell.fyi
+Description: Tests for Authority token functions
+
+Tests for Authority token functions
+-}
+module Spec.AuthorityToken (specs) where
+
+--------------------------------------------------------------------------------
+
+import Agora.AuthorityToken (singleAuthorityTokenBurned)
+import Plutarch
+import Prelude
+
+--------------------------------------------------------------------------------
+
+import Plutus.V1.Ledger.Api (
+  Address (Address),
+  Credential (PubKeyCredential, ScriptCredential),
+  CurrencySymbol,
+  Script,
+  TxInInfo (TxInInfo),
+  TxInfo (..),
+  TxOut (TxOut),
+  TxOutRef (TxOutRef),
+  ValidatorHash (ValidatorHash),
+  Value,
+ )
+import Plutus.V1.Ledger.Interval qualified as Interval
+import Plutus.V1.Ledger.Value qualified as Value
+import PlutusTx.AssocMap qualified as AssocMap
+import Spec.Spec (
+  SpecificationTree,
+  group,
+  scriptFails,
+  scriptSucceeds,
+ )
+
+currencySymbol :: CurrencySymbol
+currencySymbol = "deadbeef"
+
+mkTxInfo :: Value -> [TxOut] -> TxInfo
+mkTxInfo mint outs =
+  TxInfo
+    { txInfoInputs = fmap (TxInInfo (TxOutRef "" 0)) outs
+    , txInfoOutputs = []
+    , txInfoFee = Value.singleton "" "" 1000
+    , txInfoMint = mint
+    , txInfoDCert = []
+    , txInfoWdrl = []
+    , txInfoValidRange = Interval.always
+    , txInfoSignatories = []
+    , txInfoData = []
+    , txInfoId = ""
+    }
+
+singleAuthorityTokenBurnedTest :: Value -> [TxOut] -> Script
+singleAuthorityTokenBurnedTest mint outs =
+  let actual :: ClosedTerm PBool
+      actual = singleAuthorityTokenBurned (pconstant currencySymbol) (pconstantData (mkTxInfo mint outs)) (pconstant mint)
+      s :: ClosedTerm POpaque
+      s =
+        pif
+          actual
+          (popaque (pconstant ()))
+          perror
+   in compile s
+
+specs :: [SpecificationTree]
+specs =
+  [ -- This is better suited for plutarch-test
+    group
+      "singleAuthorityTokenBurned"
+      [ scriptSucceeds
+          "Correct simple"
+          ( singleAuthorityTokenBurnedTest
+              ( Value.singleton currencySymbol "deadbeef" (-1)
+                  <> Value.singleton "aa" "USDC" 100_000
+              )
+              [ TxOut
+                  (Address (ScriptCredential (ValidatorHash "deadbeef")) Nothing)
+                  (Value.singleton currencySymbol "deadbeef" 1)
+                  Nothing
+              ]
+          )
+      , scriptSucceeds
+          "Correct many inputs"
+          ( singleAuthorityTokenBurnedTest
+              ( Value.singleton currencySymbol "deadbeef" (-1)
+                  <> Value.singleton "aa" "USDC" 100_000
+              )
+              [ TxOut
+                  (Address (PubKeyCredential "") Nothing)
+                  (Value.singleton "aaabcc" "hello-token" 1)
+                  Nothing
+              , TxOut
+                  (Address (ScriptCredential (ValidatorHash "deadbeef")) Nothing)
+                  (Value.singleton currencySymbol "deadbeef" 1)
+                  Nothing
+              , TxOut
+                  (Address (PubKeyCredential "") Nothing)
+                  (Value.singleton "" "" 1_000_000_000)
+                  Nothing
+              ]
+          )
+      , scriptFails
+          "Incorrect no burn"
+          ( singleAuthorityTokenBurnedTest
+              ( Value.Value AssocMap.empty
+              )
+              []
+          )
+      , scriptFails
+          "Incorrect no GAT burn"
+          ( singleAuthorityTokenBurnedTest
+              ( Value.singleton "aabbcc" "not a GAT!" (-100)
+              )
+              []
+          )
+      , scriptFails
+          "Incorrect script mismatch"
+          ( singleAuthorityTokenBurnedTest
+              ( Value.singleton currencySymbol "i'm not deadbeef!" (-1)
+              )
+              [ TxOut
+                  (Address (ScriptCredential (ValidatorHash "deadbeef")) Nothing)
+                  (Value.singleton currencySymbol "i'm not deadbeef!" 1)
+                  Nothing
+              ]
+          )
+      , scriptFails
+          "Incorrect spent from PK"
+          ( singleAuthorityTokenBurnedTest
+              ( Value.singleton currencySymbol "doesn't matter" (-1)
+              )
+              [ TxOut
+                  (Address (PubKeyCredential "") Nothing)
+                  (Value.singleton currencySymbol "doesn't matter" 1)
+                  Nothing
+              ]
+          )
+      , scriptFails
+          "Incorrect two GATs"
+          ( singleAuthorityTokenBurnedTest
+              ( Value.singleton currencySymbol "deadbeef" (-2)
+                  <> Value.singleton "aa" "USDC" 100_000
+              )
+              [ TxOut
+                  (Address (ScriptCredential (ValidatorHash "deadbeef")) Nothing)
+                  (Value.singleton currencySymbol "deadbeef" 2)
+                  Nothing
+              ]
+          )
+      ]
+  ]

agora-spec/Spec/Effect/GovernorMutation.hs

@@ -0,0 +1,76 @@
+module Spec.Effect.GovernorMutation (specs) where
+
+import Agora.Effect.GovernorMutation (mutateGovernorValidator)
+import Agora.Governor (GovernorDatum (..), GovernorRedeemer (MutateGovernor))
+import Agora.Governor.Scripts (governorValidator)
+import Agora.Proposal (ProposalId (..))
+import Data.Default.Class (Default (def))
+import Plutus.V1.Ledger.Api (ScriptContext (ScriptContext), ScriptPurpose (Spending))
+import Sample.Effect.GovernorMutation (
+  effectRef,
+  govRef,
+  invalidNewGovernorDatum,
+  mkEffectDatum,
+  mkEffectTxInfo,
+  validNewGovernorDatum,
+ )
+import Sample.Shared qualified as Shared
+import Spec.Spec (
+  SpecificationTree,
+  effectFailsWith,
+  effectSucceedsWith,
+  group,
+  validatorFailsWith,
+  validatorSucceedsWith,
+ )
+
+specs :: [SpecificationTree]
+specs =
+  [ group
+      "validator"
+      [ group
+          "valid new governor datum"
+          [ validatorSucceedsWith
+              "governor validator should pass"
+              (governorValidator Shared.governor)
+              ( GovernorDatum
+                  Shared.defaultProposalThresholds
+                  (ProposalId 0)
+                  def
+                  def
+              )
+              MutateGovernor
+              ( ScriptContext
+                  (mkEffectTxInfo validNewGovernorDatum)
+                  (Spending govRef)
+              )
+          , effectSucceedsWith
+              "effect validator should pass"
+              (mutateGovernorValidator Shared.governor)
+              (mkEffectDatum validNewGovernorDatum)
+              (ScriptContext (mkEffectTxInfo validNewGovernorDatum) (Spending effectRef))
+          ]
+      , group
+          "invalid new governor datum"
+          [ validatorFailsWith
+              "governor validator should fail"
+              (governorValidator Shared.governor)
+              ( GovernorDatum
+                  Shared.defaultProposalThresholds
+                  (ProposalId 0)
+                  def
+                  def
+              )
+              MutateGovernor
+              ( ScriptContext
+                  (mkEffectTxInfo invalidNewGovernorDatum)
+                  (Spending govRef)
+              )
+          , effectFailsWith
+              "effect validator should fail"
+              (mutateGovernorValidator Shared.governor)
+              (mkEffectDatum validNewGovernorDatum)
+              (ScriptContext (mkEffectTxInfo invalidNewGovernorDatum) (Spending effectRef))
+          ]
+      ]
+  ]

agora-spec/Spec/Effect/TreasuryWithdrawal.hs

@@ -0,0 +1,172 @@
+{- |
+Module     : Spec.Effect.TreasuryWithdrawalEffect
+Maintainer : seungheon.ooh@gmail.com
+Description: Sample based testing for Treasury Withdrawal Effect
+
+This module specs the Treasury Withdrawal Effect.
+-}
+module Spec.Effect.TreasuryWithdrawal (specs) where
+
+import Agora.Effect.TreasuryWithdrawal (
+  TreasuryWithdrawalDatum (TreasuryWithdrawalDatum),
+  treasuryWithdrawalValidator,
+ )
+import Plutus.V1.Ledger.Value qualified as Value
+import Sample.Effect.TreasuryWithdrawal (
+  buildReceiversOutputFromDatum,
+  buildScriptContext,
+  currSymbol,
+  inputCollateral,
+  inputGAT,
+  inputTreasury,
+  inputUser,
+  outputTreasury,
+  outputUser,
+  treasuries,
+  users,
+ )
+import Spec.Spec (
+  SpecificationTree,
+  effectFailsWith,
+  effectSucceedsWith,
+  group,
+ )
+
+specs :: [SpecificationTree]
+specs =
+  [ group
+      "effect"
+      [ effectSucceedsWith
+          "Simple"
+          (treasuryWithdrawalValidator currSymbol)
+          datum1
+          ( buildScriptContext
+              [ inputGAT
+              , inputCollateral 10
+              , inputTreasury 1 (asset1 10)
+              ]
+              $ outputTreasury 1 (asset1 7) :
+              buildReceiversOutputFromDatum datum1
+          )
+      , effectSucceedsWith
+          "Simple with multiple treasuries "
+          (treasuryWithdrawalValidator currSymbol)
+          datum1
+          ( buildScriptContext
+              [ inputGAT
+              , inputCollateral 10
+              , inputTreasury 1 (asset1 10)
+              , inputTreasury 2 (asset1 100)
+              , inputTreasury 3 (asset1 500)
+              ]
+              $ [ outputTreasury 1 (asset1 7)
+                , outputTreasury 2 (asset1 100)
+                , outputTreasury 3 (asset1 500)
+                ]
+                ++ buildReceiversOutputFromDatum datum1
+          )
+      , effectSucceedsWith
+          "Mixed Assets"
+          (treasuryWithdrawalValidator currSymbol)
+          datum2
+          ( buildScriptContext
+              [ inputGAT
+              , inputCollateral 10
+              , inputTreasury 1 (asset1 20)
+              , inputTreasury 2 (asset2 20)
+              ]
+              $ [ outputTreasury 1 (asset1 13)
+                , outputTreasury 2 (asset2 14)
+                ]
+                ++ buildReceiversOutputFromDatum datum2
+          )
+      , effectFailsWith
+          "Pay to uknown 3rd party"
+          (treasuryWithdrawalValidator currSymbol)
+          datum2
+          ( buildScriptContext
+              [ inputGAT
+              , inputCollateral 10
+              , inputTreasury 1 (asset1 20)
+              , inputTreasury 2 (asset2 20)
+              ]
+              $ [ outputUser 100 (asset1 2)
+                , outputTreasury 1 (asset1 11)
+                , outputTreasury 2 (asset2 14)
+                ]
+                ++ buildReceiversOutputFromDatum datum2
+          )
+      , effectFailsWith
+          "Missing receiver"
+          (treasuryWithdrawalValidator currSymbol)
+          datum2
+          ( buildScriptContext
+              [ inputGAT
+              , inputCollateral 10
+              , inputTreasury 1 (asset1 20)
+              , inputTreasury 2 (asset2 20)
+              ]
+              $ [ outputTreasury 1 (asset1 13)
+                , outputTreasury 2 (asset2 14)
+                ]
+                ++ drop 1 (buildReceiversOutputFromDatum datum2)
+          )
+      , effectFailsWith
+          "Unauthorized treasury"
+          (treasuryWithdrawalValidator currSymbol)
+          datum3
+          ( buildScriptContext
+              [ inputGAT
+              , inputCollateral 10
+              , inputTreasury 999 (asset1 20)
+              ]
+              $ outputTreasury 999 (asset1 17) :
+              buildReceiversOutputFromDatum datum3
+          )
+      , effectFailsWith
+          "Prevent transactions besides the withdrawal"
+          (treasuryWithdrawalValidator currSymbol)
+          datum3
+          ( buildScriptContext
+              [ inputGAT
+              , inputTreasury 1 (asset1 20)
+              , inputTreasury 999 (asset1 20)
+              , inputUser 99 (asset2 100)
+              ]
+              $ [ outputTreasury 1 (asset1 17)
+                , outputUser 100 (asset2 100)
+                ]
+                ++ buildReceiversOutputFromDatum datum3
+          )
+      ]
+  ]
+  where
+    asset1 = Value.singleton "abbc12" "OrangeBottle"
+    asset2 = Value.singleton "abbc12" "19721121"
+    datum1 =
+      TreasuryWithdrawalDatum
+        [ (head users, asset1 1)
+        , (users !! 1, asset1 1)
+        , (users !! 2, asset1 1)
+        ]
+        [ treasuries !! 1
+        , treasuries !! 2
+        , treasuries !! 3
+        ]
+    datum2 =
+      TreasuryWithdrawalDatum
+        [ (head users, asset1 4 <> asset2 5)
+        , (users !! 1, asset1 2 <> asset2 1)
+        , (users !! 2, asset1 1)
+        ]
+        [ head treasuries
+        , treasuries !! 1
+        , treasuries !! 2
+        ]
+    datum3 =
+      TreasuryWithdrawalDatum
+        [ (head users, asset1 1)
+        , (users !! 1, asset1 1)
+        , (users !! 2, asset1 1)
+        ]
+        [treasuries !! 1]

agora-spec/Spec/Effect/TreasuryWithdrawal.hs~

@@ -0,0 +1,422 @@
+{- |
+Module     : Spec.Effect.TreasuryWithdrawalEffect
+Maintainer : seungheon.ooh@gmail.com
+Description: Sample based testing for Treasury Withdrawal Effect
+
+This module tests the Treasury Withdrawal Effect.
+-}
+module Spec.Effect.TreasuryWithdrawal (tests) where
+
+import Agora.Effect.TreasuryWithdrawal (
+  TreasuryWithdrawalDatum (TreasuryWithdrawalDatum),
+  treasuryWithdrawalValidator,
+  PTreasuryWithdrawalDatum
+ )
+import Plutus.V1.Ledger.Api
+import Plutarch.Builtin
+import Plutus.V1.Ledger.Value qualified as Value
+import Plutus.V1.Ledger.Interval qualified as Interval
+import Plutarch.Api.V1
+import Sample.Effect.TreasuryWithdrawal
+import Sample.Sample
+import Test.Util (effectFailsWith, effectSucceedsWith)
+import Agora.Utils
+import Test.QuickCheck
+import Test.QuickCheck.Monadic
+
+import Test.Tasty (TestTree, testGroup)
+import Test.Tasty.QuickCheck 
+import Test.Tasty.Plutarch.Property (classifiedProperty)
+
+import Data.Tagged
+import Data.Universe
+
+import Control.Applicative
+
+type TWETestInput = (TreasuryWithdrawalDatum, TxInfo)
+data TWETestCases
+  = PaysToEffect
+  | OutputsDoNotMatchReceivers
+  | InputsHaveOtherScriptInput
+  | RemaindersDoNotReturnToTreasuries
+  | EffectShouldPass
+  deriving stock (Eq)
+
+instance Show TWETestCases where
+  show = \case
+    PaysToEffect -> "Transaction pays to effect"
+    OutputsDoNotMatchReceivers -> "Transaction outputs do not match receivers"
+    InputsHaveOtherScriptInput -> "Transaction has script input that is not specified in datum"
+    RemaindersDoNotReturnToTreasuries -> "Remainding Values do not return to input treasuries"
+    EffectShouldPass -> "Effect should pass"
+
+instance Universe TWETestCases where
+  universe =
+    [ PaysToEffect
+    , OutputsDoNotMatchReceivers
+    , InputsHaveOtherScriptInput
+    , RemaindersDoNotReturnToTreasuries
+--    , EffectShouldPass
+    ]
+
+instance Finite TWETestCases where
+  universeF = universe
+  cardinality = Tagged 5
+  
+-- TODO: Some unideal repeated patterns here
+genTWECases :: TWETestCases -> Gen TWETestInput
+genTWECases PaysToEffect                      = do
+  datum <- genTWEDatum
+  -- Would be nice to randomize number of outputs to effect
+  vals <- listOf1 genAnyValue
+  let toEffect =
+        (\val -> TxOut
+        { txOutAddress = Address (ScriptCredential $ validatorHash validator) Nothing
+        , txOutValue = val
+        , txOutDatumHash = Nothing
+        }) <$> vals
+      modify (i, o) = return (i, o <> toEffect)
+  txinfo <- txInfoFromTWEDatum modify datum
+  return (datum, txinfo)
+genTWECases OutputsDoNotMatchReceivers        = do
+  datum <- genTWEDatum
+  let modify (i, o) = do
+        -- unfortunately `sublistOf` sometimes returns same array.
+        -- So tail is used to make sure there is aleast one thing missing
+        output <- sublistOf $ tail o
+        return (i, output)
+  txinfo <- txInfoFromTWEDatum modify datum
+  return (datum, txinfo)
+genTWECases InputsHaveOtherScriptInput        = do
+  datum <- genTWEDatum
+  let modify (i, o) = do
+        d <- listOf1 $ liftA2 (,) genScriptCredential genAnyValue 
+        
+        let unauthorizedScriptInputs =
+              (\(addr, val) ->
+                  TxInInfo
+                  (TxOutRef "0b2086cbf8b6900f8cb65e012de4516cb66b5cb08a9aaba12a8b88be" 1)
+                  TxOut
+                  { txOutAddress = Address addr Nothing
+                  , txOutValue = val
+                  , txOutDatumHash = Nothing
+                  }) <$> d
+        return (i <> unauthorizedScriptInputs, o)
+  txinfo <- txInfoFromTWEDatum modify datum
+  return (datum, txinfo)
+genTWECases RemaindersDoNotReturnToTreasuries = do
+  -- suchThat here might be unideal, but it's what we've got...
+  -- Possible Fix, use random input amount for treasury inputs
+  -- so that it always have excess
+  datum <- genTWEDatum `suchThat` (\(TreasuryWithdrawalDatum r t) ->
+                                     let totalExpected = mconcat $ snd <$> r
+                                         ts = length t
+                                         in
+                                     totalExpected /= mconcat (replicate ts $ distributeValue ts totalExpected)
+                                     )
+  let modify (i, o) = do
+        -- We'll drop all outputs directed to ScriptCredential
+        let treasuryDroppedOutput =
+              filter (\(addressCredential . txOutAddress -> x) -> case x of
+                         PubKeyCredential _ -> True
+                         ScriptCredential _ -> False
+                        ) o
+        return (i, treasuryDroppedOutput)
+  txinfo <- txInfoFromTWEDatum modify datum
+  return (datum, txinfo)
+genTWECases EffectShouldPass                  = do
+  datum <- genTWEDatum
+  txinfo <- txInfoFromTWEDatum return datum
+  return (datum, txinfo)
+
+classifyTWE :: TWETestInput -> TWETestCases
+classifyTWE ((TreasuryWithdrawalDatum r t), info)
+  | paysToEffect = PaysToEffect
+  | outputsDoNotMatchReceivers = OutputsDoNotMatchReceivers
+  | inputsHaveOtherScriptInput = InputsHaveOtherScriptInput
+  | remaindersDoNotReturnToTreasuries = RemaindersDoNotReturnToTreasuries
+  | otherwise = EffectShouldPass
+  where
+    extractCredVal txout = (addressCredential (txOutAddress txout), txOutValue txout)
+    credentialValuePairs = extractCredVal <$> txInfoOutputs info
+    paysToEffect = elem (ScriptCredential $ validatorHash validator) $ fst . extractCredVal <$> (txInfoOutputs info)
+    outputsDoNotMatchReceivers = not $ and $ fmap (\x -> elem x credentialValuePairs) r
+    inputsHaveOtherScriptInput = or $ (\(fst . extractCredVal . txInInfoResolved -> x) ->
+                                         (not $ elem x t) &&
+                                         x /= (ScriptCredential $ validatorHash validator)
+                                      ) <$> txInfoInputs info
+
+    sumValueOfTreasury x = mconcat $ snd <$> (filter (\(c,_) -> elem c t) $ x)
+    treasuryInputSum = sumValueOfTreasury $ extractCredVal . txInInfoResolved <$> txInfoInputs info
+    treasuryOutputSum = sumValueOfTreasury credentialValuePairs
+    expected = Value.unionWith (-) treasuryInputSum (mconcat $ snd <$> r)
+    remaindersDoNotReturnToTreasuries = treasuryOutputSum /= expected
+    
+shrinkTWE :: TWETestInput -> [TWETestInput]
+shrinkTWE = const [] -- currently this should work...
+
+expectedTWE :: Term s (PBuiltinPair PTreasuryWithdrawalDatum PTxInfo :--> PMaybe PUnit)
+expectedTWE = plam $ \_input -> pcon $ PNothing
+
+opaqueToUnit :: Term s (POpaque :--> PUnit)
+opaqueToUnit = plam $ \_ -> pconstant ()
+
+definitionTWE :: Term s (PBuiltinPair PTreasuryWithdrawalDatum PTxInfo :--> PUnit)
+definitionTWE = plam $ \input -> unTermCont $ do
+  datum <- tclet $ pfstBuiltin # input
+  txinfo <- tclet $ psndBuiltin # input
+
+  let scriptContext =
+        pcon $ PScriptContext $
+          pdcons @"txInfo" # pdata txinfo
+          #$ pdcons @"purpose" # pdata (pconstant $ Spending (TxOutRef "0b2086cbf8b6900f8cb65e012de4516cb66b5cb08a9aaba12a8b88be" 1))
+          # pdnil
+
+  pure $ opaqueToUnit #$ treasuryWithdrawalValidator currSymbol
+    # pforgetData (pdata datum)
+    # pforgetData (pdata (pconstant ()))
+    # scriptContext
+
+propertyTWE :: Property
+propertyTWE = classifiedProperty genTWECases shrinkTWE expectedTWE classifyTWE definitionTWE
+
+{- | Generates "lawful" ScriptContext from given TreasuryWithdrawalDatum.
+Other cases can use this ScriptContext to derive from and develop
+a case specific contexts with generators.
+
+TODO: will this work okay with generators adding and removing
+parts? I don't see particular reason it will not to, but will
+that be a "good" generator?
+-}
+txInfoFromTWEDatum :: (([TxInInfo], [TxOut]) -> Gen ([TxInInfo], [TxOut])) -> TreasuryWithdrawalDatum -> Gen TxInfo
+txInfoFromTWEDatum cb datum = do
+  (input, output) <- cb (expectedInput, expectedOutput)
+  return $
+      TxInfo
+      { txInfoInputs = input
+      , txInfoOutputs = output
+      , txInfoFee = Value.singleton "" "" 2
+      , txInfoMint = Value.singleton currSymbol validatorHashTN (-1)
+      , txInfoDCert = []
+      , txInfoWdrl = []
+      , txInfoValidRange = Interval.always
+      , txInfoSignatories = [signer]
+      , txInfoData = []
+      , txInfoId = "0b123412341234"
+      }
+  where
+    (expectedInput, excessOutputs)  = expectedTxInInfoFromTWEDatum datum
+    expectedOutput = expectedTxOutFromTWEDatum datum <> excessOutputs
+
+expectedTxOutFromTWEDatum :: TreasuryWithdrawalDatum -> [TxOut]
+expectedTxOutFromTWEDatum (TreasuryWithdrawalDatum r _) =
+  f <$> r -- add outputs to treasuries, returning excess STs.
+  where 
+    f (addr, val) = TxOut
+      { txOutAddress = Address addr Nothing
+      , txOutValue = val
+      , txOutDatumHash = Nothing
+      }
+
+{- | Generates expected inputs from given Datum
+-}
+expectedTxInInfoFromTWEDatum :: TreasuryWithdrawalDatum -> ([TxInInfo], [TxOut])
+expectedTxInInfoFromTWEDatum (TreasuryWithdrawalDatum r t) =
+  (inputGAT:((\addr -> TxInInfo
+    (TxOutRef "0b2086cbf8b6900f8cb65e012de4516cb66b5cb08a9aaba12a8b88be" 1)
+    TxOut
+    { txOutAddress = Address addr Nothing
+    , txOutValue = treasuryInputValue
+    , txOutDatumHash = Nothing
+    })
+  <$> t)
+  , [TxOut
+    { txOutAddress = Address (head t) Nothing
+    , txOutValue = extras
+    , txOutDatumHash = Nothing
+    }])
+  where
+    totalValues = mconcat $ snd <$> r
+    treasuryInputValue = distributeValue (length t) totalValues
+    extras = Value.unionWith (-) (mconcat (replicate (length t) treasuryInputValue)) $ totalValues
+
+distributeValue :: Int -> Value -> Value
+distributeValue n v = mconcat $ (\(cs, tn, (toInteger -> val)) -> Value.singleton cs tn val) <$> vals
+  where
+     vals = (\(cs, tn, (fromInteger -> val)) -> (cs, tn, val `divRound` n)) <$> Value.flattenValue v
+     divRound x y = case divMod x y of
+                      (x, 0) -> x
+                      (x, _) -> x + 1
+
+genTWEDatum :: Gen TreasuryWithdrawalDatum
+genTWEDatum = do
+  -- Make several random assetclasses to choose from
+  ac <- listOf1 genAssetClass
+
+  -- Make several random users
+  users <- listOf1 genUserCredential
+
+  -- Make several random treasuries
+  treas <- listOf1 genScriptCredential
+
+  -- Make random amounts of values that transaction will have
+  values <- listOf1 $ elements ac >>= genValue
+
+  let receiverList = zipWith (,) users values
+  pure $ TreasuryWithdrawalDatum receiverList treas
+
+prop :: PropertyM IO Bool
+prop = forAllM (elements (universe :: [TWETestCases])) (\c -> run $ generate (genTWECases c) >>= (\gen -> return $ c == classifyTWE gen))
+
+tests :: [TestTree]
+tests =
+  [ testProperty "Generator <-> Classifier" (monadicIO prop)
+  , testProperty "effect" propertyTWE
+  , effectSucceedsWith
+          "test"
+          (treasuryWithdrawalValidator currSymbol)
+          datum1
+          ( buildScriptContext
+              [ inputGAT
+              , inputCollateral 10
+              , inputTreasury 1 (asset1 10)
+              ]
+              $ outputTreasury 1 (asset1 7) :
+              buildReceiversOutputFromDatum datum1
+          )
+  , testGroup
+      "effect"
+      [ effectSucceedsWith
+          "Simple"
+          (treasuryWithdrawalValidator currSymbol)
+          datum1
+          ( buildScriptContext
+              [ inputGAT
+              , inputCollateral 10
+              , inputTreasury 1 (asset1 10)
+              ]
+              $ outputTreasury 1 (asset1 7) :
+              buildReceiversOutputFromDatum datum1
+          )
+      , effectSucceedsWith
+          "Simple with multiple treasuries "
+          (treasuryWithdrawalValidator currSymbol)
+          datum1
+          ( buildScriptContext
+              [ inputGAT
+              , inputCollateral 10
+              , inputTreasury 1 (asset1 10)
+              , inputTreasury 2 (asset1 100)
+              , inputTreasury 3 (asset1 500)
+              ]
+              $ [ outputTreasury 1 (asset1 7)
+                , outputTreasury 2 (asset1 100)
+                , outputTreasury 3 (asset1 500)
+                ]
+                ++ buildReceiversOutputFromDatum datum1
+          )
+      , effectSucceedsWith
+          "Mixed Assets"
+          (treasuryWithdrawalValidator currSymbol)
+          datum2
+          ( buildScriptContext
+              [ inputGAT
+              , inputCollateral 10
+              , inputTreasury 1 (asset1 20)
+              , inputTreasury 2 (asset2 20)
+              ]
+              $ [ outputTreasury 1 (asset1 13)
+                , outputTreasury 2 (asset2 14)
+                ]
+                ++ buildReceiversOutputFromDatum datum2
+          )
+      , effectFailsWith
+          "Pay to uknown 3rd party"
+          (treasuryWithdrawalValidator currSymbol)
+          datum2
+          ( buildScriptContext
+              [ inputGAT
+              , inputCollateral 10
+              , inputTreasury 1 (asset1 20)
+              , inputTreasury 2 (asset2 20)
+              ]
+              $ [ outputUser 100 (asset1 2)
+                , outputTreasury 1 (asset1 11)
+                , outputTreasury 2 (asset2 14)
+                ]
+                ++ buildReceiversOutputFromDatum datum2
+          )
+      , effectFailsWith
+          "Missing receiver"
+          (treasuryWithdrawalValidator currSymbol)
+          datum2
+          ( buildScriptContext
+              [ inputGAT
+              , inputCollateral 10
+              , inputTreasury 1 (asset1 20)
+              , inputTreasury 2 (asset2 20)
+              ]
+              $ [ outputTreasury 1 (asset1 13)
+                , outputTreasury 2 (asset2 14)
+                ]
+                ++ drop 1 (buildReceiversOutputFromDatum datum2)
+          )
+      , effectFailsWith
+          "Unauthorized treasury"
+          (treasuryWithdrawalValidator currSymbol)
+          datum3
+          ( buildScriptContext
+              [ inputGAT
+              , inputCollateral 10
+              , inputTreasury 999 (asset1 20)
+              ]
+              $ outputTreasury 999 (asset1 17) :
+              buildReceiversOutputFromDatum datum3
+          )
+      , effectFailsWith
+          "Prevent transactions besides the withdrawal"
+          (treasuryWithdrawalValidator currSymbol)
+          datum3
+          ( buildScriptContext
+              [ inputGAT
+              , inputTreasury 1 (asset1 20)
+              , inputTreasury 999 (asset1 20)
+              , inputUser 99 (asset2 100)
+              ]
+              $ [ outputTreasury 1 (asset1 17)
+                , outputUser 100 (asset2 100)
+                ]
+                ++ buildReceiversOutputFromDatum datum3
+          )
+      ]
+  ]
+  where
+    asset1 = Value.singleton "abbc12" "OrangeBottle"
+    asset2 = Value.singleton "abbc12" "19721121"
+    datum1 =
+      TreasuryWithdrawalDatum
+        [ (head users, asset1 1)
+        , (users !! 1, asset1 1)
+        , (users !! 2, asset1 1)
+        ]
+        [ treasuries !! 1
+        , treasuries !! 2
+        , treasuries !! 3
+        ]
+    datum2 =
+      TreasuryWithdrawalDatum
+        [ (head users, asset1 4 <> asset2 5)
+        , (users !! 1, asset1 2 <> asset2 1)
+        , (users !! 2, asset1 1)
+        ]
+        [ head treasuries
+        , treasuries !! 1
+        , treasuries !! 2
+        ]
+    datum3 =
+      TreasuryWithdrawalDatum
+        [ (head users, asset1 1)
+        , (users !! 1, asset1 1)
+        , (users !! 2, asset1 1)
+        ]
+        [treasuries !! 1]

agora-spec/Spec/Governor.hs

@@ -0,0 +1,77 @@
+{- |
+Module     : Spec.Governor
+Maintainer : connor@mlabs.city
+Description: Tests for Agora governor.
+
+Thie module exports `specs`, a list of `TestTree`s, which ensure
+that Agora's governor component workds as intended.
+
+Tests should pass when the validator or policy is given one of the
+valid script contexts, which are defined in 'Agora.Sample.Governor'.
+
+TODO: Add negative test cases, see [#76](https://github.com/Liqwid-Labs/agora/issues/76).
+-}
+module Spec.Governor (specs) where
+
+import Agora.Governor (GovernorDatum (..), GovernorRedeemer (..))
+import Agora.Governor.Scripts (governorPolicy, governorValidator)
+import Agora.Proposal (ProposalId (..))
+import Data.Default.Class (Default (def))
+import Sample.Governor (createProposal, mintGATs, mintGST, mutateState)
+import Sample.Shared qualified as Shared
+import Spec.Spec (
+  SpecificationTree,
+  group,
+  policySucceedsWith,
+  validatorSucceedsWith,
+ )
+
+--------------------------------------------------------------------------------
+
+specs :: [SpecificationTree]
+specs =
+  [ group
+      "policy"
+      [ policySucceedsWith
+          "GST minting"
+          (governorPolicy Shared.governor)
+          ()
+          mintGST
+      ]
+  , group
+      "validator"
+      [ validatorSucceedsWith
+          "proposal creation"
+          (governorValidator Shared.governor)
+          ( GovernorDatum
+              Shared.defaultProposalThresholds
+              (ProposalId 0)
+              def
+              def
+          )
+          CreateProposal
+          createProposal
+      , validatorSucceedsWith
+          "GATs minting"
+          (governorValidator Shared.governor)
+          ( GovernorDatum
+              Shared.defaultProposalThresholds
+              (ProposalId 5)
+              def
+              def
+          )
+          MintGATs
+          mintGATs
+      , validatorSucceedsWith
+          "mutate governor state"
+          (governorValidator Shared.governor)
+          ( GovernorDatum
+              Shared.defaultProposalThresholds
+              (ProposalId 5)
+              def
+              def
+          )
+          MutateGovernor
+          mutateState
+      ]
+  ]

agora-spec/Spec/Model/MultiSig.hs

@@ -0,0 +1,194 @@
+{- |
+Module     : Spec.Model.MultiSig
+Maintainer : emi@haskell.fyi
+Description: apropos-tx model and tests for 'MultiSig' functions
+
+apropos-tx model and tests for 'MultiSig' functions
+-}
+module Spec.Model.MultiSig (
+  plutarchTests,
+  genTests,
+) where
+
+import Data.List (intersect)
+
+--------------------------------------------------------------------------------
+
+import Plutus.V1.Ledger.Api (
+  Script,
+  ScriptContext (scriptContextPurpose),
+  ScriptPurpose (Spending),
+  TxInfo (
+    txInfoDCert,
+    txInfoData,
+    txInfoFee,
+    txInfoId,
+    txInfoInputs,
+    txInfoMint,
+    txInfoOutputs,
+    txInfoValidRange,
+    txInfoWdrl
+  ),
+  TxOutRef (TxOutRef),
+  scriptContextTxInfo,
+  txInfoSignatories,
+ )
+import Plutus.V1.Ledger.Contexts (ScriptContext (ScriptContext), TxInfo (TxInfo))
+import Plutus.V1.Ledger.Crypto (PubKeyHash)
+import Plutus.V1.Ledger.Interval qualified as Interval
+import Plutus.V1.Ledger.Value qualified as Value
+
+--------------------------------------------------------------------------------
+
+import Apropos (
+  Apropos (Apropos),
+  Formula (ExactlyOne, Var, Yes),
+  HasLogicalModel (..),
+  HasParameterisedGenerator,
+  LogicalModel (logic),
+  parameterisedGenerator,
+  runGeneratorTestsWhere,
+  (:+),
+ )
+import Apropos.Gen (Gen, choice, int, linear, list)
+import Apropos.LogicalModel (Enumerable)
+import Apropos.LogicalModel.Enumerable (Enumerable (enumerated))
+import Apropos.Script (ScriptModel (expect, runScriptTestsWhere, script))
+import Test.Tasty (TestTree, testGroup)
+import Test.Tasty.Hedgehog (fromGroup)
+
+--------------------------------------------------------------------------------
+
+import Agora.MultiSig (MultiSig (..), validatedByMultisig)
+
+--------------------------------------------------------------------------------
+
+-- | apropos model for testing multisigs.
+data MultiSigModel = MultiSigModel
+  { ms :: MultiSig
+  -- ^ `MultiSig` value to be tested.
+  , ctx :: ScriptContext
+  -- ^ The `ScriptContext` of the transaction.
+  }
+  deriving stock (Eq, Show)
+
+-- | Propositions that may hold true of a `MultiSigModel`.
+data MultiSigProp
+  = -- | Sufficient number of signatories in the script context.
+    MeetsMinSigs
+  | -- | Insufficient number of signatories in the script context.
+    DoesNotMeetMinSigs
+  deriving stock (Eq, Show, Ord)
+
+instance Enumerable MultiSigProp where
+  enumerated = [MeetsMinSigs, DoesNotMeetMinSigs]
+
+instance LogicalModel MultiSigProp where
+  -- Only logical relationship between the two propositions is
+  -- that exactly one of them holds for a given model.
+  logic = ExactlyOne [Var MeetsMinSigs, Var DoesNotMeetMinSigs]
+
+instance HasLogicalModel MultiSigProp MultiSigModel where
+  satisfiesProperty :: MultiSigProp -> MultiSigModel -> Bool
+  satisfiesProperty p m =
+    let minSigs = m.ms.minSigs
+        signatories = txInfoSignatories $ scriptContextTxInfo $ m.ctx
+        matchingSigs = intersect m.ms.keys signatories
+     in case p of
+          MeetsMinSigs -> length matchingSigs >= fromInteger minSigs
+          DoesNotMeetMinSigs -> length matchingSigs < fromInteger minSigs
+
+{- | Given a list of key hashes, returns a dummy `ScriptContext`,
+     with those hashes as signatories.
+-}
+contextWithSignatures :: [PubKeyHash] -> ScriptContext
+contextWithSignatures sigs =
+  ScriptContext
+    { scriptContextTxInfo =
+        TxInfo
+          { txInfoInputs = []
+          , txInfoOutputs = []
+          , txInfoFee = Value.singleton "" "" 2
+          , txInfoMint = mempty
+          , txInfoDCert = []
+          , txInfoWdrl = []
+          , txInfoValidRange = Interval.always
+          , txInfoSignatories = sigs
+          , txInfoData = []
+          , txInfoId = "0b2086cbf8b6900f8cb65e012de4516cb66b5cb08a9aaba12a8b88be"
+          }
+    , scriptContextPurpose = Spending (TxOutRef "" 0)
+    }
+
+-- | Generator returning one of four dummy public key hashes.
+genPK :: Gen PubKeyHash
+genPK =
+  choice
+    [ pure "8a30896c4fd5e79843e4ca1bd2cdbaa36f8c0bc3be7401214142019c"
+    , pure "0b12051dd2da4b3629cebb92e2be111e0e99c63c04727ed55b74a296"
+    , pure "87f5f31e4d7437463cd901c4c9edb7a51903ac858661503e9d72f492"
+    , pure "f74ccaee8244264b3c73fce3b66bd2337de3db70efff4261d6ff145b"
+    ]
+
+instance HasParameterisedGenerator MultiSigProp MultiSigModel where
+  parameterisedGenerator s = do
+    -- Gen between one and four signatures for the `MultiSig`.
+    expectedSignatures <- list (linear 1 4) genPK
+
+    -- Gen the value of `MultiSig.minSigs`.
+    minSigs <- toInteger <$> int (linear 1 (length expectedSignatures))
+
+    -- Assign values to msig.
+    let msig = MultiSig expectedSignatures minSigs
+
+    actualSignaturesLength <-
+      -- If we would like to generate a MultiSig model which passes...
+      if MeetsMinSigs `elem` s
+        then -- ... have a sufficient number of signatories.
+          int (linear (fromInteger minSigs) (length expectedSignatures))
+        else -- ... have zero signatories.
+          pure 0
+
+    -- Get a list of signatories for the script context.
+    let actualSignatures = take actualSignaturesLength expectedSignatures
+
+    let ctx = contextWithSignatures actualSignatures
+
+    -- Return the generated model.
+    pure (MultiSigModel msig ctx)
+
+instance ScriptModel MultiSigProp MultiSigModel where
+  -- When the script runs, we want the model to meet the minimum signatures.
+  expect :: (MultiSigModel :+ MultiSigProp) -> Formula MultiSigProp
+  expect Apropos = Var MeetsMinSigs
+
+  -- Function making a valid script from the model and propositions.
+  script :: (MultiSigModel :+ MultiSigProp) -> MultiSigModel -> Script
+  script Apropos msm =
+    compile $
+      pif
+        (validatedByMultisig msm.ms # pconstant msm.ctx.scriptContextTxInfo)
+        (pcon PUnit)
+        perror
+
+-- | Consistency tests for the 'HasParameterisedGenerator' instance of 'MultiSigModel'.
+genTests :: TestTree
+genTests =
+  testGroup "genTests" $
+    fromGroup
+      <$> [ runGeneratorTestsWhere
+              (Apropos :: MultiSigModel :+ MultiSigProp)
+              "Generator"
+              Yes
+          ]
+
+-- | Tests for the 'ScriptModel' instance of 'MultiSigModel'.
+plutarchTests :: TestTree
+plutarchTests =
+  testGroup "plutarchTests" $
+    fromGroup
+      <$> [ runScriptTestsWhere
+              (Apropos :: MultiSigModel :+ MultiSigProp)
+              "ScriptValid"
+              Yes
+          ]

agora-spec/Spec/Proposal.hs

@@ -0,0 +1,162 @@
+{-# LANGUAGE QuasiQuotes #-}
+
+{- |
+Module     : Spec.Proposal
+Maintainer : emi@haskell.fyi
+Description: Tests for Proposal policy and validator
+
+Tests for Proposal policy and validator
+-}
+module Spec.Proposal (specs) where
+
+--------------------------------------------------------------------------------
+
+import Agora.Proposal (
+  Proposal (..),
+  ProposalDatum (..),
+  ProposalId (ProposalId),
+  ProposalRedeemer (Cosign, Vote),
+  ProposalStatus (Draft, VotingReady),
+  ProposalVotes (ProposalVotes),
+  ResultTag (ResultTag),
+  cosigners,
+  effects,
+  emptyVotesFor,
+  proposalId,
+  status,
+  thresholds,
+  votes,
+ )
+import Agora.Proposal.Scripts (
+  proposalPolicy,
+  proposalValidator,
+ )
+import Agora.Proposal.Time (ProposalStartingTime (ProposalStartingTime))
+import Agora.Stake (
+  ProposalLock (ProposalLock),
+  StakeDatum (StakeDatum),
+  StakeRedeemer (PermitVote, WitnessStake),
+ )
+import Agora.Stake.Scripts (stakeValidator)
+import Data.Default.Class (Default (def))
+import Plutarch.SafeMoney (Tagged (Tagged))
+import Plutus.V1.Ledger.Api (ScriptContext (..), ScriptPurpose (..))
+import PlutusTx.AssocMap qualified as AssocMap
+import Sample.Proposal qualified as Proposal
+import Sample.Shared (signer, signer2)
+import Sample.Shared qualified as Shared
+import Spec.Spec (
+  SpecificationTree,
+  group,
+  policySucceedsWith,
+  validatorSucceedsWith,
+ )
+
+--------------------------------------------------------------------------------
+
+-- | Stake specs.
+specs :: [SpecificationTree]
+specs =
+  [ group
+      "policy"
+      [ policySucceedsWith
+          "proposalCreation"
+          (proposalPolicy Shared.proposal.governorSTAssetClass)
+          ()
+          Proposal.proposalCreation
+      ]
+  , group
+      "validator"
+      [ group
+          "cosignature"
+          [ validatorSucceedsWith
+              "proposal"
+              (proposalValidator Shared.proposal)
+              ( ProposalDatum
+                  { proposalId = ProposalId 0
+                  , effects =
+                      AssocMap.fromList
+                        [ (ResultTag 0, AssocMap.empty)
+                        , (ResultTag 1, AssocMap.empty)
+                        ]
+                  , status = Draft
+                  , cosigners = [signer]
+                  , thresholds = Shared.defaultProposalThresholds
+                  , votes =
+                      emptyVotesFor $
+                        AssocMap.fromList
+                          [ (ResultTag 0, AssocMap.empty)
+                          , (ResultTag 1, AssocMap.empty)
+                          ]
+                  , timingConfig = def
+                  , startingTime = ProposalStartingTime 0
+                  }
+              )
+              (Cosign [signer2])
+              (ScriptContext (Proposal.cosignProposal [signer2]) (Spending Proposal.proposalRef))
+          , validatorSucceedsWith
+              "stake"
+              (stakeValidator Shared.stake)
+              (StakeDatum (Tagged 50_000_000) signer2 [])
+              WitnessStake
+              (ScriptContext (Proposal.cosignProposal [signer2]) (Spending Proposal.stakeRef))
+          ]
+      , group
+          "voting"
+          [ validatorSucceedsWith
+              "proposal"
+              (proposalValidator Shared.proposal)
+              ( ProposalDatum
+                  { proposalId = ProposalId 42
+                  , effects =
+                      AssocMap.fromList
+                        [ (ResultTag 0, AssocMap.empty)
+                        , (ResultTag 1, AssocMap.empty)
+                        ]
+                  , status = VotingReady
+                  , cosigners = [signer]
+                  , thresholds = Shared.defaultProposalThresholds
+                  , votes =
+                      ProposalVotes
+                        ( AssocMap.fromList
+                            [ (ResultTag 0, 42)
+                            , (ResultTag 1, 4242)
+                            ]
+                        )
+                  , timingConfig = def
+                  , startingTime = ProposalStartingTime 0
+                  }
+              )
+              (Vote (ResultTag 0))
+              ( ScriptContext
+                  ( Proposal.voteOnProposal
+                      Proposal.VotingParameters
+                        { Proposal.voteFor = ResultTag 0
+                        , Proposal.voteCount = 27
+                        }
+                  )
+                  (Spending Proposal.proposalRef)
+              )
+          , validatorSucceedsWith
+              "stake"
+              (stakeValidator Shared.stake)
+              ( StakeDatum
+                  (Tagged 27)
+                  signer
+                  [ ProposalLock (ResultTag 0) (ProposalId 0)
+                  , ProposalLock (ResultTag 2) (ProposalId 1)
+                  ]
+              )
+              (PermitVote $ ProposalLock (ResultTag 0) (ProposalId 42))
+              ( ScriptContext
+                  ( Proposal.voteOnProposal
+                      Proposal.VotingParameters
+                        { Proposal.voteFor = ResultTag 0
+                        , Proposal.voteCount = 27
+                        }
+                  )
+                  (Spending Proposal.stakeRef)
+              )
+          ]
+      ]
+  ]

agora-spec/Spec/Spec.hs

@@ -0,0 +1,208 @@
+module Spec.Spec (
+  Specification (..),
+  SpecificationExpectation (..),
+  SpecificationTree (..),
+  group,
+  toTestTree,
+  getSpecification,
+  getSpecificationTree,
+  scriptSucceeds,
+  scriptFails,
+  policySucceedsWith,
+  policyFailsWith,
+  validatorSucceedsWith,
+  validatorFailsWith,
+  effectSucceedsWith,
+  effectFailsWith,
+) where
+
+import Data.Maybe (catMaybes)
+import Plutarch.Api.V1 (PMintingPolicy, PValidator)
+import Plutarch.Builtin (pforgetData)
+import Plutarch.Evaluate (evalScript)
+import Plutarch.Lift (PUnsafeLiftDecl (PLifted))
+import Plutus.V1.Ledger.Api (Script, ScriptContext)
+import PlutusTx.IsData qualified as PlutusTx (ToData)
+import Test.Tasty (TestTree, testGroup)
+import Test.Tasty.HUnit (assertFailure, testCase)
+
+data SpecificationExpectation
+  = Success
+  | Failure
+  | FailureWith String
+  deriving stock (Show)
+
+data Specification = Specification
+  { sName :: String
+  , sExpectation :: SpecificationExpectation
+  , sScript :: Script
+  }
+  deriving stock (Show)
+
+data SpecificationTree
+  = Terminal Specification
+  | Group String [SpecificationTree]
+  deriving stock (Show)
+
+exists :: String -> SpecificationTree -> Bool
+exists s (Terminal (Specification name _ _)) = s == name
+exists s (Group name st) = or (exists s <$> st) || s == name
+
+group :: String -> [SpecificationTree] -> SpecificationTree
+group name st
+  | or $ exists name <$> st = error "Name already exists"
+  | otherwise = Group name st
+
+getSpecification :: String -> SpecificationTree -> Maybe Specification
+getSpecification name (Terminal spec@(Specification sn _ _))
+  | name == sn = Just spec
+  | otherwise = Nothing
+getSpecification name (Group _ st)
+  | length specs == 1 = Just $ head specs
+  | otherwise = Nothing
+  where
+    specs = catMaybes $ getSpecification name <$> st
+
+getSpecificationTree :: String -> SpecificationTree -> Maybe SpecificationTree
+getSpecificationTree name specTree@(Group gn st)
+  | gn == name = Just specTree
+  | length trees == 1 = Just $ head trees
+  | otherwise = Nothing
+  where
+    trees = catMaybes $ getSpecificationTree name <$> st
+getSpecificationTree _ _ = Nothing
+
+toTestTree :: SpecificationTree -> TestTree
+toTestTree (Group name st) = testGroup name $ toTestTree <$> st
+toTestTree (Terminal (Specification name expectation script)) =
+  testCase name $ do
+    case expectation of
+      Success -> onSuccess
+      Failure -> onFailure
+      FailureWith s -> onFailureWith s
+  where
+    (res, _budget, traces) = evalScript script
+    ts = " Traces: " <> show traces
+    onSuccess = case res of
+      Left e ->
+        assertFailure $
+          show e <> ts
+      _ -> pure ()
+    onFailure = case res of
+      Right v ->
+        assertFailure $
+          "Expected failure, but succeeded. "
+            <> show v
+            <> ts
+      _ -> pure ()
+    onFailureWith _s = case res of -- TODO: check Trace for this
+      Right v ->
+        assertFailure $
+          "Expected failure, but succeeded. "
+            <> show v
+            <> ts
+      _ -> pure ()
+
+scriptSucceeds :: String -> Script -> SpecificationTree
+scriptSucceeds name script = Terminal $ Specification name Success script
+
+scriptFails :: String -> Script -> SpecificationTree
+scriptFails name script = Terminal $ Specification name Failure script
+
+policySucceedsWith ::
+  ( PLift redeemer
+  , PlutusTx.ToData (PLifted redeemer)
+  ) =>
+  String ->
+  ClosedTerm PMintingPolicy ->
+  PLifted redeemer ->
+  ScriptContext ->
+  SpecificationTree
+policySucceedsWith tag policy redeemer scriptContext =
+  scriptSucceeds tag $
+    compile
+      ( policy
+          # pforgetData (pconstantData redeemer)
+          # pconstant scriptContext
+      )
+
+policyFailsWith ::
+  ( PLift redeemer
+  , PlutusTx.ToData (PLifted redeemer)
+  ) =>
+  String ->
+  ClosedTerm PMintingPolicy ->
+  PLifted redeemer ->
+  ScriptContext ->
+  SpecificationTree
+policyFailsWith tag policy redeemer scriptContext =
+  scriptFails tag $
+    compile
+      ( policy
+          # pforgetData (pconstantData redeemer)
+          # pconstant scriptContext
+      )
+
+validatorSucceedsWith ::
+  ( PLift datum
+  , PlutusTx.ToData (PLifted datum)
+  , PLift redeemer
+  , PlutusTx.ToData (PLifted redeemer)
+  ) =>
+  String ->
+  ClosedTerm PValidator ->
+  PLifted datum ->
+  PLifted redeemer ->
+  ScriptContext ->
+  SpecificationTree
+validatorSucceedsWith tag validator datum redeemer scriptContext =
+  scriptSucceeds tag $
+    compile
+      ( validator
+          # pforgetData (pconstantData datum)
+          # pforgetData (pconstantData redeemer)
+          # pconstant scriptContext
+      )
+
+validatorFailsWith ::
+  ( PLift datum
+  , PlutusTx.ToData (PLifted datum)
+  , PLift redeemer
+  , PlutusTx.ToData (PLifted redeemer)
+  ) =>
+  String ->
+  ClosedTerm PValidator ->
+  PLifted datum ->
+  PLifted redeemer ->
+  ScriptContext ->
+  SpecificationTree
+validatorFailsWith tag validator datum redeemer scriptContext =
+  scriptFails tag $
+    compile
+      ( validator
+          # pforgetData (pconstantData datum)
+          # pforgetData (pconstantData redeemer)
+          # pconstant scriptContext
+      )
+
+effectSucceedsWith ::
+  ( PLift datum
+  , PlutusTx.ToData (PLifted datum)
+  ) =>
+  String ->
+  ClosedTerm PValidator ->
+  PLifted datum ->
+  ScriptContext ->
+  SpecificationTree
+effectSucceedsWith tag eff datum = validatorSucceedsWith tag eff datum ()
+
+effectFailsWith ::
+  ( PLift datum
+  , PlutusTx.ToData (PLifted datum)
+  ) =>
+  String ->
+  ClosedTerm PValidator ->
+  PLifted datum ->
+  ScriptContext ->
+  SpecificationTree
+effectFailsWith tag eff datum = validatorFailsWith tag eff datum ()

agora-spec/Spec/Stake.hs

@@ -0,0 +1,78 @@
+{-# LANGUAGE QuasiQuotes #-}
+
+{- |
+Module     : Spec.Stake
+Maintainer : emi@haskell.fyi
+Description: Tests for Stake policy and validator
+
+Tests for Stake policy and validator
+-}
+module Spec.Stake (specs) where
+
+--------------------------------------------------------------------------------
+
+import Prelude
+
+--------------------------------------------------------------------------------
+
+import Agora.Stake (Stake (..), StakeDatum (StakeDatum), StakeRedeemer (DepositWithdraw))
+import Agora.Stake.Scripts (stakePolicy, stakeValidator)
+
+--------------------------------------------------------------------------------
+
+import Sample.Stake (DepositWithdrawExample (DepositWithdrawExample, delta, startAmount), signer)
+import Sample.Stake qualified as Stake
+import Spec.Spec (
+  SpecificationTree,
+  group,
+  policyFailsWith,
+  policySucceedsWith,
+  validatorFailsWith,
+  validatorSucceedsWith,
+ )
+import Test.Util (toDatum)
+
+--------------------------------------------------------------------------------
+
+specs :: [SpecificationTree]
+specs =
+  [ group
+      "policy"
+      [ policySucceedsWith
+          "stakeCreation"
+          (stakePolicy Stake.stake.gtClassRef)
+          ()
+          Stake.stakeCreation
+      , policyFailsWith
+          "stakeCreationWrongDatum"
+          (stakePolicy Stake.stake.gtClassRef)
+          ()
+          Stake.stakeCreationWrongDatum
+      , policyFailsWith
+          "stakeCreationUnsigned"
+          (stakePolicy Stake.stake.gtClassRef)
+          ()
+          Stake.stakeCreationUnsigned
+      ]
+  , group
+      "validator"
+      [ validatorSucceedsWith
+          "stakeDepositWithdraw deposit"
+          (stakeValidator Stake.stake)
+          (toDatum $ StakeDatum 100_000 signer [])
+          (toDatum $ DepositWithdraw 100_000)
+          (Stake.stakeDepositWithdraw $ DepositWithdrawExample {startAmount = 100_000, delta = 100_000})
+      , validatorSucceedsWith
+          "stakeDepositWithdraw withdraw"
+          (stakeValidator Stake.stake)
+          (toDatum $ StakeDatum 100_000 signer [])
+          (toDatum $ DepositWithdraw $ negate 100_000)
+          (Stake.stakeDepositWithdraw $ DepositWithdrawExample {startAmount = 100_000, delta = negate 100_000})
+      , validatorFailsWith
+          "stakeDepositWithdraw negative GT"
+          (stakeValidator Stake.stake)
+          (toDatum $ StakeDatum 100_000 signer [])
+          (toDatum $ DepositWithdraw 1_000_000)
+          (Stake.stakeDepositWithdraw $ DepositWithdrawExample {startAmount = 100_000, delta = negate 1_000_000})
+      ]
+  ]

agora-spec/Spec/Treasury.hs

@@ -0,0 +1,146 @@
+{-# LANGUAGE TemplateHaskell #-}
+
+{- |
+Module: Spec.Treasury
+Description: Tests for Agora treasury.
+Maintainer: jack@mlabs.city
+
+This module exports `specs`, a list of `TestTree`s, which ensure
+that Agora's treasury component works as desired.
+
+Tests need to fail when:
+
+  1. The reedeemer is of inproper form. TODO: Inquire.
+  2. The script purpose is not minting.
+  3. `singleAuthorityTokenBurned` returns false.
+    a. @n /= -1@ GATs burned.
+    b. An input returns 'False' for 'authorityTokensValidIn'
+      i. A wallet input has a GAT.
+      ii. A script has a GAT, the token name for which does /not/
+          match the script's validator hash.
+-}
+module Spec.Treasury (specs) where
+
+import Agora.Treasury (
+  TreasuryRedeemer (SpendTreasuryGAT),
+  treasuryValidator,
+ )
+import Plutus.V1.Ledger.Api (
+  DCert (DCertDelegRegKey),
+ )
+import Plutus.V1.Ledger.Contexts (
+  ScriptContext (scriptContextPurpose, scriptContextTxInfo),
+  ScriptPurpose (Certifying, Rewarding, Spending),
+  TxInfo (txInfoInputs, txInfoMint),
+ )
+import Plutus.V1.Ledger.Credential (
+  StakingCredential (StakingHash),
+ )
+import Plutus.V1.Ledger.Value qualified as Value
+import Sample.Shared (
+  trCredential,
+ )
+import Sample.Treasury (
+  gatCs,
+  gatTn,
+  trCtxGATNameNotAddress,
+  treasuryRef,
+  validCtx,
+  walletIn,
+ )
+import Spec.Spec (
+  SpecificationTree,
+  group,
+  validatorFailsWith,
+  validatorSucceedsWith,
+ )
+
+specs :: [SpecificationTree]
+specs =
+  [ group
+      "Validator"
+      [ group
+          "Positive"
+          [ validatorSucceedsWith
+              "Allows for effect changes"
+              (treasuryValidator gatCs)
+              ()
+              SpendTreasuryGAT
+              validCtx
+          ]
+      , group
+          "Negative"
+          [ group
+              "Fails with ScriptPurpose not Minting"
+              [ validatorFailsWith
+                  "Spending"
+                  (treasuryValidator gatCs)
+                  ()
+                  SpendTreasuryGAT
+                  validCtx
+                    { scriptContextPurpose = Spending treasuryRef
+                    }
+              , validatorFailsWith
+                  "Rewarding"
+                  (treasuryValidator gatCs)
+                  ()
+                  SpendTreasuryGAT
+                  validCtx
+                    { scriptContextPurpose =
+                        Rewarding $
+                          StakingHash trCredential
+                    }
+              , validatorFailsWith
+                  "Certifying"
+                  (treasuryValidator gatCs)
+                  ()
+                  SpendTreasuryGAT
+                  validCtx
+                    { scriptContextPurpose =
+                        Certifying $
+                          DCertDelegRegKey $
+                            StakingHash trCredential
+                    }
+              ]
+          , validatorFailsWith -- TODO: Use QuickCheck.
+              "Fails when multiple GATs burned"
+              (treasuryValidator gatCs)
+              ()
+              SpendTreasuryGAT
+              validCtx
+                { scriptContextTxInfo =
+                    validCtx.scriptContextTxInfo
+                      { txInfoMint =
+                          Value.singleton
+                            gatCs
+                            gatTn
+                            (-2)
+                      }
+                }
+          , validatorFailsWith
+              "Fails when GAT token name is not script address"
+              (treasuryValidator gatCs)
+              ()
+              SpendTreasuryGAT
+              trCtxGATNameNotAddress
+          , validatorFailsWith
+              "Fails with wallet as input"
+              (treasuryValidator gatCs)
+              ()
+              SpendTreasuryGAT
+              ( let txInfo = validCtx.scriptContextTxInfo
+                    inputs = txInfo.txInfoInputs
+                    newInputs =
+                      [ head inputs
+                      , walletIn
+                      ]
+                 in validCtx
+                      { scriptContextTxInfo =
+                          txInfo
+                            { txInfoInputs = newInputs
+                            }
+                      }
+              )
+          ]
+      ]
+  ]

agora-spec/Spec/Utils.hs

@@ -0,0 +1,226 @@
+{- |
+Module     : Spec.Utils
+Maintainer : emi@haskell.fyi
+Description: Tests for utility functions in 'Agora.Utils'.
+
+Tests for utility functions in 'Agora.Utils'.
+-}
+module Spec.Utils (tests) where
+
+--------------------------------------------------------------------------------
+
+import Agora.Utils (phalve, pisUniq, pmergeBy, pmsort, pnubSort, pupdate)
+
+--------------------------------------------------------------------------------
+
+import Data.List (nub, sort)
+import Data.Map qualified as M
+import Data.Set qualified as S
+
+--------------------------------------------------------------------------------
+
+import Control.Monad.Cont (cont, runCont)
+import Test.Tasty (TestTree)
+import Test.Tasty.QuickCheck (
+  Arbitrary (arbitrary),
+  Property,
+  Testable (property),
+  elements,
+  forAll,
+  suchThat,
+  testProperty,
+  (.&&.),
+ )
+import Test.Util (updateMap)
+
+--------------------------------------------------------------------------------
+
+import PlutusTx.AssocMap qualified as AssocMap
+
+--------------------------------------------------------------------------------
+
+tests :: [TestTree]
+tests =
+  [ testProperty "'pmsort' sorts a list properly" prop_msortCorrect
+  , testProperty "'pmerge' merges two sorted lists into one sorted list" prop_mergeCorrect
+  , testProperty "'phalve' splits a list in half as expected" prop_halveCorrect
+  , testProperty "'pnubSort' sorts a list and remove duplicate elements" prop_nubSortProperly
+  , testProperty "'pisUniq' can tell whether all elements in a list are unique" prop_uniqueList
+  , testProperty "'pupdate' updates assoc maps as 'updateMap' does" prop_updateAssocMapParity
+  ]
+
+--------------------------------------------------------------------------------
+
+-- | Yield true if 'Agora.Utils.pmsort' sorts a given list correctly.
+prop_msortCorrect :: [Integer] -> Bool
+prop_msortCorrect l = sorted == expected
+  where
+    -- Expected sorted list, using 'Data.List.sort'.
+    expected :: [Integer]
+    expected = sort l
+
+    --
+
+    psorted :: Term _ (PBuiltinList PInteger)
+    psorted = pmsort # pconstant l
+
+    sorted :: [Integer]
+    sorted = plift psorted
+
+-- | Yield true if 'Agora.Utils.pmerge' merges two list into a ordered list correctly.
+prop_mergeCorrect :: [Integer] -> [Integer] -> Bool
+prop_mergeCorrect a b = merged == expected
+  where
+    -- Sorted list a and b
+    sa = sort a
+    sb = sort b
+
+    -- Merge two lists which are assumed to be ordered.
+    merge :: [Integer] -> [Integer] -> [Integer]
+    merge xs [] = xs
+    merge [] ys = ys
+    merge sx@(x : xs) sy@(y : ys)
+      | x <= y = x : merge xs sy
+      | otherwise = y : merge sx ys
+
+    expected :: [Integer]
+    expected = merge sa sb
+
+    --
+
+    pmerged :: Term _ (PBuiltinList PInteger)
+    pmerged = pmergeBy # plam (#<) # pconstant sa # pconstant sb
+
+    merged :: [Integer]
+    merged = plift pmerged
+
+{- | Yield true if Plutarch level 'Agora.Utils.phalve' splits a given list
+   as its Haskell level counterpart does.
+-}
+prop_halveCorrect :: [Integer] -> Bool
+prop_halveCorrect l = halved == expected
+  where
+    -- Halve a list.
+    halve :: [Integer] -> ([Integer], [Integer])
+    halve xs = go xs xs
+      where
+        go xs [] = ([], xs)
+        go (x : xs) [_] = ([x], xs)
+        go (x : xs) (_ : _ : ys) =
+          let (first, last) =
+                go xs ys
+           in (x : first, last)
+        go [] _ = ([], [])
+
+    expected :: ([Integer], [Integer])
+    expected = halve l
+
+    --
+
+    phalved :: Term _ (PPair (PBuiltinList PInteger) (PBuiltinList PInteger))
+    phalved = phalve # pconstant l
+
+    halved :: ([Integer], [Integer])
+    halved =
+      let f = plift $ pmatch phalved $ \(PPair x _) -> x
+          s = plift $ pmatch phalved $ \(PPair _ x) -> x
+       in (f, s)
+
+{- | Yield true if 'Agora.Utils.pnubSort' sorts and removes
+   duplicate elements from a given list.
+-}
+prop_nubSortProperly :: [Integer] -> Bool
+prop_nubSortProperly l = nubbed == expected
+  where
+    -- Sort and list and then nub it.
+    expected :: [Integer]
+    expected = nub $ sort l
+
+    --
+
+    pnubbed :: Term _ (PBuiltinList PInteger)
+    pnubbed = pnubSort # pconstant l
+
+    nubbed :: [Integer]
+    nubbed = plift pnubbed
+
+{- | Yield true if 'Agora.Utils.isUnique' can correctly determine
+   whether a given list only contains unique elements or not.
+-}
+prop_uniqueList :: [Integer] -> Bool
+prop_uniqueList l = isUnique == expected
+  where
+    -- Convert input list to a set.
+    -- If the set's size equals to list's size,
+    --   the list only contains unique elements.
+    expected :: Bool
+    expected = S.size (S.fromList l) == length l
+
+    --
+
+    isUnique = plift $ pisUniq # pconstant l
+
+{- | Test the parity between 'updateMap' and 'pupdate',
+     also ensure they both work correctly.
+-}
+prop_updateAssocMapParity :: Property
+prop_updateAssocMapParity =
+  runCont
+    ( do
+        -- Generate a bunch unique keys.
+        keys <-
+          cont $
+            forAll $
+              arbitrary @(S.Set Integer) `suchThat` (not . S.null)
+
+        -- Generate key-value pairs.
+        kvPairs <- cont $ forAll $ mapM (\k -> (k,) <$> (arbitrary @Integer)) $ S.toList keys
+
+        let initialMap = AssocMap.fromList kvPairs
+
+            pinitialMap :: Term _ _
+            pinitialMap = phoistAcyclic $ pconstant initialMap
+
+            referenceMap = M.fromList kvPairs
+
+        let pupdatedValue :: Maybe Integer -> Term _ (PMaybe PInteger)
+            pupdatedValue updatedValue = phoistAcyclic $ case updatedValue of
+              Nothing -> pcon PNothing
+              Just v -> pcon $ PJust $ pconstant v
+
+            -- Given the key and the updated value, test the parity
+            parity key updatedValue =
+              let native = updateMap (const updatedValue) key initialMap
+
+                  plutarch :: AssocMap.Map Integer Integer
+                  plutarch =
+                    plift $
+                      pupdate
+                        # plam (\_ -> pupdatedValue updatedValue)
+                        # pconstant key
+                        # pinitialMap
+
+                  expected =
+                    AssocMap.fromList $
+                      M.toList $
+                        M.update (const updatedValue) key referenceMap
+               in expected == native
+                    && expected == plutarch
+
+        -- Select a key, generate a maybe value.
+        -- The value at the key should be set to the new value or removed.
+        (targetKey, _) <- cont $ forAll $ elements kvPairs
+        updatedValue <- cont $ forAll $ arbitrary @(Maybe Integer)
+
+        -- Now what if the key doesn't exist in our map?
+        nonexistentKey <-
+          cont $
+            forAll $
+              arbitrary @Integer `suchThat` (\k -> not $ S.member k keys)
+
+        pure
+          ( property (parity targetKey updatedValue)
+              .&&. property (parity nonexistentKey updatedValue)
+          )
+    )
+    id