Merge branch 'emiflake/cleanup-tests' of github.com:Liqwid-Labs/agora into jhodgdev/treasury-tests

.github/workflows/integrate.yaml

@@ -89,4 +89,4 @@ jobs:
           key: ${{ runner.os }}-cabal
 
       - name: Build the project
-        run: nix build
+        run: nix build .#check.x86_64-linux

Makefile

@@ -1,4 +1,5 @@
-SHELL := /usr/bin/env bash
+# This really ought to be `/usr/bin/env bash`, but nix flakes don't like that.
+SHELL := /bin/sh
 
 .PHONY: hoogle format haddock usage
 
@@ -10,7 +11,7 @@ usage:
 	@echo "  format -- Format the project"
 	@echo "  haddock -- Generate Haddock docs for project"
 
-hoogle: 
+hoogle:
 	hoogle generate --local=haddock --database=hoo/local.hoo
 	hoogle server --local -p 8081 >> /dev/null &
 	hoogle server --local --database=hoo/local.hoo -p 8082 >> /dev/null &
@@ -21,5 +22,8 @@ format:
 	git ls-tree -r HEAD --full-tree --name-only | grep -E '.*\.nix' | xargs nixfmt
 	git ls-tree -r HEAD --full-tree --name-only | grep -E '.*\.cabal' | xargs cabal-fmt -i
 
+format_check:
+	find -name '*.hs' -not -path './dist-*/*' | xargs fourmolu $(FORMAT_EXTENSIONS) -m check
+
 haddock:
 	cabal haddock --haddock-html --haddock-hoogle --builddir=haddock

agora-test/Spec.hs

@@ -8,7 +8,7 @@ import Test.Tasty (defaultMain, testGroup)
 
 --------------------------------------------------------------------------------
 
-import Spec.Int
+import Spec.Model.MultiSig qualified as MultiSig
 import Spec.Stake qualified as Stake
 
 main :: IO ()
