add shared Sample values module

- add Proposal validator testing
- add some Agora.Record improvements

agora/Agora/AuthorityToken.hs

@@ -18,6 +18,7 @@ import Plutarch.Api.V1 (
   PCurrencySymbol (..),
   PScriptContext (..),
   PScriptPurpose (..),
+  PTxInInfo (PTxInInfo),
   PTxInfo (..),
   PTxOut (..),
  )

agora/Agora/Proposal.hs

@@ -58,7 +58,7 @@ import PlutusTx qualified
 import PlutusTx.AssocMap qualified as AssocMap
 
 --------------------------------------------------------------------------------
-
+import Agora.Record (mkRecordConstr, (.&), (.=))
 import Agora.SafeMoney (GTTag)
 import Agora.Utils (
   anyOutput,
@@ -354,7 +354,7 @@ newtype PProposalDatum (s :: S) = PProposalDatum
     Term
       s
       ( PDataRecord
-          '[ "id" ':= PProposalId
+          '[ "proposalId" ':= PProposalId
            , "effects" ':= PMap PResultTag (PMap PValidatorHash PDatumHash)
            , "status" ':= PProposalStatus
            , "cosigners" ':= PBuiltinList (PAsData PPubKeyHash)
@@ -438,7 +438,7 @@ proposalValidator proposal =
     PScriptContext ctx' <- pmatch ctx'
     ctx <- pletFields @'["txInfo", "purpose"] ctx'
     txInfo <- plet $ pfromData ctx.txInfo
-    PTxInfo txInfo' <- pmatch $ txInfo
+    PTxInfo txInfo' <- pmatch txInfo
     txInfoF <- pletFields @'["inputs", "mint"] txInfo'
     PSpending ((pfield @"_0" #) -> txOutRef) <- pmatch $ pfromData ctx.purpose
 
@@ -452,7 +452,7 @@ proposalValidator proposal =
 
     proposalF <-
       pletFields
-        @'[ "id"
+        @'[ "proposalId"
           , "effects"
           , "status"
           , "cosigners"
@@ -464,7 +464,10 @@ proposalValidator proposal =
     ownAddress <- plet $ txOutF.address
 
     stCurrencySymbol <- plet $ pconstant $ mintingPolicySymbol $ mkMintingPolicy (proposalPolicy proposal)
-    spentST <- plet $ psymbolValueOf # stCurrencySymbol #$ pvalueSpent # txInfoF.inputs
+    valueSpent <- plet $ pvalueSpent # txInfoF.inputs
+    spentST <- plet $ psymbolValueOf # stCurrencySymbol #$ valueSpent
+    let AssetClass (stakeSym, stakeTn) = proposal.stakeSTAssetClass
+    spentStakeST <- plet $ passetClassValueOf # valueSpent # (passetClass # pconstant stakeSym # pconstant stakeTn)
 
     pmatch proposalRedeemer $ \case
       PVote _r -> P.do
@@ -482,37 +485,33 @@ proposalValidator proposal =
         passert "Signed by all new cosigners" $
           pall # plam (\sig -> ptxSignedBy # ctx.txInfo # sig) # newSigs
 
+        passert "As many new cosigners as Stake datums" $
+          spentStakeST #== plength # newSigs
+
         passert "Signatures are correctly added to cosignature list" $
           anyOutput @PProposalDatum # ctx.txInfo
             #$ plam
             $ \newValue address newProposalDatum -> P.do
-              newProposalF <-
-                pletFields
-                  @'[ "id"
-                    , "effects"
-                    , "status"
-                    , "cosigners"
-                    , "thresholds"
-                    , "votes"
-                    ]
-                  newProposalDatum
-
               -- This is a little sad. Can we do better by
               -- building a new ProposalDatum and then comparing?
               let correctDatum =
-                    foldr1
-                      (#&&)
-                      [ newProposalF.cosigners #== pconcat # newSigs # proposalF.cosigners
-                      , newProposalF.id #== proposalF.id
-                      , newProposalF.effects #== proposalF.effects
-                      , newProposalF.status #== proposalF.status
-                      , newProposalF.thresholds #== proposalF.thresholds
-                      , newProposalF.votes #== proposalF.votes
-                      ]
+                    pdata newProposalDatum
+                      #== pdata
+                        ( mkRecordConstr
+                            PProposalDatum
+                            ( #proposalId .= proposalF.proposalId
+                                .& #effects .= proposalF.effects
+                                .& #status .= proposalF.status
+                                .& #cosigners .= pdata (pconcat # newSigs # proposalF.cosigners)
+                                .& #thresholds .= proposalF.thresholds
+                                .& #votes .= proposalF.votes
+                            )
+                        )
 
               foldr1
                 (#&&)
-                [ ptraceIfFalse "Datum must be correct" $ correctDatum
+                [ pcon PTrue
+                , ptraceIfFalse "Datum must be correct" correctDatum
                 , ptraceIfFalse "Value should be correct" $ pdata txOutF.value #== pdata newValue
                 , ptraceIfFalse "Must be sent to Proposal's address" $ ownAddress #== pdata address
                 ]

agora/Agora/Proposal/Time.hs

@@ -24,7 +24,7 @@ module Agora.Proposal.Time (
   isDraftRange,
 ) where
 
-import Agora.Record (build, (.&), (.=))
+import Agora.Record (mkRecordConstr, (.&), (.=))
 import GHC.Generics qualified as GHC
 import Generics.SOP (Generic, I (I))
 import Plutarch.Api.V1 (PExtended (PFinite), PInterval (PInterval), PLowerBound (PLowerBound), PMaybeData (PDJust, PDNothing), PPOSIXTime, PPOSIXTimeRange, PUpperBound (PUpperBound))
@@ -149,23 +149,20 @@ currentProposalTime = phoistAcyclic $
     PUpperBound ub <- pmatch ivf.to
     lbf <- pletFields @'["_0", "_1"] lb
     ubf <- pletFields @'["_0", "_1"] ub
-    pcon
-      ( PProposalTime $
-          build $
-            #lowerBound
-              .= pdata
-                ( pmatch lbf._0 $
-                    \case
-                      PFinite d -> pcon (PDJust d)
-                      _ -> pcon (PDNothing pdnil)
-                )
-              .& #upperBound
-              .= pdata
-                ( pmatch ubf._0 $ \case
-                    PFinite d -> pcon (PDJust d)
-                    _ -> pcon (PDNothing pdnil)
-                )
-      )
+    mkRecordConstr PProposalTime $
+      #lowerBound
+        .= pdata
+          ( pmatch lbf._0 $
+              \case
+                PFinite d -> pcon (PDJust d)
+                _ -> pcon (PDNothing pdnil)
+          )
+        .& #upperBound
+        .= pdata
+          ( pmatch ubf._0 $ \case
+              PFinite d -> pcon (PDJust d)
+              _ -> pcon (PDNothing pdnil)
+          )
 
 -- | Check if 'PProposalTime' is within two 'PPOSIXTime'. Inclusive.
 proposalTimeWithin :: Term s (PPOSIXTime :--> PPOSIXTime :--> PProposalTime :--> PBool)

agora/Agora/Record.hs

@@ -3,9 +3,16 @@ Module     : Agora.Record
 Maintainer : emi@haskell.fyi
 Description: PDataRecord helper functions.
 
-PDataRecord helper functions.
+'PDataRecord' helper functions.
 -}
-module Agora.Record (build, (.=), (.&)) where
+module Agora.Record (
+  mkRecord,
+  mkRecordConstr,
+  (.=),
+  (.&),
+  RecordMorphism,
+  FieldName,
+) where
 
 import Control.Category (Category (..))
 import Data.Coerce (coerce)
@@ -20,17 +27,47 @@ data FieldName (sym :: Symbol) = FieldName
 {- | The use of two different 'Symbol's here allows unification to happen,
      ensuring 'FieldName' has a fully inferred 'Symbol'.
 
-     For example, @'build' (#foo .= 'pconstantData' (42 :: 'Integer'))@ gets
+     For example, @'mkRecord' (#foo .= 'pconstantData' (42 :: 'Integer'))@ gets
      the correct type. Namely, @'Term' s ('PDataRecord' '["foo" ':= 'PInteger'])@.
 -}
-instance forall (sym :: Symbol) (sym' :: Symbol). sym ~ sym' => IsLabel sym (FieldName sym') where
+instance forall (sym :: Symbol) (sym' :: Symbol). sym ~ sym' => IsLabel sym (FieldName sym) where
   fromLabel = FieldName
 
--- | Turn a builder into a fully built 'PDataRecord'.
-build :: forall (s :: S) (r :: [PLabeledType]). RecordMorphism s '[] r -> Term s (PDataRecord r)
-build f = coerce f pdnil
+-- | Turn a constant 'RecordMorphism' into a fully built 'PDataRecord'.
+mkRecord :: forall (r :: [PLabeledType]) (s :: S). RecordMorphism s '[] r -> Term s (PDataRecord r)
+mkRecord f = f.runRecordMorphism pdnil
 
--- | A morphism from one PDataRecord to another, representing some sort of consing of data.
+{- | 'mkRecord' but for known data-types.
+
+This allows you to dynamically construct a record type constructor.
+
+=== Example:
+@
+'mkRecordConstr'
+  'Agora.Stake.PStakeDatum'
+  ( #stakedAmount '.=' 'pconstantData' ('Plutarch.SafeMoney.Tagged' @GTTag 42)
+      '.&' #owner '.=' 'pconstantData' "aabbcc"
+      '.&' #lockedBy '.=' 'pdata' pnil
+  )
+@
+Is the same as
+
+@
+'pconstant' ('Agora.Stake.StakeDatum' ('Plutarch.SafeMoney.Tagged' 42) "aabbcc" [])
+@
+-}
+mkRecordConstr ::
+  forall (r :: [PLabeledType]) (s :: S) (pt :: PType).
+  PlutusType pt =>
+  -- | The constructor. This is just the Haskell-level constructor for the type.
+  --   For 'PMaybeData', this could be 'PDJust', or 'PNothing'.
+  (forall s'. Term s' (PDataRecord r) -> pt s') ->
+  -- | The morphism that builds the record.
+  RecordMorphism s '[] r ->
+  Term s pt
+mkRecordConstr ctr = pcon . ctr . mkRecord
+
+-- | A morphism from one 'PDataRecord' to another, representing some sort of consing of data.
 newtype RecordMorphism (s :: S) (as :: [PLabeledType]) (bs :: [PLabeledType]) = RecordMorphism
   { runRecordMorphism ::
     Term s (PDataRecord as) ->
@@ -46,14 +83,18 @@ infix 7 .=
 -- | Cons a labeled type as a 'RecordMorphism'.
 (.=) ::
   forall (sym :: Symbol) (a :: PType) (as :: [PLabeledType]) (s :: S).
+  -- | The field name. You can use @-XOverloadedLabels@ to enable the syntax:
+  --   @#hello ~ 'FieldName' "hello"@
   FieldName sym ->
+  -- | The value at that field. This must be 'PAsData', because the underlying
+  --   type is @'Constr' 'Integer' ['Data']@.
   Term s (PAsData a) ->
   RecordMorphism s as ((sym ':= a) ': as)
 _ .= x = RecordMorphism $ pcon . PDCons x
 
 infixr 6 .&
 
--- | Compose two morphisms between records.
+-- | Compose two 'RecordMorphism's.
 (.&) ::
   forall
     (s :: S)

agora/Agora/Stake.hs

@@ -441,15 +441,20 @@ stakeValidator stake =
           anyOutput @PStakeDatum # txInfo
             #$ plam
             $ \value address newStakeDatum' -> P.do
+              PStakeDatum newStakeDatum <- pmatch newStakeDatum'
+              newStakeDatumF <- pletFields @'["stakedAmount"] newStakeDatum
               let isScriptAddress = pdata address #== ownAddress
               let correctOutputDatum = pdata newStakeDatum' #== pdata stakeDatum'
               let valueCorrect = pdata continuingValue #== pdata value
-              foldr1
-                (#&&)
-                [ ptraceIfFalse "isScriptAddress" isScriptAddress
-                , ptraceIfFalse "correctOutputDatum" correctOutputDatum
-                , ptraceIfFalse "valueCorrect" valueCorrect
-                ]
+              pif
+                isScriptAddress
+                ( foldl1
+                    (#&&)
+                    [ ptraceIfFalse "valueCorrect" valueCorrect
+                    , ptraceIfFalse "correctOutputDatum" correctOutputDatum
+                    ]
+                )
+                (pcon PFalse)
         popaque (pconstant ())
       PDepositWithdraw r -> P.do
         passert "ST at inputs must be 1" $