Treasury Withdrawal Effect checks if remainder is to the treasury

It checks if transaction is paying the remainders to the treasury.

agora/Agora/Effect/TreasuryWithdrawal.hs

@@ -13,15 +13,16 @@ import GHC.Generics qualified as GHC
 import Generics.SOP (Generic, I (I))
 
 import Agora.Effect (makeEffect)
-import Agora.Utils (findTxOutByTxOutRef, passert)
+import Agora.Utils ( paddValue, passert ) 
 import Plutarch (popaque)
-import Plutarch.Api.V1 (
+import Plutarch.Api.V1
-  PCredential,
+    ( PCredential,
-  PTuple,
+      PValue,
-  PValidator,
+      PTxOut(PTxOut),
-  PValue,
+      PTxInInfo(PTxInInfo),
-  ptuple,
+      PTuple,
- )
+      ptuple,
+      PValidator )
 
 import Plutarch.DataRepr (
   DerivePConstantViaData (..),
@@ -78,9 +79,9 @@ It can be more flexiable over...
 -}
 treasuryWithdrawalValidator :: forall {s :: S}. CurrencySymbol -> Term s PValidator
 treasuryWithdrawalValidator currSymbol = makeEffect currSymbol $
-  \_cs (datum' :: Term _ PTreasuryWithdrawalDatum) txOutRef' txInfo' -> P.do
+  \_cs (datum' :: Term _ PTreasuryWithdrawalDatum) _txOutRef' txInfo' -> P.do
     receivers <- plet $ pfromData $ pfield @"receivers" # datum'
-    txInfo <- pletFields @'["outputs"] txInfo'
+    txInfo <- pletFields @'["outputs", "inputs"] txInfo'
     let outputValues =
           pmap
             # plam
@@ -89,25 +90,41 @@ treasuryWithdrawalValidator currSymbol = makeEffect currSymbol $
                   cred <- pletFields @'["credential"] $ pfromData out.address
                   pdata $ ptuple # cred.credential # out.value
               )
-            #$ txInfo.outputs
+            # txInfo.outputs
         outputContentMatchesRecivers =
           pall # plam (\out -> pelem # out # outputValues)
             #$ receivers
-        outputNumberMatchesReceivers = plength # receivers #== plength # (pfromData txInfo.outputs)
+        sumValues = 
-        outputIsNotPayingToEffect = P.do
+          pfoldr
-          PJust txOut <- pmatch $ findTxOutByTxOutRef # txOutRef' # pfromData txInfo'
+            # plam
-          input <- pletFields @'["address", "value"] $ txOut
+              ( \((pfield @"_1" #) . pfromData -> x) y -> P.do
-          let notPayingToEffect =
+                  paddValue # (pfromData x) # y
-                pnot #$ pany
+              )
-                  # plam
+            # (pconstant (mempty :: Value))
-                    ( \x ->
+        inputCred =
-                        input.address #== pfield @"address" # pfromData x
+          pmap
-                    )
+            # plam (\inInfo -> P.do
-                  # pfromData txInfo.outputs
+                     PTxInInfo inInfo' <- pmatch $ pfromData inInfo
-          notPayingToEffect
+                     PTxOut out <- pmatch $ pfromData $ pfield @"resolved" # inInfo'
+                     let addr = pfromData $ pfield @"address" # out
+                     pfield @"credential" # addr)
+            # pfromData txInfo.inputs
+        totalInput =
+          pfoldr
+            # plam (\x' y -> P.do
+                   PTxInInfo x <- pmatch $ pfromData x'
+                   PTxOut out <- pmatch $ pfromData $ pfield @"resolved" # x
+                   paddValue # (pfromData $ pfield @"value" # out) # y)
+            # (pconstant (mempty :: Value))
+            # pfromData txInfo.inputs
+        sumOutputsToInputAddr = sumValues #$
+          pfilter
+            # plam (\((pfield @"_0" #) . pfromData -> addr) -> pelem # (addr) # inputCred) # outputValues
+        sumReceivers = sumValues # receivers
+-- TODO: Probably need to check/exclude the effect input...
+        excessShouldBePaidToInputs = pdata (paddValue # sumReceivers # sumOutputsToInputAddr) #== pdata totalInput
 
     passert "Transaction output does not match receivers" outputContentMatchesRecivers
-    passert "" outputNumberMatchesReceivers
+    passert "Remainders should be returned to the treasury" excessShouldBePaidToInputs
-    passert "" outputIsNotPayingToEffect
 
     popaque $ pconstant ()