@@ -17,13 +17,14 @@ main =
     testGroup
       "test suite"
       [ testGroup
-          "sample-tests"
+          "Stake tests"
           Stake.tests
       , testGroup
-          "apropos-tx"
+          "Multisig tests"
           [ testGroup
-              "Int"
+              "MultiSig"
-              [ intPlutarchTests
+              [ MultiSig.plutarchTests
+              , MultiSig.genTests
               ]
           ]
       ]

agora-test/Spec/Model/MultiSig.hs

@@ -0,0 +1,186 @@
+module Spec.Model.MultiSig (
+  plutarchTests,
+  genTests,
+) where
+
+import Data.List (intersect)
+
+--------------------------------------------------------------------------------
+
+import Plutarch (compile)
+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 (HasScriptRunner (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 HasScriptRunner 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
+
+genTests :: TestTree
+genTests =
+  testGroup "genTests" $
+    fromGroup
+      <$> [ runGeneratorTestsWhere
+              (Apropos :: MultiSigModel :+ MultiSigProp)
+              "Generator"
+              Yes
+          ]
+
+plutarchTests :: TestTree
+plutarchTests =
+  testGroup "plutarchTests" $
+    fromGroup
+      <$> [ runScriptTestsWhere
+              (Apropos :: MultiSigModel :+ MultiSigProp)
+              "ScriptValid"
+              Yes
+          ]

agora-test/Spec/Sample/Stake.hs

@@ -10,11 +10,14 @@ module Spec.Sample.Stake (
   policy,
   policySymbol,
   validatorHashTN,
+  signer,
 
   -- * Script contexts
   stakeCreation,
   stakeCreationWrongDatum,
   stakeCreationUnsigned,
+  stakeDepositWithdraw,
+  DepositWithdrawExample (..),
 ) where
 
 --------------------------------------------------------------------------------
@@ -36,11 +39,12 @@ import Plutus.V1.Ledger.Api (
   ScriptContext (..),
   ScriptPurpose (..),
   ToData (toBuiltinData),
+  TxInInfo (TxInInfo),
   TxInfo (..),
   TxOut (txOutAddress, txOutDatumHash, txOutValue),
   ValidatorHash (ValidatorHash),
  )
-import Plutus.V1.Ledger.Contexts (TxOut (TxOut))
+import Plutus.V1.Ledger.Contexts (TxOut (TxOut), TxOutRef (TxOutRef))
 import Plutus.V1.Ledger.Interval qualified as Interval
 import Plutus.V1.Ledger.Scripts (Validator)
 import Plutus.V1.Ledger.Value (TokenName (TokenName))
@@ -50,6 +54,7 @@ import Plutus.V1.Ledger.Value qualified as Value
 
 import Agora.SafeMoney
 import Agora.Stake
+import Spec.Util (datumPair, toDatumHash)
 
 --------------------------------------------------------------------------------
 
@@ -120,3 +125,59 @@ stakeCreationUnsigned =
           }
     , scriptContextPurpose = Minting policySymbol
     }
+
+--------------------------------------------------------------------------------
+
+data DepositWithdrawExample = DepositWithdrawExample
+  { startAmount :: Integer
+  , delta :: Integer
+  }
+
+stakeDepositWithdraw :: DepositWithdrawExample -> ScriptContext
+stakeDepositWithdraw config =
+  let st = Value.singleton policySymbol validatorHashTN 1 -- Stake ST
+      stakeBefore :: StakeDatum
+      stakeBefore = StakeDatum config.startAmount signer
+
+      stakeAfter :: StakeDatum
+      stakeAfter = stakeBefore {stakedAmount = stakeBefore.stakedAmount + config.delta}
+   in ScriptContext
+        { scriptContextTxInfo =
+            TxInfo
+              { txInfoInputs =
+                  [ TxInInfo
+                      (TxOutRef "0b2086cbf8b6900f8cb65e012de4516cb66b5cb08a9aaba12a8b88be" 1)
+                      TxOut
+                        { txOutAddress = Address (ScriptCredential $ validatorHash validator) Nothing
+                        , txOutValue =
+                            st
+                              <> Value.singleton
+                                "da8c30857834c6ae7203935b89278c532b3995245295456f993e1d24"
+                                "LQ"
+                                stakeBefore.stakedAmount
+                        , txOutDatumHash = Just (toDatumHash stakeAfter)
+                        }
+                  ]
+              , txInfoOutputs =
+                  [ TxOut
+                      { txOutAddress = Address (ScriptCredential $ validatorHash validator) Nothing
+                      , txOutValue =
+                          st
+                            <> Value.singleton
+                              "da8c30857834c6ae7203935b89278c532b3995245295456f993e1d24"
+                              "LQ"
+                              stakeAfter.stakedAmount
+                      , txOutDatumHash = Just (toDatumHash stakeAfter)
+                      }
+                  ]
+              , txInfoFee = Value.singleton "" "" 2
+              , txInfoMint = st
+              , txInfoDCert = []
+              , txInfoWdrl = []
+              , txInfoValidRange = Interval.always
+              , txInfoSignatories = [signer]
+              , txInfoData = [datumPair stakeAfter]
+              , txInfoId = "0b2086cbf8b6900f8cb65e012de4516cb66b5cb08a9aaba12a8b88be"
+              }
+        , scriptContextPurpose = Spending (TxOutRef "0b2086cbf8b6900f8cb65e012de4516cb66b5cb08a9aaba12a8b88be" 1)
+        }

agora-test/Spec/Stake.hs

@@ -10,16 +10,13 @@ import Test.Tasty (TestTree, testGroup)
 
 --------------------------------------------------------------------------------
 
-import Plutarch.Builtin (pforgetData)
+import Agora.Stake (StakeDatum (StakeDatum), StakeRedeemer (DepositWithdraw), stakePolicy, stakeValidator)
-
---------------------------------------------------------------------------------
-
-import Agora.Stake (stakePolicy)
 
 --------------------------------------------------------------------------------
 
+import Spec.Sample.Stake (DepositWithdrawExample (DepositWithdrawExample, delta, startAmount), signer)
 import Spec.Sample.Stake qualified as Stake
-import Spec.Util (policyFailsWith, policySucceedsWith)
+import Spec.Util (policyFailsWith, policySucceedsWith, toDatum, validatorFailsWith, validatorSucceedsWith)
 
 --------------------------------------------------------------------------------
 
@@ -30,17 +27,35 @@ tests =
       [ policySucceedsWith
           "stakeCreation"
           (stakePolicy Stake.stake)
-          (pforgetData (pconstantData ()))
+          ()
           Stake.stakeCreation
       , policyFailsWith
           "stakeCreationWrongDatum"
           (stakePolicy Stake.stake)
-          (pforgetData (pconstantData ()))
+          ()
           Stake.stakeCreationWrongDatum
       , policyFailsWith
           "stakeCreationUnsigned"
           (stakePolicy Stake.stake)
-          (pforgetData (pconstantData ()))
+          ()
           Stake.stakeCreationUnsigned
+      , 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 (negate 1_000_000))
+          (Stake.stakeDepositWithdraw $ DepositWithdrawExample {startAmount = 100_000, delta = negate 1_000_000})
       ]
   ]

