From f417f32f4e9c88ba4ce3214096e05e9d432601db Mon Sep 17 00:00:00 2001
From: Jack Hodgkinson <30505104+jhodgdev@users.noreply.github.com>
Date: Fri, 18 Mar 2022 12:19:45 +0000
Subject: [PATCH 01/12] paired programming work

---
 agora-test/Model/MultiSig.hs | 59 ++++++++++++++++++++++++++++++++++++
 agora-test/Spec/Int.hs       | 11 ++++++-
 agora.cabal                  |  9 ++----
 3 files changed, 72 insertions(+), 7 deletions(-)
 create mode 100644 agora-test/Model/MultiSig.hs

diff --git a/agora-test/Model/MultiSig.hs b/agora-test/Model/MultiSig.hs
new file mode 100644
index 0000000..bafb9b4
--- /dev/null
+++ b/agora-test/Model/MultiSig.hs
@@ -0,0 +1,59 @@
+module Model.MultiSig () where
+
+import Agora.MultiSig (MultiSig (..))
+import Apropos (Apropos (Apropos), Formula (ExactlyOne), (:+))
+import Apropos.Script (HasScriptRunner (expect, script))
+import Plutus.V1.Ledger.Api (PubKeyHash, Script)
+
+{-
+
+1. Create proposition sum type.
+2. Create logical model defining relationships between propositions.
+3. Associating propositions with the "concrete" type i.e. MultiSig.
+4. Create Generators.
+5. Run tests (with magic).
+
+-}
+
+{-
+
+1. Create a
+
+Define a prop, as if it is the way a script can pass.
+  1. keys signed exceeds `minSigs`
+  2. `minSigs` is lte zero.
+
+Props not passing:
+  1. No signatures present.
+  2. Signatures present is less than `minSigs`.
+
+-}
+
+data MultiSigModel = MultiSigModel
+  { ms :: MultiSig
+  , ctx :: ScriptContext
+  }
+
+data MultiSigProp
+  = MeetsMinSigs
+  | DoesNotMeetMinSigs
+
+instance LogicalModel MultiSigModel where
+  logic = ExactlyOne [Var MeetsMinSigs, Var DoesNotMeetMinSigs]
+
+instance HasLogicalModel MultiSigProp MultiSigModel where
+  satisfiesProperty :: MultiSigProp -> MultiSigModel -> Bool
+  satisfiesProperty p m =
+    let minSigs = m.ms.minSigs
+        signatories = m.ctx.txInfo.txInfoSignatories
+        matchingSigs = intersect m.ms.keys signatories
+     in case p of
+          MeetsMinSigs -> length matchingSigs >= minSigs
+          DoesNotMeetMinSigs -> length matchingSigs < minSigs
+
+instance HasScriptRunner MultiSigProp MultiSig where
+  expect :: (MultiSigModel :+ MultiSigProp) -> Formula MultiSigProp
+  expect = undefined
+
+  script :: (MultiSigModel :+ MultiSigProp) -> MultiSig -> Script
+  script Apropos msm = compile $ validatedByMultisig msm . ms
diff --git a/agora-test/Spec/Int.hs b/agora-test/Spec/Int.hs
index 8063784..f89abdc 100644
--- a/agora-test/Spec/Int.hs
+++ b/agora-test/Spec/Int.hs
@@ -78,7 +78,16 @@ instance HasScriptRunner IntProp Int where
   expect _ = Var IsSmall :&&: Var IsNegative
   script _ i =
     let ii = fromIntegral i :: Integer
-     in compile (pif ((fromInteger ii #< (0 :: Term s PInteger)) #&& ((fromInteger (-10) :: Term s PInteger) #<= fromInteger ii)) (pcon PUnit) perror)
+     in compile
+          ( pif
+              ( ( fromInteger ii
+                    #< (0 :: Term s PInteger)
+                )
+                  #&& ((fromInteger (-10) :: Term s PInteger) #<= fromInteger ii)
+              )
+              (pcon PUnit)
+              perror
+          )
 
 intPlutarchTests :: TestTree
 intPlutarchTests =
diff --git a/agora.cabal b/agora.cabal
index 8d17d47..6ffd3b3 100644
--- a/agora.cabal
+++ b/agora.cabal
@@ -107,12 +107,12 @@ common deps
 
 common test-deps
   build-depends:
+    , apropos-tx
     , QuickCheck
     , quickcheck-instances
     , tasty
     , tasty-hedgehog
     , tasty-hunit
-    , apropos-tx
 
 library
   import:          lang, deps
@@ -151,16 +151,13 @@ test-suite agora-test
     Spec.Int
     Spec.Sample.Stake
     Spec.Stake
-
     Spec.Util
 
-  build-depends:
-    , agora
+  build-depends:  agora
 
 benchmark agora-bench
   import:         lang, deps
   hs-source-dirs: agora-bench
   main-is:        Main.hs
   type:           exitcode-stdio-1.0
-  build-depends:
-    , agora
+  build-depends:  agora

From 7ef5606cd7c2317d4d27def7f1ccfee0f92e1b52 Mon Sep 17 00:00:00 2001
From: Emily Martins <emi@haskell.fyi>
Date: Fri, 18 Mar 2022 15:23:07 +0100
Subject: [PATCH 02/12] add HasParameterisedGenerator and wire tests up

---
 agora-test/Model/MultiSig.hs | 112 +++++++++++++++++++++++++++++++----
 agora-test/Spec.hs           |   6 ++
 agora.cabal                  |   1 +
 agora/Agora/MultiSig.hs      |   2 +-
 4 files changed, 107 insertions(+), 14 deletions(-)

diff --git a/agora-test/Model/MultiSig.hs b/agora-test/Model/MultiSig.hs
index bafb9b4..3ff1b04 100644
--- a/agora-test/Model/MultiSig.hs
+++ b/agora-test/Model/MultiSig.hs
@@ -1,9 +1,28 @@
-module Model.MultiSig () where
+module Model.MultiSig (plutarchTests, genTests) where
 
-import Agora.MultiSig (MultiSig (..))
-import Apropos (Apropos (Apropos), Formula (ExactlyOne), (:+))
-import Apropos.Script (HasScriptRunner (expect, script))
-import Plutus.V1.Ledger.Api (PubKeyHash, Script)
+import Agora.MultiSig (MultiSig (..), validatedByMultisig)
+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 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 Test.Tasty (TestTree, testGroup)
+import Test.Tasty.Hedgehog (fromGroup)
 
 {-
 
@@ -33,27 +52,94 @@ data MultiSigModel = MultiSigModel
   { ms :: MultiSig
   , ctx :: ScriptContext
   }
+  deriving stock (Eq, Show)
 
 data MultiSigProp
   = MeetsMinSigs
   | DoesNotMeetMinSigs
+  deriving stock (Eq, Show, Ord)
 
-instance LogicalModel MultiSigModel where
+instance Enumerable MultiSigProp where
+  enumerated = [MeetsMinSigs, DoesNotMeetMinSigs]
+
+instance LogicalModel MultiSigProp where
   logic = ExactlyOne [Var MeetsMinSigs, Var DoesNotMeetMinSigs]
 
 instance HasLogicalModel MultiSigProp MultiSigModel where
   satisfiesProperty :: MultiSigProp -> MultiSigModel -> Bool
   satisfiesProperty p m =
     let minSigs = m.ms.minSigs
-        signatories = m.ctx.txInfo.txInfoSignatories
+        signatories = txInfoSignatories $ scriptContextTxInfo $ m.ctx
         matchingSigs = intersect m.ms.keys signatories
      in case p of
-          MeetsMinSigs -> length matchingSigs >= minSigs
-          DoesNotMeetMinSigs -> length matchingSigs < minSigs
+          MeetsMinSigs -> length matchingSigs >= fromInteger minSigs
+          DoesNotMeetMinSigs -> length matchingSigs < fromInteger minSigs
 
-instance HasScriptRunner MultiSigProp MultiSig where
+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)
+    }
+
+genPK :: Gen PubKeyHash
+genPK =
+  choice
+    [ pure "8a30896c4fd5e79843e4ca1bd2cdbaa36f8c0bc3be7401214142019c"
+    , pure "0b12051dd2da4b3629cebb92e2be111e0e99c63c04727ed55b74a296"
+    , pure "87f5f31e4d7437463cd901c4c9edb7a51903ac858661503e9d72f492"
+    , pure "f74ccaee8244264b3c73fce3b66bd2337de3db70efff4261d6ff145b"
+    ]
+
+instance HasParameterisedGenerator MultiSigProp MultiSigModel where
+  parameterisedGenerator s = do
+    expectedSignatures <- list (linear 1 4) genPK
+    minSigs <- toInteger <$> int (linear 1 (length expectedSignatures))
+    let msig = MultiSig expectedSignatures minSigs
+
+    actualSignaturesLength <-
+      if MeetsMinSigs `elem` s
+        then int (linear (fromInteger minSigs) (length expectedSignatures))
+        else pure 0
+    let actualSignatures = take actualSignaturesLength expectedSignatures
+
+    let ctx = contextWithSignatures actualSignatures
+    pure (MultiSigModel msig ctx)
+
+instance HasScriptRunner MultiSigProp MultiSigModel where
   expect :: (MultiSigModel :+ MultiSigProp) -> Formula MultiSigProp
-  expect = undefined
+  expect Apropos = Var MeetsMinSigs
 
-  script :: (MultiSigModel :+ MultiSigProp) -> MultiSig -> Script
-  script Apropos msm = compile $ validatedByMultisig msm . ms
+  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
+          ]
diff --git a/agora-test/Spec.hs b/agora-test/Spec.hs
index 37def06..fada856 100644
--- a/agora-test/Spec.hs
+++ b/agora-test/Spec.hs
@@ -8,6 +8,7 @@ import Test.Tasty (defaultMain, testGroup)
 
 --------------------------------------------------------------------------------
 
+import Model.MultiSig qualified
 import Spec.Int
 import Spec.Stake qualified as Stake
 
@@ -25,5 +26,10 @@ main =
               "Int"
               [ intPlutarchTests
               ]
+          , testGroup
+              "MultiSig"
+              [ Model.MultiSig.plutarchTests
+              , Model.MultiSig.genTests
+              ]
           ]
       ]
