apropos-tx setup

agora/Agora/AuthorityToken.hs

@@ -0,0 +1,126 @@
+{- |
+Module     : Agora.AuthorityToken
+Maintainer : emi@haskell.fyi
+Description: Tokens acting as redeemable proofs of DAO authority.
+
+Tokens acting as redeemable proofs of DAO authority.
+-}
+module Agora.AuthorityToken (
+  authorityTokenPolicy,
+  authorityTokensValidIn,
+  AuthorityToken (..),
+) where
+
+import Plutarch.Api.V1 (
+  PAddress (..),
+  PCredential (..),
+  PCurrencySymbol (..),
+  PMap (..),
+  PScriptContext (..),
+  PScriptPurpose (..),
+  PTxInInfo (..),
+  PTxInfo (..),
+  PTxOut (..),
+  PValue (..),
+ )
+import Plutarch.Builtin (pforgetData)
+import Plutarch.List (pfoldr')
+import Plutarch.Monadic qualified as P
+import Plutus.V1.Ledger.Value (AssetClass)
+
+import Prelude
+
+--------------------------------------------------------------------------------
+
+import Agora.Utils (allOutputs, passert, passetClassValueOf, passetClassValueOf', plookup)
+
+--------------------------------------------------------------------------------
+
+{- | 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
+     said transaction. Said validator should be made aware of
+     *this* token's existence in order to prevent incorrect minting.
+-}
+newtype AuthorityToken = AuthorityToken
+  { authority :: AssetClass
+  -- ^ Token that must move in order for minting this to be valid.
+  }
+
+--------------------------------------------------------------------------------
+
+{- | Check that all GATs are valid in a particular TxOut.
+     How this is checked: an AuthorityToken should never leave
+     the Effect it was initially sent to, so we simply check that
+     the script address the token resides in matches the TokenName.
+     Since the TokenName was tagged upon mint with the Effect script
+     it was sent to, this is enough to prove validity.
+
+     In other words, check that all assets of a particular currency symbol
+     are tagged with a TokenName that matches where they live.
+-}
+authorityTokensValidIn :: Term s (PCurrencySymbol :--> PTxOut :--> PBool)
+authorityTokensValidIn = phoistAcyclic $
+  plam $ \authorityTokenSym txOut'' -> P.do
+    PTxOut txOut' <- pmatch txOut''
+    txOut <- pletFields @'["address", "value"] $ txOut'
+    PAddress address <- pmatch txOut.address
+    PValue value' <- pmatch txOut.value
+    PMap value <- pmatch value'
+    pmatch (plookup # pdata authorityTokenSym # value) $ \case
+      PJust (pfromData -> tokenMap') ->
+        pmatch (pfield @"credential" # address) $ \case
+          PPubKeyCredential _ ->
+            -- GATs should only be sent to Effect validators
+            pconstant False
+          PScriptCredential ((pfromData . (pfield @"_0" #)) -> cred) -> P.do
+            PMap tokenMap <- pmatch tokenMap'
+            pall
+              # plam
+                ( \pair ->
+                    pforgetData (pfstBuiltin # pair) #== pforgetData (pdata cred)
+                )
+              # tokenMap
+      PNothing ->
+        -- No GATs exist at this output!
+        pconstant True
+
+-- | Policy given 'AuthorityToken' params.
+authorityTokenPolicy ::
+  AuthorityToken ->
+  Term s (PData :--> PScriptContext :--> PUnit)
+authorityTokenPolicy params =
+  plam $ \_redeemer ctx' ->
+    pmatch ctx' $ \(PScriptContext ctx') -> P.do
+      ctx <- pletFields @'["txInfo", "purpose"] ctx'
+      PTxInfo txInfo' <- pmatch $ pfromData ctx.txInfo
+      txInfo <- pletFields @'["inputs", "mint"] txInfo'
+      let inputs = txInfo.inputs
+      let authorityTokenInputs =
+            pfoldr' @PBuiltinList
+              ( \txInInfo' acc -> P.do
+                  PTxInInfo txInInfo <- pmatch (pfromData txInInfo')
+                  PTxOut txOut' <- pmatch $ pfromData $ pfield @"resolved" # txInInfo
+                  txOut <- pletFields @'["value"] txOut'
+                  let txOutValue = pfromData txOut.value
+                  passetClassValueOf' params.authority # txOutValue + acc
+              )
+              # 0
+              # inputs
+      let mintedValue = pfromData txInfo.mint
+      let tokenMoved = 0 #< authorityTokenInputs
+      PMinting ownSymbol' <- pmatch $ pfromData ctx.purpose
+      let ownSymbol = pfromData $ pfield @"_0" # ownSymbol'
+      let mintedATs = passetClassValueOf # ownSymbol # pconstant "" # mintedValue
+      pif
+        (0 #< mintedATs)
+        ( P.do
+            passert "Parent token did not move in minting GATs" tokenMoved
+            passert "All outputs only emit valid GATs" $
+              allOutputs @PUnit # pfromData ctx.txInfo #$ plam $ \txOut _value _address _datum ->
+                authorityTokensValidIn
+                  # ownSymbol
+                  # txOut
+            pconstant ()
+        )
+        (pconstant ())

agora/Agora/SafeMoney.hs

@@ -0,0 +1,113 @@
+{- |
+Module     : Agora.SafeMoney
+Maintainer : emi@haskell.fyi
+Description: Phantom-type protected types for handling money in Plutus.
+
+Phantom-type protected types for handling money in Plutus.
+-}
+module Agora.SafeMoney (
+  -- * Types
+  MoneyClass,
+  PDiscrete,
+
+  -- * Utility functions
+  paddDiscrete,
+
+  -- * Conversions
+  pdiscreteValue,
+  pvalueDiscrete,
+
+  -- * Example MoneyClasses
+  LQ,
+  ADA,
+) where
+
+import Data.Proxy (Proxy (Proxy))
+import Data.String
+import GHC.TypeLits (
+  KnownSymbol,
+  Nat,
+  Symbol,
+  symbolVal,
+ )
+import Prelude
+
+--------------------------------------------------------------------------------
+
+import Plutarch.Api.V1 (PValue)
+import Plutarch.Builtin ()
+import Plutarch.Internal ()
+import Plutarch.Monadic qualified as P
+
+--------------------------------------------------------------------------------
+
+import Agora.Utils
+
+--------------------------------------------------------------------------------
+
+-- | Type-level unique identifier for an `AssetClass`
+type MoneyClass =
+  ( -- AssetClass
+    Symbol
+  , -- TokenName
+    Symbol
+  , -- Decimal places
+    Nat
+  )
+
+-- | A `PDiscrete` amount of currency tagged on the type level with the `MoneyClass` it belong sto
+newtype PDiscrete (mc :: MoneyClass) (s :: S)
+  = PDiscrete (Term s PInteger)
+  deriving (PlutusType, PIsData, PEq, POrd) via (DerivePNewtype (PDiscrete mc) PInteger)
+
+-- | Add two `PDiscrete` values of the same `MoneyClass`.
+paddDiscrete :: Term s (PDiscrete mc :--> PDiscrete mc :--> PDiscrete mc)
+paddDiscrete = phoistAcyclic $
+  -- In the future, this should use plutarch-numeric
+  plam $ \x y -> P.do
+    PDiscrete x' <- pmatch x
+    PDiscrete y' <- pmatch y
+    pcon (PDiscrete $ x' + y')
+
+-- | The MoneyClass of LQ.
+type LQ :: MoneyClass
+type LQ = '("da8c30857834c6ae7203935b89278c532b3995245295456f993e1d24", "LQ", 6)
+
+-- | The MoneyClass of ADA.
+type ADA :: MoneyClass
+type ADA = '("", "", 6)
+
+--------------------------------------------------------------------------------
+
+-- | Downcast a `PValue` to a `PDiscrete` unit.
+pvalueDiscrete ::
+  forall (moneyClass :: MoneyClass) (ac :: Symbol) (n :: Symbol) (scale :: Nat) s.
+  ( KnownSymbol ac
+  , KnownSymbol n
+  , moneyClass ~ '(ac, n, scale)
+  ) =>
+  Term s (PValue :--> PDiscrete moneyClass)
+pvalueDiscrete = phoistAcyclic $
+  plam $ \f ->
+    pcon . PDiscrete $
+      passetClassValueOf # pconstant (fromString $ symbolVal $ Proxy @ac)
+        # pconstant (fromString $ symbolVal $ Proxy @n)
+        # f
+
+{- | Get a `PValue` from a `PDiscrete`.
+     __NOTE__: `pdiscreteValue` after `pvalueDiscrete` is loses information
+-}
+pdiscreteValue ::
+  forall (moneyClass :: MoneyClass) (ac :: Symbol) (n :: Symbol) (scale :: Nat) s.
+  ( KnownSymbol ac
+  , KnownSymbol n
+  , moneyClass ~ '(ac, n, scale)
+  ) =>
+  Term s (PDiscrete moneyClass :--> PValue)
+pdiscreteValue = phoistAcyclic $
+  plam $ \f -> pmatch f $ \case
+    PDiscrete p ->
+      psingletonValue
+        # pconstant (fromString $ symbolVal $ Proxy @ac)
+        # pconstant (fromString $ symbolVal $ Proxy @n)
+        # p

agora/Agora/SafeMoney/QQ.hs

@@ -0,0 +1,96 @@
+{-# LANGUAGE TemplateHaskell #-}
+
+{- |
+Module     : Agora.SafeMoney.QQ
+Maintainer : emi@haskell.fyi
+Description: Quasiquoter for SafeMoney types.
+
+Quasiquoter for SafeMoney types.
+-}
+module Agora.SafeMoney.QQ (discrete) where
+
+import GHC.Real (Ratio ((:%)))
+import Language.Haskell.TH qualified as TH (Type)
+import Language.Haskell.TH.Quote (QuasiQuoter (QuasiQuoter))
+import Language.Haskell.TH.Syntax (
+  Dec (TySynD),
+  Exp (AppE, AppTypeE, LitE, VarE),
+  Info (TyConI),
+  Lit (IntegerL),
+  Pat,
+  Q,
+  TyLit (NumTyLit, StrTyLit),
+  Type (AppT, ConT, LitT, PromotedTupleT),
+  lookupTypeName,
+  reify,
+ )
+import Text.ParserCombinators.ReadP (readP_to_S, skipSpaces)
+import Text.Read (lexP, readPrec_to_P)
+import Text.Read.Lex (Lexeme (Ident, Number), Number, numberToFixed, numberToRational)
+import Prelude
+
+--------------------------------------------------------------------------------
+
+import Plutarch.Internal (punsafeCoerce)
+
+import Agora.SafeMoney (MoneyClass, PDiscrete)
+
+--------------------------------------------------------------------------------
+
+{- | Generate 'PDiscrete' values tagged by a particular MoneyClass
+
+@
+  [discrete| 123.456 ADA |] :: 'Term' s ('PDiscrete' 'ADA')
+@
+-}
+discrete :: QuasiQuoter
+discrete = QuasiQuoter discreteExp errorDiscretePat errorDiscreteType errorDiscreteDiscretelaration
+
+discreteConstant :: forall (moneyClass :: MoneyClass) s. Integer -> Term s (PDiscrete moneyClass)
+discreteConstant n = punsafeCoerce (pconstant n :: Term s PInteger)
+
+fixedToInteger :: Integer -> (Integer, Integer) -> Integer
+fixedToInteger places (i, f) = i * 10 ^ places + f
+
+safeIntegerUpcast :: Integer -> Number -> Either String Integer
+safeIntegerUpcast places num =
+  case (numberToFixed places num, numberToRational num * 10 ^ places) of
+    (Just (i, f), _n :% 1) ->
+      Right $ fixedToInteger places (i, f)
+    (Just (i, f), _n :% _d) ->
+      Left $ "Using more than the available decimal places (" <> show places <> "). Would round to " <> show i <> "." <> show f
+    _ -> Left "Some error occurred while getting number"
+
+discreteExp :: String -> Q Exp
+discreteExp s = case parseDiscreteRatioExp s of
+  Nothing ->
+    fail $ "Input malformed. Got: " <> s
+  Just (num, mc) -> do
+    mcName <-
+      lookupTypeName mc >>= \case
+        Nothing -> fail $ "MoneyClass with the name " <> show mc <> " is not in scope."
+        Just v -> pure v
+    reified <- reify mcName
+    case reified of
+      TyConI (TySynD tyName [] (AppT (AppT (AppT (PromotedTupleT 3) (LitT (StrTyLit _))) (LitT _)) (LitT (NumTyLit n)))) ->
+        case safeIntegerUpcast n num of
+          Right i ->
+            pure $ AppE (AppTypeE (VarE 'discreteConstant) (ConT tyName)) (LitE (IntegerL i))
+          Left e -> fail e
+      ty' -> fail $ "Could not reify type, got: " <> show ty'
+
+parseDiscreteRatioExp :: String -> Maybe (Number, String)
+parseDiscreteRatioExp s =
+  let p = skipSpaces *> ((,) <$> readPrec_to_P lexP 0 <* skipSpaces <*> readPrec_to_P lexP 0) <* skipSpaces
+   in case readP_to_S p s of
+        [((Number n, Ident i), "")] -> Just (n, i)
+        _ -> Nothing
+
+errorDiscretePat :: String -> Q Pat
+errorDiscretePat _ = fail "Cannot use 'discrete' in a pattern context."
+
+errorDiscreteType :: String -> Q TH.Type
+errorDiscreteType _ = fail "Cannot use 'discrete' in a type context."
+
+errorDiscreteDiscretelaration :: String -> Q [Dec]
+errorDiscreteDiscretelaration _ = fail "Cannot use 'discrete' in a declaration context."

agora/Agora/Stake.hs

@@ -0,0 +1,268 @@
+{- |
+Module     : Agora.Stake
+Maintainer : emi@haskell.fyi
+Description: Vote-lockable stake UTXOs holding GT.
+
+Vote-lockable stake UTXOs holding GT.
+-}
+module Agora.Stake (
+  PStakeDatum (..),
+  PStakeAction (..),
+  Stake (..),
+  stakePolicy,
+  stakeValidator,
+  stakeLocked,
+) where
+
+--------------------------------------------------------------------------------
+
+import GHC.Generics qualified as GHC
+import GHC.TypeLits (
+  KnownSymbol,
+ )
+import Generics.SOP (Generic, I (I))
+import Prelude
+
+--------------------------------------------------------------------------------
+
+import Plutarch (popaque)
+import Plutarch.Api.V1 (
+  PCredential (PPubKeyCredential, PScriptCredential),
+  PMintingPolicy,
+  PPubKeyHash,
+  PScriptPurpose (PMinting, PSpending),
+  PValidator,
+  mintingPolicySymbol,
+  mkMintingPolicy,
+ )
+import Plutarch.DataRepr (
+  PDataFields,
+  PIsDataReprInstances (PIsDataReprInstances),
+ )
+import Plutarch.Internal (punsafeCoerce)
+import Plutarch.Monadic qualified as P
+
+--------------------------------------------------------------------------------
+
+import Agora.SafeMoney (
+  MoneyClass,
+  PDiscrete,
+  paddDiscrete,
+  pdiscreteValue,
+ )
+import Agora.Utils (
+  anyInput,
+  anyOutput,
+  paddValue,
+  passert,
+  pfindTxInByTxOutRef,
+  psingletonValue,
+  psymbolValueOf,
+  ptxSignedBy,
+  pvalueSpent,
+ )
+
+--------------------------------------------------------------------------------
+
+-- | Parameters for creating Stake scripts.
+data Stake (gt :: MoneyClass) = Stake
+
+-- | Plutarch-level redeemer for Stake scripts.
+data PStakeAction (gt :: MoneyClass) (s :: S)
+  = -- | Deposit or withdraw a discrete amount of the staked governance token.
+    PDepositWithdraw (Term s (PDataRecord '["delta" ':= PDiscrete gt]))
+  | -- | Destroy a stake, retrieving its LQ, the minimum ADA and any other assets.
+    PDestroy (Term s (PDataRecord '[]))
+  deriving stock (GHC.Generic)
+  deriving anyclass (Generic)
+  deriving anyclass (PIsDataRepr)
+  deriving
+    (PlutusType, PIsData)
+    via PIsDataReprInstances (PStakeAction gt)
+
+-- | Plutarch-level datum for Stake scripts.
+newtype PStakeDatum (gt :: MoneyClass) (s :: S) = PStakeDatum
+  { getStakeDatum ::
+    Term s (PDataRecord '["stakedAmount" ':= PDiscrete gt, "owner" ':= PPubKeyHash])
+  }
+  deriving stock (GHC.Generic)
+  deriving anyclass (Generic)
+  deriving anyclass (PIsDataRepr)
+  deriving
+    (PlutusType, PIsData, PDataFields)
+    via (PIsDataReprInstances (PStakeDatum gt))
+
+--------------------------------------------------------------------------------
+{- What this Policy does
+
+   For minting:
+     Check that exactly one state thread is minted
+     Check that an output exists with a state thread and a valid datum
+     Check that no state thread is an input
+     assert TokenName == ValidatorHash of the script that we pay to
+
+   For burning:
+     Check that exactly one state thread is burned
+     Check that datum at state thread is valid and not locked
+-}
+--------------------------------------------------------------------------------
+
+-- | Policy for Stake state threads.
+stakePolicy ::
+  forall (gt :: MoneyClass) ac n scale s.
+  ( KnownSymbol ac
+  , KnownSymbol n
+  , gt ~ '(ac, n, scale)
+  ) =>
+  Stake gt ->
+  Term s PMintingPolicy
+stakePolicy _stake =
+  plam $ \_redeemer ctx' -> P.do
+    ctx <- pletFields @'["txInfo", "purpose"] ctx'
+    txInfo' <- plet ctx.txInfo
+    txInfo <- pletFields @'["mint", "inputs", "outputs"] txInfo'
+
+    PMinting ownSymbol' <- pmatch $ pfromData ctx.purpose
+    ownSymbol <- plet $ pfield @"_0" # ownSymbol'
+    spentST <- plet $ psymbolValueOf # ownSymbol #$ pvalueSpent # pfromData txInfo'
+    mintedST <- plet $ psymbolValueOf # ownSymbol # txInfo.mint
+
+    let burning = P.do
+          passert "ST at inputs must be 1" $
+            spentST #== 1
+
+          passert "ST burned" $
+            mintedST #== -1
+
+          passert "An unlocked input existed containing an ST" $
+            anyInput @(PStakeDatum gt) # pfromData txInfo'
+              #$ plam
+              $ \value _ stakeDatum' -> P.do
+                let hasST = psymbolValueOf # ownSymbol # value #== 1
+                let unlocked = pnot # (stakeLocked # stakeDatum')
+                hasST #&& unlocked
+
+          popaque (pconstant ())
+
+    let minting = P.do
+          passert "ST at inputs must be 0" $
+            spentST #== 0
+
+          passert "Minted ST must be exactly 1" $
+            mintedST #== 1
+
+          passert "A UTXO must exist with the correct output" $
+            anyOutput @(PStakeDatum gt) # pfromData txInfo'
+              #$ plam
+              $ \value address stakeDatum' -> P.do
+                let cred = pfield @"credential" # address
+                pmatch cred $ \case
+                  -- Should pay to a script address
+                  PPubKeyCredential _ -> pcon PFalse
+                  PScriptCredential validatorHash' -> P.do
+                    validatorHash <- pletFields @'["_0"] validatorHash'
+                    stakeDatum <- pletFields @'["owner", "stakedAmount"] stakeDatum'
+                    let stValue =
+                          psingletonValue
+                            # ownSymbol
+                            -- This coerce is safe because the structure
+                            -- of PValidatorHash is the same as PTokenName.
+                            # punsafeCoerce validatorHash._0
+                            # 1
+                    let expectedValue =
+                          paddValue
+                            # (pdiscreteValue # stakeDatum.stakedAmount)
+                            # stValue
+                    let ownerSignsTransaction =
+                          ptxSignedBy
+                            # ctx.txInfo
+                            # stakeDatum.owner
+
+                    -- TODO: Needs to be >=, rather than ==
+                    let valueCorrect = pdata value #== pdata expectedValue
+                    ownerSignsTransaction #&& valueCorrect
+
+          popaque (pconstant ())
+
+    pif (0 #< mintedST) minting burning
+
+--------------------------------------------------------------------------------
+
+-- | Validator intended for Stake UTXOs to live in.
+stakeValidator ::
+  forall (gt :: MoneyClass) ac n scale s.
+  ( KnownSymbol ac
+  , KnownSymbol n
+  , gt ~ '(ac, n, scale)
+  ) =>
+  Stake gt ->
+  Term s PValidator
+stakeValidator stake =
+  plam $ \datum redeemer ctx' -> P.do
+    ctx <- pletFields @'["txInfo", "purpose"] ctx'
+    txInfo' <- plet ctx.txInfo
+    txInfo <- pletFields @'["mint", "inputs", "outputs"] txInfo'
+
+    -- Coercion is safe in that if coercion fails we crash hard.
+    let stakeAction :: Term _ (PStakeAction gt)
+        stakeAction = pfromData $ punsafeCoerce redeemer
+        stakeDatum' :: Term _ (PStakeDatum gt)
+        stakeDatum' = pfromData $ punsafeCoerce datum
+    stakeDatum <- pletFields @'["owner", "stakedAmount"] stakeDatum'
+
+    PSpending txOutRef <- pmatch $ pfromData ctx.purpose
+
+    PJust txInInfo <- pmatch $ pfindTxInByTxOutRef # (pfield @"_0" # txOutRef) # txInfo'
+    ownAddress <- plet $ pfield @"address" #$ pfield @"resolved" # txInInfo
+    let continuingValue = pfield @"value" #$ pfield @"resolved" # txInInfo
+    ownerSignsTransaction <- plet $ ptxSignedBy # ctx.txInfo # stakeDatum.owner
+    stCurrencySymbol <- plet $ pconstant $ mintingPolicySymbol $ mkMintingPolicy (stakePolicy stake)
+    mintedST <- plet $ psymbolValueOf # stCurrencySymbol # txInfo.mint
+    spentST <- plet $ psymbolValueOf # stCurrencySymbol #$ pvalueSpent # txInfo'
+
+    pmatch stakeAction $ \case
+      PDestroy _ -> P.do
+        passert "ST at inputs must be 1" $
+          spentST #== 1
+        passert "Should burn ST" $
+          mintedST #== -1
+        passert "Stake unlocked" $
+          pnot #$ stakeLocked # stakeDatum'
+        passert
+          "Owner signs this transaction"
+          ownerSignsTransaction
+        popaque (pconstant ())
+      PDepositWithdraw r -> P.do
+        passert "ST at inputs must be 1" $
+          spentST #== 1
+        passert "Stake unlocked" $
+          pnot #$ stakeLocked # stakeDatum'
+        passert
+          "Owner signs this transaction"
+          ownerSignsTransaction
+        passert "A UTXO must exist with the correct output" $
+          anyOutput @(PStakeDatum gt) # txInfo'
+            #$ plam
+            $ \value address newStakeDatum' -> P.do
+              newStakeDatum <- pletFields @'["owner", "stakedAmount"] newStakeDatum'
+              delta <- plet $ pfield @"delta" # r
+              let isScriptAddress = pdata address #== ownAddress
+              let correctOutputDatum =
+                    stakeDatum.owner #== newStakeDatum.owner
+                      #&& (paddDiscrete # stakeDatum.stakedAmount # delta) #== newStakeDatum.stakedAmount
+              let expectedValue = paddValue # continuingValue # (pdiscreteValue # delta)
+
+              -- TODO: As above, needs to be >=, rather than ==
+              let correctValue = pdata value #== pdata expectedValue
+              isScriptAddress #&& correctOutputDatum #&& correctValue
+
+        popaque (pconstant ())
+
+--------------------------------------------------------------------------------
+
+-- | Check whether a Stake is locked. If it is locked, various actions are unavailable.
+stakeLocked :: forall (gt :: MoneyClass) s. Term s (PStakeDatum gt :--> PBool)
+stakeLocked = phoistAcyclic $
+  plam $ \_stakeDatum ->
+    -- TODO: when we extend this to support proposals, this will need to do something
+    pcon PFalse

agora/Agora/Treasury.hs

@@ -0,0 +1,100 @@
+{- |
+Module: Agora.Treasury
+Maintainer: jack@mlabs.city
+Description: Treasury scripts.
+
+Contains the datum, redeemer and validator for a template DAO
+treasury.
+-}
+module Agora.Treasury (module Agora.Treasury) where
+
+import GHC.Generics qualified as GHC
+import Generics.SOP
+import Plutarch.Api.V1.Contexts (PScriptContext, PScriptPurpose (PMinting))
+import Plutarch.Api.V1.Value (PCurrencySymbol, PValue)
+import Plutarch.DataRepr (
+  PDataFields,
+  PIsDataReprInstances (PIsDataReprInstances),
+ )
+import Plutarch.Monadic qualified as P
+import Plutus.V1.Ledger.Value (CurrencySymbol)
+
+--------------------------------------------------------------------------------
+
+import Agora.AuthorityToken (authorityTokensValidIn)
+import Agora.Utils (allInputs, passert, psymbolValueOf)
+
+{- | Validator ensuring that transactions consuming the treasury
+     do so in a valid manner.
+-}
+treasuryV ::
+  forall {s :: S}.
+  CurrencySymbol ->
+  Term
+    s
+    ( PAsData PTreasuryDatum
+        :--> PAsData PTreasuryRedeemer
+        :--> PAsData PScriptContext
+        :--> PUnit
+    )
+treasuryV cs = plam $ \_d r ctx' -> P.do
+  -- plet required fields from script context.
+  ctx <- pletFields @["txInfo", "purpose"] ctx'
+
+  -- Ensure that script is for burning i.e. minting a negative amount.
+  PMinting _ <- pmatch ctx.purpose
+
+  -- Ensure redeemer type is valid.
+  PAlterTreasuryParams _ <- pmatch $ pfromData r
+
+  -- Get the minted value from txInfo.
+  txInfo' <- plet ctx.txInfo
+  txInfo <- pletFields @'["mint"] txInfo'
+  let mint :: Term s PValue
+      mint = txInfo.mint
+      gatAmountMinted :: Term s PInteger
+      gatAmountMinted = psymbolValueOf # pconstant cs # mint
+
+  passert "GAT not burned." $ gatAmountMinted #== -1
+
+  passert "All inputs only have valid GATs" $
+    allInputs @PUnit # pfromData ctx.txInfo #$ plam $ \txOut _value _address _datum ->
+      authorityTokensValidIn
+        # pconstant cs
+        # txOut
+
+  pconstant ()
+
+{- | Plutarch level type representing datum of the treasury.
+     Contains:
+
+       - @stateThread@ representing the asset class of the
+         treasury's state thread token.
+-}
+newtype PTreasuryDatum (s :: S)
+  = PTreasuryDatum
+      ( Term
+          s
+          ( PDataRecord
+              '[ "stateThread" ':= PCurrencySymbol
+               ]
+          )
+      )
+  deriving stock (GHC.Generic)
+  deriving anyclass (Generic, PIsDataRepr)
+  deriving
+    (PlutusType, PIsData, PDataFields)
+    via PIsDataReprInstances PTreasuryDatum
+
+{- | Plutarch level type representing valid redeemers of the
+     treasury.
+-}
+newtype PTreasuryRedeemer (s :: S)
+  = -- | Alters treasury parameters, subject to the burning of a
+    --   governance authority token.
+    PAlterTreasuryParams (Term s (PDataRecord '[]))
+  deriving stock (GHC.Generic)
+  deriving anyclass (Generic, PIsDataRepr)
+  deriving
+    (PlutusType, PIsData)
+    via PIsDataReprInstances PTreasuryRedeemer

agora/Agora/Utils.hs

@@ -0,0 +1,364 @@
+{- |
+Module     : Agora.Utils
+Maintainer : emi@haskell.fyi
+Description: Plutarch utility functions that should be upstreamed or don't belong anywhere else.
+
+Plutarch utility functions that should be upstreamed or don't belong anywhere else.
+-}
+module Agora.Utils (
+  -- * Validator-level utility functions
+  passert,
+  pfind',
+  pfindDatum,
+  pfindDatum',
+  pvalueSpent,
+  ptxSignedBy,
+  paddValue,
+  plookup,
+  pfromMaybe,
+  psymbolValueOf,
+  passetClassValueOf,
+  passetClassValueOf',
+  pfindTxInByTxOutRef,
+  psingletonValue,
+  pfindMap,
+
+  -- * Functions which should (probably) not be upstreamed
+  anyOutput,
+  allOutputs,
+  anyInput,
+  allInputs,
+) where
+
+--------------------------------------------------------------------------------
+
+import Plutus.V1.Ledger.Value (AssetClass (..))
+
+--------------------------------------------------------------------------------
+
+import Plutarch.Api.V1 (
+  PAddress,
+  PCurrencySymbol,
+  PDatum,
+  PDatumHash,
+  PMap (PMap),
+  PMaybeData (PDJust),
+  PPubKeyHash,
+  PTokenName,
+  PTuple,
+  PTxInInfo (PTxInInfo),
+  PTxInfo (PTxInfo),
+  PTxOut (PTxOut),
+  PTxOutRef,
+  PValue (PValue),
+ )
+import Plutarch.Builtin (ppairDataBuiltin)
+import Plutarch.Internal (punsafeCoerce)
+import Plutarch.Monadic qualified as P
+
+--------------------------------------------------------------------------------
+-- Validator-level utility functions
+
+-- | Assert a particular 'PBool', trace if false. Use in monadic context.
+passert :: Term s PString -> Term s PBool -> Term s k -> Term s k
+passert errorMessage check k = pif check k (ptraceError errorMessage)
+
+-- | Find a datum with the given hash.
+pfindDatum :: Term s (PDatumHash :--> PTxInfo :--> PMaybe PDatum)
+pfindDatum = phoistAcyclic $
+  plam $ \datumHash txInfo'' -> P.do
+    PTxInfo txInfo' <- pmatch txInfo''
+    plookupTuple # datumHash #$ pfield @"data" # txInfo'
+
+{- | Find a datum with the given hash.
+NOTE: this is unsafe in the sense that, if the data layout is wrong, this is UB.
+-}
+pfindDatum' :: PIsData a => Term s (PDatumHash :--> PTxInfo :--> PMaybe (PAsData a))
+pfindDatum' = phoistAcyclic $ plam $ \dh x -> punsafeCoerce $ pfindDatum # dh # x
+
+-- | Check if a PubKeyHash signs this transaction.
+ptxSignedBy :: Term s (PTxInfo :--> PAsData PPubKeyHash :--> PBool)
+ptxSignedBy = phoistAcyclic $
+  plam $ \txInfo' pkh -> P.do
+    txInfo <- pletFields @'["signatories"] txInfo'
+    pelem @PBuiltinList # pkh # txInfo.signatories
+
+-- | 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
+
+-- | Escape with a particular value on expecting 'Just'. For use in monadic context.
+pexpectJust ::
+  forall r a s.
+  Term s r ->
+  Term s (PMaybe a) ->
+  (Term s a -> Term s r) ->
+  Term s r
+pexpectJust escape ma f =
+  pmatch ma $ \case
+    PJust v -> f v
+    PNothing -> escape
+
+-- | Get the sum of all values belonging to a particular CurrencySymbol.
+psymbolValueOf :: Term s (PCurrencySymbol :--> PValue :--> PInteger)
+psymbolValueOf =
+  phoistAcyclic $
+    plam $ \sym value'' -> P.do
+      PValue value' <- pmatch value''
+      PMap value <- pmatch value'
+      m' <- pexpectJust 0 (plookup # pdata sym # value)
+      PMap m <- pmatch (pfromData m')
+      pfoldr # plam (\x v -> pfromData (psndBuiltin # x) + v) # 0 # m
+
+-- | Extract amount from PValue belonging to a Plutarch-level asset class.
+passetClassValueOf ::
+  Term s (PCurrencySymbol :--> PTokenName :--> PValue :--> PInteger)
+passetClassValueOf =
+  phoistAcyclic $
+    plam $ \sym token value'' -> P.do
+      PValue value' <- pmatch value''
+      PMap value <- pmatch value'
+      m' <- pexpectJust 0 (plookup # pdata sym # value)
+      PMap m <- pmatch (pfromData m')
+      v <- pexpectJust 0 (plookup # pdata token # m)
+      pfromData v
+
+-- | Extract amount from PValue belonging to a Haskell-level AssetClass.
+passetClassValueOf' :: AssetClass -> Term s (PValue :--> PInteger)
+passetClassValueOf' (AssetClass (sym, token)) =
+  passetClassValueOf # pconstant sym # pconstant token
+
+-- | Union two maps using a merge function on collisions.
+pmapUnionWith :: forall k v s. PIsData v => Term s ((v :--> v :--> v) :--> PMap k v :--> PMap k v :--> PMap k v)
+pmapUnionWith = phoistAcyclic $
+  -- TODO: this function is kinda suspect. I feel like a lot of optimizations could be done here
+  plam $ \f xs' ys' -> P.do
+    PMap xs <- pmatch xs'
+    PMap ys <- pmatch ys'
+    let ls =
+          pmap
+            # plam
+              ( \p -> P.do
+                  pf <- plet $ pfstBuiltin # p
+                  ps <- plet $ psndBuiltin # p
+                  pmatch (plookup # pf # ys) $ \case
+                    PJust v ->
+                      -- Data conversions here are silly, aren't they?
+                      ppairDataBuiltin # pf # pdata (f # pfromData ps # pfromData v)
+                    PNothing -> p
+              )
+            # xs
+        rs =
+          pfilter
+            # plam
+              ( \p ->
+                  pnot #$ pany # plam (\p' -> pfstBuiltin # p' #== pfstBuiltin # p) # xs
+              )
+            # ys
+    pcon (PMap $ pconcat # ls # rs)
+
+-- | Add two 'PValue's together
+paddValue :: forall s. Term s (PValue :--> PValue :--> PValue)
+paddValue = phoistAcyclic $
+  plam $ \a' b' -> P.do
+    PValue a <- pmatch a'
+    PValue b <- pmatch b'
+    pcon
+      ( PValue $
+          pmapUnionWith # plam (\a' b' -> pmapUnionWith # plam (+) # a' # b') # a # b
+      )
+
+-- | Sum of all value at input.
+pvalueSpent :: Term s (PTxInfo :--> PValue)
+pvalueSpent = phoistAcyclic $
+  plam $ \txInfo' ->
+    pmatch txInfo' $ \(PTxInfo txInfo) ->
+      pfoldr
+        # plam
+          ( \txInInfo' v ->
+              pmatch
+                (pfromData txInInfo')
+                $ \(PTxInInfo txInInfo) ->
+                  paddValue
+                    # pmatch
+                      (pfield @"resolved" # txInInfo)
+                      (\(PTxOut o) -> pfromData $ pfield @"value" # o)
+                    # v
+          )
+        # pconstant mempty
+        # (pfield @"inputs" # txInfo)
+
+-- | Find the TxInInfo by a TxOutRef.
+pfindTxInByTxOutRef :: Term s (PTxOutRef :--> PTxInfo :--> PMaybe PTxInInfo)
+pfindTxInByTxOutRef = phoistAcyclic $
+  plam $ \txOutRef txInfo' ->
+    pmatch txInfo' $ \(PTxInfo txInfo) ->
+      pfindMap
+        # plam
+          ( \txInInfo' ->
+              plet (pfromData txInInfo') $ \r ->
+                pmatch r $ \(PTxInInfo txInInfo) ->
+                  pif
+                    (pdata txOutRef #== pfield @"outRef" # txInInfo)
+                    (pcon (PJust r))
+                    (pcon PNothing)
+          )
+        #$ (pfield @"inputs" # txInfo)
+
+--------------------------------------------------------------------------------
+{- Functions which should (probably) not be upstreamed
+   All of these functions are quite inefficient.
+-}
+
+-- | Check if any output matches the predicate.
+anyOutput ::
+  forall (datum :: PType) s.
+  ( PIsData datum
+  ) =>
+  Term s (PTxInfo :--> (PValue :--> PAddress :--> datum :--> PBool) :--> PBool)
+anyOutput = phoistAcyclic $
+  plam $ \txInfo' predicate -> P.do
+    txInfo <- pletFields @'["outputs"] txInfo'
+    pany
+      # plam
+        ( \txOut'' -> P.do
+            PTxOut txOut' <- pmatch (pfromData txOut'')
+            txOut <- pletFields @'["value", "datumHash", "address"] txOut'
+            PDJust dh <- pmatch txOut.datumHash
+            pmatch (pfindDatum' @datum # (pfield @"_0" # dh) # txInfo') $ \case
+              PJust datum -> P.do
+                predicate # txOut.value # txOut.address # pfromData datum
+              PNothing -> pcon PFalse
+        )
+      # pfromData txInfo.outputs
+
+-- | Check if all outputs match the predicate.
+allOutputs ::
+  forall (datum :: PType) s.
+  ( PIsData datum
+  ) =>
+  Term s (PTxInfo :--> (PTxOut :--> PValue :--> PAddress :--> datum :--> PBool) :--> PBool)
+allOutputs = phoistAcyclic $
+  plam $ \txInfo' predicate -> P.do
+    txInfo <- pletFields @'["outputs"] txInfo'
+    pall
+      # plam
+        ( \txOut'' -> P.do
+            PTxOut txOut' <- pmatch (pfromData txOut'')
+            txOut <- pletFields @'["value", "datumHash", "address"] txOut'
+            PDJust dh <- pmatch txOut.datumHash
+            pmatch (pfindDatum' @datum # (pfield @"_0" # dh) # txInfo') $ \case
+              PJust datum -> P.do
+                predicate # pfromData txOut'' # txOut.value # txOut.address # pfromData datum
+              PNothing -> pcon PFalse
+        )
+      # pfromData txInfo.outputs
+
+-- | Check if any (resolved) input matches the predicate.
+anyInput ::
+  forall (datum :: PType) s.
+  ( PIsData datum
+  ) =>
+  Term s (PTxInfo :--> (PValue :--> PAddress :--> datum :--> PBool) :--> PBool)
+anyInput = phoistAcyclic $
+  plam $ \txInfo' predicate -> P.do
+    txInfo <- pletFields @'["inputs"] txInfo'
+    pany
+      # plam
+        ( \txInInfo'' -> P.do
+            PTxInInfo txInInfo' <- pmatch (pfromData txInInfo'')
+            let txOut'' = pfield @"resolved" # txInInfo'
+            PTxOut txOut' <- pmatch (pfromData txOut'')
+            txOut <- pletFields @'["value", "datumHash", "address"] txOut'
+            PDJust dh <- pmatch txOut.datumHash
+            pmatch (pfindDatum' @datum # (pfield @"_0" # dh) # txInfo') $ \case
+              PJust datum -> P.do
+                predicate # txOut.value # txOut.address # pfromData datum
+              PNothing -> pcon PFalse
+        )
+      # pfromData txInfo.inputs
+
+-- | Check if all (resolved) inputs match the predicate.
+allInputs ::
+  forall (datum :: PType) s.
+  ( PIsData datum
+  ) =>
+  Term s (PTxInfo :--> (PTxOut :--> PValue :--> PAddress :--> datum :--> PBool) :--> PBool)
+allInputs = phoistAcyclic $
+  plam $ \txInfo' predicate -> P.do
+    txInfo <- pletFields @'["inputs"] txInfo'
+    pall
+      # plam
+        ( \txInInfo'' -> P.do
+            PTxInInfo txInInfo' <- pmatch (pfromData txInInfo'')
+            let txOut'' = pfield @"resolved" # txInInfo'
+            PTxOut txOut' <- pmatch (pfromData txOut'')
+            txOut <- pletFields @'["value", "datumHash", "address"] txOut'
+            PDJust dh <- pmatch txOut.datumHash
+            pmatch (pfindDatum' @datum # (pfield @"_0" # dh) # txInfo') $ \case
+              PJust datum -> P.do
+                predicate # pfromData txOut'' # txOut.value # txOut.address # pfromData datum
+              PNothing -> pcon PFalse
+        )
+      # pfromData txInfo.inputs
+
+-- | Create a value with a single asset class.
+psingletonValue :: forall s. Term s (PCurrencySymbol :--> PTokenName :--> PInteger :--> PValue)
+psingletonValue = phoistAcyclic $
+  plam $ \sym tok int ->
+    let innerTup = pcon $ PMap $ psingleton #$ ppairDataBuiltin # pdata tok # pdata int
+        outerTup = pcon $ PMap $ psingleton #$ ppairDataBuiltin # pdata sym # pdata innerTup
+        res = pcon $ PValue outerTup
+     in res

agora/Agora/Utils/Value.hs

@@ -0,0 +1,93 @@
+{-# OPTIONS_GHC -Wno-unused-imports #-}
+{-# OPTIONS_GHC -Wno-unused-top-binds #-}
+
+module Agora.Utils.Value (pgeq, pleq, pgt, plt) where
+
+import Plutarch.Api.V1.AssocMap (PMap (PMap))
+import Plutarch.Api.V1.These (PTheseData (..))
+import Plutarch.Api.V1.Tuple (ptupleFromBuiltin)
+import Plutarch.Api.V1.Value (PCurrencySymbol, PTokenName, PValue)
+import Plutarch.Lift (PUnsafeLiftDecl)
+import Plutarch.List (pconvertLists)
+import Plutarch.Monadic qualified as P
+
+punionVal ::
+  Term
+    s
+    ( PValue
+        :--> PValue
+        :--> PMap
+              PCurrencySymbol
+              (PMap PTokenName (PTheseData PInteger PInteger))
+    )
+punionVal = undefined
+
+-- | Determines if a condition is true for all values in a map.
+pmapAll ::
+  (PUnsafeLiftDecl v, PIsData v) =>
+  Term s ((v :--> PBool) :--> PMap k v :--> PBool)
+pmapAll = plam $ \f m -> P.do
+  PMap builtinMap <- pmatch m
+
+  let getV = plam $ \bip -> P.do
+        let tuple = pfromData $ ptupleFromBuiltin (pdata bip)
+        pfromData $ pfield @"_1" # tuple
+
+  let vs = pmap # getV # builtinMap
+  pall # f # vs
+
+pcheckPred ::
+  forall {s :: S}.
+  Term
+    s
+    ( (PTheseData PInteger PInteger :--> PBool)
+        :--> PValue
+        :--> PValue
+        :--> PBool
+    )
+pcheckPred = plam $ \_f _l _r -> P.do
+  undefined
+
+--  let inner :: Term s (PMap PTokenName (PTheseData PInteger PInteger) :--> PBool)
+--      inner = pmapAll # f
+--  pmapAll # inner # (punionVal # l # r)
+
+pcheckBinRel ::
+  forall {s :: S}.
+  Term
+    s
+    ( (PInteger :--> PInteger :--> PBool)
+        :--> PValue
+        :--> PValue
+        :--> PBool
+    )
+pcheckBinRel = plam $ \f l r -> P.do
+  let unThese :: Term s (PTheseData PInteger PInteger :--> PBool)
+      unThese = plam $ \k' ->
+        pmatch k' $ \case
+          PDThis r -> f # (pfield @"_0" # r) # 0
+          PDThat r -> f # 0 # (pfield @"_0" # r)
+          PDThese r -> f # (pfield @"_0" # r) # (pfield @"_1" # r)
+  pcheckPred # unThese # l # r
+
+-- | Establishes if a value is less than or equal to another.
+pleq :: Term s (PValue :--> PValue :--> PBool)
+pleq = plam $ \v0 v1 -> (pcheckBinRel # pleq') # v0 # v1
+
+pleq' :: Term s (PInteger :--> PInteger :--> PBool)
+pleq' = plam $ \m n -> m #<= n
+
+-- | Establishes if a value is strictly less than another.
+plt :: Term s (PValue :--> PValue :--> PBool)
+plt = plam $ \v0 v1 -> (pcheckBinRel # plt') # v0 # v1
+
+plt' :: Term s (PInteger :--> PInteger :--> PBool)
+plt' = plam $ \m n -> m #< n
+
+-- | Establishes if a value is greater than or equal to another.
+pgeq :: Term s (PValue :--> PValue :--> PBool)
+pgeq = plam $ \v0 v1 -> pnot #$ plt # v0 # v1
+
+-- | Establishes if a value is strictly greater than another.
+pgt :: Term s (PValue :--> PValue :--> PBool)
+pgt = plam $ \v0 v1 -> pnot #$ pleq # v0 # v1

agora/Agora/Voting.hs

@@ -0,0 +1,11 @@
+{- |
+Module     : Agora.Voting
+Maintainer : emi@haskell.fyi
+Description: Types for votes and vote counting
+-}
+module Agora.Voting (
+  Vote (..),
+) where
+
+-- | Type representing direction of vote.
+data Vote = InFavorOf | OpposedTo

agora/PPrelude.hs

@@ -0,0 +1,7 @@
+module PPrelude (
+  module Prelude,
+  module Plutarch.Prelude,
+) where
+
+import Plutarch.Prelude
+import Prelude

agora/Plutarch/Api/V1/These.hs

@@ -0,0 +1,62 @@
+{-# OPTIONS_GHC -Wno-orphans #-}
+
+module Plutarch.Api.V1.These (PTheseData (..)) where
+
+import GHC.Generics qualified as GHC
+import Generics.SOP
+import Plutarch.DataRepr (PIsDataReprInstances (PIsDataReprInstances))
+import Plutarch.Lift (
+  PConstantRepr,
+  PConstanted,
+  PLifted,
+  PUnsafeLiftDecl,
+  pconstantFromRepr,
+  pconstantToRepr,
+ )
+import Plutus.V1.Ledger.Api qualified as Plutus
+import PlutusTx.These qualified as PlutusThese
+
+data PTheseData (a :: PType) (b :: PType) (s :: S)
+  = PDThis (Term s (PDataRecord '["_0" ':= a]))
+  | PDThat (Term s (PDataRecord '["_0" ':= b]))
+  | PDThese (Term s (PDataRecord '["_0" ':= a, "_1" ':= b]))
+  deriving stock (GHC.Generic)
+  deriving anyclass (Generic, PIsDataRepr)
+  deriving
+    (PlutusType, PIsData)
+    via PIsDataReprInstances (PTheseData a b)
+
+instance
+  ( Plutus.ToData (PLifted a)
+  , Plutus.ToData (PLifted b)
+  , Plutus.FromData (PLifted a)
+  , Plutus.FromData (PLifted b)
+  , PLift a
+  , PLift b
+  ) =>
+  PUnsafeLiftDecl (PTheseData a b)
+  where
+  type PLifted (PTheseData a b) = PlutusThese.These (PLifted a) (PLifted b)
+
+{- TODO: Make PTheseData an instance of PConstant:
+         https://github.com/Plutonomicon/plutarch/pull/355
+-}
+
+instance
+  ( PLifted (PConstanted a) ~ a
+  , Plutus.ToData b
+  , Plutus.FromData b
+  , Plutus.ToData a
+  , Plutus.FromData a
+  , PConstant a
+  , PLifted (PConstanted b) ~ b
+  , Plutus.FromData b
+  , Plutus.ToData b
+  , PConstant b
+  ) =>
+  PConstant (PlutusThese.These a b)
+  where
+  type PConstantRepr (PlutusThese.These a b) = [(Plutus.Data, Plutus.Data)]
+  type PConstanted (PlutusThese.These a b) = PTheseData (PConstanted a) (PConstanted b)
+  pconstantToRepr _t = undefined
+  pconstantFromRepr _t = undefined

agora/Plutarch/These.hs

@@ -0,0 +1,12 @@
+module Plutarch.These (PThese (..)) where
+
+import GHC.Generics qualified as GHC
+import Generics.SOP
+
+-- | Plutus These type with Scott-encoded representation.
+data PThese (a :: PType) (b :: PType) (s :: S)
+  = PThis (Term s a)
+  | PThat (Term s b)
+  | PThese (Term s a) (Term s b)
+  deriving stock (GHC.Generic)
+  deriving anyclass (Generic, PlutusType)