agora-test/Spec/Treasury.hs

@@ -1,4 +1,4 @@
-module Spec.Treasury () where
+module Spec.Treasury (tests) where
 
 import Test.Tasty (TestTree, testGroup)
 

agora-test/Spec/Util.hs

@@ -1,8 +1,17 @@
 module Spec.Util (
+  -- * Testing utils
   scriptSucceeds,
   scriptFails,
   policySucceedsWith,
   policyFailsWith,
+  validatorSucceedsWith,
+  validatorFailsWith,
+
+  -- * Plutus land utils
+  datumHash,
+  toDatum,
+  toDatumHash,
+  datumPair,
 ) where
 
 --------------------------------------------------------------------------------
@@ -11,31 +20,105 @@ import Prelude
 
 --------------------------------------------------------------------------------
 
+import Codec.Serialise (serialise)
+import Data.ByteString.Lazy qualified as LBS
+
+--------------------------------------------------------------------------------
+
 import Test.Tasty (TestTree)
 import Test.Tasty.HUnit (assertFailure, testCase)
 
 --------------------------------------------------------------------------------
 
 import Plutarch
-import Plutarch.Api.V1 (PMintingPolicy)
+import Plutarch.Api.V1 (PMintingPolicy, PValidator)
+import Plutarch.Builtin (pforgetData)
+import Plutarch.Crypto (pblake2b_256)
 import Plutarch.Evaluate (evalScript)
+import Plutarch.Lift (PUnsafeLiftDecl (PLifted))
 import Plutarch.Prelude ()
-import Plutus.V1.Ledger.Scripts (Script)
+import Plutus.V1.Ledger.Contexts (ScriptContext)
+import Plutus.V1.Ledger.Scripts (Datum (Datum), DatumHash (DatumHash), Script)
+import PlutusTx.Builtins qualified as PlutusTx
+import PlutusTx.IsData qualified as PlutusTx
 
 --------------------------------------------------------------------------------
 
 policySucceedsWith ::
+  ( PLift redeemer
+  , PlutusTx.ToData (PLifted redeemer)
+  ) =>
   String ->
   ClosedTerm PMintingPolicy ->
-  ClosedTerm PData ->
+  PLifted redeemer ->
-  _ ->
+  ScriptContext ->
   TestTree
 policySucceedsWith tag policy redeemer scriptContext =
