-- SPDX-FileCopyrightText: 2021 Tocqueville Group
--
-- SPDX-License-Identifier: LicenseRef-MIT-TQ

{-# 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 qualified Prelude 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 :: ErrorClass
customErrClass = ErrorClass
ErrClassActionException
  customErrDocMdCause :: Markdown
customErrDocMdCause = Markdown
"Ticket emitted by the wrong entity."

type instance ErrorArg "nOT_TICKET_TARGET" = NoErrorArg

instance CustomErrorHasDoc "nOT_TICKET_TARGET" where
  customErrClass :: ErrorClass
customErrClass = ErrorClass
ErrClassBadArgument
  customErrDocMdCause :: Markdown
customErrDocMdCause =
    Markdown
"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 :: ErrorClass
customErrClass = ErrorClass
ErrClassBadArgument
  customErrDocMdCause :: Markdown
customErrDocMdCause =
    Markdown
"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 : Ticket td : s :-> Ticket td : s'
verifyTicketGeneric' :: (forall (s0 :: [*]). (Address : Address : s0) :-> s0)
-> (forall (s0 :: [*]). (Natural : s0) :-> s0)
-> ((td : s) :-> s')
-> (TAddress emitterParam : Ticket td : s) :-> (Ticket td : s')
verifyTicketGeneric' forall (s0 :: [*]). (Address : Address : s0) :-> s0
verifyTicketer' forall (s0 :: [*]). (Natural : s0) :-> s0
verifyTokens (td : s) :-> s'
verifyData = do
  ((Ticket td : s) :-> (Ticket td : Address : td : Natural : s))
-> (TAddress emitterParam : Ticket td : s)
   :-> (TAddress emitterParam
          : Ticket td : Address : td : Natural : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip do
    (Ticket td : s) :-> (ReadTicket td : Ticket td : s)
forall a (s :: [*]).
(Ticket a : s) :-> (ReadTicket a : Ticket a : s)
readTicket; (ReadTicket td : Ticket td : s) :-> (Ticket td : ReadTicket td : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap; ((ReadTicket td : s) :-> (Address : td : Natural : s))
-> (Ticket td : ReadTicket td : s)
   :-> (Ticket td : Address : td : Natural : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (ReadTicket td : s) :-> (Address : td : Natural : s)
forall dt (fields :: [*]) (st :: [*]).
(InstrDeconstructC dt, KnownList fields,
 fields ~ ConstructorFieldTypes dt) =>
(dt : st) :-> (fields ++ st)
deconstruct
  (TAddress emitterParam : Ticket td : Address : td : Natural : s)
:-> (Ticket td
       : TAddress emitterParam : Address : td : Natural : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap; forall (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (Ticket td : s) :-> (Ticket td : s')
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip @(Ticket _) (((TAddress emitterParam : Address : td : Natural : s) :-> s')
 -> (Ticket td : TAddress emitterParam : Address : td : Natural : s)
    :-> (Ticket td : s'))
-> ((TAddress emitterParam : Address : td : Natural : s) :-> s')
-> (Ticket td : TAddress emitterParam : Address : td : Natural : s)
   :-> (Ticket td : s')
forall a b. (a -> b) -> a -> b
$ do
    (TAddress emitterParam : Address : td : Natural : s)
:-> (Address : Address : td : Natural : s)
forall a b (s :: [*]). Castable_ a b => (a : s) :-> (b : s)
checkedCoerce_; (Address : Address : td : Natural : s) :-> (td : Natural : s)
forall (s0 :: [*]). (Address : Address : s0) :-> s0
verifyTicketer'
    (td : Natural : s) :-> (Natural : td : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap
    (Natural : td : s) :-> (td : s)
forall (s0 :: [*]). (Natural : s0) :-> s0
verifyTokens
    (td : s) :-> s'
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 : Ticket td : s :-> Ticket td : s'
verifyTicketGeneric :: (forall (s0 :: [*]). (Natural : s0) :-> s0)
-> ((td : s) :-> s')
-> (TAddress emitterParam : Ticket td : s) :-> (Ticket td : s')
verifyTicketGeneric = (forall (s0 :: [*]). (Address : Address : s0) :-> s0)
-> (forall (s0 :: [*]). (Natural : s0) :-> s0)
-> ((td : s) :-> s')
-> (TAddress emitterParam : Ticket td : s) :-> (Ticket td : s')
forall td (s :: [*]) (s' :: [*]) emitterParam.
IsoValue td =>
(forall (s0 :: [*]). (Address : Address : s0) :-> s0)
-> (forall (s0 :: [*]). (Natural : s0) :-> s0)
-> ((td : s) :-> s')
-> (TAddress emitterParam : Ticket td : s) :-> (Ticket td : s')
verifyTicketGeneric' forall (s0 :: [*]). (Address : Address : s0) :-> s0
verifyTicketer

-- | Generic method for verifying the ticketer.
verifyTicketer :: Address : Address : s :-> s
verifyTicketer :: (Address : Address : s) :-> s
verifyTicketer = if Condition (Address : Address : s) s s s s
forall a (s :: [*]) (o :: [*]).
NiceComparable a =>
Condition (a : a : s) s s o o
IsEq then s :-> s
forall (s :: [*]). s :-> s
nop else Label "wRONG_TICKETER" -> s :-> s
forall (tag :: Symbol) (s :: [*]) (any :: [*]).
(MustHaveErrorArg tag MText, CustomErrorHasDoc tag) =>
Label tag -> s :-> any
failCustomNoArg Label "wRONG_TICKETER"
forall a. IsLabel "wRONG_TICKETER" a => a
forall (x :: Symbol) a. IsLabel x a => a
#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, d) : s :-> s'
verifyTargetContractAnd :: ((d : s) :-> s') -> ((TAddress selfParam, d) : s) :-> s'
verifyTargetContractAnd (d : s) :-> s'
verifyData = do
  ((TAddress selfParam, d) : s) :-> (TAddress selfParam : d : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : b : s)
unpair; (TAddress selfParam : d : s) :-> (d : s)
forall selfParam (s :: [*]). (TAddress selfParam : s) :-> s
verifyTargetContract; (d : s) :-> s'
verifyData

-- | Check data in a ticket when it solely carries target contract address.
verifyTargetContract :: TAddress selfParam : s :-> s
verifyTargetContract :: (TAddress selfParam : s) :-> s
verifyTargetContract =
  if (TAddress selfParam : s) :-> (Address : s)
forall a b (s :: [*]). Castable_ a b => (a : s) :-> (b : s)
checkedCoerce_ ((TAddress selfParam : s) :-> (Address : s))
-> Expr s s Address -> Expr (TAddress selfParam : s) s Bool
forall a (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
NiceComparable a =>
Expr s0 s1 a -> Expr s1 s2 a -> Expr s0 s2 Bool
|==| Expr s s Address
forall (s :: [*]). s :-> (Address : s)
selfAddress
  then s :-> s
forall (s :: [*]). s :-> s
nop
  else Label "nOT_TICKET_TARGET" -> s :-> s
forall (tag :: Symbol) (s :: [*]) (any :: [*]).
(MustHaveErrorArg tag MText, CustomErrorHasDoc tag) =>
Label tag -> s :-> any
failCustomNoArg Label "nOT_TICKET_TARGET"
forall a. IsLabel "nOT_TICKET_TARGET" a => a
forall (x :: Symbol) a. IsLabel x a => a
#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 : Ticket td : s :-> s'
authorizeAction :: ((td : s) :-> s') -> (TAddress emitterParam : Ticket td : s) :-> s'
authorizeAction (td : s) :-> s'
verifyTicketData = do
  (forall (s0 :: [*]). (Natural : s0) :-> s0)
-> ((td : s) :-> s')
-> (TAddress emitterParam : Ticket td : s) :-> (Ticket td : s')
forall td (s :: [*]) (s' :: [*]) emitterParam.
IsoValue td =>
(forall (s0 :: [*]). (Natural : s0) :-> s0)
-> ((td : s) :-> s')
-> (TAddress emitterParam : Ticket td : s) :-> (Ticket td : s')
verifyTicketGeneric
    forall (s0 :: [*]). (Natural : s0) :-> s0
verifySingleToken
    (td : s) :-> s'
verifyTicketData
  (Ticket td : s') :-> s'
forall a (s :: [*]). (a : s) :-> s
drop
  where
    verifySingleToken :: Natural : s :-> s
    verifySingleToken :: (Natural : s) :-> s
verifySingleToken =
      if Expr (Natural : s) s Natural
forall a (s :: [*]). Expr (a : s) s a
take Expr (Natural : s) s Natural
-> Expr s s Natural -> Expr (Natural : s) s Bool
forall a (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
NiceComparable a =>
Expr s0 s1 a -> Expr s1 s2 a -> Expr s0 s2 Bool
|==| Natural -> Expr s s Natural
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push Natural
1
      then s :-> s
forall (s :: [*]). s :-> s
nop
      else Label "nOT_SINGLE_TICKET_TOKEN" -> s :-> s
forall (tag :: Symbol) (s :: [*]) (any :: [*]).
(MustHaveErrorArg tag MText, CustomErrorHasDoc tag) =>
Label tag -> s :-> any
failCustomNoArg Label "nOT_SINGLE_TICKET_TOKEN"
forall a. IsLabel "nOT_SINGLE_TICKET_TOKEN" a => a
forall (x :: Symbol) a. IsLabel x a => a
#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 ((forall x. STicket action td -> Rep (STicket action td) x)
-> (forall x. Rep (STicket action td) x -> STicket action td)
-> Generic (STicket action td)
forall x. Rep (STicket action td) x -> STicket action td
forall x. STicket action td -> Rep (STicket action td) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall k (action :: k) td x.
Rep (STicket action td) x -> STicket action td
forall k (action :: k) td x.
STicket action td -> Rep (STicket action td) x
$cto :: forall k (action :: k) td x.
Rep (STicket action td) x -> STicket action td
$cfrom :: forall k (action :: k) td x.
STicket action td -> Rep (STicket action td) x
Generic)
  deriving anyclass (ToT (STicket action td) ~ ToT (Unwrappabled (STicket action td))
(ToT (STicket action td) ~ ToT (Unwrappabled (STicket action td)))
-> Unwrappable (STicket action td)
forall s. (ToT s ~ ToT (Unwrappabled s)) -> Unwrappable s
forall k (action :: k) td.
ToT (STicket action td) ~ ToT (Unwrappabled (STicket action td))
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 :: (STicket action d : s) :-> (Maybe (STicket action d) : s)
nonZero = do (STicket action d : s) :-> (Ticket d : s)
forall a (s :: [*]).
Unwrappable a =>
(a : s) :-> (Unwrappabled a : s)
coerceUnwrap; (Ticket d : s) :-> (Maybe (Ticket d) : s)
forall t (s :: [*]). NonZero t => (t : s) :-> (Maybe t : s)
nonZero; ((Ticket d : s) :-> (STicket action d : s))
-> (Maybe (Ticket d) : s) :-> (Maybe (STicket action d) : s)
forall (c :: * -> *) b a (s :: [*]).
(LorentzFunctor c, KnownValue b) =>
((a : s) :-> (b : s)) -> (c a : s) :-> (c b : s)
lmap (Ticket d : s) :-> (STicket action d : s)
forall a (s :: [*]).
Unwrappable a =>
(Unwrappabled a : s) :-> (a : s)
unsafeCoerceWrap

instance (Typeable k, Typeable action, TypeHasDoc td) =>
         TypeHasDoc (STicket (action :: k) td) where
  typeDocMdDescription :: Markdown
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 :: Proxy (STicket action td) -> WithinParens -> Markdown
typeDocMdReference Proxy (STicket action td)
p =
    (Text, DType)
-> [WithinParens -> Markdown] -> WithinParens -> Markdown
customTypeDocMdReference' (Text
"STicket", Proxy (STicket action td) -> DType
forall a. TypeHasDoc a => Proxy a -> DType
DType Proxy (STicket action td)
p)
      [ \WithinParens
wp -> Markdown -> Markdown
mdTicked (Markdown -> Markdown) -> Markdown -> Markdown
forall a b. (a -> b) -> a -> b
$ WithinParens -> Markdown
forall k (a :: k). Typeable a => WithinParens -> Markdown
buildTypeWithinParens @action WithinParens
wp
      , Proxy td -> WithinParens -> Markdown
forall a. TypeHasDoc a => Proxy a -> WithinParens -> Markdown
typeDocMdReference (Proxy td
forall k (t :: k). Proxy t
P.Proxy @td)
      ]
  typeDocDependencies :: Proxy (STicket action td) -> [SomeDocDefinitionItem]
typeDocDependencies Proxy (STicket action td)
_ = [TypeHasDoc (Ticket Natural) => SomeDocDefinitionItem
forall t. TypeHasDoc t => SomeDocDefinitionItem
dTypeDep @(Ticket Natural)]
  typeDocHaskellRep :: TypeDocHaskellRep (STicket action td)
typeDocHaskellRep =
    -- Have to use unsafe version since kinds of @action@ and @"myTokens"@
    -- are different
    forall b.
(Typeable (STicket "myTokens" Natural),
 GenericIsoValue (STicket "myTokens" Natural),
 GTypeHasDoc (Rep (STicket "myTokens" Natural))) =>
TypeDocHaskellRep b
forall a b.
(Typeable a, GenericIsoValue a, GTypeHasDoc (Rep a)) =>
TypeDocHaskellRep b
unsafeConcreteTypeDocHaskellRep @(STicket "myTokens" Natural)
  typeDocMichelsonRep :: TypeDocMichelsonRep (STicket action td)
typeDocMichelsonRep =
    forall b.
(Typeable (STicket "myTokens" Natural),
 KnownIsoT (STicket "myTokens" Natural)) =>
TypeDocMichelsonRep b
forall k a (b :: k).
(Typeable a, KnownIsoT a) =>
TypeDocMichelsonRep b
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 :: (Ticket td : s) :-> (Address : td : STicket action td : s)
toSTicket = do
  (Ticket td : s) :-> (ReadTicket td : Ticket td : s)
forall a (s :: [*]).
(Ticket a : s) :-> (ReadTicket a : Ticket a : s)
readTicket
  ((Ticket td : s) :-> (STicket action td : s))
-> (ReadTicket td : Ticket td : s)
   :-> (ReadTicket td : STicket action td : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Ticket td : s) :-> (STicket action td : s)
forall a (s :: [*]).
Unwrappable a =>
(Unwrappabled a : s) :-> (a : s)
unsafeCoerceWrap
  (ReadTicket td : STicket action td : s)
:-> (Address : td : Natural : STicket action td : s)
forall dt (fields :: [*]) (st :: [*]).
(InstrDeconstructC dt, KnownList fields,
 fields ~ ConstructorFieldTypes dt) =>
(dt : st) :-> (fields ++ st)
deconstruct
  ((Natural : STicket action td : s) :-> (STicket action td : s))
-> (Address : td : Natural : STicket action td : s)
   :-> (Address : td : STicket action td : s)
forall (n :: Nat) (inp :: [*]) (out :: [*]) (s :: [*]) (s' :: [*]).
ConstraintDIPNLorentz (ToPeano n) inp out s s' =>
(s :-> s') -> inp :-> out
dipN @2 (Natural : STicket action td : s) :-> (STicket action td : s)
forall a (s :: [*]). (a : s) :-> s
drop

-- | Read contents of 'STicket'.
readSTicket
  :: STicket action td : s
  :-> ReadTicket td : STicket action td : s
readSTicket :: (STicket action td : s) :-> (ReadTicket td : STicket action td : s)
readSTicket = do
  (STicket action td : s) :-> (Ticket td : s)
forall a (s :: [*]).
Unwrappable a =>
(a : s) :-> (Unwrappabled a : s)
coerceUnwrap; (Ticket td : s) :-> (ReadTicket td : Ticket td : s)
forall a (s :: [*]).
(Ticket a : s) :-> (ReadTicket a : Ticket a : s)
readTicket; ((Ticket td : s) :-> (STicket action td : s))
-> (ReadTicket td : Ticket td : s)
   :-> (ReadTicket td : STicket action td : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Ticket td : s) :-> (STicket action td : s)
forall a (s :: [*]).
Unwrappable a =>
(Unwrappabled a : s) :-> (a : s)
unsafeCoerceWrap

-- | Read tokens amount in 'STicket'.
sTicketAmount
  :: (IsoValue td)
  => Maybe (STicket action td) : s
  :-> Natural : s
sTicketAmount :: (Maybe (STicket action td) : s) :-> (Natural : s)
sTicketAmount =
  if Condition
  (Maybe (STicket action td) : s)
  (STicket action td : s)
  s
  (Natural : s)
  (Natural : s)
forall a (s :: [*]) (o :: [*]).
Condition (Maybe a : s) (a : s) s o o
IsSome then (STicket action td : s) :-> (Natural : s)
forall k td (action :: k) (s :: [*]).
IsoValue td =>
(STicket action td : s) :-> (Natural : s)
sTicketAmountPlain else Natural -> s :-> (Natural : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push Natural
0

-- | Version of 'sTicketAmount' that works without @Maybe@.
sTicketAmountPlain
  :: (IsoValue td)
  => STicket action td : s
  :-> Natural : s
sTicketAmountPlain :: (STicket action td : s) :-> (Natural : s)
sTicketAmountPlain = do
  (STicket action td : s) :-> (ReadTicket td : STicket action td : s)
forall k (action :: k) td (s :: [*]).
(STicket action td : s) :-> (ReadTicket td : STicket action td : s)
readSTicket; Label "rtAmount"
-> (ReadTicket td : STicket action td : s)
   :-> (GetFieldType (ReadTicket td) "rtAmount"
          : STicket action td : s)
forall dt (name :: Symbol) (st :: [*]).
InstrGetFieldC dt name =>
Label name -> (dt : st) :-> (GetFieldType dt name : st)
toField Label "rtAmount"
forall a. IsLabel "rtAmount" a => a
forall (x :: Symbol) a. IsLabel x a => a
#rtAmount; ((STicket action td : s) :-> s)
-> (Natural : STicket action td : s) :-> (Natural : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (STicket action td : s) :-> s
forall a (s :: [*]). (a : s) :-> s
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 :: (forall (s0 :: [*]).
 ErrInstr (("permitted" :! Natural, "spent" :! Natural) : s0))
-> (Natural : Maybe (STicket action d) : s)
   :-> (Maybe (STicket action d) : s)
subtractSTicket forall (s0 :: [*]).
ErrInstr (("permitted" :! Natural, "spent" :! Natural) : s0)
onInsufficientTokens = do
  (Natural : Maybe (STicket action d) : s)
:-> (Maybe (STicket action d) : Natural : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap
  if Condition
  (Maybe (STicket action d) : Natural : s)
  (Natural : s)
  (STicket action d : Natural : s)
  (Maybe (STicket action d) : s)
  (Maybe (STicket action d) : s)
forall a (s :: [*]) (o :: [*]).
Condition (Maybe a : s) s (a : s) o o
IsNone
  then do forall (s0 :: [*]). (Natural : s0) :-> s0
forall a (s :: [*]). (a : s) :-> s
drop @Natural; s :-> (Maybe (STicket action d) : s)
forall a (s :: [*]). KnownValue a => s :-> (Maybe a : s)
none
  else do (STicket action d : Natural : s)
:-> (Natural : STicket action d : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap; (forall (s0 :: [*]).
 ErrInstr (("permitted" :! Natural, "spent" :! Natural) : s0))
-> (Natural : STicket action d : s) :-> (STicket action d : s)
forall k d (action :: k) (s :: [*]).
IsoValue d =>
(forall (s0 :: [*]).
 ErrInstr (("permitted" :! Natural, "spent" :! Natural) : s0))
-> (Natural : STicket action d : s) :-> (STicket action d : s)
subtractSTicketPlain forall (s0 :: [*]).
ErrInstr (("permitted" :! Natural, "spent" :! Natural) : s0)
onInsufficientTokens; (STicket action d : s) :-> (Maybe (STicket action d) : s)
forall a (s :: [*]). (a : s) :-> (Maybe a : s)
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 :: (forall (s0 :: [*]).
 ErrInstr (("permitted" :! Natural, "spent" :! Natural) : s0))
-> (Natural : STicket action d : s) :-> (STicket action d : s)
subtractSTicketPlain forall (s0 :: [*]).
ErrInstr (("permitted" :! Natural, "spent" :! Natural) : s0)
onInsufficientTokens = do
  Label "spent"
-> (Natural : STicket action d : s)
   :-> (("spent" :! Natural) : STicket action d : s)
forall (name :: Symbol) a (s :: [*]).
Label name -> (a : s) :-> ((name :! a) : s)
toNamed Label "spent"
forall a. IsLabel "spent" a => a
forall (x :: Symbol) a. IsLabel x a => a
#spent
  ((STicket action d : s)
 :-> (("permitted" :! Natural) : Ticket d : s))
-> (("spent" :! Natural) : STicket action d : s)
   :-> (("spent" :! Natural)
          : ("permitted" :! Natural) : Ticket d : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip do
    (STicket action d : s) :-> (Ticket d : s)
forall a (s :: [*]).
Unwrappable a =>
(a : s) :-> (Unwrappabled a : s)
coerceUnwrap;
    (Ticket d : s) :-> (ReadTicket d : Ticket d : s)
forall a (s :: [*]).
(Ticket a : s) :-> (ReadTicket a : Ticket a : s)
readTicket; Label "rtAmount"
-> (ReadTicket d : Ticket d : s)
   :-> (GetFieldType (ReadTicket d) "rtAmount" : Ticket d : s)
forall dt (name :: Symbol) (st :: [*]).
InstrGetFieldC dt name =>
Label name -> (dt : st) :-> (GetFieldType dt name : st)
toField Label "rtAmount"
forall a. IsLabel "rtAmount" a => a
forall (x :: Symbol) a. IsLabel x a => a
#rtAmount; Label "permitted"
-> (Natural : Ticket d : s)
   :-> (("permitted" :! Natural) : Ticket d : s)
forall (name :: Symbol) a (s :: [*]).
Label name -> (a : s) :-> ((name :! a) : s)
toNamed Label "permitted"
forall a. IsLabel "permitted" a => a
forall (x :: Symbol) a. IsLabel x a => a
#permitted
  (("spent" :! Natural) : ("permitted" :! Natural) : Ticket d : s)
:-> (("permitted" :! Natural)
       : ("spent" :! Natural) : Ticket d : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap; (("permitted" :! Natural) : ("spent" :! Natural) : Ticket d : s)
:-> (("permitted" :! Natural)
       : ("spent" :! Natural) : ("permitted" :! Natural)
       : ("spent" :! Natural) : Ticket d : s)
forall a b (s :: [*]).
(Dupable a, Dupable b) =>
(a : b : s) :-> (a : b : a : b : s)
dupTop2
  forall (s :: [*]). (Integer : s) :-> (Maybe Natural : s)
isNat (forall (s :: [*]). (Integer : s) :-> (Maybe Natural : s))
-> Expr
     (("permitted" :! Natural)
        : ("spent" :! Natural) : ("permitted" :! Natural)
        : ("spent" :! Natural) : Ticket d : s)
     (("permitted" :! Natural) : ("spent" :! Natural) : Ticket d : s)
     Integer
-> Expr
     (("permitted" :! Natural)
        : ("spent" :! Natural) : ("permitted" :! Natural)
        : ("spent" :! Natural) : Ticket d : s)
     (("permitted" :! Natural) : ("spent" :! Natural) : Ticket d : s)
     (Maybe Natural)
forall a r (s0 :: [*]) (s1 :: [*]).
(forall (s :: [*]). (a : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s0 s1 r
$: (Label "permitted"
-> (("permitted" :! Natural)
      : ("spent" :! Natural) : ("permitted" :! Natural)
      : ("spent" :! Natural) : Ticket d : s)
   :-> (Natural
          : ("spent" :! Natural) : ("permitted" :! Natural)
          : ("spent" :! Natural) : Ticket d : s)
forall (name :: Symbol) a (s :: [*]).
Label name -> ((name :! a) : s) :-> (a : s)
fromNamed Label "permitted"
forall a. IsLabel "permitted" a => a
forall (x :: Symbol) a. IsLabel x a => a
#permitted ((("permitted" :! Natural)
    : ("spent" :! Natural) : ("permitted" :! Natural)
    : ("spent" :! Natural) : Ticket d : s)
 :-> (Natural
        : ("spent" :! Natural) : ("permitted" :! Natural)
        : ("spent" :! Natural) : Ticket d : s))
-> Expr
     (("spent" :! Natural)
        : ("permitted" :! Natural) : ("spent" :! Natural) : Ticket d : s)
     (("permitted" :! Natural) : ("spent" :! Natural) : Ticket d : s)
     Natural
-> Expr
     (("permitted" :! Natural)
        : ("spent" :! Natural) : ("permitted" :! Natural)
        : ("spent" :! Natural) : Ticket d : s)
     (("permitted" :! Natural) : ("spent" :! Natural) : Ticket d : s)
     Integer
forall a b r (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
ArithOpHs Sub a b r =>
Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
|-| Label "spent"
-> Expr
     (("spent" :! Natural)
        : ("permitted" :! Natural) : ("spent" :! Natural) : Ticket d : s)
     (("permitted" :! Natural) : ("spent" :! Natural) : Ticket d : s)
     Natural
forall (name :: Symbol) a (s :: [*]).
Label name -> ((name :! a) : s) :-> (a : s)
fromNamed Label "spent"
forall a. IsLabel "spent" a => a
forall (x :: Symbol) a. IsLabel x a => a
#spent)
  if Condition
  (Maybe Natural
     : ("permitted" :! Natural) : ("spent" :! Natural) : Ticket d : s)
  (Natural
     : ("permitted" :! Natural) : ("spent" :! Natural) : Ticket d : s)
  (("permitted" :! Natural) : ("spent" :! Natural) : Ticket d : s)
  (("remainder" :! Natural) : ("spent" :! Natural) : Ticket d : s)
  (("remainder" :! Natural) : ("spent" :! Natural) : Ticket d : s)
forall a (s :: [*]) (o :: [*]).
Condition (Maybe a : s) (a : s) s o o
IsSome
    then do Label "remainder"
-> (Natural
      : ("permitted" :! Natural) : ("spent" :! Natural) : Ticket d : s)
   :-> (("remainder" :! Natural)
          : ("permitted" :! Natural) : ("spent" :! Natural) : Ticket d : s)
forall (name :: Symbol) a (s :: [*]).
Label name -> (a : s) :-> ((name :! a) : s)
toNamed Label "remainder"
forall a. IsLabel "remainder" a => a
forall (x :: Symbol) a. IsLabel x a => a
#remainder; ((("permitted" :! Natural) : ("spent" :! Natural) : Ticket d : s)
 :-> (("spent" :! Natural) : Ticket d : s))
-> (("remainder" :! Natural)
      : ("permitted" :! Natural) : ("spent" :! Natural) : Ticket d : s)
   :-> (("remainder" :! Natural)
          : ("spent" :! Natural) : Ticket d : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (((("permitted" :! Natural) : ("spent" :! Natural) : Ticket d : s)
  :-> (("spent" :! Natural) : Ticket d : s))
 -> (("remainder" :! Natural)
       : ("permitted" :! Natural) : ("spent" :! Natural) : Ticket d : s)
    :-> (("remainder" :! Natural)
           : ("spent" :! Natural) : Ticket d : s))
-> ((("permitted" :! Natural)
       : ("spent" :! Natural) : Ticket d : s)
    :-> (("spent" :! Natural) : Ticket d : s))
-> (("remainder" :! Natural)
      : ("permitted" :! Natural) : ("spent" :! Natural) : Ticket d : s)
   :-> (("remainder" :! Natural)
          : ("spent" :! Natural) : Ticket d : s)
forall a b. (a -> b) -> a -> b
$ forall (s :: [*]). (("permitted" :! Natural) : s) :-> s
forall a (s :: [*]). (a : s) :-> s
drop @("permitted" :! _)
    else do (("permitted" :! Natural) : ("spent" :! Natural) : Ticket d : s)
:-> (("permitted" :! Natural, "spent" :! Natural) : Ticket d : s)
forall a b (s :: [*]). (a : b : s) :-> ((a, b) : s)
pair; (("permitted" :! Natural, "spent" :! Natural) : Ticket d : s)
:-> (("remainder" :! Natural)
       : ("spent" :! Natural) : Ticket d : s)
forall (s0 :: [*]).
ErrInstr (("permitted" :! Natural, "spent" :! Natural) : s0)
onInsufficientTokens
  (("remainder" :! Natural) : ("spent" :! Natural) : Ticket d : s)
:-> (("remainder" :! Natural, "spent" :! Natural) : Ticket d : s)
forall a b (s :: [*]). (a : b : s) :-> ((a, b) : s)
pair; (("remainder" :! Natural, "spent" :! Natural) : Ticket d : s)
:-> (Ticket d : ("remainder" :! Natural, "spent" :! Natural) : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap; (Ticket d : ("remainder" :! Natural, "spent" :! Natural) : s)
:-> (Maybe ("remainder" :! Ticket d, "spent" :! Ticket d) : s)
forall (n1 :: Symbol) (n2 :: Symbol) a (s :: [*]).
(Ticket a : (n1 :! Natural, n2 :! Natural) : s)
:-> (Maybe (n1 :! Ticket a, n2 :! Ticket a) : s)
splitTicketNamed
  Impossible "by construction of token parts"
-> (Maybe ("remainder" :! Ticket d, "spent" :! Ticket d) : s)
   :-> (("remainder" :! Ticket d, "spent" :! Ticket d) : s)
forall err a (s :: [*]).
IsError err =>
err -> (Maybe a : s) :-> (a : s)
assertSome (HasCallStack => Impossible "by construction of token parts"
forall (reason :: Symbol). HasCallStack => Impossible reason
Impossible @"by construction of token parts")
  (("remainder" :! Ticket d, "spent" :! Ticket d) : s)
:-> (("remainder" :! Ticket d) : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : s)
car; Label "remainder"
-> (("remainder" :! Ticket d) : s) :-> (Ticket d : s)
forall (name :: Symbol) a (s :: [*]).
Label name -> ((name :! a) : s) :-> (a : s)
fromNamed Label "remainder"
forall a. IsLabel "remainder" a => a
forall (x :: Symbol) a. IsLabel x a => a
#remainder
  (Ticket d : s) :-> (STicket action d : s)
forall a (s :: [*]).
Unwrappable a =>
(Unwrappabled a : s) :-> (a : s)
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 :: (STicket action d : Maybe (STicket action d) : s)
:-> (Maybe (STicket action d) : s)
addSTicket = do
  (STicket action d : Maybe (STicket action d) : s)
:-> (Maybe (STicket action d) : STicket action d : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap; ((STicket action d : STicket action d : s)
 :-> (STicket action d : s))
-> ((STicket action d : s) :-> (STicket action d : s))
-> (Maybe (STicket action d) : STicket action d : s)
   :-> (STicket action d : s)
forall a (s :: [*]) (s' :: [*]).
((a : s) :-> s') -> (s :-> s') -> (Maybe a : s) :-> s'
ifSome (STicket action d : STicket action d : s)
:-> (STicket action d : s)
forall k (action :: k) d (s :: [*]).
(STicket action d : STicket action d : s)
:-> (STicket action d : s)
addSTicketPlain (STicket action d : s) :-> (STicket action d : s)
forall (s :: [*]). s :-> s
nop; (STicket action d : s) :-> (Maybe (STicket action d) : s)
forall a (s :: [*]). (a : s) :-> (Maybe a : s)
some

-- | Similar to 'addSTicket', but without @Maybe@.
addSTicketPlain
  :: STicket action d : STicket action d : s
  :-> STicket action d : s
addSTicketPlain :: (STicket action d : STicket action d : s)
:-> (STicket action d : s)
addSTicketPlain = do
  (STicket action d : STicket action d : s)
:-> (Ticket d : STicket action d : s)
forall a (s :: [*]).
Unwrappable a =>
(a : s) :-> (Unwrappabled a : s)
coerceUnwrap; ((STicket action d : s) :-> (Ticket d : s))
-> (Ticket d : STicket action d : s) :-> (Ticket d : Ticket d : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (STicket action d : s) :-> (Ticket d : s)
forall a (s :: [*]).
Unwrappable a =>
(a : s) :-> (Unwrappabled a : s)
coerceUnwrap
  (Ticket d : Ticket d : s) :-> ((Ticket d, Ticket d) : s)
forall a b (s :: [*]). (a : b : s) :-> ((a, b) : s)
pair; ((Ticket d, Ticket d) : s) :-> (Maybe (Ticket d) : s)
forall a (s :: [*]).
((Ticket a, Ticket a) : s) :-> (Maybe (Ticket a) : s)
joinTickets
  MText -> (Maybe (Ticket d) : s) :-> (Ticket d : s)
forall err a (s :: [*]).
IsError err =>
err -> (Maybe a : s) :-> (a : s)
assertSome [mt|badtjoin|]
  (Ticket d : s) :-> (STicket action d : s)
forall a (s :: [*]).
Unwrappable a =>
(Unwrappabled a : s) :-> (a : s)
unsafeCoerceWrap