Tickets.hs

-- SPDX-FileCopyrightText: 2021 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

{-# OPTIONS_GHC -Wno-orphans #-}
{-# OPTIONS_GHC -Wno-unused-do-bind #-}
{-# LANGUAGE RebindableSyntax #-}
{-# LANGUAGE NoApplicativeDo #-}

{- | Extended support for the tickets feature.

This module has to be imported explicitly, it is not re-exported by "Lorentz".

The primary use case for tickets: authorization tokens for specific actions.
For instance, in @Pause@ entrypoint a contract may accept a ticket, checking
that it is emitted from the administrator address.
The mechanism of tickets is more flexible than 'sender' and 'source' instructions:

* a ticket can be carried through an arbitrary chain of intermediate agents;
* it can permit a limited number of certain actions;
* tickets may have a restricted set of authorized actions.

More details below.

The amount of tokens in a ticket may stand for a number of allowed actions
invocations, in this case accepted tickets are checked to contain just @1@ token.
This semantics makes sense, taking @SPLIT_TICKET@ and @JOIN_TICKETS@ instructions
into account, and also the fact that tickets are not dupable.

One important precaution to be kept in mind is that an emitted ticket must
permit exactly one kind of action in exactly one contract. This way the ticket
emitter can be sure that his ticket cannot be used in an unexpected way.
We see two main approaches to this:

* Make the data carried by the ticket identify the target contract and the
action that is being permitted. The contract has to verify the data in the
ticket.

* Make tickets carry as little data as possible, and instead let the main
authorized entity keep a single tickets emitting contract per target contract
per action (the latter is optional). This way, the burden of separating
tickets' area of applicability lies on that main authorized entity instead of
the target contract, but actions become cheaper.

Some examples of use cases:

* An administrator may emit a ticket that permits some delegate to pause the
  contract.
  In this case, the ticket should carry a description of the pausing
  capability (string or enum value) and permission's expiry time.

  It is also easy to share admin privileges among other participants by
  providing them with a ticket with a very large tokens amount.
  The target contract does not even need to know about many administrators
  being involved.

* A user may wish to delegate some actions to an intermediate service.
  In this case, tickets can serve as signatures made on behalf of the user's
  contract, with replay protection provided out-of-the-box.

  Note that at the moment of writing, implicit addresses cannot serve as ticket
  emitters.

* The allowances mechanism known by FA1.2/FA2 may be replaced with tickets.
  In this case, the tokens amount in a ticket will correspond to the amount of
  tokens that can be spent by an operator.

This module provides helpers to cover the mentioned cases.

-}
module Lorentz.Tickets
  ( -- * Actions authorization
    authorizeAction

    -- * Ticket data verification
  , verifyTargetContract
  , verifyTargetContractAnd

    -- * Tokens spending authorization
  , STicket (..)
  , toSTicket
  , coerceUnwrap

    -- ** Permitted tokens arithmetics
  , readSTicket
  , sTicketAmount
  , subtractSTicket
  , subtractSTicketPlain
  , addSTicket
  , addSTicketPlain

    -- * Generic tickets verification
  , verifyTicketGeneric
  , verifyTicketGeneric'
  , verifyTicketer
  ) where

import Prelude (Generic, Typeable, ($))
import Prelude qualified as P

import Lorentz.ADT
import Lorentz.Annotation
import Lorentz.Base
import Lorentz.Coercions
import Lorentz.Constraints
import Lorentz.Doc
import Lorentz.Errors
import Lorentz.Expr
import Lorentz.Instr
import Lorentz.Macro
import Lorentz.Rebinded
import Lorentz.Value
import Morley.Michelson.Typed.Haskell.Doc
import Morley.Util.Markdown

-- Common errors
----------------------------------------------------------------------------

type instance ErrorArg "wRONG_TICKETER" = NoErrorArg

instance CustomErrorHasDoc "wRONG_TICKETER" where
  customErrClass = ErrClassActionException
  customErrDocMdCause = "Ticket emitted by the wrong entity."

type instance ErrorArg "nOT_TICKET_TARGET" = NoErrorArg

instance CustomErrorHasDoc "nOT_TICKET_TARGET" where
  customErrClass = ErrClassBadArgument
  customErrDocMdCause =
    "Data in the ticket tells that it is intended for a different contract."

type instance ErrorArg "nOT_SINGLE_TICKET_TOKEN" = NoErrorArg

instance CustomErrorHasDoc "nOT_SINGLE_TICKET_TOKEN" where
  customErrClass = ErrClassBadArgument
  customErrDocMdCause =
    "This action expected a ticket with exactly one token."

----------------------------------------------------------------------------
-- Tickets verification
----------------------------------------------------------------------------

-- | Verifies a ticket.
--
-- This is an extremely generified 'verifyTicketGeneric', allows providing
-- verifiers for all the ticket's parts. Provided just in case.
verifyTicketGeneric'
  :: (IsoValue td)
  => (forall s0. Address : Address : s0 :-> s0)
      -- ^ Ticket emitter verifier
  -> (forall s0. Natural : s0 :-> s0)
      -- ^ Ticket tokens verifier
  -> td : s :-> s'
      -- ^ Ticket data verifier
  -> TAddress emitterParam vd : Ticket td : s :-> Ticket td : s'
verifyTicketGeneric' verifyTicketer' verifyTokens verifyData = do
  dip do
    readTicket; swap; dip deconstruct
  swap; dip @(Ticket _) $ do
    checkedCoerce_; verifyTicketer'
    swap
    verifyTokens
    verifyData

-- | Generic method for verifying tickets that authorize some action.
--
-- For concrete example of use see 'authorizeAction'.
verifyTicketGeneric
  :: (IsoValue td)
  => (forall s0. Natural : s0 :-> s0)  -- ^ Ticket tokens verifier
  -> td : s :-> s'                     -- ^ Ticket data verifier
  -> TAddress emitterParam vd : Ticket td : s :-> Ticket td : s'
verifyTicketGeneric = verifyTicketGeneric' verifyTicketer

-- | Generic method for verifying the ticketer.
verifyTicketer :: Address : Address : s :-> s
verifyTicketer = if IsEq then nop else failCustomNoArg #wRONG_TICKETER

-- Helpers for checking tickets that remember their target contract
----------------------------------------------------------------------------

-- | Check data in a ticket when it carries target contract address and some
-- other data that is to be verified with the given handler.
verifyTargetContractAnd
  :: (d : s :-> s')
  -> (TAddress selfParam vd, d) : s :-> s'
verifyTargetContractAnd verifyData = do
  unpair; verifyTargetContract; verifyData

-- | Check data in a ticket when it solely carries target contract address.
verifyTargetContract :: TAddress selfParam vd : s :-> s
verifyTargetContract =
  if checkedCoerce_ |==| selfAddress
  then nop
  else failCustomNoArg #nOT_TICKET_TARGET

-- Tickets for actions
----------------------------------------------------------------------------

-- | Verifies the given ticket value that permits running an action.
--
-- 1. Ticketer is checked to match the given address.
-- 2. Tokens amount in the ticket is checked to be equal to @1@.
-- 3. Ticket data is checked with the provided handler.
--    In case the data contains target contract, consider using
--    'verifyTargetContract' or 'verifyTargetContractAnd'.
authorizeAction
  :: (IsoValue td)
  => (td : s :-> s')
  -> TAddress emitterParam vd : Ticket td : s :-> s'
authorizeAction verifyTicketData = do
  verifyTicketGeneric
    verifySingleToken
    verifyTicketData
  drop
  where
    verifySingleToken :: Natural : s :-> s
    verifySingleToken =
      if take |==| push 1
      then nop
      else failCustomNoArg #nOT_SINGLE_TICKET_TOKEN

-- Tickets for tokens
----------------------------------------------------------------------------

-- | A ticket kept in storage.
--
-- The common pattern of use here is
-- 1. A ticket that permits spending few tokens comes in, it is partially
--    validated and this 'STicket' type is produced.
-- 2. This type can repeatedly be used to consume up to the amount of permitted
--    tokens.
--
-- So in order to count allowed tokens, in storage you usually put this type,
-- not bare 'Ticket'.
--
-- The @action@ type parameter serves to distinguish tickets for different
-- actions at type level and usually just matches the value in ticket data:
--
-- * If the data in ticket is validated to be @"pause"@, then the result of
--   validation can be @STicket "pause" ...@; This is the preferred
--   option.
-- * If the data in ticket has enum type, and the value is validated to be
--   some @PauseAction@, then validation can produce
--   @STicket PauseAction ...@.
--
-- CAUTION: when working with this type, you __must__ ensure that the
-- expected ticket emitter (the one you validate tickets against, e.g. admin
-- address) is __constant__ for the lifetime of the 'STicket' value.
-- Otherwise, tickets arithmetics (provided via methods below) won't work.
-- So do one of
--
-- * Either never change the expected ticket emitter;
-- * Or, when it is changed, wipe all the 'STicket' values validated
--   against the old ticketer from storage;
-- * Or keep ticket values in a map where key is the currently expected
--   ticket emitter.
--
-- Note some specificity of this type - its values mostly always appear
-- optionally, either in a map, or in 'Maybe' (this is clear from the
-- potential use cases).
newtype STicket (action :: k) td = STicket (Ticket td)
  deriving stock (Generic)
  deriving anyclass (Unwrappable)

deriving newtype instance
  NiceComparable td =>
  IsoValue (STicket action td)
deriving newtype instance
  (HasAnnotation td, NiceComparable td) =>
  HasAnnotation (STicket action td)

instance (a `CanCastTo` a2, td `CanCastTo` td2) =>
         STicket a td `CanCastTo` STicket a2 td2

instance (NiceComparable d, Typeable k, Typeable action) =>
          NonZero (STicket (action :: k) d) where
  nonZero = do coerceUnwrap; nonZero; lmap unsafeCoerceWrap

instance (Typeable k, Typeable action, TypeHasDoc td) =>
         TypeHasDoc (STicket (action :: k) td) where
  typeDocMdDescription = [md|
    Ticket kept in storage that remembers permissions to spend something.

    The first type argument describes the kind of action or currency that is
    being permitted to perform/spend.
    |]
  typeDocMdReference p =
    customTypeDocMdReference' ("STicket", DType p)
      [ \wp -> mdTicked $ buildTypeWithinParens @action wp
      , typeDocMdReference (P.Proxy @td)
      ]
  typeDocDependencies _ = [dTypeDep @(Ticket Natural)]
  typeDocHaskellRep =
    -- Have to use unsafe version since kinds of @action@ and @"myTokens"@
    -- are different
    unsafeConcreteTypeDocHaskellRep @(STicket "myTokens" Natural)
  typeDocMichelsonRep =
    unsafeConcreteTypeDocMichelsonRep @(STicket "myTokens" Natural)

-- | Constructs an 'STicket'.
--
-- This also emits the ticketer address and ticket data for further use.
-- You are oblidged to do something with both of them:
--
-- * Either validate against the expected value, you can use 'verifyTicketer',
--   'verifyTargetContract' and 'verifyTargetContractAnd' helpers here.
-- * Or use as key in a map where 'STicket' should be put to as a value.
--
-- This way you can be sure that arithmetics on @STickets@ works smoothly
-- and there are no, for instance, attempts to join two tickets from different
-- emitters.
toSTicket
  :: (IsoValue td)
  => Ticket td : s
  :-> Address : td : STicket action td : s
toSTicket = do
  readTicket
  dip unsafeCoerceWrap
  deconstruct
  dipN @2 drop

-- | Read contents of 'STicket'.
readSTicket
  :: STicket action td : s
  :-> ReadTicket td : STicket action td : s
readSTicket = do
  coerceUnwrap; readTicket; dip unsafeCoerceWrap

-- | Read tokens amount in 'STicket'.
sTicketAmount
  :: (IsoValue td)
  => Maybe (STicket action td) : s
  :-> Natural : s
sTicketAmount =
  if IsSome then sTicketAmountPlain else push 0

-- | Version of 'sTicketAmount' that works without @Maybe@.
sTicketAmountPlain
  :: (IsoValue td)
  => STicket action td : s
  :-> Natural : s
sTicketAmountPlain = do
  readSTicket; toField #rtAmount; dip drop

-- | Consume given amount of tokens from the ticket, failing with given handler
-- if amount of tokens in the ticket is insufficient.
--
-- We do not provide a ready error for this case since it will probably depend
-- on particular tokens that the given @STicket@ serves to permit.
--
-- Note that you may want to run @isSome nonZero none@ on the result to save
-- storage space.
subtractSTicket
  :: (IsoValue d, KnownValue (STicket action d))
  => (forall s0. ErrInstr (("permitted" :! Natural, "spent" :! Natural) : s0))
  -> Natural : Maybe (STicket action d) : s
  :-> Maybe (STicket action d) : s
subtractSTicket onInsufficientTokens = do
  swap
  if IsNone
  then do drop @Natural; none
  else do swap; subtractSTicketPlain onInsufficientTokens; some

-- | Similar to 'subtractSTicket', but without @Maybe@.
--
-- You may want to run 'nonZero' after this function call to save
-- storage space.
subtractSTicketPlain
  :: (IsoValue d)
  => (forall s0. ErrInstr (("permitted" :! Natural, "spent" :! Natural) : s0))
  -> Natural : STicket action d : s
  :-> STicket action d : s
subtractSTicketPlain onInsufficientTokens = do
  toNamed #spent
  dip do
    coerceUnwrap;
    readTicket; toField #rtAmount; toNamed #permitted
  swap; dupTop2
  isNat $: (fromNamed #permitted |-| fromNamed #spent)
  if IsSome
    then do toNamed #remainder; dip $ drop @("permitted" :! _)
    else do pair; onInsufficientTokens
  pair; swap; splitTicketNamed
  assertSome (Impossible @"by construction of token parts")
  car; fromNamed #remainder
  unsafeCoerceWrap

-- | Adds tokens permitted by an incoming ticket.
--
-- Useful when someone permits you to spend even more tokens than you already
-- have been allowed to spend.
--
-- This assumes that the ticket being added has already been verified.
-- The passed tickets must be verified against the same ticket data and ticket
-- emitter.
addSTicket
  :: STicket action d : Maybe (STicket action d) : s
  :-> Maybe (STicket action d) : s
addSTicket = do
  swap; ifSome addSTicketPlain nop; some

-- | Similar to 'addSTicket', but without @Maybe@.
addSTicketPlain
  :: STicket action d : STicket action d : s
  :-> STicket action d : s
addSTicketPlain = do
  coerceUnwrap; dip coerceUnwrap
  pair; joinTickets
  assertSome [mt|badtjoin|]
  unsafeCoerceWrap