diff --git a/agora.cabal b/agora.cabal
index 6ffd3b3..be8ab96 100644
--- a/agora.cabal
+++ b/agora.cabal
@@ -151,6 +151,7 @@ test-suite agora-test
     Spec.Int
     Spec.Sample.Stake
     Spec.Stake
+    Model.MultiSig
     Spec.Util
 
   build-depends:  agora
diff --git a/agora/Agora/MultiSig.hs b/agora/Agora/MultiSig.hs
index 2014c02..1e8a548 100644
--- a/agora/Agora/MultiSig.hs
+++ b/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

From 0b422f83da129608a4a11e870757ed523cd7d1aa Mon Sep 17 00:00:00 2001
From: Jack Hodgkinson <30505104+jhodgdev@users.noreply.github.com>
Date: Fri, 18 Mar 2022 14:46:47 +0000
Subject: [PATCH 03/12] Added some annotations to work on multisig apropos
 testing

---
 agora-test/Model/MultiSig.hs | 104 +++++++++++++++++++++++++----------
 1 file changed, 76 insertions(+), 28 deletions(-)

diff --git a/agora-test/Model/MultiSig.hs b/agora-test/Model/MultiSig.hs
index 3ff1b04..8630617 100644
--- a/agora-test/Model/MultiSig.hs
+++ b/agora-test/Model/MultiSig.hs
@@ -1,7 +1,16 @@
 module Model.MultiSig (plutarchTests, genTests) where
 
 import Agora.MultiSig (MultiSig (..), validatedByMultisig)
