Merge pull request #118 from Liqwid-Labs/connor/use-upstreamed-utils

Use upstreamed utilities
2022-06-17 21:24:41 +08:00 · 2022-06-17 21:24:41 +08:00 · 2d9bf1733e
commit 2d9bf1733e
parent 25f7f58880 adcf6e6347
20 changed files with 1736 additions and 1309 deletions
--- a/agora-specs/Property/MultiSig.hs
+++ b/agora-specs/Property/MultiSig.hs
@ -12,7 +12,6 @@ import Agora.MultiSig (
  PMultiSig,
  pvalidatedByMultisig,
 )
 import Agora.Utils (tclet)
 import Data.Maybe (fromJust)
 import Data.Tagged (Tagged (Tagged))
 import Data.Universe (Finite (..), Universe (..))
@ -24,6 +23,7 @@ import Plutarch.Context.Spending (
  signedWith,
  spendingContext,
 )
 import Plutarch.Extra.TermCont (pletC)
 import PlutusLedgerApi.V1 (
  ScriptContext (scriptContextTxInfo),
  TxInfo (txInfoSignatories),
@ -98,8 +98,8 @@ expectedHs model = case classifyMultiSigProp model of
 -- | Actual implementation of @pvalidatedByMultisig@.
 actual :: Term s (PBuiltinPair PMultiSig PScriptContext :--> PBool)
 actual = plam $ \x -> unTermCont $ do
-  ms <- tclet $ pfstBuiltin # x
+  ms <- pletC $ pfstBuiltin # x
-  sc <- tclet $ psndBuiltin # x
+  sc <- pletC $ psndBuiltin # x
  pure $ pvalidatedByMultisig # ms # (pfield @"txInfo" # sc)
 -- | Proposed property.
--- a/agora-specs/Spec/Effect/TreasuryWithdrawal.hs
+++ b/agora-specs/Spec/Effect/TreasuryWithdrawal.hs
@ -155,8 +155,8 @@ specs =
        ]
    datum2 =
      TreasuryWithdrawalDatum