-  scriptSucceeds tag $ compile (policy # redeemer # pconstant scriptContext)
+  scriptSucceeds tag $
+    compile
+      ( policy
+          # pforgetData (pconstantData redeemer)
+          # pconstant scriptContext
+      )
 
-policyFailsWith :: String -> ClosedTerm PMintingPolicy -> ClosedTerm PData -> _ -> TestTree
+policyFailsWith ::
+  ( PLift redeemer
+  , PlutusTx.ToData (PLifted redeemer)
+  ) =>
+  String ->
+  ClosedTerm PMintingPolicy ->
+  PLifted redeemer ->
+  ScriptContext ->
+  TestTree
 policyFailsWith tag policy redeemer scriptContext =
-  scriptFails tag $ compile (policy # redeemer # pconstant 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 ->
+  TestTree
+validatorSucceedsWith tag policy datum redeemer scriptContext =
+  scriptSucceeds tag $
+    compile
+      ( policy
+          # 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 ->
+  TestTree
+validatorFailsWith tag policy datum redeemer scriptContext =
+  scriptFails tag $
+    compile
+      ( policy
+          # pforgetData (pconstantData datum)
+          # pforgetData (pconstantData redeemer)
+          # pconstant scriptContext
+      )
 
 scriptSucceeds :: String -> Script -> TestTree
 scriptSucceeds name script = testCase name $ do
@@ -56,3 +139,30 @@ scriptFails name script = testCase name $ do
     Right v ->
       assertFailure $
         "Expected failure, but succeeded. " <> show v <> " Traces: " <> show traces
+
+--------------------------------------------------------------------------------
+
+{- | Create a pair from data for use in 'txInfoData'
+
+   Example:
+   @
+     myTxInfo { 'txInfoData' = ['datumPair' myDatum] }
+   @
+-}
+datumPair :: PlutusTx.ToData a => a -> (DatumHash, Datum)
+datumPair = (,) <$> toDatumHash <*> toDatum
+
+datumHash :: Datum -> DatumHash
+datumHash (Datum data') = toDatumHash data'
+
+toDatum :: PlutusTx.ToData a => a -> Datum
+toDatum = Datum . PlutusTx.toBuiltinData
+
+-- Shamelessly go through plutus.
+toDatumHash :: PlutusTx.ToData a => a -> DatumHash
+toDatumHash datum =
+  DatumHash $
+    PlutusTx.toBuiltin $
+      plift $
+        pblake2b_256
+          # pconstant (LBS.toStrict $ serialise $ PlutusTx.toData datum)

agora.cabal

@@ -148,7 +148,7 @@ test-suite agora-test
   main-is:        Spec.hs
   hs-source-dirs: agora-test
   other-modules:
-    Spec.Int
+    Spec.Model.MultiSig
     Spec.Sample.Stake
     Spec.Sample.Treasury
     Spec.Stake

agora/Agora/MultiSig.hs

@@ -47,7 +47,7 @@ data MultiSig = MultiSig
   -- ^ List of PubKeyHashes that must be present in the list of signatories.
   , minSigs :: Integer
   }
-  deriving stock (GHC.Generic)
+  deriving stock (GHC.Generic, Eq, Show)
   deriving anyclass (Generic)
 
 PlutusTx.makeLift ''MultiSig

agora/Agora/SafeMoney.hs

@@ -13,6 +13,8 @@ module Agora.SafeMoney (
 
   -- * Utility functions
   paddDiscrete,
+  pgeqDiscrete,
+  pzeroDiscrete,
 
   -- * Conversions
   pdiscreteValue,
@@ -56,7 +58,7 @@ type MoneyClass =
     Nat
   )
 
--- | A `PDiscrete` amount of currency tagged on the type level with the `MoneyClass` it belong sto
+-- | A 'PDiscrete' amount of currency tagged on the type level with the 'MoneyClass' it belongs to
 newtype PDiscrete (mc :: MoneyClass) (s :: S)
   = PDiscrete (Term s PInteger)
   deriving (PlutusType, PIsData, PEq, POrd) via (DerivePNewtype (PDiscrete mc) PInteger)
@@ -65,7 +67,19 @@ newtype Discrete (mc :: MoneyClass)
   = Discrete Integer
   deriving stock (Show)
 
--- | Add two `PDiscrete` values of the same `MoneyClass`.
+-- | Check if one 'PDiscrete' is greater than another.
+pgeqDiscrete :: forall (mc :: MoneyClass) (s :: S). Term s (PDiscrete mc :--> PDiscrete mc :--> PBool)
+pgeqDiscrete = phoistAcyclic $
+  plam $ \x y -> P.do
+    PDiscrete x' <- pmatch x
+    PDiscrete y' <- pmatch y
+    y' #<= x'
+
+-- | Conjure zero discrete unit for any moneyclass
+pzeroDiscrete :: forall (mc :: MoneyClass) (s :: S). Term s (PDiscrete mc)
+pzeroDiscrete = phoistAcyclic $ pcon (PDiscrete 0)
+
+-- | Add two 'PDiscrete' values of the same 'MoneyClass'.
 paddDiscrete :: Term s (PDiscrete mc :--> PDiscrete mc :--> PDiscrete mc)
 paddDiscrete = phoistAcyclic $
   -- In the future, this should use plutarch-numeric
@@ -100,7 +114,7 @@ pvalueDiscrete = phoistAcyclic $
         # f
 
 {- | Get a `PValue` from a `PDiscrete`.
-     __NOTE__: `pdiscreteValue` after `pvalueDiscrete` is loses information
+     __NOTE__: `pdiscreteValue` after `pvalueDiscrete` loses information
 -}
 pdiscreteValue ::
   forall (moneyClass :: MoneyClass) (ac :: Symbol) (n :: Symbol) (scale :: Nat) s.

agora/Agora/Stake.hs

@@ -9,8 +9,9 @@ Vote-lockable stake UTXOs holding GT.
 -}
 module Agora.Stake (
   PStakeDatum (..),
-  PStakeAction (..),
+  PStakeRedeemer (..),
   StakeDatum (..),
+  StakeRedeemer (..),
   Stake (..),
   stakePolicy,
   stakeValidator,
@@ -19,9 +20,12 @@ module Agora.Stake (
 
 --------------------------------------------------------------------------------
 
+import Data.Proxy (Proxy (Proxy))
+import Data.String (IsString (fromString))
 import GHC.Generics qualified as GHC
 import GHC.TypeLits (
   KnownSymbol,
+  symbolVal,
  )
 import Generics.SOP (Generic, I (I))
 import Prelude
@@ -50,6 +54,7 @@ import Plutarch.DataRepr (
  )
 import Plutarch.Internal (punsafeCoerce)
 import Plutarch.Monadic qualified as P
+import Plutus.V1.Ledger.Value (AssetClass (AssetClass))
 
 --------------------------------------------------------------------------------
 
@@ -58,6 +63,8 @@ import Agora.SafeMoney (
   PDiscrete,
   paddDiscrete,
   pdiscreteValue,
+  pgeqDiscrete,
+  pzeroDiscrete,
  )
 import Agora.Utils (
   anyInput,
@@ -65,6 +72,9 @@ import Agora.Utils (
   paddValue,
   passert,
   pfindTxInByTxOutRef,
+  pgeqBy,
+  pgeqBy',
+  pgeqBySymbol,
   psingletonValue,
   psymbolValueOf,
   ptxSignedBy,
@@ -77,7 +87,7 @@ import Agora.Utils (
 data Stake (gt :: MoneyClass) = Stake
 
 -- | Plutarch-level redeemer for Stake scripts.
-data PStakeAction (gt :: MoneyClass) (s :: S)
+data PStakeRedeemer (gt :: MoneyClass) (s :: S)
   = -- | Deposit or withdraw a discrete amount of the staked governance token.
     PDepositWithdraw (Term s (PDataRecord '["delta" ':= PDiscrete gt]))
   | -- | Destroy a stake, retrieving its LQ, the minimum ADA and any other assets.
@@ -87,7 +97,23 @@ data PStakeAction (gt :: MoneyClass) (s :: S)
   deriving anyclass (PIsDataRepr)
   deriving
     (PlutusType, PIsData)
-    via PIsDataReprInstances (PStakeAction gt)
+    via PIsDataReprInstances (PStakeRedeemer gt)
+
+-- FIXME: 'StakeRedeemer' and 'StakeDatum' are stripped of their
+-- typesafe `PDiscrete` equivalent due to issues with `makeIsDataIndexed`
+-- when using the kind @gt :: MoneyClass@. This ought to be fixed with
+-- a future patch in Plutarch upstream. For now, we will deal with lower
+-- type safety off-chain.
+
+-- | Haskell-level redeemer for Stake scripts.
+data StakeRedeemer
+  = -- | Deposit or withdraw a discrete amount of the staked governance token.
+    DepositWithdraw Integer
+  | -- | Destroy a stake, retrieving its LQ, the minimum ADA and any other assets.
+    Destroy
+  deriving stock (Show, GHC.Generic)
+
+PlutusTx.makeIsDataIndexed ''StakeRedeemer [('DepositWithdraw, 0), ('Destroy, 1)]
 
 -- | Plutarch-level datum for Stake scripts.
 newtype PStakeDatum (gt :: MoneyClass) (s :: S) = PStakeDatum
@@ -103,7 +129,8 @@ newtype PStakeDatum (gt :: MoneyClass) (s :: S) = PStakeDatum
 
 -- | Haskell-level datum for Stake scripts.
 data StakeDatum = StakeDatum
-  { stakedAmount :: Integer
+  { -- FIXME: This needs to be gt
+  stakedAmount :: Integer
   , owner :: PubKeyHash
   }
   deriving stock (Show, GHC.Generic)
@@ -200,8 +227,28 @@ stakePolicy _stake =
                             # ctx.txInfo
                             # stakeDatum.owner
 
-                    -- TODO: Needs to be >=, rather than ==
+                    -- TODO: This is quite inefficient now, as it does two lookups
-                    let valueCorrect = pdata value #== pdata expectedValue
+                    -- instead of a more efficient single pass,
+                    -- but it doesn't really matter for this. At least it's correct.
+                    let valueCorrect =
+                          foldr1
+                            (#&&)
+                            [ pgeqBy' (AssetClass ("", "")) # value # expectedValue
+                            , pgeqBy'
+                                ( AssetClass
+                                    ( fromString . symbolVal $ Proxy @ac
+                                    , fromString . symbolVal $ Proxy @n
+                                    )
+                                )
+                                # value
+                                # expectedValue
+                            , pgeqBy
+                                # ownSymbol
+                                # tn
+                                # value
+                                # expectedValue
+                            ]
+
                     ownerSignsTransaction
                       #&& valueCorrect
           popaque (pconstant ())
@@ -226,8 +273,8 @@ stakeValidator stake =
     txInfo <- pletFields @'["mint", "inputs", "outputs"] txInfo'
 
     -- Coercion is safe in that if coercion fails we crash hard.
-    let stakeAction :: Term _ (PStakeAction gt)
+    let stakeRedeemer :: Term _ (PStakeRedeemer gt)
-        stakeAction = pfromData $ punsafeCoerce redeemer
+        stakeRedeemer = pfromData $ punsafeCoerce redeemer
         stakeDatum' :: Term _ (PStakeDatum gt)
         stakeDatum' = pfromData $ punsafeCoerce datum
     stakeDatum <- pletFields @'["owner", "stakedAmount"] stakeDatum'
@@ -242,7 +289,7 @@ stakeValidator stake =
     mintedST <- plet $ psymbolValueOf # stCurrencySymbol # txInfo.mint
     spentST <- plet $ psymbolValueOf # stCurrencySymbol #$ pvalueSpent # txInfo'
 
-    pmatch stakeAction $ \case
+    pmatch stakeRedeemer $ \case
       PDestroy _ -> P.do
         passert "ST at inputs must be 1" $
           spentST #== 1
@@ -270,13 +317,43 @@ stakeValidator stake =
               delta <- plet $ pfield @"delta" # r
               let isScriptAddress = pdata address #== ownAddress
               let correctOutputDatum =
-                    stakeDatum.owner #== newStakeDatum.owner
+                    foldr1
-                      #&& (paddDiscrete # stakeDatum.stakedAmount # delta) #== newStakeDatum.stakedAmount
+                      (#&&)
+                      [ stakeDatum.owner #== newStakeDatum.owner
+                      , (paddDiscrete # stakeDatum.stakedAmount # delta) #== newStakeDatum.stakedAmount
+                      , -- We can't magically conjure GT anyway (no input to spend!)
+                        -- do we need to check this, really?
+                        pgeqDiscrete # (pfromData newStakeDatum.stakedAmount) # pzeroDiscrete
+                      ]
               let expectedValue = paddValue # continuingValue # (pdiscreteValue # delta)
 
-              -- TODO: As above, needs to be >=, rather than ==
+              -- TODO: Same as above. This is quite inefficient now, as it does two lookups
-              let correctValue = pdata value #== pdata expectedValue
+              -- instead of a more efficient single pass,
-              isScriptAddress #&& correctOutputDatum #&& correctValue
+              -- but it doesn't really matter for this. At least it's correct.
+              let valueCorrect =
+                    foldr1
+                      (#&&)
+                      [ pgeqBy' (AssetClass ("", "")) # value # expectedValue
+                      , pgeqBy'
+                          ( AssetClass
+                              ( fromString . symbolVal $ Proxy @ac
+                              , fromString . symbolVal $ Proxy @n
+                              )
+                          )
+                          # value
+                          # expectedValue
+                      , pgeqBySymbol
+                          # stCurrencySymbol
+                          # value
+                          # expectedValue
+                      ]
+
+              foldr1
+                (#&&)
+                [ ptraceIfFalse "isScriptAddress" isScriptAddress
+                , ptraceIfFalse "correctOutputDatum" correctOutputDatum
+                , ptraceIfFalse "valueCorrect" valueCorrect
+                ]
 
         popaque (pconstant ())
 

agora/Agora/Utils.hs

@@ -19,6 +19,9 @@ module Agora.Utils (
   psymbolValueOf,
   passetClassValueOf,
   passetClassValueOf',
+  pgeqBy,
+  pgeqBySymbol,
+  pgeqBy',
   pfindTxInByTxOutRef,
   psingletonValue,
   pfindMap,
@@ -180,6 +183,27 @@ passetClassValueOf' :: AssetClass -> Term s (PValue :--> PInteger)
 passetClassValueOf' (AssetClass (sym, token)) =
   passetClassValueOf # pconstant sym # pconstant token
 
+-- | Return '>=' on two values comparing by only a particular AssetClass
+pgeqBy :: Term s (PCurrencySymbol :--> PTokenName :--> PValue :--> PValue :--> PBool)
+pgeqBy =
+  phoistAcyclic $
+    plam $ \cs tn a b ->
+      passetClassValueOf # cs # tn # b #<= passetClassValueOf # cs # tn # a
+
+-- | Return '>=' on two values comparing by only a particular AssetClass
+pgeqBySymbol :: Term s (PCurrencySymbol :--> PValue :--> PValue :--> PBool)
+pgeqBySymbol =
+  phoistAcyclic $
+    plam $ \cs a b ->
+      psymbolValueOf # cs # b #<= psymbolValueOf # cs # a
+
+-- | Return '>=' on two values comparing by only a particular Haskell-level AssetClass
+pgeqBy' :: AssetClass -> Term s (PValue :--> PValue :--> PBool)
+pgeqBy' ac =
+  phoistAcyclic $
+    plam $ \a b ->
+      passetClassValueOf' ac # b #<= passetClassValueOf' ac # a
+
 -- | Union two maps using a merge function on collisions.
 pmapUnionWith :: forall k v s. PIsData v => Term s ((v :--> v :--> v) :--> PMap k v :--> PMap k v :--> PMap k v)
 pmapUnionWith = phoistAcyclic $

flake.nix

@@ -93,9 +93,9 @@
           pkgs = nixpkgsFor system;
           pkgs' = nixpkgsFor' system;
           inherit (pkgs.haskell-nix.tools ghcVersion {
-            inherit (plutarch.tools) fourmolu hlint;
+            inherit (plutarch.tools) fourmolu;
           })
-            fourmolu hlint;
+            fourmolu;
         in pkgs.runCommand "format-check" {
           nativeBuildInputs = [
             pkgs'.git
@@ -103,14 +103,13 @@
             pkgs'.haskellPackages.cabal-fmt
             pkgs'.nixpkgs-fmt
             fourmolu
-            hlint
           ];
         } ''
           export LC_CTYPE=C.UTF-8
           export LC_ALL=C.UTF-8
           export LANG=C.UTF-8
           cd ${self}
-          make format_check
+          make format_check || (echo "    Please run 'make format'" ; exit 1)
           mkdir $out
         '';
     in {
@@ -118,9 +117,13 @@
       flake = perSystem (system: (projectFor system).flake { });
 
       packages = perSystem (system: self.flake.${system}.packages);
+
+      # Define what we want to test
       checks = perSystem (system:
         self.flake.${system}.checks // {
           formatCheck = formatCheckFor system;
+          agora = self.flake.${system}.packages."agora:lib:agora";
+          agora-test = self.flake.${system}.packages."agora:test:agora-test";
         });
       check = perSystem (system:
         (nixpkgsFor system).runCommand "combined-test" {
@@ -130,7 +133,5 @@
           touch $out
         '');
       devShell = perSystem (system: self.flake.${system}.devShell);
-      defaultPackage =
-        perSystem (system: self.flake.${system}.packages."agora:lib:agora");
     };
 }