-import Apropos (Apropos (Apropos), Formula (ExactlyOne, Var, Yes), HasLogicalModel (..), HasParameterisedGenerator, LogicalModel (logic), parameterisedGenerator, runGeneratorTestsWhere, (:+))
+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))
@@ -12,7 +21,17 @@ import Plutus.V1.Ledger.Api (
   Script,
   ScriptContext (scriptContextPurpose),
   ScriptPurpose (Spending),
-  TxInfo (txInfoDCert, txInfoData, txInfoFee, txInfoId, txInfoInputs, txInfoMint, txInfoOutputs, txInfoValidRange, txInfoWdrl),
+  TxInfo (
+    txInfoDCert,
+    txInfoData,
+    txInfoFee,
+    txInfoId,
+    txInfoInputs,
+    txInfoMint,
+    txInfoOutputs,
+    txInfoValidRange,
+    txInfoWdrl
+  ),
   TxOutRef (TxOutRef),
   scriptContextTxInfo,
   txInfoSignatories,
@@ -24,45 +43,50 @@ import Plutus.V1.Ledger.Value qualified as Value
 import Test.Tasty (TestTree, testGroup)
 import Test.Tasty.Hedgehog (fromGroup)
 
-{-
+{- Function definitions for reference:
 
-1. Create proposition sum type.
-2. Create logical model defining relationships between propositions.
-3. Associating propositions with the "concrete" type i.e. MultiSig.
-4. Create Generators.
-5. Run tests (with magic).
-
--}
-
-{-
-
-1. Create a
-
-Define a prop, as if it is the way a script can pass.
-  1. keys signed exceeds `minSigs`
-  2. `minSigs` is lte zero.
-
-Props not passing:
-  1. No signatures present.
-  2. Signatures present is less than `minSigs`.
+{- | A MultiSig represents a proof that a particular set of
+     signatures are present on a transaction.
+-}
+data MultiSig = MultiSig
+  { keys :: [PubKeyHash]
+  -- ^ List of PubKeyHashes that must be present in the list of signatories.
+  , minSigs :: Integer
+  }
+  deriving stock (GHC.Generic, Eq, Show)
+  deriving anyclass (Generic)
+
+-- | Check if a Haskell-level MultiSig signs this transaction.
+validatedByMultisig :: MultiSig -> Term s (PTxInfo :--> PBool)
+validatedByMultisig params =
+  phoistAcyclic $
+    pvalidatedByMultisig # pconstant params
 
 -}
 
+-- | 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
-  = MeetsMinSigs
-  | DoesNotMeetMinSigs
+  = -- | 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
@@ -75,6 +99,9 @@ instance HasLogicalModel MultiSigProp MultiSigModel where
           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
@@ -94,6 +121,7 @@ contextWithSignatures sigs =
     , scriptContextPurpose = Spending (TxOutRef "" 0)
     }
 
+-- | Generator returning one of four dummy public key hashes.
 genPK :: Gen PubKeyHash
 genPK =
   choice
@@ -105,23 +133,37 @@ genPK =
 
 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 int (linear (fromInteger minSigs) (length expectedSignatures))
-        else pure 0
+        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 $
@@ -134,12 +176,18 @@ genTests :: TestTree
 genTests =
   testGroup "genTests" $
     fromGroup
-      <$> [ runGeneratorTestsWhere (Apropos :: MultiSigModel :+ MultiSigProp) "Generator" Yes
+      <$> [ runGeneratorTestsWhere
+              (Apropos :: MultiSigModel :+ MultiSigProp)
+              "Generator"
+              Yes
           ]
 
 plutarchTests :: TestTree
 plutarchTests =
   testGroup "plutarchTests" $
     fromGroup
-      <$> [ runScriptTestsWhere (Apropos :: MultiSigModel :+ MultiSigProp) "ScriptValid" Yes
+      <$> [ runScriptTestsWhere
+              (Apropos :: MultiSigModel :+ MultiSigProp)
+              "ScriptValid"
+              Yes
           ]

From f7721f13eba1ee826608cba61ea30edb93350273 Mon Sep 17 00:00:00 2001
From: Emily Martins <emi@haskell.fyi>
Date: Mon, 21 Mar 2022 15:39:38 +0100
Subject: [PATCH 04/12] remove Int apropos-tx example, move Model.* to
 Spec.Model.*

---
 agora-test/Spec.hs                      | 15 ++--
 agora-test/Spec/Int.hs                  | 97 -------------------------
 agora-test/{ => Spec}/Model/MultiSig.hs | 61 +++++++---------
 agora.cabal                             |  7 +-
 4 files changed, 36 insertions(+), 144 deletions(-)
 delete mode 100644 agora-test/Spec/Int.hs
 rename agora-test/{ => Spec}/Model/MultiSig.hs (89%)

diff --git a/agora-test/Spec.hs b/agora-test/Spec.hs
index fada856..d326e84 100644
--- a/agora-test/Spec.hs
+++ b/agora-test/Spec.hs
@@ -8,8 +8,7 @@ import Test.Tasty (defaultMain, testGroup)
 
 --------------------------------------------------------------------------------
 
-import Model.MultiSig qualified
-import Spec.Int
+import Spec.Model.MultiSig qualified as MultiSig
 import Spec.Stake qualified as Stake
 
 main :: IO ()
@@ -18,18 +17,14 @@ main =
     testGroup
       "test suite"
       [ testGroup
-          "sample-tests"
+          "Stake tests"
           Stake.tests
       , testGroup
-          "apropos-tx"
+          "Multisig tests"
           [ testGroup
-              "Int"
-              [ intPlutarchTests
-              ]
-          , testGroup
               "MultiSig"
-              [ Model.MultiSig.plutarchTests
-              , Model.MultiSig.genTests
+              [ MultiSig.plutarchTests
+              , MultiSig.genTests
               ]
           ]
       ]
diff --git a/agora-test/Spec/Int.hs b/agora-test/Spec/Int.hs
deleted file mode 100644
index f89abdc..0000000
--- a/agora-test/Spec/Int.hs
+++ /dev/null
@@ -1,97 +0,0 @@
-module Spec.Int (HasLogicalModel (..), IntProp (..), intGenTests, intPureTests, intPlutarchTests) where
-
-import Apropos
-import Apropos.Script
-import Test.Tasty (TestTree, testGroup)
-import Test.Tasty.Hedgehog (fromGroup)
-
-import Plutarch (compile)
-
-data IntProp
-  = IsNegative
-  | IsPositive
-  | IsZero
-  | IsLarge
-  | IsSmall
-  | IsMaxBound
-  | IsMinBound
-  deriving stock (Eq, Ord, Enum, Show, Bounded)
-
-instance Enumerable IntProp where
-  enumerated = [minBound .. maxBound]
-
-instance LogicalModel IntProp where
-  logic =
-    ExactlyOne [Var IsNegative, Var IsPositive, Var IsZero]
-      :&&: ExactlyOne [Var IsLarge, Var IsSmall]
-      :&&: (Var IsZero :->: Var IsSmall)
-      :&&: (Var IsMaxBound :->: (Var IsLarge :&&: Var IsPositive))
-      :&&: (Var IsMinBound :->: (Var IsLarge :&&: Var IsNegative))
-
-instance HasLogicalModel IntProp Int where
-  satisfiesProperty IsNegative i = i < 0
-  satisfiesProperty IsPositive i = i > 0
-  satisfiesProperty IsMaxBound i = i == maxBound
-  satisfiesProperty IsMinBound i = i == minBound
-  satisfiesProperty IsZero i = i == 0
-  satisfiesProperty IsLarge i = i > 10 || i < -10
-  satisfiesProperty IsSmall i = i <= 10 && i >= -10
-
-instance HasParameterisedGenerator IntProp Int where
-  parameterisedGenerator s = do
-    i <-
-      if IsZero `elem` s
-        then pure 0
-        else
-          if IsSmall `elem` s
-            then int (linear 1 10)
-            else
-              if IsMaxBound `elem` s
-                then pure maxBound
-                else int (linear 11 (maxBound - 1))
-    if IsNegative `elem` s
-      then
-        if IsMinBound `elem` s
-          then pure minBound
-          else pure (-i)
-      else pure i
-
-intGenTests :: TestTree
-intGenTests =
-  testGroup "intGenTests" $
-    fromGroup
-      <$> [ runGeneratorTestsWhere (Apropos :: Int :+ IntProp) "Int Generator" Yes
-          ]
-
-instance HasPureRunner IntProp Int where
-  expect _ = Var IsSmall :&&: Var IsNegative
-  script _ i = i < 0 && i >= -10
-
-intPureTests :: TestTree
-intPureTests =
-  testGroup "intPureTests" $
-    fromGroup
-      <$> [ runPureTestsWhere (Apropos :: Int :+ IntProp) "AcceptsSmallNegativeInts" Yes
-          ]
-
-instance HasScriptRunner IntProp Int where
-  expect _ = Var IsSmall :&&: Var IsNegative
-  script _ i =
-    let ii = fromIntegral i :: Integer
-     in compile
-          ( pif
-              ( ( fromInteger ii
-                    #< (0 :: Term s PInteger)
-                )
-                  #&& ((fromInteger (-10) :: Term s PInteger) #<= fromInteger ii)
-              )
-              (pcon PUnit)
-              perror
-          )
-
-intPlutarchTests :: TestTree
-intPlutarchTests =
-  testGroup "intPlutarchTests" $
-    fromGroup
-      <$> [ runScriptTestsWhere (Apropos :: Int :+ IntProp) "AcceptsSmallNegativeInts" Yes
-          ]
diff --git a/agora-test/Model/MultiSig.hs b/agora-test/Spec/Model/MultiSig.hs
similarity index 89%
rename from agora-test/Model/MultiSig.hs
rename to agora-test/Spec/Model/MultiSig.hs
index 8630617..67fea2d 100644
--- a/agora-test/Model/MultiSig.hs
+++ b/agora-test/Spec/Model/MultiSig.hs
@@ -1,21 +1,12 @@
-module Model.MultiSig (plutarchTests, genTests) where
+module Spec.Model.MultiSig (
+  plutarchTests,
+  genTests,
+) where
 
-import Agora.MultiSig (MultiSig (..), validatedByMultisig)
-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 Data.List (intersect)
+
+--------------------------------------------------------------------------------
+
 import Plutarch (compile)
 import Plutus.V1.Ledger.Api (
   Script,
@@ -40,29 +31,31 @@ 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)
 
-{- Function definitions for reference:
+--------------------------------------------------------------------------------
 
-{- | A MultiSig represents a proof that a particular set of
-     signatures are present on a transaction.
--}
-data MultiSig = MultiSig
-  { keys :: [PubKeyHash]
-  -- ^ List of PubKeyHashes that must be present in the list of signatories.
-  , minSigs :: Integer
-  }
-  deriving stock (GHC.Generic, Eq, Show)
-  deriving anyclass (Generic)
+import Agora.MultiSig (MultiSig (..), validatedByMultisig)
 
--- | Check if a Haskell-level MultiSig signs this transaction.
-validatedByMultisig :: MultiSig -> Term s (PTxInfo :--> PBool)
-validatedByMultisig params =
-  phoistAcyclic $
-    pvalidatedByMultisig # pconstant params
-
--}
+--------------------------------------------------------------------------------
 
 -- | apropos model for testing multisigs.
 data MultiSigModel = MultiSigModel
diff --git a/agora.cabal b/agora.cabal
index be8ab96..23748b3 100644
--- a/agora.cabal
+++ b/agora.cabal
@@ -148,10 +148,11 @@ test-suite agora-test
   main-is:        Spec.hs
   hs-source-dirs: agora-test
   other-modules:
-    Spec.Int
-    Spec.Sample.Stake
     Spec.Stake
-    Model.MultiSig
+    Spec.Sample.Stake
+
+    Spec.Model.MultiSig
+
     Spec.Util
 
   build-depends:  agora

From 14e1d66f6068d05fd2030869e212354dd8d95fa3 Mon Sep 17 00:00:00 2001
From: Emily Martins <emi@haskell.fyi>
Date: Mon, 21 Mar 2022 18:11:38 +0100
Subject: [PATCH 05/12] hacky fix for stake policy using filtered `<=`

---
 agora/Agora/Stake.hs | 55 ++++++++++++++++++++++++++++++++++++++++----
 agora/Agora/Utils.hs | 24 +++++++++++++++++++
 2 files changed, 74 insertions(+), 5 deletions(-)

diff --git a/agora/Agora/Stake.hs b/agora/Agora/Stake.hs
index 44199a6..610d49a 100644
--- a/agora/Agora/Stake.hs
+++ b/agora/Agora/Stake.hs
@@ -19,9 +19,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 +53,7 @@ import Plutarch.DataRepr (
  )
 import Plutarch.Internal (punsafeCoerce)
 import Plutarch.Monadic qualified as P
+import Plutus.V1.Ledger.Value (AssetClass (AssetClass))
 
 --------------------------------------------------------------------------------
 
@@ -65,6 +69,9 @@ import Agora.Utils (
   paddValue,
   passert,
   pfindTxInByTxOutRef,
+  pgeqBy,
+  pgeqBy',
+  pgeqBySymbol,
   psingletonValue,
   psymbolValueOf,
   ptxSignedBy,
@@ -200,8 +207,28 @@ stakePolicy _stake =
                             # ctx.txInfo
                             # stakeDatum.owner
 
-                    -- TODO: Needs to be >=, rather than ==
-                    let valueCorrect = pdata value #== pdata expectedValue
+                    -- TODO: This is quite inefficient now, as it does two lookups
+                    -- 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 ())
@@ -274,9 +301,27 @@ stakeValidator stake =
                       #&& (paddDiscrete # stakeDatum.stakedAmount # delta) #== newStakeDatum.stakedAmount
               let expectedValue = paddValue # continuingValue # (pdiscreteValue # delta)
 
-              -- TODO: As above, needs to be >=, rather than ==
-              let correctValue = pdata value #== pdata expectedValue
-              isScriptAddress #&& correctOutputDatum #&& correctValue
+              -- TODO: Same as above. This is quite inefficient now, as it does two lookups
+              -- 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
+                      , pgeqBySymbol
+                          # stCurrencySymbol
+                          # value
+                          # expectedValue
+                      ]
+              isScriptAddress #&& correctOutputDatum #&& valueCorrect
 
         popaque (pconstant ())
 
diff --git a/agora/Agora/Utils.hs b/agora/Agora/Utils.hs
index 2afa33a..8f70a2f 100644
--- a/agora/Agora/Utils.hs
+++ b/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 $

From a0ed9391754d27b6b8a961375a951e80775d1dbb Mon Sep 17 00:00:00 2001
From: Emily Martins <emi@haskell.fyi>
Date: Tue, 22 Mar 2022 16:27:20 +0100
Subject: [PATCH 06/12] flake: run tests in flake check, actually check
 fourmolu

---
 Makefile    |  8 ++++++--
 agora.cabal |  6 ++----
 flake.nix   | 13 +++++++------
 3 files changed, 15 insertions(+), 12 deletions(-)

diff --git a/Makefile b/Makefile
index feb2a3d..e155973 100644
--- a/Makefile
+++ b/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
diff --git a/agora.cabal b/agora.cabal
index 23748b3..11dc271 100644
--- a/agora.cabal
+++ b/agora.cabal
@@ -148,11 +148,9 @@ test-suite agora-test
   main-is:        Spec.hs
   hs-source-dirs: agora-test
   other-modules:
-    Spec.Stake
-    Spec.Sample.Stake
-
     Spec.Model.MultiSig
-
+    Spec.Sample.Stake
+    Spec.Stake
     Spec.Util
 
   build-depends:  agora
diff --git a/flake.nix b/flake.nix
index fdf0dd8..87fabb1 100644
--- a/flake.nix
+++ b/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");
     };
 }

From 3ada0095b369241835640a0ad261e186c5511e5f Mon Sep 17 00:00:00 2001
From: Emily Martins <emi@haskell.fyi>
Date: Tue, 22 Mar 2022 16:28:14 +0100
Subject: [PATCH 07/12] ci: build checks instead of defaultPackage

---
 .github/workflows/integrate.yaml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/integrate.yaml b/.github/workflows/integrate.yaml
index 662e290..42b0d14 100644
--- a/.github/workflows/integrate.yaml
+++ b/.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

From 3578e7c47eb00155e1731c20584666b6283f51cc Mon Sep 17 00:00:00 2001
From: Emily Martins <emi@haskell.fyi>
Date: Wed, 23 Mar 2022 21:35:05 +0100
Subject: [PATCH 08/12] add some tests for Stake validator

---
 agora-test/Spec/Sample/Stake.hs | 63 ++++++++++++++++++++++++++++++++-
 agora-test/Spec/Stake.hs        | 23 ++++++++++--
 agora-test/Spec/Util.hs         | 56 +++++++++++++++++++++++++++--
 agora/Agora/SafeMoney.hs        | 17 +++++++--
 agora/Agora/Stake.hs            | 52 +++++++++++++++++++++------
 5 files changed, 194 insertions(+), 17 deletions(-)

diff --git a/agora-test/Spec/Sample/Stake.hs b/agora-test/Spec/Sample/Stake.hs
index 96a54ad..a2fa049 100644
--- a/agora-test/Spec/Sample/Stake.hs
+++ b/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)
+        }
diff --git a/agora-test/Spec/Stake.hs b/agora-test/Spec/Stake.hs
index dd51749..c58598f 100644
--- a/agora-test/Spec/Stake.hs
+++ b/agora-test/Spec/Stake.hs
@@ -14,12 +14,13 @@ import Plutarch.Builtin (pforgetData)
 
 --------------------------------------------------------------------------------
 
