simplify some PTxInfo functions

agora/Agora/Proposal.hs

@@ -60,7 +60,16 @@ import PlutusTx.AssocMap qualified as AssocMap
 --------------------------------------------------------------------------------
 
 import Agora.SafeMoney (GTTag)
-import Agora.Utils (passert, pnotNull, psymbolValueOf, ptokenSpent, pvalueSpent)
+import Agora.Utils (
+  anyOutput,
+  findTxOutByTxOutRef,
+  passert,
+  pnotNull,
+  psymbolValueOf,
+  ptokenSpent,
+  ptxSignedBy,
+  pvalueSpent,
+ )
 import Control.Arrow (first)
 import Plutarch.Api.V1.Extra (passetClass, passetClassValueOf)
 import Plutarch.Builtin (PBuiltinMap)
@@ -427,17 +436,25 @@ proposalValidator proposal =
   plam $ \datum redeemer ctx' -> P.do
     PScriptContext ctx' <- pmatch ctx'
     ctx <- pletFields @'["txInfo", "purpose"] ctx'
-    PTxInfo txInfo' <- pmatch $ pfromData ctx.txInfo
+    txInfo <- plet $ pfromData ctx.txInfo
-    _txInfo <- pletFields @'["inputs", "mint"] txInfo'
+    PTxInfo txInfo' <- pmatch $ txInfo
-    PSpending _txOutRef <- pmatch $ pfromData ctx.purpose
+    txInfoF <- pletFields @'["inputs", "mint"] txInfo'
+    PSpending ((pfield @"_0" #) -> txOutRef) <- pmatch $ pfromData ctx.purpose
 
-    let _proposalDatum' :: Term _ PProposalDatum
+    PJust txOut <- pmatch $ findTxOutByTxOutRef # txOutRef # txInfoF.inputs
-        _proposalDatum' = pfromData $ punsafeCoerce datum
+    txOutF <- pletFields @'["address"] $ txOut
+
+    let proposalDatum :: Term _ PProposalDatum
+        proposalDatum = pfromData $ punsafeCoerce datum
         proposalRedeemer :: Term _ PProposalRedeemer
         proposalRedeemer = pfromData $ punsafeCoerce redeemer
 
+    proposalF <- pletFields @'["cosigners"] proposalDatum
+
+    ownAddress <- plet $ txOutF.address
+
     stCurrencySymbol <- plet $ pconstant $ mintingPolicySymbol $ mkMintingPolicy (proposalPolicy proposal)
-    spentST <- plet $ psymbolValueOf # stCurrencySymbol #$ pvalueSpent # ctx.txInfo
+    spentST <- plet $ psymbolValueOf # stCurrencySymbol #$ pvalueSpent # txInfoF.inputs
 
     pmatch proposalRedeemer $ \case
       PVote _r -> P.do
@@ -446,10 +463,33 @@ proposalValidator proposal =
 
         popaque (pconstant ())
       --------------------------------------------------------------------------
-      PCosign _r -> P.do
+      PCosign r -> P.do
+        newSigs <- plet $ pfield @"newCosigners" # r
+
         passert "ST at inputs must be 1" $
           spentST #== 1
 
+        passert "Signed by all new cosigners" $
+          pall # plam (\sig -> ptxSignedBy # ctx.txInfo # sig) # newSigs
+
+        passert "Signatures are correctly added to cosignature list" $
+          anyOutput @PProposalDatum # ctx.txInfo
+            #$ plam
+            $ \_value address newProposalDatum -> P.do
+              newProposalF <- pletFields @'["cosigners"] newProposalDatum
+
+              let correctDatum =
+                    foldr1
+                      (#&&)
+                      [ newProposalF.cosigners #== proposalF.cosigners
+                      ]
+
+              foldr1
+                (#&&)
+                [ ptraceIfFalse "Datum must be correct" $ correctDatum
+                , ptraceIfFalse "Must be sent to Proposal's address" $ ownAddress #== pdata address
+                ]
+
         popaque (pconstant ())
       --------------------------------------------------------------------------
       PUnlock _r -> P.do

agora/Agora/Record.hs

@@ -48,8 +48,7 @@ infix 7 .=
   forall (sym :: Symbol) (a :: PType) (as :: [PLabeledType]) (s :: S).
   FieldName sym ->
   Term s (PAsData a) ->
-  ( RecordMorphism s as ((sym ':= a) ': as)
+  RecordMorphism s as ((sym ':= a) ': as)
-  )
 _ .= x = RecordMorphism $ pcon . PDCons x
 
 infixr 6 .&

agora/Agora/Stake.hs

@@ -39,6 +39,7 @@ import Plutarch.Api.V1 (
   PPubKeyHash,
   PScriptPurpose (PMinting, PSpending),
   PTokenName,
+  PTxInfo,
   PValidator,
   mintingPolicySymbol,
   mkMintingPolicy,
@@ -266,13 +267,15 @@ stakePolicy :: Stake -> ClosedTerm PMintingPolicy
 stakePolicy stake =
   plam $ \_redeemer ctx' -> P.do
     ctx <- pletFields @'["txInfo", "purpose"] ctx'
-    txInfo' <- plet ctx.txInfo
+    txInfo <- plet $ ctx.txInfo
-    txInfo <- pletFields @'["mint", "inputs", "outputs"] txInfo'
+    let _a :: Term _ PTxInfo
+        _a = txInfo
+    txInfoF <- pletFields @'["mint", "inputs", "outputs"] txInfo
 
     PMinting ownSymbol' <- pmatch $ pfromData ctx.purpose
     ownSymbol <- plet $ pfield @"_0" # ownSymbol'
-    spentST <- plet $ psymbolValueOf # ownSymbol #$ pvalueSpent # pfromData txInfo'
+    spentST <- plet $ psymbolValueOf # ownSymbol #$ pvalueSpent # txInfoF.inputs
-    mintedST <- plet $ psymbolValueOf # ownSymbol # txInfo.mint
+    mintedST <- plet $ psymbolValueOf # ownSymbol # txInfoF.mint
 
     let burning = P.do
           passert "ST at inputs must be 1" $
@@ -282,7 +285,7 @@ stakePolicy stake =
             mintedST #== -1
 
           passert "An unlocked input existed containing an ST" $
-            anyInput @PStakeDatum # pfromData txInfo'
+            anyInput @PStakeDatum # txInfo
               #$ plam
               $ \value _ stakeDatum' -> P.do
                 let hasST = psymbolValueOf # ownSymbol # value #== 1
@@ -299,7 +302,7 @@ stakePolicy stake =
             mintedST #== 1
 
           passert "A UTXO must exist with the correct output" $
-            anyOutput @PStakeDatum # pfromData txInfo'
+            anyOutput @PStakeDatum # txInfo
               #$ plam
               $ \value address stakeDatum' -> P.do
                 let cred = pfield @"credential" # address
@@ -359,8 +362,8 @@ stakeValidator :: Stake -> ClosedTerm PValidator
 stakeValidator stake =
   plam $ \datum redeemer ctx' -> P.do
     ctx <- pletFields @'["txInfo", "purpose"] ctx'
-    txInfo' <- plet ctx.txInfo
+    txInfo <- plet $ pfromData ctx.txInfo
-    txInfo <- pletFields @'["mint", "inputs", "outputs"] txInfo'
+    txInfoF <- pletFields @'["mint", "inputs", "outputs"] txInfo
 
     (pfromData -> stakeRedeemer, _) <- ptryFrom redeemer
 
@@ -371,7 +374,7 @@ stakeValidator stake =
 
     PSpending txOutRef <- pmatch $ pfromData ctx.purpose
 
-    PJust txInInfo <- pmatch $ pfindTxInByTxOutRef # (pfield @"_0" # txOutRef) # txInfo'
+    PJust txInInfo <- pmatch $ pfindTxInByTxOutRef # (pfield @"_0" # txOutRef) # txInfoF.inputs
     ownAddress <- plet $ pfield @"address" #$ pfield @"resolved" # txInInfo
     let continuingValue = pfield @"value" #$ pfield @"resolved" # txInInfo
 
@@ -379,8 +382,8 @@ stakeValidator stake =
     ownerSignsTransaction <- plet $ ptxSignedBy # ctx.txInfo # stakeDatum.owner
 
     stCurrencySymbol <- plet $ pconstant $ mintingPolicySymbol $ mkMintingPolicy (stakePolicy stake)
-    mintedST <- plet $ psymbolValueOf # stCurrencySymbol # txInfo.mint
+    mintedST <- plet $ psymbolValueOf # stCurrencySymbol # txInfoF.mint
-    spentST <- plet $ psymbolValueOf # stCurrencySymbol #$ pvalueSpent # txInfo'
+    spentST <- plet $ psymbolValueOf # stCurrencySymbol #$ pvalueSpent # txInfoF.inputs
 
     -- Is the stake currently locked?
     stakeIsLocked <- plet $ stakeLocked # stakeDatum'
@@ -420,7 +423,7 @@ stakeValidator stake =
           "Owner signs this transaction"
           ownerSignsTransaction
         passert "A UTXO must exist with the correct output" $
-          anyOutput @PStakeDatum # txInfo'
+          anyOutput @PStakeDatum # txInfo
             #$ plam
             $ \value address newStakeDatum' -> P.do
               newStakeDatum <- pletFields @'["owner", "stakedAmount"] newStakeDatum'

agora/Agora/Utils.hs

@@ -249,46 +249,61 @@ paddValue = phoistAcyclic $
       )
 
 -- | Sum of all value at input.
-pvalueSpent :: Term s (PTxInfo :--> PValue)
+pvalueSpent :: Term s (PBuiltinList (PAsData PTxInInfo) :--> PValue)
 pvalueSpent = phoistAcyclic $
-  plam $ \txInfo' ->
+  plam $ \inputs ->
-    pmatch txInfo' $ \(PTxInfo txInfo) ->
+    pfoldr
-      pfoldr
+      # plam
-        # plam
+        ( \txInInfo' v ->
-          ( \txInInfo' v ->
+            pmatch
-              pmatch
+              (pfromData txInInfo')
-                (pfromData txInInfo')
+              $ \(PTxInInfo txInInfo) ->
-                $ \(PTxInInfo txInInfo) ->
+                paddValue
-                  paddValue
+                  # pmatch
-                    # pmatch
+                    (pfield @"resolved" # txInInfo)
-                      (pfield @"resolved" # txInInfo)
+                    (\(PTxOut o) -> pfromData $ pfield @"value" # o)
-                      (\(PTxOut o) -> pfromData $ pfield @"value" # o)
+                  # v
-                    # v
+        )
-          )
+      # pconstant mempty
-        # pconstant mempty
+      # inputs
-        # (pfield @"inputs" # txInfo)
 
 -- | Find the TxInInfo by a TxOutRef.
-pfindTxInByTxOutRef :: Term s (PTxOutRef :--> PTxInfo :--> PMaybe PTxInInfo)
+pfindTxInByTxOutRef :: Term s (PTxOutRef :--> PBuiltinList (PAsData PTxInInfo) :--> PMaybe PTxInInfo)
 pfindTxInByTxOutRef = phoistAcyclic $
-  plam $ \txOutRef txInfo' ->
+  plam $ \txOutRef inputs ->
-    pmatch txInfo' $ \(PTxInfo txInfo) ->
+    pfindMap
-      pfindMap
+      # plam
-        # plam
+        ( \txInInfo' ->
-          ( \txInInfo' ->
+            plet (pfromData txInInfo') $ \r ->
-              plet (pfromData txInInfo') $ \r ->
+              pmatch r $ \(PTxInInfo txInInfo) ->
-                pmatch r $ \(PTxInInfo txInInfo) ->
+                pif
-                  pif
+                  (pdata txOutRef #== pfield @"outRef" # txInInfo)
-                    (pdata txOutRef #== pfield @"outRef" # txInInfo)
+                  (pcon (PJust r))
-                    (pcon (PJust r))
+                  (pcon PNothing)
-                    (pcon PNothing)
+        )
-          )
+      #$ inputs
-        #$ (pfield @"inputs" # txInfo)
 
 -- | True if a list is not empty.
 pnotNull :: forall list a. PIsListLike list a => Term _ (list a :--> PBool)
 pnotNull = phoistAcyclic $ plam $ pelimList (\_ _ -> pcon PTrue) (pcon PFalse)
 
+-- | Check if a particular asset class has been spent in the input list.
+ptokenSpent :: forall {s :: S}. Term s (PAssetClass :--> PBuiltinList (PAsData PTxInInfo) :--> PBool)
+ptokenSpent =
+  plam $ \tokenClass inputs ->
+    0
+      #< pfoldr @PBuiltinList
+        # plam
+          ( \txInInfo' acc -> P.do
+              PTxInInfo txInInfo <- pmatch (pfromData txInInfo')
+              PTxOut txOut' <- pmatch $ pfromData $ pfield @"resolved" # txInInfo
+              txOut <- pletFields @'["value"] txOut'
+              let txOutValue = pfromData txOut.value
+              acc + passetClassValueOf # txOutValue # tokenClass
+          )
+        # 0
+        # inputs
+
 --------------------------------------------------------------------------------
 {- Functions which should (probably) not be upstreamed
    All of these functions are quite inefficient.
@@ -372,10 +387,10 @@ psingletonValue = phoistAcyclic $
      in res
 
 -- | Finds the TxOut of an effect from TxInfo and TxOutRef
-findTxOutByTxOutRef :: Term s (PTxOutRef :--> PTxInfo :--> PMaybe PTxOut)
+findTxOutByTxOutRef :: Term s (PTxOutRef :--> PBuiltinList (PAsData PTxInInfo) :--> PMaybe PTxOut)
 findTxOutByTxOutRef = phoistAcyclic $
-  plam $ \txOutRef txInfo ->
+  plam $ \txOutRef inputs ->
-    pmatch (pfindTxInByTxOutRef # txOutRef # txInfo) $ \case
+    pmatch (pfindTxInByTxOutRef # txOutRef # inputs) $ \case
       PJust ((pfield @"resolved" #) -> txOut) -> pcon $ PJust txOut
       PNothing -> pcon PNothing
 
@@ -408,20 +423,3 @@ findTxOutDatum = phoistAcyclic $
     case datumHash' of
       PDJust ((pfield @"_0" #) -> datumHash) -> pfindDatum # datumHash # info
       _ -> pcon PNothing
-
--- | Check if a particular asset class has been spent in the input list.
-ptokenSpent :: forall {s :: S}. Term s (PAssetClass :--> PBuiltinList (PAsData PTxInInfo) :--> PBool)
-ptokenSpent =
-  plam $ \tokenClass inputs ->
-    0
-      #< pfoldr @PBuiltinList
-        # plam
-          ( \txInInfo' acc -> P.do
-              PTxInInfo txInInfo <- pmatch (pfromData txInInfo')
-              PTxOut txOut' <- pmatch $ pfromData $ pfield @"resolved" # txInInfo
-              txOut <- pletFields @'["value"] txOut'
-              let txOutValue = pfromData txOut.value
-              acc + passetClassValueOf # txOutValue # tokenClass
-          )
-        # 0
-        # inputs