-        [ (head users, asset1 4 <> asset2 5)
+        [ (head users, asset2 5 <> asset1 4)
-        , (users !! 1, asset1 2 <> asset2 1)
+        , (users !! 1, asset2 1 <> asset1 2)
        , (users !! 2, asset1 1)
        ]
        [ head treasuries
--- a/agora-specs/Spec/Utils.hs
+++ b/agora-specs/Spec/Utils.hs
@ -7,220 +7,9 @@ Tests for utility functions in 'Agora.Utils'.
 -}
 module Spec.Utils (tests) where
 --------------------------------------------------------------------------------
 import Agora.Utils (phalve, pisUniq, pmergeBy, pmsort, pnubSort, pupdate)
 --------------------------------------------------------------------------------
 import Data.List (nub, sort)
 import Data.Map qualified as M
 import Data.Set qualified as S
 --------------------------------------------------------------------------------
 import Control.Monad.Cont (cont, runCont)
 import Test.Tasty (TestTree)
 import Test.Tasty.QuickCheck (
  Arbitrary (arbitrary),
  Property,
  Testable (property),
  elements,
  forAll,
  suchThat,
  testProperty,
  (.&&.),
 )
 import Test.Util (updateMap)
 --------------------------------------------------------------------------------
 import PlutusTx.AssocMap qualified as AssocMap
 --------------------------------------------------------------------------------
 tests :: [TestTree]
-tests =
+tests = []
  [ testProperty "'pmsort' sorts a list properly" prop_msortCorrect
  , testProperty "'pmerge' merges two sorted lists into one sorted list" prop_mergeCorrect
  , testProperty "'phalve' splits a list in half as expected" prop_halveCorrect
  , testProperty "'pnubSort' sorts a list and remove duplicate elements" prop_nubSortProperly
  , testProperty "'pisUniq' can tell whether all elements in a list are unique" prop_uniqueList
  , testProperty "'pupdate' updates assoc maps as 'updateMap' does" prop_updateAssocMapParity
  ]
 --------------------------------------------------------------------------------
 -- | Yield true if 'Agora.Utils.pmsort' sorts a given list correctly.
 prop_msortCorrect :: [Integer] -> Bool
 prop_msortCorrect l = sorted == expected
  where
    -- Expected sorted list, using 'Data.List.sort'.
    expected :: [Integer]
    expected = sort l
    --
    psorted :: Term _ (PBuiltinList PInteger)
    psorted = pmsort # pconstant l
    sorted :: [Integer]
    sorted = plift psorted
 -- | Yield true if 'Agora.Utils.pmerge' merges two list into a ordered list correctly.
 prop_mergeCorrect :: [Integer] -> [Integer] -> Bool
 prop_mergeCorrect a b = merged == expected
  where
    -- Sorted list a and b
    sa = sort a
    sb = sort b
    -- Merge two lists which are assumed to be ordered.
    merge :: [Integer] -> [Integer] -> [Integer]
    merge xs [] = xs
    merge [] ys = ys
    merge sx@(x : xs) sy@(y : ys)
      | x <= y = x : merge xs sy
      | otherwise = y : merge sx ys
    expected :: [Integer]
    expected = merge sa sb
    --
    pmerged :: Term _ (PBuiltinList PInteger)
    pmerged = pmergeBy # plam (#<) # pconstant sa # pconstant sb
    merged :: [Integer]
    merged = plift pmerged
 {- | Yield true if Plutarch level 'Agora.Utils.phalve' splits a given list
   as its Haskell level counterpart does.
 -}
 prop_halveCorrect :: [Integer] -> Bool
 prop_halveCorrect l = halved == expected
  where
    -- Halve a list.
    halve :: [Integer] -> ([Integer], [Integer])
    halve xs = go xs xs
      where
        go xs [] = ([], xs)
        go (x : xs) [_] = ([x], xs)
        go (x : xs) (_ : _ : ys) =
          let (first, last) =
                go xs ys
           in (x : first, last)
        go [] _ = ([], [])
    expected :: ([Integer], [Integer])
    expected = halve l
    --
    phalved :: Term _ (PPair (PBuiltinList PInteger) (PBuiltinList PInteger))
    phalved = phalve # pconstant l
    halved :: ([Integer], [Integer])
    halved =
      let f = plift $ pmatch phalved $ \(PPair x _) -> x
          s = plift $ pmatch phalved $ \(PPair _ x) -> x
       in (f, s)
 {- | Yield true if 'Agora.Utils.pnubSort' sorts and removes
   duplicate elements from a given list.
 -}
 prop_nubSortProperly :: [Integer] -> Bool
 prop_nubSortProperly l = nubbed == expected
  where
    -- Sort and list and then nub it.
    expected :: [Integer]
    expected = nub $ sort l
    --
    pnubbed :: Term _ (PBuiltinList PInteger)
    pnubbed = pnubSort # pconstant l
    nubbed :: [Integer]
    nubbed = plift pnubbed
 {- | Yield true if 'Agora.Utils.isUnique' can correctly determine
   whether a given list only contains unique elements or not.
 -}
 prop_uniqueList :: [Integer] -> Bool
 prop_uniqueList l = isUnique == expected
  where
    -- Convert input list to a set.
    -- If the set's size equals to list's size,
    --   the list only contains unique elements.
    expected :: Bool
    expected = S.size (S.fromList l) == length l
    --
    isUnique = plift $ pisUniq # pconstant l
 {- | Test the parity between 'updateMap' and 'pupdate',
     also ensure they both work correctly.
 -}
 prop_updateAssocMapParity :: Property
 prop_updateAssocMapParity =
  runCont
    ( do
        -- Generate a bunch unique keys.
        keys <-
          cont $
            forAll $
              arbitrary @(S.Set Integer) `suchThat` (not . S.null)
        -- Generate key-value pairs.
        kvPairs <- cont $ forAll $ mapM (\k -> (k,) <$> (arbitrary @Integer)) $ S.toList keys
        let initialMap = AssocMap.fromList kvPairs
            pinitialMap :: Term _ _
            pinitialMap = phoistAcyclic $ pconstant initialMap
            referenceMap = M.fromList kvPairs
        let pupdatedValue :: Maybe Integer -> Term _ (PMaybe PInteger)
            pupdatedValue updatedValue = phoistAcyclic $ case updatedValue of
              Nothing -> pcon PNothing
              Just v -> pcon $ PJust $ pconstant v
            -- Given the key and the updated value, test the parity
            parity key updatedValue =
              let native = updateMap (const updatedValue) key initialMap
                  plutarch :: AssocMap.Map Integer Integer
                  plutarch =
                    plift $
                      pupdate
                        # plam (\_ -> pupdatedValue updatedValue)
                        # pconstant key
                        # pinitialMap
                  expected =
                    AssocMap.fromList $
                      M.toList $
                        M.update (const updatedValue) key referenceMap
               in expected == native
                    && expected == plutarch
        -- Select a key, generate a maybe value.
        -- The value at the key should be set to the new value or removed.
        (targetKey, _) <- cont $ forAll $ elements kvPairs
        updatedValue <- cont $ forAll $ arbitrary @(Maybe Integer)
        -- Now what if the key doesn't exist in our map?
        nonexistentKey <-
          cont $
            forAll $
              arbitrary @Integer `suchThat` (\k -> not $ S.member k keys)
        pure
          ( property (parity targetKey updatedValue)
              .&&. property (parity nonexistentKey updatedValue)
          )
    )
    id
--- a/agora.cabal
+++ b/agora.cabal
@ -98,7 +98,6 @@ common deps
    , generics-sop
    , liqwid-plutarch-extra
    , plutarch
    , plutarch-extra
    , plutarch-numeric
    , plutarch-safe-money
    , plutus-core
--- a/agora/Agora/AuthorityToken.hs
+++ b/agora/Agora/AuthorityToken.hs
@ -28,8 +28,12 @@ import Plutarch.Api.V1 (
 )
 import Plutarch.Api.V1.AssetClass (passetClass, passetClassValueOf)
 import Plutarch.Api.V1.AssocMap (PMap (PMap))
 import Plutarch.Api.V1.ScriptContext (pisTokenSpent)
 import "liqwid-plutarch-extra" Plutarch.Api.V1.Value (psymbolValueOf)
 import "plutarch" Plutarch.Api.V1.Value (PValue (PValue))
 import Plutarch.Builtin (pforgetData)
 import Plutarch.Extra.List (plookup)
 import Plutarch.Extra.TermCont (pguardC, pmatchC)
 import PlutusLedgerApi.V1.Value (AssetClass (AssetClass))
 --------------------------------------------------------------------------------
@ -38,16 +42,6 @@ import GHC.Generics qualified as GHC
 --------------------------------------------------------------------------------
 import Agora.Utils (
  plookup,
  psymbolValueOf,
  ptokenSpent,
  tcassert,
  tcmatch,
 )
 --------------------------------------------------------------------------------
 {- | An AuthorityToken represents a proof that a particular token
     moved while this token was minted. In effect, this means that
     the validator that locked such a token must have approved
@ -74,11 +68,11 @@ newtype AuthorityToken = AuthorityToken
 authorityTokensValidIn :: Term s (PCurrencySymbol :--> PTxOut :--> PBool)
 authorityTokensValidIn = phoistAcyclic $
  plam $ \authorityTokenSym txOut'' -> unTermCont $ do
-    PTxOut txOut' <- tcmatch txOut''
+    PTxOut txOut' <- pmatchC txOut''
    txOut <- tcont $ pletFields @'["address", "value"] $ txOut'
-    PAddress address <- tcmatch txOut.address
+    PAddress address <- pmatchC txOut.address
-    PValue value' <- tcmatch txOut.value
+    PValue value' <- pmatchC txOut.value
-    PMap value <- tcmatch value'
+    PMap value <- pmatchC value'
    pure $
      pmatch (plookup # pdata authorityTokenSym # value) $ \case
        PJust (pfromData -> tokenMap') ->
@ -87,7 +81,7 @@ authorityTokensValidIn = phoistAcyclic $
              -- GATs should only be sent to Effect validators
              ptraceIfFalse "authorityTokensValidIn: GAT incorrectly lives at PubKey" $ pconstant False
            PScriptCredential ((pfromData . (pfield @"_0" #)) -> cred) -> unTermCont $ do
-              PMap tokenMap <- tcmatch tokenMap'
+              PMap tokenMap <- pmatchC tokenMap'
              pure $
                ptraceIfFalse "authorityTokensValidIn: GAT TokenName doesn't match ScriptHash" $
                  pall
@ -121,7 +115,7 @@ singleAuthorityTokenBurned gatCs txInfo mint = unTermCont $ do
          pall
            # plam
              ( \txInInfo' -> unTermCont $ do
-                  PTxInInfo txInInfo <- tcmatch (pfromData txInInfo')
+                  PTxInInfo txInInfo <- pmatchC (pfromData txInInfo')
                  let txOut' = pfield @"resolved" # txInInfo
                  pure $ authorityTokensValidIn # gatCs # pfromData txOut'
              )
@ -134,15 +128,15 @@ authorityTokenPolicy params =
  plam $ \_redeemer ctx' ->
    pmatch ctx' $ \(PScriptContext ctx') -> unTermCont $ do
      ctx <- tcont $ pletFields @'["txInfo", "purpose"] ctx'
-      PTxInfo txInfo' <- tcmatch $ pfromData ctx.txInfo
+      PTxInfo txInfo' <- pmatchC $ pfromData ctx.txInfo
      txInfo <- tcont $ pletFields @'["inputs", "mint", "outputs"] txInfo'
      let inputs = txInfo.inputs
          mintedValue = pfromData txInfo.mint
          AssetClass (govCs, govTn) = params.authority
          govAc = passetClass # pconstant govCs # pconstant govTn
-          govTokenSpent = ptokenSpent # govAc # inputs
+          govTokenSpent = pisTokenSpent # govAc # inputs
-      PMinting ownSymbol' <- tcmatch $ pfromData ctx.purpose
+      PMinting ownSymbol' <- pmatchC $ pfromData ctx.purpose
      let ownSymbol = pfromData $ pfield @"_0" # ownSymbol'
          mintedATs = passetClassValueOf # mintedValue # (passetClass # ownSymbol # pconstant "")
@ -150,8 +144,8 @@ authorityTokenPolicy params =
        pif
          (0 #< mintedATs)
          ( unTermCont $ do
-              tcassert "Parent token did not move in minting GATs" govTokenSpent
+              pguardC "Parent token did not move in minting GATs" govTokenSpent
-              tcassert "All outputs only emit valid GATs" $
+              pguardC "All outputs only emit valid GATs" $
                pall
                  # plam
                    ( (authorityTokensValidIn # ownSymbol #)
--- a/agora/Agora/Effect.hs
+++ b/agora/Agora/Effect.hs
@ -8,8 +8,8 @@ Helpers for constructing effects.
 module Agora.Effect (makeEffect) where
 import Agora.AuthorityToken (singleAuthorityTokenBurned)
 import Agora.Utils (tcassert, tclet, tcmatch, tctryFrom)
 import Plutarch.Api.V1 (PCurrencySymbol, PScriptPurpose (PSpending), PTxInfo, PTxOutRef, PValidator, PValue)
 import Plutarch.Extra.TermCont (pguardC, pletC, pmatchC, ptryFromC)
 import Plutarch.TryFrom ()
 import PlutusLedgerApi.V1.Value (CurrencySymbol)
@ -30,16 +30,16 @@ makeEffect ::
 makeEffect gatCs' f =
  plam $ \datum _redeemer ctx' -> unTermCont $ do
    ctx <- tcont $ pletFields @'["txInfo", "purpose"] ctx'
-    txInfo' <- tclet ctx.txInfo
+    txInfo' <- pletC ctx.txInfo
    -- convert input datum, PData, into desierable type
    -- the way this conversion is performed should be defined
    -- by PTryFrom for each datum in effect script.
-    (pfromData -> datum', _) <- tctryFrom datum
+    (pfromData -> datum', _) <- ptryFromC datum
    -- ensure purpose is Spending.
-    PSpending txOutRef <- tcmatch $ pfromData ctx.purpose
+    PSpending txOutRef <- pmatchC $ pfromData ctx.purpose
-    txOutRef' <- tclet (pfield @"_0" # txOutRef)
+    txOutRef' <- pletC (pfield @"_0" # txOutRef)
    -- fetch minted values to ensure single GAT is burned
    txInfo <- tcont $ pletFields @'["mint"] txInfo'
@ -47,9 +47,9 @@ makeEffect gatCs' f =
        mint = txInfo.mint
    -- fetch script context
-    gatCs <- tclet $ pconstant gatCs'
+    gatCs <- pletC $ pconstant gatCs'
-    tcassert "A single authority token has been burned" $ singleAuthorityTokenBurned gatCs txInfo' mint
+    pguardC "A single authority token has been burned" $ singleAuthorityTokenBurned gatCs txInfo' mint
    -- run effect function
    pure $ f gatCs datum' txOutRef' txInfo'
--- a/agora/Agora/Effect/GovernorMutation.hs
+++ b/agora/Agora/Effect/GovernorMutation.hs
@ -31,12 +31,14 @@ import Plutarch.Api.V1 (
  PValidator,
  PValue,
 )
 import Plutarch.Api.V1.ScriptContext (ptryFindDatum)
 import "liqwid-plutarch-extra" Plutarch.Api.V1.Value (pvalueOf)
 import Plutarch.DataRepr (
  DerivePConstantViaData (..),
  PDataFields,
  PIsDataReprInstances (PIsDataReprInstances),
 )
 import Plutarch.Extra.TermCont (pguardC)
 import Plutarch.Lift (PConstantDecl, PLifted, PUnsafeLiftDecl)
 import Plutarch.TryFrom (PTryFrom (..))
 import Plutarch.Unsafe (punsafeCoerce)
@ -64,8 +66,6 @@ import Agora.Utils (
  isScriptAddress,
  mustBePDJust,
  mustBePJust,
  ptryFindDatum,
  tcassert,
 )
 --------------------------------------------------------------------------------
@ -145,11 +145,11 @@ mutateGovernorValidator gov = makeEffect (authorityTokenSymbolFromGovernor gov)
    let mint :: Term _ (PBuiltinList _)
        mint = pto $ pto $ pto $ pfromData txInfoF.mint
-    tcassert "Nothing should be minted/burnt other than GAT" $
+    pguardC "Nothing should be minted/burnt other than GAT" $
      plength # mint #== 1
    -- Only two script inputs are alloed: one from the effect, one from the governor.
-    tcassert "Only self and governor script inputs are allowed" $
+    pguardC "Only self and governor script inputs are allowed" $
      pfoldr
        # phoistAcyclic
          ( plam $ \inInfo count ->
@ -176,11 +176,11 @@ mutateGovernorValidator gov = makeEffect (authorityTokenSymbolFromGovernor gov)
    govInInfo <- tcont $ pletFields @'["outRef", "resolved"] $ inputWithGST
    -- The effect can only modify the governor UTXO referenced in the datum.
-    tcassert "Can only modify the pinned governor" $
+    pguardC "Can only modify the pinned governor" $
      govInInfo.outRef #== datumF.governorRef
    -- The transaction can only have one output, which should be sent to the governor.
-    tcassert "Only governor output is allowed" $
+    pguardC "Only governor output is allowed" $
      plength # pfromData txInfoF.outputs #== 1
    let govAddress = pfield @"address" #$ govInInfo.resolved
@ -188,10 +188,10 @@ mutateGovernorValidator gov = makeEffect (authorityTokenSymbolFromGovernor gov)
    govOutput <- tcont $ pletFields @'["address", "value", "datumHash"] govOutput'
-    tcassert "No output to the governor" $
+    pguardC "No output to the governor" $
      govOutput.address #== govAddress
-    tcassert "Governor output doesn't carry the GST" $
+    pguardC "Governor output doesn't carry the GST" $
      gstValueOf # govOutput.value #== 1
    let governorOutputDatumHash =
@ -202,8 +202,8 @@ mutateGovernorValidator gov = makeEffect (authorityTokenSymbolFromGovernor gov)
              #$ ptryFindDatum # governorOutputDatumHash # txInfoF.datums
    -- Ensure the output governor datum is what we want.
-    tcassert "Unexpected governor datum" $ datumF.newDatum #== governorOutputDatum
+    pguardC "Unexpected governor datum" $ datumF.newDatum #== governorOutputDatum
-    tcassert "New governor datum should be valid" $ governorDatumValid # governorOutputDatum
+    pguardC "New governor datum should be valid" $ governorDatumValid # governorOutputDatum
    return $ popaque $ pconstant ()
  where
--- a/agora/Agora/Effect/TreasuryWithdrawal.hs
+++ b/agora/Agora/Effect/TreasuryWithdrawal.hs
@ -18,7 +18,7 @@ import GHC.Generics qualified as GHC
 import Generics.SOP (Generic, I (I))
 import Agora.Effect (makeEffect)
-import Agora.Utils (findTxOutByTxOutRef, isPubKey, paddValue, tcassert, tclet, tcmatch)
+import Agora.Utils (findTxOutByTxOutRef, isPubKey)
 import Plutarch.Api.V1 (
  AmountGuarantees (Positive),
  KeyGuarantees (Sorted),
@ -28,14 +28,15 @@ import Plutarch.Api.V1 (
  PValue,
  ptuple,
 )
 import "plutarch" Plutarch.Api.V1.Value (pnormalize)
 import Plutarch.Internal (punsafeCoerce)
 import "plutarch" Plutarch.Api.V1.Value (pnormalize)
 import Plutarch.DataRepr (
  DerivePConstantViaData (..),
  PDataFields,
  PIsDataReprInstances (..),
 )
 import Plutarch.Extra.TermCont (pguardC, pletC, pmatchC)
 import Plutarch.Lift (PConstantDecl, PUnsafeLiftDecl (..))
 import Plutarch.TryFrom (PTryFrom (..))
 import PlutusLedgerApi.V1.Credential (Credential)
@ -111,10 +112,10 @@ treasuryWithdrawalValidator currSymbol = makeEffect currSymbol $
  \_cs (datum' :: Term _ PTreasuryWithdrawalDatum) txOutRef' txInfo' -> unTermCont $ do
    datum <- tcont $ pletFields @'["receivers", "treasuries"] datum'
    txInfo <- tcont $ pletFields @'["outputs", "inputs"] txInfo'
-    PJust txOut <- tcmatch $ findTxOutByTxOutRef # txOutRef' # pfromData txInfo.inputs
+    PJust txOut <- pmatchC $ findTxOutByTxOutRef # txOutRef' # pfromData txInfo.inputs
    effInput <- tcont $ pletFields @'["address", "value"] $ txOut
    outputValues <-
-      tclet $
+      pletC $
        pmap
          # plam
            ( \(pfromData -> txOut') -> unTermCont $ do
@ -124,7 +125,7 @@ treasuryWithdrawalValidator currSymbol = makeEffect currSymbol $
            )
          # txInfo.outputs
    inputValues <-
-      tclet $
+      pletC $
        pmap
          # plam
            ( \((pfield @"resolved" #) . pfromData -> txOut') -> unTermCont $ do
@ -136,10 +137,13 @@ treasuryWithdrawalValidator currSymbol = makeEffect currSymbol $
    let ofTreasury =
          pfilter
            # plam (\((pfield @"_0" #) . pfromData -> cred) -> pelem # cred # datum.treasuries)
-        sumValues =
+        sumValues = phoistAcyclic $
-          pfoldr
+          plam $ \v ->
-            # plam (\((pfield @"_1" #) . pfromData -> x) ((pnormalize #) -> y) -> paddValue # pfromData x # y)
+            pnormalize
-            # punsafeCoerce (pconstant (mempty :: Value))
+              #$ pfoldr
              # plam (\(pfromData . (pfield @"_1" #) -> x) y -> x <> y)
              # mempty
              # v
        treasuryInputValuesSum = sumValues #$ ofTreasury # inputValues
        treasuryOutputValuesSum = sumValues #$ ofTreasury # outputValues
        receiverValuesSum = sumValues # datum.receivers
@ -148,7 +152,7 @@ treasuryWithdrawalValidator currSymbol = makeEffect currSymbol $
          pall # plam (\out -> pelem # out # outputValues)
            #$ datum.receivers
        excessShouldBePaidToInputs =
-          pdata (paddValue # receiverValuesSum # treasuryOutputValuesSum) #== pdata treasuryInputValuesSum
+          treasuryOutputValuesSum <> receiverValuesSum #== treasuryInputValuesSum
        shouldNotPayToEffect =
          pnot #$ pany
            # plam
@ -166,8 +170,8 @@ treasuryWithdrawalValidator currSymbol = makeEffect currSymbol $
              )
            # inputValues
-    tcassert "Transaction should not pay to effects" shouldNotPayToEffect
+    pguardC "Transaction should not pay to effects" shouldNotPayToEffect
-    tcassert "Transaction output does not match receivers" outputContentMatchesRecivers
+    pguardC "Transaction output does not match receivers" outputContentMatchesRecivers
-    tcassert "Remainders should be returned to the treasury" excessShouldBePaidToInputs
+    pguardC "Remainders should be returned to the treasury" excessShouldBePaidToInputs
-    tcassert "Transaction should only have treasuries specified in the datum as input" inputsAreOnlyTreasuriesOrCollateral
+    pguardC "Transaction should only have treasuries specified in the datum as input" inputsAreOnlyTreasuriesOrCollateral
    pure . popaque $ pconstant ()
--- a/agora/Agora/Governor.hs
+++ b/agora/Agora/Governor.hs
@ -26,6 +26,7 @@ module Agora.Governor (
 --------------------------------------------------------------------------------
 import Control.Applicative (Const)
 import Data.Tagged (Tagged (..))
 import GHC.Generics qualified as GHC
 import Generics.SOP (Generic, I (I))
@ -44,18 +45,16 @@ import Agora.Proposal.Time (
  ProposalTimingConfig,
 )
 import Agora.SafeMoney (GTTag)
 import Agora.Utils (tclet)
 --------------------------------------------------------------------------------
 import Data.Tagged (Tagged (..))
 import Plutarch.DataRepr (
  DerivePConstantViaData (..),
  PDataFields,
  PIsDataReprInstances (PIsDataReprInstances),
 )
 import Plutarch.Extra.Comonad (pextract)
-import Plutarch.Extra.TermCont (pmatchC)
+import Plutarch.Extra.TermCont (pletC, pmatchC)
 import Plutarch.Lift (PConstantDecl, PUnsafeLiftDecl (..))
 import Plutarch.SafeMoney (PDiscrete (..))
 import Plutarch.TryFrom (PTryFrom (..))
@ -196,9 +195,9 @@ governorDatumValid = phoistAcyclic $
    PDiscrete draft' <- pmatchC thresholds.create
    PDiscrete vote' <- pmatchC thresholds.vote
-    execute <- tclet $ pextract # execute'
+    execute <- pletC $ pextract # execute'
-    draft <- tclet $ pextract # draft'
+    draft <- pletC $ pextract # draft'
-    vote <- tclet $ pextract # vote'
+    vote <- pletC $ pextract # vote'
    pure $
      foldr1
--- a/agora/Agora/Governor/Scripts.hs
+++ b/agora/Agora/Governor/Scripts.hs
@ -77,17 +77,7 @@ import Agora.Utils (
  mustBePDJust,
  mustBePJust,
  mustFindDatum',
  pfindTxInByTxOutRef,
  pisDJust,
  pisUTXOSpent,
  psymbolValueOf,
  ptryFindDatum,
  ptxSignedBy,
  pvalueSpent,
  scriptHashFromAddress,
  tcassert,
  tclet,
  tcmatch,
  validatorHashToAddress,
  validatorHashToTokenName,
 )
@ -125,6 +115,10 @@ import Plutarch.TryFrom ()
 --------------------------------------------------------------------------------
 import Plutarch.Api.V1.ScriptContext (pfindTxInByTxOutRef, pisUTXOSpent, ptryFindDatum, ptxSignedBy, pvalueSpent)
 import "liqwid-plutarch-extra" Plutarch.Api.V1.Value (psymbolValueOf)
 import Plutarch.Extra.Maybe (pisDJust)
 import Plutarch.Extra.TermCont
 import PlutusLedgerApi.V1 (
  CurrencySymbol (..),
  MintingPolicy,
@ -166,21 +160,21 @@ governorPolicy gov =
  plam $ \_ ctx' -> unTermCont $ do
    let oref = pconstant gov.gstOutRef
-    PMinting ((pfield @"_0" #) -> ownSymbol) <- tcmatch (pfromData $ pfield @"purpose" # ctx')
+    PMinting ((pfield @"_0" #) -> ownSymbol) <- pmatchC (pfromData $ pfield @"purpose" # ctx')
    let ownAssetClass = passetClass # ownSymbol # pconstant ""
        txInfo = pfromData $ pfield @"txInfo" # ctx'
    txInfoF <- tcont $ pletFields @'["mint", "inputs", "outputs", "datums", "validRange"] txInfo
-    tcassert "Referenced utxo should be spent" $
+    pguardC "Referenced utxo should be spent" $
      pisUTXOSpent # oref # txInfoF.inputs
-    tcassert "Exactly one token should be minted" $
+    pguardC "Exactly one token should be minted" $
      psymbolValueOf # ownSymbol # txInfoF.mint #== 1
        #&& passetClassValueOf # txInfoF.mint # ownAssetClass #== 1
    govOutput <-
-      tclet $
+      pletC $
        mustBePJust
          # "Governor output not found"
            #$ pfind
@ -285,13 +279,13 @@ governorValidator gov =
    (pfromData -> redeemer, _) <- tcont $ ptryFrom redeemer'
    ctxF <- tcont $ pletFields @'["txInfo", "purpose"] ctx'
-    txInfo' <- tclet $ pfromData $ ctxF.txInfo
+    txInfo' <- pletC $ pfromData $ ctxF.txInfo
    txInfoF <- tcont $ pletFields @'["mint", "inputs", "outputs", "datums", "signatories", "validRange"] txInfo'
-    PSpending (pfromData . (pfield @"_0" #) -> ownInputRef) <- tcmatch $ pfromData ctxF.purpose
+    PSpending (pfromData . (pfield @"_0" #) -> ownInputRef) <- pmatchC $ pfromData ctxF.purpose
    ((pfield @"resolved" #) -> ownInput) <-
-      tclet $
+      pletC $
        mustBePJust # "Own input not found"
          #$ pfindTxInByTxOutRef # ownInputRef # txInfoF.inputs
    ownInputF <- tcont $ pletFields @'["address", "value"] ownInput
@ -310,27 +304,27 @@ governorValidator gov =
    -- Check that GST will be returned to the governor.
    let ownInputGSTAmount = psymbolValueOf # pgstSymbol # ownInputF.value
-    tcassert "Own input should have exactly one state token" $
+    pguardC "Own input should have exactly one state token" $
      ownInputGSTAmount #== 1
-    ownOutputs <- tclet $ findOutputsToAddress # txInfoF.outputs # ownAddress
+    ownOutputs <- pletC $ findOutputsToAddress # txInfoF.outputs # ownAddress
-    tcassert "Exactly one utxo should be sent to the governor" $
+    pguardC "Exactly one utxo should be sent to the governor" $
      plength # ownOutputs #== 1
    ownOutput <- tcont $ pletFields @'["value", "datumHash"] $ phead # ownOutputs
    let ownOuputGSTAmount = psymbolValueOf # pgstSymbol # ownOutput.value
-    tcassert "State token should stay at governor's address" $
+    pguardC "State token should stay at governor's address" $
      ownOuputGSTAmount #== 1
    -- Check that own output have datum of type 'GovernorDatum'.
    let outputGovernorStateDatumHash =
          mustBePDJust # "Governor output doesn't have datum" # ownOutput.datumHash
    newGovernorDatum <-
-      tclet $
+      pletC $
        pfromData $
          mustBePJust # "Ouput governor state datum not found"
            #$ ptryFindDatum # outputGovernorStateDatumHash # txInfoF.datums
-    tcassert "New datum is not valid" $ governorDatumValid # newGovernorDatum
+    pguardC "New datum is not valid" $ governorDatumValid # newGovernorDatum
    pure $
      pmatch redeemer $ \case
@ -347,19 +341,19 @@ governorValidator gov =
                      .& #createProposalTimeRangeMaxWidth
                        .= oldGovernorDatumF.createProposalTimeRangeMaxWidth
                  )
-          tcassert "Unexpected governor state datum" $
+          pguardC "Unexpected governor state datum" $
            newGovernorDatum #== expectedNewDatum
          -- Check that exactly one proposal token is being minted.
-          tcassert "Exactly one proposal token must be minted" $
+          pguardC "Exactly one proposal token must be minted" $
            hasOnlyOneTokenOfCurrencySymbol # ppstSymbol # txInfoF.mint
          -- Check that a stake is spent to create the propsal,
          --   and the value it contains meets the requirement.
          stakeInput <-
-            tclet $
+            pletC $
              mustBePJust # "Stake input not found" #$ pfind
                # phoistAcyclic
                  ( plam $
@ -374,7 +368,7 @@ governorValidator gov =
          stakeInputF <- tcont $ pletFields @'["datumHash", "value"] $ pfield @"resolved" # stakeInput
-          tcassert "Stake input doesn't have datum" $
+          pguardC "Stake input doesn't have datum" $
            pisDJust # stakeInputF.datumHash
          let stakeInputDatum = mustFindDatum' @PStakeDatum # stakeInputF.datumHash # txInfoF.datums
@ -382,18 +376,18 @@ governorValidator gov =
          stakeInputDatumF <-
            tcont $ pletFields @["stakedAmount", "owner", "lockedBy"] stakeInputDatum
-          tcassert "Required amount of stake GTs should be presented" $
+          pguardC "Required amount of stake GTs should be presented" $
            stakeInputDatumF.stakedAmount #== (pgtValueOf # stakeInputF.value)
          -- TODO: Is this required?
-          tcassert "Tx should be signed by the stake owner" $
+          pguardC "Tx should be signed by the stake owner" $
            ptxSignedBy # txInfoF.signatories # stakeInputDatumF.owner
          -- Check that the newly minted PST is sent to the proposal validator,
          --   and the datum it carries is legal.
          outputsToProposalValidatorWithStateToken <-
-            tclet $
+            pletC $
              pfilter
                # phoistAcyclic
                  ( plam $
@ -406,18 +400,18 @@ governorValidator gov =
                  )
                # pfromData txInfoF.outputs
-          tcassert "Exactly one UTXO with proposal state token should be sent to the proposal validator" $
+          pguardC "Exactly one UTXO with proposal state token should be sent to the proposal validator" $
            plength # outputsToProposalValidatorWithStateToken #== 1
-          outputDatumHash <- tclet $ pfield @"datumHash" #$ phead # outputsToProposalValidatorWithStateToken
+          outputDatumHash <- pletC $ pfield @"datumHash" #$ phead # outputsToProposalValidatorWithStateToken
          proposalOutputDatum' <-
-            tclet $
+            pletC $
              mustFindDatum' @PProposalDatum
                # outputDatumHash
                # txInfoF.datums
-          tcassert "Proposal datum must be valid" $
+          pguardC "Proposal datum must be valid" $
            proposalDatumValid' # proposalOutputDatum'
          proposalOutputDatum <-
@ -426,7 +420,7 @@ governorValidator gov =
                @'["effects", "cosigners", "proposalId", "votes"]
                proposalOutputDatum'
-          tcassert "Proposal should have only one cosigner" $
+          pguardC "Proposal should have only one cosigner" $
            plength # pfromData proposalOutputDatum.cosigners #== 1
          let -- Votes should be empty at this point
@ -449,17 +443,17 @@ governorValidator gov =
                      .& #startingTime .= pdata expectedStartingTime
                  )
-          tcassert "Datum correct" $ expectedProposalOut #== proposalOutputDatum'
+          pguardC "Datum correct" $ expectedProposalOut #== proposalOutputDatum'
          let cosigner = phead # pfromData proposalOutputDatum.cosigners
-          tcassert "Cosigner should be the stake owner" $
+          pguardC "Cosigner should be the stake owner" $
            pdata stakeInputDatumF.owner #== cosigner
          -- Check the output stake has been proposly updated.
          stakeOutput <-
-            tclet $
+            pletC $
              mustBePJust
                # "Stake output not found"
                  #$ pfind
@ -476,7 +470,7 @@ governorValidator gov =
          stakeOutputF <- tcont $ pletFields @'["datumHash", "value"] $ stakeOutput
-          tcassert "Staked GTs should be sent back to stake validator" $
+          pguardC "Staked GTs should be sent back to stake validator" $
            stakeInputDatumF.stakedAmount #== (pgtValueOf # stakeOutputF.value)
          let stakeOutputDatumHash = mustBePDJust # "Stake output should have datum" # stakeOutputF.datumHash
@ -514,18 +508,18 @@ governorValidator gov =
                        .& #lockedBy .= pdata expectedProposalLocks
                    )
-          tcassert "Unexpected stake output datum" $ expectedStakeOutputDatum #== stakeOutputDatum
+          pguardC "Unexpected stake output datum" $ expectedStakeOutputDatum #== stakeOutputDatum
          pure $ popaque $ pconstant ()
        --------------------------------------------------------------------------
        PMintGATs _ -> unTermCont $ do
-          tcassert "Governor state should not be changed" $ newGovernorDatum #== oldGovernorDatum
+          pguardC "Governor state should not be changed" $ newGovernorDatum #== oldGovernorDatum
          -- Filter out proposal inputs and ouputs using PST and the address of proposal validator.
-          tcassert "The governor can only process one proposal at a time" $
+          pguardC "The governor can only process one proposal at a time" $
            (psymbolValueOf # ppstSymbol #$ pvalueSpent # txInfoF.inputs) #== 1
          proposalInputF <-
@ -561,17 +555,17 @@ governorValidator gov =
                    # pfromData txInfoF.outputs
          proposalInputDatum <-
-            tclet $
+            pletC $
              mustFindDatum' @PProposalDatum
                # proposalInputF.datumHash
                # txInfoF.datums
          proposalOutputDatum <-
-            tclet $
+            pletC $
              mustFindDatum' @PProposalDatum
                # proposalOutputF.datumHash
                # txInfoF.datums
-          tcassert "Proposal datum must be valid" $
+          pguardC "Proposal datum must be valid" $
            proposalDatumValid' # proposalInputDatum
              #&& proposalDatumValid' # proposalOutputDatum
@ -582,7 +576,7 @@ governorValidator gov =
          -- Check that the proposal state is advanced so that a proposal cannot be executed twice.
-          tcassert "Proposal must be in locked(executable) state in order to execute effects" $
+          pguardC "Proposal must be in locked(executable) state in order to execute effects" $
            proposalInputDatumF.status #== pconstantData Locked
          let expectedOutputProposalDatum =
@ -598,7 +592,7 @@ governorValidator gov =
                      .& #startingTime .= proposalInputDatumF.startingTime
                  )
-          tcassert "Unexpected output proposal datum" $
+          pguardC "Unexpected output proposal datum" $
            pdata proposalOutputDatum #== pdata expectedOutputProposalDatum
          -- TODO: anything else to check here?
@ -609,16 +603,16 @@ governorValidator gov =
              finalResultTag = pwinner # proposalInputDatumF.votes # quorum # neutralOption
          -- The effects of the winner outcome.
-          effectGroup <- tclet $ plookup' # finalResultTag #$ proposalInputDatumF.effects
+          effectGroup <- pletC $ plookup' # finalResultTag #$ proposalInputDatumF.effects
-          gatCount <- tclet $ plength #$ pto $ pto effectGroup
+          gatCount <- pletC $ plength #$ pto $ pto effectGroup
-          tcassert "Required amount of GATs should be minted" $
+          pguardC "Required amount of GATs should be minted" $
            psymbolValueOf # patSymbol # txInfoF.mint #== gatCount
          -- Ensure that every GAT goes to one of the effects in the winner effect group.
          outputsWithGAT <-
-            tclet $
+            pletC $
              pfilter
                # phoistAcyclic
                  ( plam
@ -628,7 +622,7 @@ governorValidator gov =
                  )
                # pfromData txInfoF.outputs
-          tcassert "Output GATs is more than minted GATs" $
+          pguardC "Output GATs is more than minted GATs" $
            plength # outputsWithGAT #== gatCount
          let gatOutputValidator' :: Term s (PMap _ PValidatorHash PDatumHash :--> PAsData PTxOut :--> PBool)
--- a/agora/Agora/Proposal.hs
+++ b/agora/Agora/Proposal.hs
@ -35,8 +35,23 @@ module Agora.Proposal (
  pneutralOption,
 ) where
 --------------------------------------------------------------------------------
 import Control.Applicative (Const)
 import Control.Arrow (first)
 import Data.Tagged (Tagged)
 import GHC.Generics qualified as GHC
 import Generics.SOP (Generic, I (I))
 --------------------------------------------------------------------------------
 import PlutusLedgerApi.V1 (DatumHash, PubKeyHash, ValidatorHash)
 import PlutusLedgerApi.V1.Value (AssetClass)
 import PlutusTx qualified
 import PlutusTx.AssocMap qualified as AssocMap
 --------------------------------------------------------------------------------
 import Plutarch.Api.V1 (
  KeyGuarantees (Unsorted),
  PDatumHash,
@ -44,18 +59,11 @@ import Plutarch.Api.V1 (
  PPubKeyHash,
  PValidatorHash,
 )
 import PlutusTx qualified
 import PlutusTx.AssocMap qualified as AssocMap
 --------------------------------------------------------------------------------
 import Agora.Proposal.Time (PProposalStartingTime, PProposalTimingConfig, ProposalStartingTime, ProposalTimingConfig)
 import Agora.SafeMoney (GTTag)
 import Agora.Utils (mustBePJust, pkeysEqual, pmapMap, pnotNull, tclet)
 import Control.Applicative (Const)
 import Control.Arrow (first)
 import Data.Tagged (Tagged)
 import Plutarch.DataRepr (DerivePConstantViaData (..), PDataFields, PIsDataReprInstances (..))
 import Plutarch.Extra.List (pnotNull)
 import Plutarch.Extra.Map qualified as PM
 import Plutarch.Extra.Map.Unsorted qualified as PUM
 import Plutarch.Extra.TermCont (pletC)
 import Plutarch.Lift (
  DerivePConstantViaNewtype (..),
  PConstantDecl,
@ -64,8 +72,12 @@ import Plutarch.Lift (
 import Plutarch.SafeMoney (PDiscrete)
 import Plutarch.TryFrom (PTryFrom (PTryFromExcess, ptryFrom'))
 import Plutarch.Unsafe (punsafeCoerce)
-import PlutusLedgerApi.V1 (DatumHash, PubKeyHash, ValidatorHash)
+
-import PlutusLedgerApi.V1.Value (AssetClass)
+--------------------------------------------------------------------------------
 import Agora.Proposal.Time (PProposalStartingTime, PProposalTimingConfig, ProposalStartingTime, ProposalTimingConfig)
 import Agora.SafeMoney (GTTag)
 import Agora.Utils (mustBePJust)
 --------------------------------------------------------------------------------
 -- Haskell-land
@ -278,6 +290,10 @@ instance PTryFrom PData (PAsData PResultTag) where
  type PTryFromExcess PData (PAsData PResultTag) = PTryFromExcess PData (PAsData PInteger)
  ptryFrom' d k =
    ptryFrom' @_ @(PAsData PInteger) d $
      -- JUSTIFICATION:
      -- We are coercing from @PAsData PInteger@ to @PAsData PResultTag@.
      -- Since 'PResultTag' is a simple newtype, their shape is the same.
      -- JUSTIFICATION:
      -- We are coercing from @PAsData PInteger@ to @PAsData PResultTag@.
      -- Since 'PResultTag' is a simple newtype, their shape is the same.
@ -291,6 +307,10 @@ instance PTryFrom PData (PAsData PProposalId) where
  type PTryFromExcess PData (PAsData PProposalId) = PTryFromExcess PData (PAsData PInteger)
  ptryFrom' d k =
    ptryFrom' @_ @(PAsData PInteger) d $
      -- JUSTIFICATION:
      -- We are coercing from @PAsData PInteger@ to @PAsData PProposalId@.
      -- Since 'PProposalId' is a simple newtype, their shape is the same.
      -- JUSTIFICATION:
      -- We are coercing from @PAsData PInteger@ to @PAsData PProposalId@.
      -- Since 'PProposalId' is a simple newtype, their shape is the same.
@ -360,7 +380,7 @@ pemptyVotesFor =
    plam
      ( \m ->
          pcon $
-            PProposalVotes $ pmapMap # plam (const $ pconstant 0) # m
+            PProposalVotes $ PM.pmap # plam (const $ pconstant 0) # m
      )
 -- | Plutarch-level version of 'ProposalDatum'.
@ -448,8 +468,8 @@ proposalDatumValid proposal =
          (#&&)
          [ ptraceIfFalse "Proposal has at least one ResultTag has no effects" atLeastOneNegativeResult
          , ptraceIfFalse "Proposal has at least one cosigner" $ pnotNull # pfromData datum.cosigners
-          , ptraceIfFalse "Proposal has fewer cosigners than the limit" $ plength # (pfromData datum.cosigners) #<= pconstant proposal.maximumCosigners
+          , ptraceIfFalse "Proposal has fewer cosigners than the limit" $ plength # pfromData datum.cosigners #<= pconstant proposal.maximumCosigners
-          , ptraceIfFalse "Proposal votes and effects are compatible with each other" $ pkeysEqual # datum.effects # pto (pfromData datum.votes)
+          , ptraceIfFalse "Proposal votes and effects are compatible with each other" $ PUM.pkeysEqual # datum.effects # pto (pfromData datum.votes)
          ]
 {- | Find the winner result tag, given the votes, the quorum the "neutral" result tag.
@ -467,9 +487,9 @@ pwinner ::
    )
 pwinner = phoistAcyclic $
  plam $ \votes quorum neutral -> unTermCont $ do
-    winner <- tclet $ phighestVotes # votes
+    winner <- pletC $ phighestVotes # votes
-    winnerResultTag <- tclet $ pfromData $ pfstBuiltin # winner
+    winnerResultTag <- pletC $ pfromData $ pfstBuiltin # winner
-    highestVotes <- tclet $ pfromData $ psndBuiltin # winner
+    highestVotes <- pletC $ pfromData $ psndBuiltin # winner
    let l :: Term _ (PBuiltinList _)
        l = pto $ pto votes
--- a/agora/Agora/Proposal/Scripts.hs
+++ b/agora/Agora/Proposal/Scripts.hs
@ -31,17 +31,6 @@ import Agora.Utils (
  getMintingPolicySymbol,
  mustBePJust,
  mustFindDatum',
  pisJust,
  pisUniqBy,
  psymbolValueOf,
  ptokenSpent,
  ptxSignedBy,
  pupdate,
  pvalueSpent,
  tcassert,
  tclet,
  tcmatch,
  tctryFrom,
 )
 import Plutarch.Api.V1 (
  PMintingPolicy,
@ -51,10 +40,23 @@ import Plutarch.Api.V1 (
  PValidator,
 )
 import Plutarch.Api.V1.AssetClass (passetClass, passetClassValueOf)
 import Plutarch.Api.V1.ScriptContext (
  pisTokenSpent,
  ptxSignedBy,
  pvalueSpent,
 )
 import "liqwid-plutarch-extra" Plutarch.Api.V1.Value (psymbolValueOf)
 import Plutarch.Extra.Comonad (pextract)
-import Plutarch.Extra.Map (plookup)
+import Plutarch.Extra.List (pisUniqBy)
 import Plutarch.Extra.Map (plookup, pupdate)
 import Plutarch.Extra.Maybe (pisJust)
 import Plutarch.Extra.Record (mkRecordConstr, (.&), (.=))
-import Plutarch.Extra.TermCont (pmatchC)
+import Plutarch.Extra.TermCont (
  pguardC,
  pletC,
  pmatchC,
  ptryFromC,
 )
 import Plutarch.SafeMoney (PDiscrete (..))
 import PlutusLedgerApi.V1.Value (AssetClass (AssetClass))
@ -82,27 +84,27 @@ proposalPolicy ::
  ClosedTerm PMintingPolicy
 proposalPolicy (AssetClass (govCs, govTn)) =
  plam $ \_redeemer ctx' -> unTermCont $ do
-    PScriptContext ctx' <- tcmatch ctx'
+    PScriptContext ctx' <- pmatchC ctx'
    ctx <- tcont $ pletFields @'["txInfo", "purpose"] ctx'
-    PTxInfo txInfo' <- tcmatch $ pfromData ctx.txInfo
+    PTxInfo txInfo' <- pmatchC $ pfromData ctx.txInfo
    txInfo <- tcont $ pletFields @'["inputs", "mint"] txInfo'
-    PMinting _ownSymbol <- tcmatch $ pfromData ctx.purpose
+    PMinting _ownSymbol <- pmatchC $ pfromData ctx.purpose
    let inputs = txInfo.inputs
        mintedValue = pfromData txInfo.mint
-    PMinting ownSymbol' <- tcmatch $ pfromData ctx.purpose
+    PMinting ownSymbol' <- pmatchC $ pfromData ctx.purpose
    let mintedProposalST =
          passetClassValueOf
            # mintedValue
            # (passetClass # (pfield @"_0" # ownSymbol') # pconstant "")
-    tcassert "Governance state-thread token must move" $
+    pguardC "Governance state-thread token must move" $
-      ptokenSpent
+      pisTokenSpent
        # (passetClass # pconstant govCs # pconstant govTn)
        # inputs
-    tcassert "Minted exactly one proposal ST" $
+    pguardC "Minted exactly one proposal ST" $
      mintedProposalST #== 1
    pure $ popaque (pconstant ())
@ -136,10 +138,10 @@ A list of all time-sensitive redeemers and their requirements:
 proposalValidator :: Proposal -> ClosedTerm PValidator
 proposalValidator proposal =
  plam $ \datum redeemer ctx' -> unTermCont $ do
-    PScriptContext ctx' <- tcmatch ctx'
+    PScriptContext ctx' <- pmatchC ctx'
    ctx <- tcont $ pletFields @'["txInfo", "purpose"] ctx'
-    txInfo <- tclet $ pfromData ctx.txInfo
+    txInfo <- pletC $ pfromData ctx.txInfo
-    PTxInfo txInfo' <- tcmatch txInfo
+    PTxInfo txInfo' <- pmatchC txInfo
    txInfoF <-
      tcont $
        pletFields
@ -151,15 +153,15 @@ proposalValidator proposal =
            , "validRange"
            ]
          txInfo'
-    PSpending ((pfield @"_0" #) -> txOutRef) <- tcmatch $ pfromData ctx.purpose
+    PSpending ((pfield @"_0" #) -> txOutRef) <- pmatchC $ pfromData ctx.purpose
-    PJust txOut <- tcmatch $ findTxOutByTxOutRef # txOutRef # txInfoF.inputs
+    PJust txOut <- pmatchC $ findTxOutByTxOutRef # txOutRef # txInfoF.inputs
    txOutF <- tcont $ pletFields @'["address", "value"] $ txOut
    (pfromData -> proposalDatum, _) <-
-      tctryFrom @(PAsData PProposalDatum) datum
+      ptryFromC @(PAsData PProposalDatum) datum
    (pfromData -> proposalRedeemer, _) <-
-      tctryFrom @(PAsData PProposalRedeemer) redeemer
+      ptryFromC @(PAsData PProposalRedeemer) redeemer
    proposalF <-
      tcont $
@ -175,29 +177,29 @@ proposalValidator proposal =
            ]
          proposalDatum
-    ownAddress <- tclet $ txOutF.address
+    ownAddress <- pletC $ txOutF.address
    let stCurrencySymbol =
          pconstant $ getMintingPolicySymbol (proposalPolicy proposal.governorSTAssetClass)
-    valueSpent <- tclet $ pvalueSpent # txInfoF.inputs
+    valueSpent <- pletC $ pvalueSpent # txInfoF.inputs
-    spentST <- tclet $ psymbolValueOf # stCurrencySymbol #$ valueSpent
+    spentST <- pletC $ psymbolValueOf # stCurrencySymbol #$ valueSpent
    let AssetClass (stakeSym, stakeTn) = proposal.stakeSTAssetClass
    stakeSTAssetClass <-
-      tclet $ passetClass # pconstant stakeSym # pconstant stakeTn
+      pletC $ passetClass # pconstant stakeSym # pconstant stakeTn
    spentStakeST <-
-      tclet $ passetClassValueOf # valueSpent # stakeSTAssetClass
+      pletC $ passetClassValueOf # valueSpent # stakeSTAssetClass
-    signedBy <- tclet $ ptxSignedBy # txInfoF.signatories
+    signedBy <- pletC $ ptxSignedBy # txInfoF.signatories
-    tcassert "ST at inputs must be 1" (spentST #== 1)
+    pguardC "ST at inputs must be 1" (spentST #== 1)
-    currentTime <- tclet $ currentProposalTime # txInfoF.validRange
+    currentTime <- pletC $ currentProposalTime # txInfoF.validRange
    -- Filter out own output with own address and PST.
    -- Delay the evaluation cause in some cases there won't be any continuing output.
    ownOutput <-
-      tclet $
+      pletC $
        mustBePJust # "Own output should be present" #$ pfind
          # plam
            ( \input -> unTermCont $ do
@ -209,7 +211,7 @@ proposalValidator proposal =
          # pfromData txInfoF.outputs
    proposalOut <-
-      tclet $
+      pletC $
        mustFindDatum' @PProposalDatum
          # (pfield @"datumHash" # ownOutput)
          # txInfoF.datums
@ -217,17 +219,17 @@ proposalValidator proposal =
    pure $
      pmatch proposalRedeemer $ \case
        PVote r -> unTermCont $ do
-          tcassert "Input proposal must be in VotingReady state" $
+          pguardC "Input proposal must be in VotingReady state" $
            proposalF.status #== pconstant VotingReady
-          tcassert "Proposal time should be wthin the voting period" $
+          pguardC "Proposal time should be wthin the voting period" $
            isVotingPeriod # proposalF.timingConfig # proposalF.startingTime # currentTime
          -- Ensure the transaction is voting to a valid 'ResultTag'(outcome).
-          PProposalVotes voteMap <- tcmatch proposalF.votes
+          PProposalVotes voteMap <- pmatchC proposalF.votes
-          voteFor <- tclet $ pfromData $ pfield @"resultTag" # r
+          voteFor <- pletC $ pfromData $ pfield @"resultTag" # r
-          tcassert "Vote option should be valid" $
+          pguardC "Vote option should be valid" $
            pisJust #$ plookup # voteFor # voteMap
          -- Find the input stake, the amount of new votes should be the 'stakedAmount'.
@ -248,7 +250,7 @@ proposalValidator proposal =
          stakeInF <- tcont $ pletFields @'["stakedAmount", "lockedBy", "owner"] stakeIn
          -- Ensure that no lock with the current proposal id has been put on the stake.
-          tcassert "Same stake shouldn't vote on the same propsoal twice" $
+          pguardC "Same stake shouldn't vote on the same propsoal twice" $
            pnot #$ pany
              # plam
                ( \((pfield @"proposalTag" #) . pfromData -> pid) ->
@ -281,7 +283,7 @@ proposalValidator proposal =
                      .& #startingTime .= proposalF.startingTime
                  )
-          tcassert "Output proposal should be valid" $ proposalOut #== expectedProposalOut
+          pguardC "Output proposal should be valid" $ proposalOut #== expectedProposalOut
          -- We validate the output stake datum here as well: We need the vote option
          -- to create a valid 'ProposalLock', however the vote option is encoded
@ -318,26 +320,26 @@ proposalValidator proposal =
                      .& #lockedBy .= pdata expectedProposalLocks
                  )
-          tcassert "Output stake should be locked by the proposal" $ expectedStakeOut #== stakeOut
+          pguardC "Output stake should be locked by the proposal" $ expectedStakeOut #== stakeOut
          pure $ popaque (pconstant ())
        --------------------------------------------------------------------------
        PCosign r -> unTermCont $ do
-          newSigs <- tclet $ pfield @"newCosigners" # r
+          newSigs <- pletC $ pfield @"newCosigners" # r
-          tcassert "Cosigners are unique" $
+          pguardC "Cosigners are unique" $
            pisUniqBy
              # phoistAcyclic (plam (#==))
              # phoistAcyclic (plam $ \(pfromData -> x) (pfromData -> y) -> x #< y)
              # newSigs
-          tcassert "Signed by all new cosigners" $
+          pguardC "Signed by all new cosigners" $
            pall # signedBy # newSigs
-          tcassert "As many new cosigners as Stake datums" $
+          pguardC "As many new cosigners as Stake datums" $
            spentStakeST #== plength # newSigs
-          tcassert "All new cosigners are witnessed by their Stake datums" $
+          pguardC "All new cosigners are witnessed by their Stake datums" $
            pall
              # plam
                ( \sig ->
@ -367,7 +369,7 @@ proposalValidator proposal =
                      .& #startingTime .= proposalF.startingTime
                  )
-          tcassert "Signatures are correctly added to cosignature list" $
+          pguardC "Signatures are correctly added to cosignature list" $
            proposalOut #== expectedDatum
          pure $ popaque (pconstant ())
@ -376,10 +378,10 @@ proposalValidator proposal =
          popaque (pconstant ())
        --------------------------------------------------------------------------
        PAdvanceProposal _r -> unTermCont $ do
-          tcassert "No stake input is allowed" $ spentStakeST #== 0
+          pguardC "No stake input is allowed" $ spentStakeST #== 0
-          currentTime <- tclet $ currentProposalTime # txInfoF.validRange
+          currentTime <- pletC $ currentProposalTime # txInfoF.validRange
-          proposalOutStatus <- tclet $ pfield @"status" # proposalOut
+          proposalOutStatus <- pletC $ pfield @"status" # proposalOut
          let -- Only the status of proposals should be updated in this case.
              templateProposalOut =
@ -395,13 +397,13 @@ proposalValidator proposal =
                      .& #startingTime .= proposalF.startingTime
                  )
-          tcassert "Only status changes in the output proposal" $
+          pguardC "Only status changes in the output proposal" $
            templateProposalOut #== proposalOut
-          inDraftPeriod <- tclet $ isDraftPeriod # proposalF.timingConfig # proposalF.startingTime # currentTime
+          inDraftPeriod <- pletC $ isDraftPeriod # proposalF.timingConfig # proposalF.startingTime # currentTime
-          inVotingPeriod <- tclet $ isVotingPeriod # proposalF.timingConfig # proposalF.startingTime # currentTime
+          inVotingPeriod <- pletC $ isVotingPeriod # proposalF.timingConfig # proposalF.startingTime # currentTime
-          inLockedPeriod <- tclet $ isLockingPeriod # proposalF.timingConfig # proposalF.startingTime # currentTime
+          inLockedPeriod <- pletC $ isLockingPeriod # proposalF.timingConfig # proposalF.startingTime # currentTime
-          inExecutionPeriod <- tclet $ isExecutionPeriod # proposalF.timingConfig # proposalF.startingTime # currentTime
+          inExecutionPeriod <- pletC $ isExecutionPeriod # proposalF.timingConfig # proposalF.startingTime # currentTime
          -- Check the timings.
          let isFinished = proposalF.status #== pconstantData Finished
@ -418,8 +420,8 @@ proposalValidator proposal =
                PLocked _ -> pnot # inLockedPeriod
                _ -> pconstant True
-          tcassert "Cannot advance ahead of time" notTooEarly
+          pguardC "Cannot advance ahead of time" notTooEarly
-          tcassert "Finished proposals cannot be advanced" $ pnot # isFinished
+          pguardC "Finished proposals cannot be advanced" $ pnot # isFinished
          pure $
            pif
@ -430,19 +432,19 @@ proposalValidator proposal =
                    -- TODO: Perform other necessary checks.
                    -- 'Draft' -> 'VotingReady'
-                    tcassert "Proposal status set to VotingReady" $
+                    pguardC "Proposal status set to VotingReady" $
                      proposalOutStatus #== pconstantData VotingReady
                    pure $ popaque (pconstant ())
                  PVotingReady _ -> unTermCont $ do
                    -- 'VotingReady' -> 'Locked'
-                    tcassert "Proposal status set to Locked" $
+                    pguardC "Proposal status set to Locked" $
                      proposalOutStatus #== pconstantData Locked
                    pure $ popaque (pconstant ())
                  PLocked _ -> unTermCont $ do
                    -- 'Locked' -> 'Finished'
-                    tcassert "Proposal status set to Finished" $
+                    pguardC "Proposal status set to Finished" $
                      proposalOutStatus #== pconstantData Finished
                    -- TODO: Perform other necessary checks.
--- a/agora/Agora/Proposal/Time.hs
+++ b/agora/Agora/Proposal/Time.hs
@ -29,7 +29,6 @@ module Agora.Proposal.Time (
  isExecutionPeriod,
 ) where
 import Agora.Utils (tcassert, tcmatch)
 import GHC.Generics qualified as GHC
 import Generics.SOP (Generic, HasDatatypeInfo, I (I))
 import Plutarch.Api.V1 (
@ -45,6 +44,7 @@ import Plutarch.DataRepr (
  PDataFields,
  PIsDataReprInstances (..),
 )
 import Plutarch.Extra.TermCont (pguardC, pmatchC)
 import Plutarch.Lift (
  DerivePConstantViaNewtype (..),
  PConstantDecl,
@ -184,7 +184,7 @@ instance AdditiveSemigroup (Term s PPOSIXTime) where
 createProposalStartingTime :: forall (s :: S). Term s (PMaxTimeRangeWidth :--> PPOSIXTimeRange :--> PProposalStartingTime)
 createProposalStartingTime = phoistAcyclic $
  plam $ \(pto -> maxDuration) iv -> unTermCont $ do
-    currentTimeF <- tcmatch $ currentProposalTime # iv
+    currentTimeF <- pmatchC $ currentProposalTime # iv
    -- Use the middle of the current time range as the starting time.
    let duration = currentTimeF.upperBound - currentTimeF.lowerBound
@ -194,7 +194,7 @@ createProposalStartingTime = phoistAcyclic $
            # (currentTimeF.lowerBound + currentTimeF.upperBound)
            # 2
-    tcassert "createProposalStartingTime: given time range should be tight enough" $
+    pguardC "createProposalStartingTime: given time range should be tight enough" $
      duration #<= maxDuration
    pure $ pcon $ PProposalStartingTime startingTime
@ -207,10 +207,10 @@ createProposalStartingTime = phoistAcyclic $
 currentProposalTime :: forall (s :: S). Term s (PPOSIXTimeRange :--> PProposalTime)
 currentProposalTime = phoistAcyclic $
  plam $ \iv -> unTermCont $ do
-    PInterval iv' <- tcmatch iv
+    PInterval iv' <- pmatchC iv
    ivf <- tcont $ pletFields @'["from", "to"] iv'
-    PLowerBound lb <- tcmatch ivf.from
+    PLowerBound lb <- pmatchC ivf.from
-    PUpperBound ub <- tcmatch ivf.to
+    PUpperBound ub <- pmatchC ivf.to
    lbf <- tcont $ pletFields @'["_0", "_1"] lb
    ubf <- tcont $ pletFields @'["_0", "_1"] ub
    pure $
@ -243,7 +243,7 @@ proposalTimeWithin ::
    )
 proposalTimeWithin = phoistAcyclic $
  plam $ \l h proposalTime' -> unTermCont $ do
-    PProposalTime ut lt <- tcmatch proposalTime'
+    PProposalTime ut lt <- pmatchC proposalTime'
    pure $
      foldr1
        (#&&)
--- a/agora/Agora/Stake.hs
+++ b/agora/Agora/Stake.hs
@ -26,6 +26,8 @@ module Agora.Stake (
 --------------------------------------------------------------------------------
 import Control.Applicative (Const)
 import Data.Tagged (Tagged (..))
 import GHC.Generics qualified as GHC
 import Generics.SOP (Generic, I (I))
 import Prelude hiding (Num (..))
@ -33,6 +35,7 @@ import Prelude hiding (Num (..))
 --------------------------------------------------------------------------------
 import PlutusLedgerApi.V1 (PubKeyHash)
 import PlutusLedgerApi.V1.Value (AssetClass)
 import PlutusTx qualified
 --------------------------------------------------------------------------------
@ -46,30 +49,24 @@ import Plutarch.Api.V1 (
  PTxInInfo (PTxInInfo),
  PTxOut (PTxOut),
 )
 import Plutarch.Api.V1.AssetClass (PAssetClass, passetClassValueOf)
 import Plutarch.Api.V1.ScriptContext (ptryFindDatum)
 import Plutarch.DataRepr (
  DerivePConstantViaData (..),
  PDataFields,
  PIsDataReprInstances (PIsDataReprInstances),
 )
 import Plutarch.Extra.List (pnotNull)
 import Plutarch.Extra.TermCont (pletC, pmatchC)
 import Plutarch.Internal (punsafeCoerce)
 import Plutarch.Lift (PConstantDecl, PUnsafeLiftDecl (..))
-import PlutusLedgerApi.V1.Value (AssetClass)
+import Plutarch.SafeMoney (PDiscrete)
 import Plutarch.TryFrom (PTryFrom (PTryFromExcess, ptryFrom'))
 --------------------------------------------------------------------------------
 import Agora.Proposal (PProposalId, PResultTag, ProposalId (..), ResultTag (..))
 import Agora.SafeMoney (GTTag)
 import Agora.Utils (
  pnotNull,
  ptryFindDatum,
  tclet,
  tcmatch,
 )
 import Control.Applicative (Const)
 import Data.Tagged (Tagged (..))
 import Plutarch.Api.V1.AssetClass (PAssetClass, passetClassValueOf)
 import Plutarch.SafeMoney (PDiscrete)
 import Plutarch.TryFrom (PTryFrom (PTryFromExcess, ptryFrom'))
 --------------------------------------------------------------------------------
@ -300,10 +297,10 @@ isInputStakeOwnedBy ::
    )
 isInputStakeOwnedBy =
  plam $ \ac ss datums txInInfo' -> unTermCont $ do
-    PTxInInfo ((pfield @"resolved" #) -> txOut) <- tcmatch $ pfromData txInInfo'
+    PTxInInfo ((pfield @"resolved" #) -> txOut) <- pmatchC $ pfromData txInInfo'
-    PTxOut txOut' <- tcmatch txOut
+    PTxOut txOut' <- pmatchC txOut
    txOutF <- tcont $ pletFields @'["value", "datumHash"] txOut'
-    outStakeST <- tclet $ passetClassValueOf # txOutF.value # ac
+    outStakeST <- pletC $ passetClassValueOf # txOutF.value # ac
    pure $
      pmatch txOutF.datumHash $ \case
        PDNothing _ -> pcon PFalse
--- a/agora/Agora/Stake/Scripts.hs
+++ b/agora/Agora/Stake/Scripts.hs
@ -12,19 +12,7 @@ import Agora.Stake
 import Agora.Utils (
  mustBePJust,
  mustFindDatum',
  paddValue,
  pfindTxInByTxOutRef,
  pgeqByClass',
  pgeqBySymbol,
  psymbolValueOf,
  ptokenSpent,
  ptxSignedBy,
  pvalidatorHashToTokenName,
  pvalueSpent,
  tcassert,
  tclet,
  tcmatch,
  tctryFrom,
 )
 import Data.Tagged (Tagged (..), untag)
 import Plutarch.Api.V1 (
@ -40,7 +28,10 @@ import Plutarch.Api.V1 (
  mkMintingPolicy,
 )
 import Plutarch.Api.V1.AssetClass (passetClass, passetClassValueOf, pvalueOf)
 import Plutarch.Api.V1.ScriptContext (pfindTxInByTxOutRef, pisTokenSpent, ptxSignedBy, pvalueSpent)
 import "liqwid-plutarch-extra" Plutarch.Api.V1.Value (pgeqByClass', pgeqBySymbol, psymbolValueOf)
 import Plutarch.Extra.Record (mkRecordConstr, (.&), (.=))
 import Plutarch.Extra.TermCont (pguardC, pletC, pmatchC, ptryFromC)
 import Plutarch.Internal (punsafeCoerce)
 import Plutarch.Numeric.Additive (AdditiveMonoid (zero), AdditiveSemigroup ((+)))
 import Plutarch.SafeMoney (
@ -74,24 +65,24 @@ stakePolicy ::
 stakePolicy gtClassRef =
  plam $ \_redeemer ctx' -> unTermCont $ do
    ctx <- tcont $ pletFields @'["txInfo", "purpose"] ctx'
-    txInfo <- tclet $ ctx.txInfo
+    txInfo <- pletC $ ctx.txInfo
    let _a :: Term _ PTxInfo
        _a = txInfo
    txInfoF <- tcont $ pletFields @'["mint", "inputs", "outputs", "signatories", "datums"] txInfo
-    PMinting ownSymbol' <- tcmatch $ pfromData ctx.purpose
+    PMinting ownSymbol' <- pmatchC $ pfromData ctx.purpose
-    ownSymbol <- tclet $ pfield @"_0" # ownSymbol'
+    ownSymbol <- pletC $ pfield @"_0" # ownSymbol'
-    spentST <- tclet $ psymbolValueOf # ownSymbol #$ pvalueSpent # txInfoF.inputs
+    spentST <- pletC $ psymbolValueOf # ownSymbol #$ pvalueSpent # txInfoF.inputs
-    mintedST <- tclet $ psymbolValueOf # ownSymbol # txInfoF.mint
+    mintedST <- pletC $ psymbolValueOf # ownSymbol # txInfoF.mint
    let burning = unTermCont $ do
-          tcassert "ST at inputs must be 1" $
+          pguardC "ST at inputs must be 1" $
            spentST #== 1
-          tcassert "ST burned" $
+          pguardC "ST burned" $
            mintedST #== -1
-          tcassert "An unlocked input existed containing an ST" $
+          pguardC "An unlocked input existed containing an ST" $
            pany
              # plam
                ( \((pfield @"resolved" #) -> txOut) -> unTermCont $ do
@ -109,13 +100,13 @@ stakePolicy gtClassRef =
          pure $ popaque (pconstant ())
    let minting = unTermCont $ do
-          tcassert "ST at inputs must be 0" $
+          pguardC "ST at inputs must be 0" $
            spentST #== 0
-          tcassert "Minted ST must be exactly 1" $
+          pguardC "Minted ST must be exactly 1" $
            mintedST #== 1
-          tcassert "A UTXO must exist with the correct output" $
+          pguardC "A UTXO must exist with the correct output" $
            unTermCont $ do
              let scriptOutputWithStakeST =
                    mustBePJust
@ -214,50 +205,50 @@ stakeValidator :: Stake -> ClosedTerm PValidator
 stakeValidator stake =
  plam $ \datum redeemer ctx' -> unTermCont $ do
    ctx <- tcont $ pletFields @'["txInfo", "purpose"] ctx'
-    txInfo <- tclet $ pfromData ctx.txInfo
+    txInfo <- pletC $ pfromData ctx.txInfo
    txInfoF <- tcont $ pletFields @'["mint", "inputs", "outputs", "signatories", "datums"] txInfo
-    (pfromData -> stakeRedeemer, _) <- tctryFrom redeemer
+    (pfromData -> stakeRedeemer, _) <- ptryFromC redeemer
    -- TODO: Use PTryFrom
    let stakeDatum' :: Term _ PStakeDatum
        stakeDatum' = pfromData $ punsafeCoerce datum
    stakeDatum <- tcont $ pletFields @'["owner", "stakedAmount", "lockedBy"] stakeDatum'
-    PSpending txOutRef <- tcmatch $ pfromData ctx.purpose
+    PSpending txOutRef <- pmatchC $ pfromData ctx.purpose
-    PJust txInInfo <- tcmatch $ pfindTxInByTxOutRef # (pfield @"_0" # txOutRef) # txInfoF.inputs
+    PJust txInInfo <- pmatchC $ pfindTxInByTxOutRef # (pfield @"_0" # txOutRef) # txInfoF.inputs
-    ownAddress <- tclet $ pfield @"address" #$ pfield @"resolved" # txInInfo
+    ownAddress <- pletC $ pfield @"address" #$ pfield @"resolved" # txInInfo
    let continuingValue :: Term _ (PValue _ _)
        continuingValue = pfield @"value" #$ pfield @"resolved" # txInInfo
    -- Whether the owner signs this transaction or not.
-    ownerSignsTransaction <- tclet $ ptxSignedBy # txInfoF.signatories # stakeDatum.owner
+    ownerSignsTransaction <- pletC $ ptxSignedBy # txInfoF.signatories # stakeDatum.owner
-    stCurrencySymbol <- tclet $ pconstant $ mintingPolicySymbol $ mkMintingPolicy (stakePolicy stake.gtClassRef)
+    stCurrencySymbol <- pletC $ pconstant $ mintingPolicySymbol $ mkMintingPolicy (stakePolicy stake.gtClassRef)
-    mintedST <- tclet $ psymbolValueOf # stCurrencySymbol # txInfoF.mint
+    mintedST <- pletC $ psymbolValueOf # stCurrencySymbol # txInfoF.mint
-    valueSpent <- tclet $ pvalueSpent # txInfoF.inputs
+    valueSpent <- pletC $ pvalueSpent # txInfoF.inputs
-    spentST <- tclet $ psymbolValueOf # stCurrencySymbol #$ valueSpent
+    spentST <- pletC $ psymbolValueOf # stCurrencySymbol #$ valueSpent
    let AssetClass (propCs, propTn) = stake.proposalSTClass
        proposalSTClass = passetClass # pconstant propCs # pconstant propTn
-    spentProposalST <- tclet $ passetClassValueOf # valueSpent # proposalSTClass
+    spentProposalST <- pletC $ passetClassValueOf # valueSpent # proposalSTClass
    -- Is the stake currently locked?
-    stakeIsLocked <- tclet $ stakeLocked # stakeDatum'
+    stakeIsLocked <- pletC $ stakeLocked # stakeDatum'
    pure $
      pmatch stakeRedeemer $ \case
        PDestroy _ -> unTermCont $ do
-          tcassert "ST at inputs must be 1" $
+          pguardC "ST at inputs must be 1" $
            spentST #== 1
-          tcassert "Should burn ST" $
+          pguardC "Should burn ST" $
            mintedST #== -1
-          tcassert "Stake unlocked" $ pnot # stakeIsLocked
+          pguardC "Stake unlocked" $ pnot # stakeIsLocked
-          tcassert "Owner signs this transaction" ownerSignsTransaction
+          pguardC "Owner signs this transaction" ownerSignsTransaction
          pure $ popaque (pconstant ())
        --------------------------------------------------------------------------
@ -265,7 +256,7 @@ stakeValidator stake =
        _ -> unTermCont $ do
          -- Filter out own output with own address and PST.
          ownOutput <-
-            tclet $
+            pletC $
              mustBePJust # "Own output should be present" #$ pfind
                # plam
                  ( \input -> unTermCont $ do
@ -277,39 +268,39 @@ stakeValidator stake =
                # pfromData txInfoF.outputs
          stakeOut <-
-            tclet $
+            pletC $
              mustFindDatum' @PStakeDatum
                # (pfield @"datumHash" # ownOutput)
                # txInfoF.datums
          ownOutputValue <-
-            tclet $
+            pletC $
              pfield @"value" # ownOutput
          ownOutputValueUnchanged <-
-            tclet $
+            pletC $
              pdata continuingValue #== pdata ownOutputValue
          stakeOutUnchanged <-
-            tclet $
+            pletC $
              pdata stakeOut #== pdata stakeDatum'
          pure $
            pmatch stakeRedeemer $ \case
              PRetractVotes _ -> unTermCont $ do
-                tcassert
+                pguardC
                  "Owner signs this transaction"
                  ownerSignsTransaction
-                tcassert "ST at inputs must be 1" $
+                pguardC "ST at inputs must be 1" $
                  spentST #== 1
                -- This puts trust into the Proposal. The Proposal must necessarily check
                -- that this is not abused.
-                tcassert "Proposal ST spent" $
+                pguardC "Proposal ST spent" $
                  spentProposalST #== 1
-                tcassert "A UTXO must exist with the correct output" $
+                pguardC "A UTXO must exist with the correct output" $
                  unTermCont $ do
                    let valueCorrect = ownOutputValueUnchanged
@ -324,13 +315,13 @@ stakeValidator stake =
                pure $ popaque (pconstant ())
              --------------------------------------------------------------------------
              PPermitVote l -> unTermCont $ do
-                tcassert
+                pguardC
                  "Owner signs this transaction"
                  ownerSignsTransaction
                -- This puts trust into the Proposal. The Proposal must necessarily check
                -- that this is not abused.
-                tcassert "Proposal ST spent" $
+                pguardC "Proposal ST spent" $
                  spentProposalST #== 1
                -- Update the stake datum, but only the 'lockedBy' field.
@ -342,7 +333,7 @@ stakeValidator stake =
                    expectedLocks = pcons # newLock # stakeDatum.lockedBy
                expectedDatum <-
-                  tclet $
+                  pletC $
                    mkRecordConstr
                      PStakeDatum
                      ( #stakedAmount .= stakeDatum.stakedAmount
@ -350,7 +341,7 @@ stakeValidator stake =
                          .& #lockedBy .= pdata expectedLocks
                      )
-                tcassert "A UTXO must exist with the correct output" $
+                pguardC "A UTXO must exist with the correct output" $
                  let correctOutputDatum = stakeOut #== expectedDatum
                      valueCorrect = ownOutputValueUnchanged
                   in foldl1
@ -362,24 +353,24 @@ stakeValidator stake =
                pure $ popaque (pconstant ())
              --------------------------------------------------------------------------
              PWitnessStake _ -> unTermCont $ do
-                tcassert "ST at inputs must be 1" $
+                pguardC "ST at inputs must be 1" $
                  spentST #== 1
                let AssetClass (propCs, propTn) = stake.proposalSTClass
                    propAssetClass = passetClass # pconstant propCs # pconstant propTn
                    proposalTokenMoved =
-                      ptokenSpent
+                      pisTokenSpent
                        # propAssetClass
                        # txInfoF.inputs
                -- In order for cosignature to be witnessed, it must be possible for a
                -- proposal to allow this transaction to happen. This puts trust into the Proposal.
                -- The Proposal must necessarily check that this is not abused.
-                tcassert
+                pguardC
                  "Owner signs this transaction OR proposal token is spent"
                  (ownerSignsTransaction #|| proposalTokenMoved)
-                tcassert "A UTXO must exist with the correct output" $
+                pguardC "A UTXO must exist with the correct output" $
                  let correctOutputDatum = stakeOutUnchanged
                      valueCorrect = ownOutputValueUnchanged
                   in foldl1
@ -390,21 +381,21 @@ stakeValidator stake =
                pure $ popaque (pconstant ())
              --------------------------------------------------------------------------
              PDepositWithdraw r -> unTermCont $ do
-                tcassert "ST at inputs must be 1" $
+                pguardC "ST at inputs must be 1" $
                  spentST #== 1
-                tcassert "Stake unlocked" $
+                pguardC "Stake unlocked" $
                  pnot #$ stakeIsLocked
-                tcassert
+                pguardC
                  "Owner signs this transaction"
                  ownerSignsTransaction
-                tcassert "A UTXO must exist with the correct output" $
+                pguardC "A UTXO must exist with the correct output" $
                  unTermCont $ do
                    let oldStakedAmount = pfromData $ stakeDatum.stakedAmount
                        delta = pfromData $ pfield @"delta" # r
-                    newStakedAmount <- tclet $ oldStakedAmount + delta
+                    newStakedAmount <- pletC $ oldStakedAmount + delta
-                    tcassert "New staked amount shoudl be greater than or equal to 0" $
+                    pguardC "New staked amount shoudl be greater than or equal to 0" $
                      zero #<= newStakedAmount
                    let expectedDatum =
@ -420,7 +411,7 @@ stakeValidator stake =
                        valueDelta = pdiscreteValue' stake.gtClassRef # delta
                        expectedValue =
-                          paddValue # continuingValue # valueDelta
+                          continuingValue <> valueDelta
                        valueCorrect =
                          foldr1
--- a/agora/Agora/Treasury.hs
+++ b/agora/Agora/Treasury.hs
@ -11,7 +11,6 @@ treasury.
 module Agora.Treasury (module Agora.Treasury) where
 import Agora.AuthorityToken (singleAuthorityTokenBurned)
 import Agora.Utils (tcassert, tclet, tcmatch, tctryFrom)
 import GHC.Generics qualified as GHC
 import Generics.SOP
 import Plutarch.Api.V1 (PValidator)
@ -21,6 +20,7 @@ import Plutarch.DataRepr (
  DerivePConstantViaData (..),
  PIsDataReprInstances (PIsDataReprInstances),
 )
 import Plutarch.Extra.TermCont (pguardC, pletC, pmatchC, ptryFromC)
 import Plutarch.Lift (PConstantDecl (..), PLifted (..), PUnsafeLiftDecl)
 import Plutarch.TryFrom ()
 import PlutusLedgerApi.V1.Value (CurrencySymbol)
@ -76,26 +76,26 @@ treasuryValidator ::
  CurrencySymbol ->
  ClosedTerm PValidator
 treasuryValidator gatCs' = plam $ \_datum redeemer ctx' -> unTermCont $ do
-  (treasuryRedeemer, _) <- tctryFrom redeemer
+  (treasuryRedeemer, _) <- ptryFromC redeemer
  -- plet required fields from script context.
  ctx <- tcont $ pletFields @["txInfo", "purpose"] ctx'
  -- Ensure that script is for burning i.e. minting a negative amount.
-  PMinting _ <- tcmatch ctx.purpose
+  PMinting _ <- pmatchC ctx.purpose
  -- Ensure redeemer type is valid.
-  PSpendTreasuryGAT _ <- tcmatch $ pfromData treasuryRedeemer
+  PSpendTreasuryGAT _ <- pmatchC $ pfromData treasuryRedeemer
  -- Get the minted value from txInfo.
-  txInfo' <- tclet ctx.txInfo
+  txInfo' <- pletC ctx.txInfo
  txInfo <- tcont $ pletFields @'["mint"] txInfo'
  let mint :: Term _ (PValue _ _)
      mint = txInfo.mint
-  gatCs <- tclet $ pconstant gatCs'
+  gatCs <- pletC $ pconstant gatCs'
-  tcassert "A single authority token has been burned" $
+  pguardC "A single authority token has been burned" $
    singleAuthorityTokenBurned gatCs txInfo' mint
  pure . popaque $ pconstant ()
--- a/agora/Agora/Utils.hs
+++ b/agora/Agora/Utils.hs
@ -6,45 +6,6 @@ Description: Plutarch utility functions that should be upstreamed or don't belon
 Plutarch utility functions that should be upstreamed or don't belong anywhere else.
 -}
 module Agora.Utils (
  -- * TermCont-based combinators. Some of these will live in plutarch eventually.
  tcassert,
  tclet,
  tcmatch,
  tctryFrom,
  -- * Validator-level utility functions
  pfind',
  pfindDatum,
  ptryFindDatum,
  pvalueSpent,
  ptxSignedBy,
  paddValue,
  plookup,
  pfromMaybe,
  psymbolValueOf,
  pgeqByClass,
  pgeqBySymbol,
  pgeqByClass',
  pfindTxInByTxOutRef,
  psingletonValue,
  pfindMap,
  pnotNull,
  pisJust,
  ptokenSpent,
  pkeysEqual,
  pnubSortBy,
  pisUniq,
  pisUniqBy,
  pisDJust,
  pisUTXOSpent,
  pmsortBy,
  pmsort,
  pnubSort,
  pupdate,
  pmapMap,
  pmapMaybe,
  -- * Functions which should (probably) not be upstreamed
  findTxOutByTxOutRef,
  scriptHashFromAddress,
  findOutputsToAddress,
@ -57,10 +18,9 @@ module Agora.Utils (
  mustBePJust,
  mustBePDJust,
  validatorHashToAddress,
  pmergeBy,
  phalve,
  isScriptAddress,
  isPubKey,
  psingletonValue,
 ) where
 --------------------------------------------------------------------------------
@ -72,541 +32,37 @@ import PlutusLedgerApi.V1 (
  TokenName (..),
  ValidatorHash (..),
 )
 import PlutusLedgerApi.V1.Value (AssetClass (..))
 --------------------------------------------------------------------------------
 import Plutarch.Api.V1 (
-  AmountGuarantees (NoGuarantees, NonZero, Positive),
+  AmountGuarantees,
-  KeyGuarantees (Sorted, Unsorted),
+  KeyGuarantees,
  PAddress,
  PCredential (PScriptCredential),
  PCurrencySymbol,
  PDatum,
  PDatumHash,
  PMap,
  PMaybeData (PDJust),
  PMintingPolicy,
  PPubKeyHash,
  PTokenName (PTokenName),
  PTuple,
-  PTxInInfo (PTxInInfo),
+  PTxInInfo,
-  PTxOut (PTxOut),
+  PTxOut,
  PTxOutRef,
  PValidatorHash,
  PValue,
  mintingPolicySymbol,
  mkMintingPolicy,
 )
 import Plutarch.Api.V1.AssetClass (PAssetClass, passetClassValueOf, pvalueOf)
 import Plutarch.Api.V1.AssocMap (PMap (PMap))
 import Plutarch.Api.V1.ScriptContext (pfindDatum, pfindTxInByTxOutRef)
 import "liqwid-plutarch-extra" Plutarch.Api.V1.Value (psymbolValueOf)
 import "plutarch" Plutarch.Api.V1.Value (PValue (PValue))
 import Plutarch.Builtin (pforgetData, ppairDataBuiltin)
-import Plutarch.Extra.Map (pkeys)
+import Plutarch.Extra.List (plookupTuple)
-import Plutarch.Reducible (Reducible (Reduce))
+import Plutarch.Extra.TermCont (pletC, pmatchC)
 import Plutarch.TryFrom (PTryFrom (PTryFromExcess))
 import Plutarch.Unsafe (punsafeCoerce)
 --------------------------------------------------------------------------------
 -- TermCont-based combinators. Some of these will live in plutarch eventually.
 -- | Assert a particular 'PBool', trace if false.
 tcassert :: forall r (s :: S). Term s PString -> Term s PBool -> TermCont @r s ()
 tcassert errorMessage check = tcont $ \k -> pif check (k ()) (ptraceError errorMessage)
 -- | 'plet' but for use in 'TermCont'.
 tclet :: forall r (s :: S) (a :: PType). Term s a -> TermCont @r s (Term s a)
 tclet = tcont . plet
 -- | 'pmatch' but for use in 'TermCont'.
 tcmatch :: forall (a :: PType) (s :: S). PlutusType a => Term s a -> TermCont s (a s)
 tcmatch = tcont . pmatch
 -- | 'ptryFrom' but for use in 'TermCont'.
 tctryFrom :: forall b a s r. PTryFrom a b => Term s a -> TermCont @r s (Term s b, Reduce (PTryFromExcess a b s))
 tctryFrom = tcont . ptryFrom
 -- | Escape with a particular value on expecting 'Just'. For use in monadic context.
 tcexpectJust ::
  forall r (a :: PType) (s :: S).
  Term s r ->
  Term s (PMaybe a) ->
  TermCont @r s (Term s a)
 tcexpectJust escape ma = tcont $ \f ->
  pmatch ma $ \case
    PJust v -> f v
    PNothing -> escape
 --------------------------------------------------------------------------------
 -- Validator-level utility functions
 -- | Find a datum with the given hash.
 pfindDatum :: Term s (PDatumHash :--> PBuiltinList (PAsData (PTuple PDatumHash PDatum)) :--> PMaybe PDatum)
 pfindDatum = phoistAcyclic $
  plam $ \datumHash datums -> plookupTuple # datumHash # datums
 -- | Find a datum with the given hash, and `ptryFrom` it.
 ptryFindDatum :: forall (a :: PType) (s :: S). PTryFrom PData a => Term s (PDatumHash :--> PBuiltinList (PAsData (PTuple PDatumHash PDatum)) :--> PMaybe a)
 ptryFindDatum = phoistAcyclic $
  plam $ \datumHash inputs ->
    pmatch (pfindDatum # datumHash # inputs) $ \case
      PNothing -> pcon PNothing
      PJust datum -> unTermCont $ do
        (datum', _) <- tctryFrom (pto datum)
        pure $ pcon (PJust datum')
 -- | Check if a PubKeyHash signs this transaction.
 ptxSignedBy :: Term s (PBuiltinList (PAsData PPubKeyHash) :--> PAsData PPubKeyHash :--> PBool)
 ptxSignedBy = phoistAcyclic $
  plam $ \sigs sig -> pelem # sig # sigs
 -- | Get the first element that matches a predicate or return Nothing.
 pfind' ::
  PIsListLike list a =>
  (Term s a -> Term s PBool) ->
  Term s (list a :--> PMaybe a)
 pfind' p =
  precList
    (\self x xs -> pif (p x) (pcon (PJust x)) (self # xs))
    (const $ pcon PNothing)
 -- | Get the first element that maps to a PJust in a list.
 pfindMap ::
  PIsListLike list a =>
  Term s ((a :--> PMaybe b) :--> list a :--> PMaybe b)
 pfindMap =
  phoistAcyclic $
    plam $ \p ->
      precList
        ( \self x xs ->
            -- In the future, this should use `pmatchSum`, I believe?
            pmatch (p # x) $ \case
              PNothing -> self # xs
              PJust v -> pcon (PJust v)
        )
        (const $ pcon PNothing)
 -- | Find the value for a given key in an associative list.
 plookup ::
  (PEq a, PIsListLike list (PBuiltinPair a b)) =>
  Term s (a :--> list (PBuiltinPair a b) :--> PMaybe b)
 plookup =
  phoistAcyclic $
    plam $ \k xs ->
      pmatch (pfind' (\p -> pfstBuiltin # p #== k) # xs) $ \case
        PNothing -> pcon PNothing
        PJust p -> pcon (PJust (psndBuiltin # p))
 -- | Find the value for a given key in an assoclist which uses 'PTuple's.
 plookupTuple ::
  (PEq a, PIsListLike list (PAsData (PTuple a b)), PIsData a, PIsData b) =>
  Term s (a :--> list (PAsData (PTuple a b)) :--> PMaybe b)
 plookupTuple =
  phoistAcyclic $
    plam $ \k xs ->
      pmatch (pfind' (\p -> (pfield @"_0" # pfromData p) #== k) # xs) $ \case
        PNothing -> pcon PNothing
        PJust p -> pcon (PJust (pfield @"_1" # pfromData p))
 -- | Extract a Maybe by providing a default value in case of Just.
 pfromMaybe :: forall a s. Term s (a :--> PMaybe a :--> a)
 pfromMaybe = phoistAcyclic $
  plam $ \e a ->
    pmatch a $ \case
      PJust a' -> a'
      PNothing -> e
 -- | Yield True if a given PMaybe is of form @'PJust' _@.
 pisJust :: forall a s. Term s (PMaybe a :--> PBool)
 pisJust = phoistAcyclic $
  plam $ \v' ->
    pmatch v' $ \case
      PJust _ -> pconstant True
      PNothing -> pconstant False
 -- | Get the sum of all values belonging to a particular CurrencySymbol.
 psymbolValueOf ::
  forall (keys :: KeyGuarantees) (amounts :: AmountGuarantees) (s :: S).
  Term s (PCurrencySymbol :--> PValue keys amounts :--> PInteger)
 psymbolValueOf =
  phoistAcyclic $
    plam $ \sym value'' -> unTermCont $ do
      PValue value' <- tcmatch value''
      PMap value <- tcmatch value'
      m' <- tcexpectJust 0 (plookup # pdata sym # value)
      PMap m <- tcmatch (pfromData m')
      pure $ pfoldr # plam (\x v -> pfromData (psndBuiltin # x) + v) # 0 # m
 -- | Extract amount from PValue belonging to a Haskell-level AssetClass.
 passetClassValueOf' ::
  forall (keys :: KeyGuarantees) (amounts :: AmountGuarantees) (s :: S).
  AssetClass ->
  Term s (PValue keys amounts :--> PInteger)
 passetClassValueOf' (AssetClass (sym, token)) =
  phoistAcyclic $ plam $ \value -> pvalueOf # value # pconstant sym # pconstant token
 -- | Return '>=' on two values comparing by only a particular AssetClass.
 pgeqByClass ::
  forall (keys :: KeyGuarantees) (amounts :: AmountGuarantees) (s :: S).
  Term s (PCurrencySymbol :--> PTokenName :--> PValue keys amounts :--> PValue keys amounts :--> PBool)
 pgeqByClass =
  phoistAcyclic $
    plam $ \cs tn a b ->
      pvalueOf # b # cs # tn #<= pvalueOf # a # cs # tn
 -- | Return '>=' on two values comparing by only a particular CurrencySymbol.
 pgeqBySymbol ::
  forall (keys :: KeyGuarantees) (amounts :: AmountGuarantees) (s :: S).
  Term s (PCurrencySymbol :--> PValue keys amounts :--> PValue keys amounts :--> 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.
 pgeqByClass' ::
  forall (keys :: KeyGuarantees) (amounts :: AmountGuarantees) (s :: S).
  AssetClass ->
  Term s (PValue keys amounts :--> PValue keys amounts :--> PBool)
 pgeqByClass' ac =
  phoistAcyclic $
    plam $ \a b ->
      passetClassValueOf' ac # b #<= passetClassValueOf' ac # a
 -- | Union two maps using a merge function on collisions.
 pmapUnionWith ::
  forall (k :: PType) (v :: PType) (keys :: KeyGuarantees) (s :: S).
  PIsData v =>
  Term s ((v :--> v :--> v) :--> PMap keys k v :--> PMap keys k v :--> PMap keys k v)
 pmapUnionWith = phoistAcyclic $
  -- TODO: this function is kinda suspect. I feel like a lot of optimizations could be done here
  plam $ \f xs' ys' -> unTermCont $ do
    PMap xs <- tcmatch xs'
    PMap ys <- tcmatch ys'
    let ls =
          pmap
            # plam
              ( \p -> unTermCont $ do
                  pf <- tclet $ pfstBuiltin # p
                  pure $
                    pmatch (plookup # pf # ys) $ \case
                      PJust v ->
                        -- Data conversions here are silly, aren't they?
                        ppairDataBuiltin # pf # pdata (f # pfromData (psndBuiltin # p) # pfromData v)
                      PNothing -> p
              )
            # xs
        rs =
          pfilter
            # plam
              ( \p ->
                  pnot #$ pany # plam (\p' -> pfstBuiltin # p' #== pfstBuiltin # p) # xs
              )
            # ys
    pure $ pcon (PMap $ pconcat # ls # rs)
 -- | A special version of `pmap` which allows list elements to be thrown out.
 pmapMaybe :: forall s a list. (PIsListLike list a) => Term s ((a :--> PMaybe a) :--> list a :--> list a)
 pmapMaybe = phoistAcyclic $
  pfix #$ plam $ \self f l -> pif (pnull # l) pnil $
    unTermCont $ do
      x <- tclet $ phead # l
      xs <- tclet $ ptail # l
      pure $
        pmatch (f # x) $ \case
          PJust ux -> pcons # ux #$ self # f # xs
          _ -> self # f # xs
 -- | / O(n) /. Update the value at a given key in a `PMap`, have the same functionalities as 'Data.Map.update'.
 pupdate ::
  forall (k :: PType) (v :: PType) (keys :: KeyGuarantees) (s :: S).
  (PIsData k, PIsData v) =>
  Term s ((v :--> PMaybe v) :--> k :--> PMap keys k v :--> PMap keys k v)
 pupdate = phoistAcyclic $
  plam $ \f (pdata -> tk) (pto -> (ps :: Term _ (PBuiltinList _))) ->
    pcon $
      PMap $
        pmapMaybe
          # plam
            ( \kv ->
                let k = pfstBuiltin # kv
                    v = pfromData $ psndBuiltin # kv
                 in pif
                      (k #== tk)
                      -- 'PBuiltinPair' doesn't have 'PFunctor', so:
                      ( pmatch (f # v) $
                          \case
                            PJust uv -> pcon $ PJust $ ppairDataBuiltin # k # pdata uv
                            _ -> pcon PNothing
                      )
                      (pcon $ PJust kv)
            )
          # ps
 -- | / O(n) /. Map a function over all values in a 'PMap'.
 pmapMap ::
  forall (k :: PType) (a :: PType) (b :: PType) (keys :: KeyGuarantees) (s :: S).
  (PIsData k, PIsData a, PIsData b) =>
  Term s ((a :--> b) :--> PMap keys k a :--> PMap keys k b)
 pmapMap = phoistAcyclic $
  plam $ \f (pto -> (ps :: Term _ (PBuiltinList _))) ->
    pcon $
      PMap $
        pmap
          # plam
            ( \kv ->
                let k = pfstBuiltin # kv
                    v = psndBuiltin # kv
                    nv = pdata $ f # pfromData v
                 in ppairDataBuiltin # k # nv
            )
          # ps
 -- | Compute the guarantees known after adding two values.
 type family AddGuarantees (a :: AmountGuarantees) (b :: AmountGuarantees) where
  AddGuarantees 'Positive 'Positive = 'Positive
  AddGuarantees _ _ = 'NoGuarantees
 -- | Add two 'PValue's together.
 paddValue ::
  forall (keys :: KeyGuarantees) (as :: AmountGuarantees) (bs :: AmountGuarantees) (s :: S).
  Term s (PValue keys as :--> PValue keys bs :--> PValue keys (AddGuarantees as bs))
 paddValue = phoistAcyclic $
  plam $ \a' b' -> unTermCont $ do
    PValue a <- tcmatch a'
    PValue b <- tcmatch b'
    pure $
      pcon
        ( PValue $
            pmapUnionWith # plam (\a' b' -> pmapUnionWith # plam (+) # a' # b') # a # b
        )
 -- | Sum of all value at input.
 pvalueSpent ::
  forall (s :: S).
  Term s (PBuiltinList (PAsData PTxInInfo) :--> PValue 'Sorted 'Positive)
 pvalueSpent = phoistAcyclic $
  plam $ \inputs ->
    pfoldr
      # plam
        ( \txInInfo' v ->
            pmatch
              (pfromData txInInfo')
              $ \(PTxInInfo txInInfo) ->
                paddValue
                  # pmatch
                    (pfield @"resolved" # txInInfo)
                    (\(PTxOut o) -> pfromData $ pfield @"value" # o)
                  # v
        )
      -- TODO: This should be possible without coercions, but I can't figure out the types atm.
      # punsafeCoerce (pconstant mempty :: Term _ (PValue 'Unsorted 'NonZero))
      # inputs
 -- | Find the TxInInfo by a TxOutRef.
 pfindTxInByTxOutRef :: Term s (PTxOutRef :--> PBuiltinList (PAsData PTxInInfo) :--> PMaybe PTxInInfo)
 pfindTxInByTxOutRef = phoistAcyclic $
  plam $ \txOutRef inputs ->
    pfindMap
      # plam
        ( \txInInfo' ->
            plet (pfromData txInInfo') $ \r ->
              pmatch r $ \(PTxInInfo txInInfo) ->
                pif
                  (pdata txOutRef #== pfield @"outRef" # txInInfo)
                  (pcon (PJust r))
                  (pcon PNothing)
        )
      #$ inputs
 -- | 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.
     When using this as an authority check, you __MUST__ ensure the authority
     knows how to ensure its end of the contract.
 -}
 ptokenSpent :: forall {s :: S}. Term s (PAssetClass :--> PBuiltinList (PAsData PTxInInfo) :--> PBool)
 ptokenSpent =
  plam $ \tokenClass inputs ->
    0
      #< pfoldr @PBuiltinList
        # plam
          ( \txInInfo' acc -> unTermCont $ do
              PTxInInfo txInInfo <- tcmatch (pfromData txInInfo')
              PTxOut txOut' <- tcmatch $ pfromData $ pfield @"resolved" # txInInfo
              txOut <- tcont $ pletFields @'["value"] txOut'
              let txOutValue = pfromData txOut.value
              pure $ acc + passetClassValueOf # txOutValue # tokenClass
          )
        # 0
        # inputs
 {- | True if both maps have exactly the same keys.
     Using @'#=='@ is not sufficient, because keys returned are not ordered.
 -}
 pkeysEqual ::
  forall (k :: PType) (a :: PType) (b :: PType) (keys :: KeyGuarantees) (s :: S).
  (POrd k, PIsData k) =>
  Term s (PMap keys k a :--> PMap keys k b :--> PBool)
 pkeysEqual = phoistAcyclic $
  plam $ \p q -> unTermCont $ do
    pks <- tclet $ pkeys # p
    qks <- tclet $ pkeys # q
    pure $
      pif
        (plength # pks #== plength # qks)
        ( unTermCont $ do
            let comp = phoistAcyclic $ plam $ \(pfromData -> x) (pfromData -> y) -> x #< y
                spks = pmsortBy # comp # pks
                sqks = pmsortBy # comp # qks
            pure $ plistEquals # spks # sqks
        )
        (pcon PFalse)
 -- | / O(nlogn) /. Sort and remove dupicate elements in a list.
 pnubSortBy ::
  forall list a (s :: S).
  (PIsListLike list a) =>
  Term s ((a :--> a :--> PBool) :--> (a :--> a :--> PBool) :--> list a :--> list a)
 pnubSortBy = phoistAcyclic $
  plam $ \eq comp l -> pif (pnull # l) l $
    unTermCont $ do
      sl <- tclet $ pmsortBy # comp # l
      let x = phead # sl
          xs = ptail # sl
      return $ pgo # eq # x # xs
  where
    pgo = phoistAcyclic pfix #$ plam pgo'
    pgo' self eq seen l =
      pif (pnull # l) (psingleton # seen) $
        unTermCont $ do
          x <- tclet $ phead # l
          xs <- tclet $ ptail # l
          return $
            pif
              (eq # x # seen)
              (self # eq # seen # xs)
              (pcons # seen #$ self # eq # x # xs)
 -- | Special version of 'pnubSortBy', which requires elements have 'POrd'.
 pnubSort ::
  forall list a (s :: S).
  (PIsListLike list a, POrd a) =>
  Term s (list a :--> list a)
 pnubSort = phoistAcyclic $ pnubSortBy # eq # comp
  where
    eq = phoistAcyclic $ plam (#==)
    comp = phoistAcyclic $ plam (#<)
 -- | / O(nlogn) /. Check if a list contains no duplicates.
 pisUniqBy ::
  forall list a (s :: S).
  (PIsListLike list a) =>
  Term s ((a :--> a :--> PBool) :--> (a :--> a :--> PBool) :--> list a :--> PBool)
 pisUniqBy = phoistAcyclic $
  plam $ \eq comp xs ->
    let nubbed = pnubSortBy # eq # comp # xs
     in plength # xs #== plength # nubbed
 -- | A special case of 'pisUniqBy' which requires elements have 'POrd' instance.
 pisUniq :: forall list a (s :: S). (POrd a, PIsListLike list a) => Term s (list a :--> PBool)
 pisUniq = phoistAcyclic $ pisUniqBy # eq # comp
  where
    eq = phoistAcyclic $ plam (#==)
    comp = phoistAcyclic $ plam (#<)
 -- | Yield True if a given PMaybeData is of form @'PDJust' _@.
 pisDJust :: Term s (PMaybeData a :--> PBool)
 pisDJust = phoistAcyclic $
  plam $ \x ->
    pmatch
      x
      ( \case
          PDJust _ -> pconstant True
          _ -> pconstant False
      )
 -- | Determines if a given UTXO is spent.
 pisUTXOSpent :: Term s (PTxOutRef :--> PBuiltinList (PAsData PTxInInfo) :--> PBool)
 pisUTXOSpent = phoistAcyclic $
  plam $ \oref inputs -> P.do
    pisJust #$ pfindTxInByTxOutRef # oref # inputs
 -- | / O(n) /. Merge two lists which are assumed to be ordered, given a custom comparator.
 pmergeBy :: (PIsListLike l a) => Term s ((a :--> a :--> PBool) :--> l a :--> l a :--> l a)
 pmergeBy = phoistAcyclic $ pfix #$ plam pmergeBy'
  where
    pmergeBy' self comp a b =
      pif (pnull # a) b $
        pif (pnull # b) a $
          unTermCont $ do
            ah <- tclet $ phead # a
            at <- tclet $ ptail # a
            bh <- tclet $ phead # b
            bt <- tclet $ ptail # b
            pure $
              pif
                (comp # ah # bh)
                (pcons # ah #$ self # comp # at # b)
                (pcons # bh #$ self # comp # a # bt)
 {- | / O(nlogn) /. Merge sort, bottom-up version, given a custom comparator.
   Elements are arranged from lowest to highest,
   keeping duplicates in the order they appeared in the input.
 -}
 pmsortBy :: (PIsListLike l a) => Term s ((a :--> a :--> PBool) :--> l a :--> l a)
 pmsortBy = phoistAcyclic $ pfix #$ plam pmsortBy'
  where
    pmsortBy' self comp xs = pif (pnull # xs) pnil $
      pif (pnull #$ ptail # xs) xs $
        pmatch (phalve # xs) $ \(PPair fh sh) ->
          let sfh = self # comp # fh
              ssh = self # comp # sh
           in pmergeBy # comp # sfh # ssh
 -- | A special case of 'pmsortBy' which requires elements have 'POrd' instance.
 pmsort :: (POrd a, PIsListLike l a) => Term s (l a :--> l a)
 pmsort = phoistAcyclic $ pmsortBy # comp
  where
    comp = phoistAcyclic $ plam (#<)
 -- | Split a list in half.
 phalve :: (PIsListLike l a) => Term s (l a :--> PPair (l a) (l a))
 phalve = phoistAcyclic $ plam $ \l -> go # l # l
  where
    go = phoistAcyclic $ pfix #$ plam go'
    go' self xs ys =
      pif
        (pnull # ys)
        (pcon $ PPair pnil xs)
        ( unTermCont $ do
            yt <- tclet $ ptail # ys
            xh <- tclet $ phead # xs
            xt <- tclet $ ptail # xs
            pure $
              pif (pnull # yt) (pcon $ PPair (psingleton # xh) xt) $
                unTermCont $ do
                  yt' <- tclet $ ptail # yt
                  pure $
                    pmatch (self # xt # yt') $ \(PPair first last) ->
                      pcon $ PPair (pcons # xh # first) last
        )
 --------------------------------------------------------------------------------
 {- Functions which should (probably) not be upstreamed
   All of these functions are quite inefficient.
 -}
@ -655,7 +111,7 @@ isPubKey = phoistAcyclic $
 findOutputsToAddress :: Term s (PBuiltinList (PAsData PTxOut) :--> PAddress :--> PBuiltinList (PAsData PTxOut))
 findOutputsToAddress = phoistAcyclic $
  plam $ \outputs address' -> unTermCont $ do
-    address <- tclet $ pdata address'
+    address <- pletC $ pdata address'
    pure $
      pfilter # plam (\(pfromData -> txOut) -> pfield @"address" # txOut #== address)
        # outputs
@ -664,7 +120,7 @@ findOutputsToAddress = phoistAcyclic $
 findTxOutDatum :: Term s (PBuiltinList (PAsData (PTuple PDatumHash PDatum)) :--> PTxOut :--> PMaybe PDatum)
 findTxOutDatum = phoistAcyclic $
  plam $ \datums out -> unTermCont $ do
-    datumHash' <- tcmatch $ pfromData $ pfield @"datumHash" # out
+    datumHash' <- pmatchC $ pfromData $ pfield @"datumHash" # out
    pure $ case datumHash' of
      PDJust ((pfield @"_0" #) -> datumHash) -> pfindDatum # datumHash # datums
      _ -> pcon PNothing
--- a/bench.csv
+++ b/bench.csv
@ -1,29 +1,29 @@
 name,cpu,mem,size
-Agora/Effects/Treasury Withdrawal Effect/effect/Simple,317467035,778238,3172
+Agora/Effects/Treasury Withdrawal Effect/effect/Simple,289461528,703055,3191
-Agora/Effects/Treasury Withdrawal Effect/effect/Simple with multiple treasuries ,555940189,1350738,3499
+Agora/Effects/Treasury Withdrawal Effect/effect/Simple with multiple treasuries ,448521458,1070167,3518
-Agora/Effects/Treasury Withdrawal Effect/effect/Mixed Assets,488765974,1174701,3364
+Agora/Effects/Treasury Withdrawal Effect/effect/Mixed Assets,408085321,966048,3383
-Agora/Effects/Governor Mutation Effect/validator/valid new governor datum/governor validator should pass,83689582,228928,7629
+Agora/Effects/Governor Mutation Effect/validator/valid new governor datum/governor validator should pass,83758582,229228,7665
 Agora/Effects/Governor Mutation Effect/validator/valid new governor datum/effect validator should pass,97345575,266935,3358
-Agora/Stake/policy/stakeCreation,43459609,126049,2116
+Agora/Stake/policy/stakeCreation,43114609,124549,2094
-Agora/Stake/validator/stakeDepositWithdraw deposit,226083166,599197,4024
+Agora/Stake/validator/stakeDepositWithdraw deposit,171823342,464745,4069
-Agora/Stake/validator/stakeDepositWithdraw withdraw,226083166,599197,4016
+Agora/Stake/validator/stakeDepositWithdraw withdraw,171823342,464745,4061
-Agora/Proposal/policy/proposalCreation,23071177,68894,1523
+Agora/Proposal/policy/proposalCreation,23140177,69194,1525
-Agora/Proposal/validator/cosignature/proposal,190181087,511819,5644
+Agora/Proposal/validator/cosignature/proposal,147258436,403167,5646
-Agora/Proposal/validator/cosignature/stake,162540553,402961,4561
+Agora/Proposal/validator/cosignature/stake,117270039,287783,4606
-Agora/Proposal/validator/voting/proposal,181998338,491168,5652
+Agora/Proposal/validator/voting/proposal,154824944,415642,5654
-Agora/Proposal/validator/voting/stake,127693475,328703,4614
+Agora/Proposal/validator/voting/stake,99545453,256941,4659
-Agora/Proposal/validator/advancing/successfully advance to next state/Draft -> VotringReady,98071575,260351,5030
+Agora/Proposal/validator/advancing/successfully advance to next state/Draft -> VotringReady,94701799,249495,5031
-Agora/Proposal/validator/advancing/successfully advance to next state/VotingReady -> Locked,97228153,258848,5033
+Agora/Proposal/validator/advancing/successfully advance to next state/VotingReady -> Locked,93858377,247992,5034
-Agora/Proposal/validator/advancing/successfully advance to next state/Locked -> Finished,98924620,262454,5033
+Agora/Proposal/validator/advancing/successfully advance to next state/Locked -> Finished,95554844,251598,5034
-Agora/Proposal/validator/advancing/successfully advance to failed state: timeout/Draft -> Finished,96941774,257621,5032
+Agora/Proposal/validator/advancing/successfully advance to failed state: timeout/Draft -> Finished,93571998,246765,5033
-Agora/Proposal/validator/advancing/successfully advance to failed state: timeout/VotingReady -> Finished,95532863,254916,5033
+Agora/Proposal/validator/advancing/successfully advance to failed state: timeout/VotingReady -> Finished,92163087,244060,5034
-Agora/Proposal/validator/advancing/successfully advance to failed state: timeout/Locked -> Finished,96663841,257320,5033
+Agora/Proposal/validator/advancing/successfully advance to failed state: timeout/Locked -> Finished,93294065,246464,5034
 Agora/AuthorityToken/singleAuthorityTokenBurned/Correct simple,21017788,55883,806
 Agora/AuthorityToken/singleAuthorityTokenBurned/Correct many inputs,33204186,88241,900
 Agora/Treasury/Validator/Positive/Allows for effect changes,29938856,79744,1841
 Agora/AuthorityToken/singleAuthorityTokenBurned/Correct simple,21017788,55883,806
 Agora/AuthorityToken/singleAuthorityTokenBurned/Correct many inputs,33204186,88241,900
 Agora/Governor/policy/GST minting,43087287,120125,1833
-Agora/Governor/validator/proposal creation,258936253,681815,8145
+Agora/Governor/validator/proposal creation,261928725,689487,8181
-Agora/Governor/validator/GATs minting,358292569,955552,8266
+Agora/Governor/validator/GATs minting,351749811,938560,8302
-Agora/Governor/validator/mutate governor state,81661538,223202,7682
+Agora/Governor/validator/mutate governor state,81730538,223502,7718
--- a/flake.lock
+++ b/flake.lock
--- a/flake.nix
+++ b/flake.nix
@ -21,7 +21,7 @@
  inputs.plutarch-numeric.url =
    "github:Liqwid-Labs/plutarch-numeric?ref=main";
  inputs.plutarch-safe-money.url =
-    "github:Liqwid-Labs/plutarch-safe-money?ref=main";
+    "github:Liqwid-Labs/plutarch-safe-money?rev=9f968b80189c7e4b335527cd5b103dc26952f667";
  # Testing
  inputs.plutarch-quickcheck.url =