-import Agora.Stake (stakePolicy)
+import Agora.Stake (StakeDatum (StakeDatum), StakeRedeemer (DepositWithdraw), stakePolicy, stakeValidator)
 
 --------------------------------------------------------------------------------
 
+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)
 
 --------------------------------------------------------------------------------
 
@@ -42,5 +43,23 @@ tests =
           (stakePolicy Stake.stake)
           (pforgetData (pconstantData ()))
           Stake.stakeCreationUnsigned
+      , validatorSucceedsWith
+          "stakeDepositWithdraw deposit"
+          (stakeValidator Stake.stake)
+          (pforgetData (pconstantData . toDatum $ StakeDatum 100_000 signer))
+          (pforgetData (pconstantData . toDatum $ DepositWithdraw 100_000))
+          (Stake.stakeDepositWithdraw $ DepositWithdrawExample {startAmount = 100_000, delta = 100_000})
+      , validatorSucceedsWith
+          "stakeDepositWithdraw withdraw"
+          (stakeValidator Stake.stake)
+          (pforgetData (pconstantData . toDatum $ StakeDatum 100_000 signer))
+          (pforgetData (pconstantData . toDatum $ DepositWithdraw (negate 100_000)))
+          (Stake.stakeDepositWithdraw $ DepositWithdrawExample {startAmount = 100_000, delta = negate 100_000})
+      , validatorFailsWith
+          "stakeDepositWithdraw negative GT"
+          (stakeValidator Stake.stake)
+          (pforgetData (pconstantData . toDatum $ StakeDatum 100_000 signer))
+          (pforgetData (pconstantData . toDatum $ DepositWithdraw (negate 1_000_000)))
+          (Stake.stakeDepositWithdraw $ DepositWithdrawExample {startAmount = 100_000, delta = negate 1_000_000})
       ]
   ]
diff --git a/agora-test/Spec/Util.hs b/agora-test/Spec/Util.hs
index 3db7f53..dafd5e2 100644
--- a/agora-test/Spec/Util.hs
+++ b/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,16 +20,24 @@ 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.Crypto (pblake2b_256)
 import Plutarch.Evaluate (evalScript)
 import Plutarch.Prelude ()
-import Plutus.V1.Ledger.Scripts (Script)
+import Plutus.V1.Ledger.Scripts (Datum (Datum), DatumHash (DatumHash), Script)
+import PlutusTx.Builtins qualified as PlutusTx
+import PlutusTx.IsData qualified as PlutusTx
 
 --------------------------------------------------------------------------------
 
@@ -32,6 +49,14 @@ policyFailsWith :: String -> ClosedTerm PMintingPolicy -> ClosedTerm PData -> _
 policyFailsWith tag policy redeemer scriptContext =
   scriptFails tag $ compile (policy # redeemer # pconstant scriptContext)
 
+validatorSucceedsWith :: String -> ClosedTerm PValidator -> ClosedTerm PData -> ClosedTerm PData -> _ -> TestTree
+validatorSucceedsWith tag policy datum redeemer scriptContext =
+  scriptSucceeds tag $ compile (policy # datum # redeemer # pconstant scriptContext)
+
+validatorFailsWith :: String -> ClosedTerm PValidator -> ClosedTerm PData -> ClosedTerm PData -> _ -> TestTree
+validatorFailsWith tag policy datum redeemer scriptContext =
+  scriptFails tag $ compile (policy # datum # redeemer # pconstant scriptContext)
+
 scriptSucceeds :: String -> Script -> TestTree
 scriptSucceeds name script = testCase name $ do
   let (res, _budget, traces) = evalScript script
@@ -51,3 +76,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)
diff --git a/agora/Agora/SafeMoney.hs b/agora/Agora/SafeMoney.hs
index d40d99d..1eeb2c7 100644
--- a/agora/Agora/SafeMoney.hs
+++ b/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,18 @@ 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'
+
+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
diff --git a/agora/Agora/Stake.hs b/agora/Agora/Stake.hs
index 610d49a..39f1eb1 100644
--- a/agora/Agora/Stake.hs
+++ b/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,
@@ -62,6 +63,8 @@ import Agora.SafeMoney (
   PDiscrete,
   paddDiscrete,
   pdiscreteValue,
+  pgeqDiscrete,
+  pzeroDiscrete,
  )
 import Agora.Utils (
   anyInput,
@@ -84,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.
@@ -94,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
@@ -110,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)
@@ -253,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)
-        stakeAction = pfromData $ punsafeCoerce redeemer
+    let stakeRedeemer :: Term _ (PStakeRedeemer gt)
+        stakeRedeemer = pfromData $ punsafeCoerce redeemer
         stakeDatum' :: Term _ (PStakeDatum gt)
         stakeDatum' = pfromData $ punsafeCoerce datum
     stakeDatum <- pletFields @'["owner", "stakedAmount"] stakeDatum'
@@ -269,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
@@ -297,8 +317,14 @@ stakeValidator stake =
               delta <- plet $ pfield @"delta" # r
               let isScriptAddress = pdata address #== ownAddress
               let correctOutputDatum =
-                    stakeDatum.owner #== newStakeDatum.owner
-                      #&& (paddDiscrete # stakeDatum.stakedAmount # delta) #== newStakeDatum.stakedAmount
+                    foldr1
+                      (#&&)
+                      [ 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: Same as above. This is quite inefficient now, as it does two lookups
@@ -321,7 +347,13 @@ stakeValidator stake =
                           # value
                           # expectedValue
                       ]
-              isScriptAddress #&& correctOutputDatum #&& valueCorrect
+
+              foldr1
+                (#&&)
+                [ ptraceIfFalse "isScriptAddress" isScriptAddress
+                , ptraceIfFalse "correctOutputDatum" correctOutputDatum
+                , ptraceIfFalse "valueCorrect" valueCorrect
+                ]
 
         popaque (pconstant ())
 

From 310be96487914dfaa8cff486f1a551a809a4aec7 Mon Sep 17 00:00:00 2001
From: Emily Martins <emi@haskell.fyi>
Date: Wed, 23 Mar 2022 22:03:11 +0100
Subject: [PATCH 09/12] improve ergonomics and add documentation

---
 agora-test/Spec/Stake.hs | 22 +++++------
 agora-test/Spec/Util.hs  | 79 ++++++++++++++++++++++++++++++++++++----
 agora/Agora/SafeMoney.hs |  3 +-
 3 files changed, 82 insertions(+), 22 deletions(-)

diff --git a/agora-test/Spec/Stake.hs b/agora-test/Spec/Stake.hs
index c58598f..f432e1b 100644
--- a/agora-test/Spec/Stake.hs
+++ b/agora-test/Spec/Stake.hs
@@ -10,10 +10,6 @@ import Test.Tasty (TestTree, testGroup)
 
 --------------------------------------------------------------------------------
 
-import Plutarch.Builtin (pforgetData)
-
---------------------------------------------------------------------------------
-
 import Agora.Stake (StakeDatum (StakeDatum), StakeRedeemer (DepositWithdraw), stakePolicy, stakeValidator)
 
 --------------------------------------------------------------------------------
@@ -31,35 +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)
-          (pforgetData (pconstantData . toDatum $ StakeDatum 100_000 signer))
-          (pforgetData (pconstantData . toDatum $ DepositWithdraw 100_000))
+          (toDatum $ StakeDatum 100_000 signer)
+          (toDatum $ DepositWithdraw 100_000)
           (Stake.stakeDepositWithdraw $ DepositWithdrawExample {startAmount = 100_000, delta = 100_000})
       , validatorSucceedsWith
           "stakeDepositWithdraw withdraw"
           (stakeValidator Stake.stake)
-          (pforgetData (pconstantData . toDatum $ StakeDatum 100_000 signer))
-          (pforgetData (pconstantData . toDatum $ DepositWithdraw (negate 100_000)))
+          (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)
-          (pforgetData (pconstantData . toDatum $ StakeDatum 100_000 signer))
-          (pforgetData (pconstantData . toDatum $ DepositWithdraw (negate 1_000_000)))
+          (toDatum $ StakeDatum 100_000 signer)
+          (toDatum $ DepositWithdraw (negate 1_000_000))
           (Stake.stakeDepositWithdraw $ DepositWithdrawExample {startAmount = 100_000, delta = negate 1_000_000})
       ]
   ]
diff --git a/agora-test/Spec/Util.hs b/agora-test/Spec/Util.hs
index dafd5e2..240ff3a 100644
--- a/agora-test/Spec/Util.hs
+++ b/agora-test/Spec/Util.hs
@@ -32,30 +32,93 @@ import Test.Tasty.HUnit (assertFailure, testCase)
 
 import Plutarch
 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.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 :: String -> ClosedTerm PMintingPolicy -> ClosedTerm PData -> _ -> TestTree
+policySucceedsWith ::
+  ( PLift redeemer
+  , PlutusTx.ToData (PLifted redeemer)
+  ) =>
+  String ->
+  ClosedTerm PMintingPolicy ->
+  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 :: String -> ClosedTerm PValidator -> ClosedTerm PData -> ClosedTerm PData -> _ -> TestTree
+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 # datum # redeemer # pconstant scriptContext)
+  scriptSucceeds tag $
+    compile
+      ( policy
+          # pforgetData (pconstantData datum)
+          # pforgetData (pconstantData redeemer)
+          # pconstant scriptContext
+      )
 
-validatorFailsWith :: String -> ClosedTerm PValidator -> ClosedTerm PData -> ClosedTerm PData -> _ -> TestTree
+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 # datum # redeemer # pconstant scriptContext)
+  scriptFails tag $
+    compile
+      ( policy
+          # pforgetData (pconstantData datum)
+          # pforgetData (pconstantData redeemer)
+          # pconstant scriptContext
+      )
 
 scriptSucceeds :: String -> Script -> TestTree
 scriptSucceeds name script = testCase name $ do
diff --git a/agora/Agora/SafeMoney.hs b/agora/Agora/SafeMoney.hs
index 1eeb2c7..6730bc7 100644
--- a/agora/Agora/SafeMoney.hs
+++ b/agora/Agora/SafeMoney.hs
@@ -75,6 +75,7 @@ pgeqDiscrete = phoistAcyclic $
     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)
 
@@ -113,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.

From 6702bfcd94497f2541a5938b71cf737900bf6c96 Mon Sep 17 00:00:00 2001
From: Emily Martins <emi@haskell.fyi>
Date: Thu, 24 Mar 2022 15:43:21 +0100
Subject: [PATCH 10/12] apply suggestions and fix remaining haddock suggestions

---
 Makefile                          |  5 ++++-
 agora-test/Spec/Model/MultiSig.hs | 10 +++++++++-
 agora-test/Spec/Sample/Stake.hs   | 15 ++++++++++++---
 agora-test/Spec/Util.hs           | 19 ++++++++++++++-----
 agora/Agora/MultiSig.hs           |  1 +
 agora/Agora/SafeMoney.hs          | 14 +++++---------
 agora/Agora/SafeMoney/QQ.hs       |  2 +-
 agora/Agora/Stake.hs              | 14 +++++++-------
 agora/Agora/Utils.hs              | 14 +++++++-------
 agora/PPrelude.hs                 | 10 ++++++++++
 10 files changed, 70 insertions(+), 34 deletions(-)

diff --git a/Makefile b/Makefile
index e155973..a2a17e7 100644
--- a/Makefile
+++ b/Makefile
@@ -23,7 +23,10 @@ format:
 	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
+	find -name '*.hs' \
+	     -not -path './dist*/*' \
+	     -not -path './haddock/*' \
+	  | xargs fourmolu $(FORMAT_EXTENSIONS) -m check
 
 haddock:
 	cabal haddock --haddock-html --haddock-hoogle --builddir=haddock
diff --git a/agora-test/Spec/Model/MultiSig.hs b/agora-test/Spec/Model/MultiSig.hs
index 67fea2d..15dcfae 100644
--- a/agora-test/Spec/Model/MultiSig.hs
+++ b/agora-test/Spec/Model/MultiSig.hs
@@ -1,3 +1,10 @@
+{- |
+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,
@@ -7,7 +14,6 @@ import Data.List (intersect)
 
 --------------------------------------------------------------------------------
 
-import Plutarch (compile)
 import Plutus.V1.Ledger.Api (
   Script,
   ScriptContext (scriptContextPurpose),
@@ -165,6 +171,7 @@ instance HasScriptRunner MultiSigProp MultiSigModel where
         (pcon PUnit)
         perror
 
+-- | Consistency tests for the 'HasParameterisedGenerator' instance of 'MultiSigModel'
 genTests :: TestTree
 genTests =
   testGroup "genTests" $
@@ -175,6 +182,7 @@ genTests =
               Yes
           ]
 
+-- | Tests for the 'HasScriptRunner' instance of 'MultiSigModel'
 plutarchTests :: TestTree
 plutarchTests =
   testGroup "plutarchTests" $
diff --git a/agora-test/Spec/Sample/Stake.hs b/agora-test/Spec/Sample/Stake.hs
index a2fa049..4bb0073 100644
--- a/agora-test/Spec/Sample/Stake.hs
+++ b/agora-test/Spec/Sample/Stake.hs
@@ -58,25 +58,30 @@ import Spec.Util (datumPair, toDatumHash)
 
 --------------------------------------------------------------------------------
 
+-- | 'Stake' parameters for 'LQ'.
 stake :: Stake LQ
 stake = Stake
 
+-- | 'Stake' policy instance.
 policy :: MintingPolicy
 policy = mkMintingPolicy (stakePolicy stake)
 
 policySymbol :: CurrencySymbol
 policySymbol = mintingPolicySymbol policy
 
+-- | A sample 'PubKeyHash'.
 signer :: PubKeyHash
 signer = "8a30896c4fd5e79843e4ca1bd2cdbaa36f8c0bc3be7401214142019c"
 
+-- | 'Stake' validator instance.
 validator :: Validator
 validator = mkValidator (stakeValidator stake)
 
+-- | 'TokenName' that represents the hash of the 'Stake' validator.
 validatorHashTN :: TokenName
 validatorHashTN = let ValidatorHash vh = validatorHash validator in TokenName vh
 
--- | This script context should be a valid transaction
+-- | This script context should be a valid transaction.
 stakeCreation :: ScriptContext
 stakeCreation =
   let st = Value.singleton policySymbol validatorHashTN 1 -- Stake ST
@@ -105,7 +110,7 @@ stakeCreation =
         , scriptContextPurpose = Minting policySymbol
         }
 
--- | This ScriptContext should fail because the datum has too much GT
+-- | This ScriptContext should fail because the datum has too much GT.
 stakeCreationWrongDatum :: ScriptContext
 stakeCreationWrongDatum =
   let datum :: Datum
@@ -115,7 +120,7 @@ stakeCreationWrongDatum =
         , scriptContextPurpose = Minting policySymbol
         }
 
--- | This ScriptContext should fail because the datum has too much GT
+-- | This ScriptContext should fail because the datum has too much GT.
 stakeCreationUnsigned :: ScriptContext
 stakeCreationUnsigned =
   ScriptContext
@@ -128,11 +133,15 @@ stakeCreationUnsigned =
 
 --------------------------------------------------------------------------------
 
+-- | Config for creating a ScriptContext that deposits or withdraws.
 data DepositWithdrawExample = DepositWithdrawExample
   { startAmount :: Integer
+  -- ^ The amount of GT stored before the transaction.
   , delta :: Integer
+  -- ^ The amount of GT deposited or withdrawn from the Stake.
   }
 
+-- | Create a ScriptContext that deposits or withdraws, given the config for it.
 stakeDepositWithdraw :: DepositWithdrawExample -> ScriptContext
 stakeDepositWithdraw config =
   let st = Value.singleton policySymbol validatorHashTN 1 -- Stake ST
diff --git a/agora-test/Spec/Util.hs b/agora-test/Spec/Util.hs
index 240ff3a..33f23be 100644
--- a/agora-test/Spec/Util.hs
+++ b/agora-test/Spec/Util.hs
@@ -7,7 +7,7 @@ module Spec.Util (
   validatorSucceedsWith,
   validatorFailsWith,
 
-  -- * Plutus land utils
+  -- * Plutus-land utils
   datumHash,
   toDatum,
   toDatumHash,
@@ -30,13 +30,11 @@ import Test.Tasty.HUnit (assertFailure, testCase)
 
 --------------------------------------------------------------------------------
 
-import Plutarch
 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.Contexts (ScriptContext)
 import Plutus.V1.Ledger.Scripts (Datum (Datum), DatumHash (DatumHash), Script)
 import PlutusTx.Builtins qualified as PlutusTx
@@ -44,6 +42,7 @@ import PlutusTx.IsData qualified as PlutusTx
 
 --------------------------------------------------------------------------------
 
+-- | Check that a policy script succeeds, given a name and arguments.
 policySucceedsWith ::
   ( PLift redeemer
   , PlutusTx.ToData (PLifted redeemer)
@@ -61,6 +60,7 @@ policySucceedsWith tag policy redeemer scriptContext =
           # pconstant scriptContext
       )
 
+-- | Check that a policy script fails, given a name and arguments.
 policyFailsWith ::
   ( PLift redeemer
   , PlutusTx.ToData (PLifted redeemer)
@@ -78,6 +78,7 @@ policyFailsWith tag policy redeemer scriptContext =
           # pconstant scriptContext
       )
 
+-- | Check that a validator script succeeds, given a name and arguments.
 validatorSucceedsWith ::
   ( PLift datum
   , PlutusTx.ToData (PLifted datum)
@@ -99,6 +100,7 @@ validatorSucceedsWith tag policy datum redeemer scriptContext =
           # pconstant scriptContext
       )
 
+-- | Check that a validator script fails, given a name and arguments.
 validatorFailsWith ::
   ( PLift datum
   , PlutusTx.ToData (PLifted datum)
@@ -120,6 +122,7 @@ validatorFailsWith tag policy datum redeemer scriptContext =
           # pconstant scriptContext
       )
 
+-- | Check that an arbitrary script doesn't error when evaluated, given a name.
 scriptSucceeds :: String -> Script -> TestTree
 scriptSucceeds name script = testCase name $ do
   let (res, _budget, traces) = evalScript script
@@ -130,6 +133,7 @@ scriptSucceeds name script = testCase name $ do
     Right _v ->
       pure ()
 
+-- | Check that an arbitrary script **does** error when evaluated, given a name.
 scriptFails :: String -> Script -> TestTree
 scriptFails name script = testCase name $ do
   let (res, _budget, traces) = evalScript script
@@ -142,7 +146,7 @@ scriptFails name script = testCase name $ do
 
 --------------------------------------------------------------------------------
 
-{- | Create a pair from data for use in 'txInfoData'
+{- | Create a pair from data for use in 'txInfoData'.
 
    Example:
    @
@@ -152,13 +156,18 @@ scriptFails name script = testCase name $ do
 datumPair :: PlutusTx.ToData a => a -> (DatumHash, Datum)
 datumPair = (,) <$> toDatumHash <*> toDatum
 
+-- | Calculate the blake2b-256 hash of a Datum.
 datumHash :: Datum -> DatumHash
 datumHash (Datum data') = toDatumHash data'
 
+-- | Convenience function to create a Datum from any type that implements ToData.
 toDatum :: PlutusTx.ToData a => a -> Datum
 toDatum = Datum . PlutusTx.toBuiltinData
 
--- Shamelessly go through plutus.
+{- | Calculate the blake2b-256 hash of any type that implements ToData
+
+     Shamelessly go through plutus.
+-}
 toDatumHash :: PlutusTx.ToData a => a -> DatumHash
 toDatumHash datum =
   DatumHash $
diff --git a/agora/Agora/MultiSig.hs b/agora/Agora/MultiSig.hs
index 1e8a548..6e8270d 100644
--- a/agora/Agora/MultiSig.hs
+++ b/agora/Agora/MultiSig.hs
@@ -10,6 +10,7 @@ A basic N of M multisignature validation function.
 module Agora.MultiSig (
   validatedByMultisig,
   pvalidatedByMultisig,
+  PMultiSig (..),
   MultiSig (..),
 ) where
 
diff --git a/agora/Agora/SafeMoney.hs b/agora/Agora/SafeMoney.hs
index 6730bc7..bec07c5 100644
--- a/agora/Agora/SafeMoney.hs
+++ b/agora/Agora/SafeMoney.hs
@@ -9,7 +9,6 @@ module Agora.SafeMoney (
   -- * Types
   MoneyClass,
   PDiscrete,
-  Discrete,
 
   -- * Utility functions
   paddDiscrete,
@@ -44,11 +43,11 @@ import Plutarch.Monadic qualified as P
 
 --------------------------------------------------------------------------------
 
-import Agora.Utils
+import Agora.Utils (passetClassValueOf, psingletonValue)
 
 --------------------------------------------------------------------------------
 
--- | Type-level unique identifier for an `AssetClass`
+-- | Type-level unique identifier for an 'Plutus.V1.Ledger.Value.AssetClass'
 type MoneyClass =
   ( -- AssetClass
     Symbol
@@ -63,10 +62,6 @@ newtype PDiscrete (mc :: MoneyClass) (s :: S)
   = PDiscrete (Term s PInteger)
   deriving (PlutusType, PIsData, PEq, POrd) via (DerivePNewtype (PDiscrete mc) PInteger)
 
-newtype Discrete (mc :: MoneyClass)
-  = Discrete Integer
-  deriving stock (Show)
-
 -- | Check if one 'PDiscrete' is greater than another.
 pgeqDiscrete :: forall (mc :: MoneyClass) (s :: S). Term s (PDiscrete mc :--> PDiscrete mc :--> PBool)
 pgeqDiscrete = phoistAcyclic $
@@ -75,7 +70,7 @@ pgeqDiscrete = phoistAcyclic $
     PDiscrete y' <- pmatch y
     y' #<= x'
 
--- | Conjure zero discrete unit for any moneyclass
+-- | Returns a zero-value 'PDiscrete' unit for any 'MoneyClass'.
 pzeroDiscrete :: forall (mc :: MoneyClass) (s :: S). Term s (PDiscrete mc)
 pzeroDiscrete = phoistAcyclic $ pcon (PDiscrete 0)
 
@@ -114,7 +109,8 @@ pvalueDiscrete = phoistAcyclic $
         # f
 
 {- | Get a `PValue` from a `PDiscrete`.
-     __NOTE__: `pdiscreteValue` after `pvalueDiscrete` loses information
+     __NOTE__: `pdiscreteValue` after `pvalueDiscrete` is not a round-trip.
+     It filters for a particular 'MoneyClass'.
 -}
 pdiscreteValue ::
   forall (moneyClass :: MoneyClass) (ac :: Symbol) (n :: Symbol) (scale :: Nat) s.
diff --git a/agora/Agora/SafeMoney/QQ.hs b/agora/Agora/SafeMoney/QQ.hs
index 96ec4c7..3fdf161 100644
--- a/agora/Agora/SafeMoney/QQ.hs
+++ b/agora/Agora/SafeMoney/QQ.hs
@@ -40,7 +40,7 @@ import Agora.SafeMoney (MoneyClass, PDiscrete)
 {- | Generate 'PDiscrete' values tagged by a particular MoneyClass
 
 @
-  [discrete| 123.456 ADA |] :: 'Term' s ('PDiscrete' 'ADA')
+  [discrete| 123.456 'Agora.SafeMoney.ADA' |] :: 'Term' s ('PDiscrete' 'Agora.SafeMoney.ADA')
 @
 -}
 discrete :: QuasiQuoter
diff --git a/agora/Agora/Stake.hs b/agora/Agora/Stake.hs
index 39f1eb1..3929449 100644
--- a/agora/Agora/Stake.hs
+++ b/agora/Agora/Stake.hs
@@ -72,8 +72,8 @@ import Agora.Utils (
   paddValue,
   passert,
   pfindTxInByTxOutRef,
-  pgeqBy,
-  pgeqBy',
+  pgeqByClass,
+  pgeqByClass',
   pgeqBySymbol,
   psingletonValue,
   psymbolValueOf,
@@ -233,8 +233,8 @@ stakePolicy _stake =
                     let valueCorrect =
                           foldr1
                             (#&&)
-                            [ pgeqBy' (AssetClass ("", "")) # value # expectedValue
-                            , pgeqBy'
+                            [ pgeqByClass' (AssetClass ("", "")) # value # expectedValue
+                            , pgeqByClass'
                                 ( AssetClass
                                     ( fromString . symbolVal $ Proxy @ac
                                     , fromString . symbolVal $ Proxy @n
@@ -242,7 +242,7 @@ stakePolicy _stake =
                                 )
                                 # value
                                 # expectedValue
-                            , pgeqBy
+                            , pgeqByClass
                                 # ownSymbol
                                 # tn
                                 # value
@@ -333,8 +333,8 @@ stakeValidator stake =
               let valueCorrect =
                     foldr1
                       (#&&)
-                      [ pgeqBy' (AssetClass ("", "")) # value # expectedValue
-                      , pgeqBy'
+                      [ pgeqByClass' (AssetClass ("", "")) # value # expectedValue
+                      , pgeqByClass'
                           ( AssetClass
                               ( fromString . symbolVal $ Proxy @ac
                               , fromString . symbolVal $ Proxy @n
diff --git a/agora/Agora/Utils.hs b/agora/Agora/Utils.hs
index 8f70a2f..4b599c8 100644
--- a/agora/Agora/Utils.hs
+++ b/agora/Agora/Utils.hs
@@ -19,9 +19,9 @@ module Agora.Utils (
   psymbolValueOf,
   passetClassValueOf,
   passetClassValueOf',
-  pgeqBy,
+  pgeqByClass,
   pgeqBySymbol,
-  pgeqBy',
+  pgeqByClass',
   pfindTxInByTxOutRef,
   psingletonValue,
   pfindMap,
@@ -184,13 +184,13 @@ 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 =
+pgeqByClass :: Term s (PCurrencySymbol :--> PTokenName :--> PValue :--> PValue :--> PBool)
+pgeqByClass =
   phoistAcyclic $
     plam $ \cs tn a b ->
       passetClassValueOf # cs # tn # b #<= passetClassValueOf # cs # tn # a
 
--- | Return '>=' on two values comparing by only a particular AssetClass
+-- | Return '>=' on two values comparing by only a particular CurrencySymbol
 pgeqBySymbol :: Term s (PCurrencySymbol :--> PValue :--> PValue :--> PBool)
 pgeqBySymbol =
   phoistAcyclic $
@@ -198,8 +198,8 @@ pgeqBySymbol =
       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 =
+pgeqByClass' :: AssetClass -> Term s (PValue :--> PValue :--> PBool)
+pgeqByClass' ac =
   phoistAcyclic $
     plam $ \a b ->
       passetClassValueOf' ac # b #<= passetClassValueOf' ac # a
diff --git a/agora/PPrelude.hs b/agora/PPrelude.hs
index 3a8025b..8fba4be 100644
--- a/agora/PPrelude.hs
+++ b/agora/PPrelude.hs
@@ -1,7 +1,17 @@
+{- |
+Module     : PPrelude
+Maintainer : emi@haskell.fyi
+Description: Prelude imported throughout this project
+
+Prelude imported throughout this project
+-}
 module PPrelude (
   module Prelude,
   module Plutarch.Prelude,
+  module Plutarch,
 ) where
 
+-- These are not exported by Plutarch.Prelude, for some reason. Maybe we can 'fix' this upstream?
+import Plutarch (ClosedTerm, compile)
 import Plutarch.Prelude
 import Prelude

From 32e0ee2b9e84cedcf2775352131a09d4a03efac1 Mon Sep 17 00:00:00 2001
From: Emily Martins <emi@haskell.fyi>
Date: Thu, 24 Mar 2022 16:09:39 +0100
Subject: [PATCH 11/12] more docs

---
 agora-test/Spec.hs       | 1 +
 agora-test/Spec/Stake.hs | 8 ++++++++
 agora-test/Spec/Util.hs  | 7 +++++++
 3 files changed, 16 insertions(+)

diff --git a/agora-test/Spec.hs b/agora-test/Spec.hs
index d326e84..502cb27 100644
--- a/agora-test/Spec.hs
+++ b/agora-test/Spec.hs
@@ -11,6 +11,7 @@ import Test.Tasty (defaultMain, testGroup)
 import Spec.Model.MultiSig qualified as MultiSig
 import Spec.Stake qualified as Stake
 
+-- | The Agora test suite
 main :: IO ()
 main =
   defaultMain $
diff --git a/agora-test/Spec/Stake.hs b/agora-test/Spec/Stake.hs
index f432e1b..8064ddf 100644
--- a/agora-test/Spec/Stake.hs
+++ b/agora-test/Spec/Stake.hs
@@ -1,3 +1,10 @@
+{- |
+Module     : Spec.Stake
+Maintainer : emi@haskell.fyi
+Description: Tests for Stake policy and validator
+
+Tests for Stake policy and validator
+-}
 module Spec.Stake (tests) where
 
 --------------------------------------------------------------------------------
@@ -20,6 +27,7 @@ import Spec.Util (policyFailsWith, policySucceedsWith, toDatum, validatorFailsWi
 
 --------------------------------------------------------------------------------
 
+-- | Stake tests
 tests :: [TestTree]
 tests =
   [ testGroup
diff --git a/agora-test/Spec/Util.hs b/agora-test/Spec/Util.hs
index 33f23be..e43f7f5 100644
--- a/agora-test/Spec/Util.hs
+++ b/agora-test/Spec/Util.hs
@@ -1,3 +1,10 @@
+{- |
+Module     : Spec.Util
+Maintainer : emi@haskell.fyi
+Description: Utility functions for testing Plutarch scripts with ScriptContext
+
+Utility functions for testing Plutarch scripts with ScriptContext
+-}
 module Spec.Util (
   -- * Testing utils
   scriptSucceeds,

From 75b6b908fd6c148612b6c754a3640347ff208bbb Mon Sep 17 00:00:00 2001
From: Emily Martins <emi@haskell.fyi>
Date: Thu, 24 Mar 2022 16:11:03 +0100
Subject: [PATCH 12/12] rename LBS to ByteString.Lazy

---
 agora-test/Spec/Util.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/agora-test/Spec/Util.hs b/agora-test/Spec/Util.hs
index e43f7f5..4350e45 100644
--- a/agora-test/Spec/Util.hs
+++ b/agora-test/Spec/Util.hs
@@ -28,7 +28,7 @@ import Prelude
 --------------------------------------------------------------------------------
 
 import Codec.Serialise (serialise)
-import Data.ByteString.Lazy qualified as LBS
+import Data.ByteString.Lazy qualified as ByteString.Lazy
 
 --------------------------------------------------------------------------------
 
@@ -181,4 +181,4 @@ toDatumHash datum =
     PlutusTx.toBuiltin $
       plift $
         pblake2b_256
-          # pconstant (LBS.toStrict $ serialise $ PlutusTx.toData datum)
+          # pconstant (ByteString.Lazy.toStrict $ serialise $ PlutusTx.toData datum)