Instr.hs

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

{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}

module Lorentz.Instr
  ( nop
  , justComment
  , comment
  , commentAroundFun
  , commentAroundStmt
  , drop
  , dropN
  , ConstraintDUPNLorentz
  , dup
  , dupNPeano
  , dupN
  , swap
  , ConstraintDIGLorentz
  , digPeano
  , dig
  , ConstraintDUGLorentz
  , dugPeano
  , dug
  , push
  , some
  , none
  , unit
  , ifNone
  , pair
  , car
  , cdr
  , left
  , right
  , ifLeft
  , nil
  , cons
  , size
  , emptySet
  , emptyMap
  , emptyBigMap
  , map
  , iter
  , mem
  , get
  , ConstraintPairGetLorentz
  , PairGetHs
  , pairGet
  , update
  , ConstraintPairUpdateLorentz
  , PairUpdateHs
  , pairUpdate
  , failingWhenPresent
  , updateNew
  , if_
  , ifCons
  , loop
  , loopLeft
  , lambda
  , exec
  , execute
  , apply
  , applicate
  , dip
  , ConstraintDIPNLorentz
  , dipNPeano
  , dipN
  , failWith
  , cast
  , pack
  , unpack
  , packRaw
  , unpackRaw
  , concat
  , concat'
  , slice, isNat, add, sub, rsub, mul, ediv, abs
  , neg
  , lsl
  , lsr
  , or
  , and
  , xor
  , not
  , compare
  , eq0
  , neq0
  , lt0
  , gt0
  , le0
  , ge0
  , int
  , toTAddress_
  , self
  , selfCalling
  , contract
  , contractCalling
  , contractCallingUnsafe
  , runFutureContract
  , epAddressToContract
  , transferTokens
  , setDelegate
  , createContract
  , implicitAccount
  , now
  , amount
  , balance
  , votingPower
  , totalVotingPower
  , checkSignature
  , sha256
  , sha512
  , blake2B
  , sha3
  , keccak
  , hashKey
  , pairingCheck
  , source
  , sender
  , address
  , selfAddress
  , chainId
  , level
  , never
  , framed
  , LorentzFunctor (..)
  , NonZero (..)
  ) where

import Prelude hiding
  (EQ, GT, LT, abs, and, compare, concat, drop, get, map, not, or, some, swap, xor)

import Data.Constraint ((\\))
import Data.Singletons (SingI, sing)
import qualified GHC.TypeNats as GHC (Nat)

import Lorentz.Address
import Lorentz.Arith
import Lorentz.Base
import Lorentz.Bytes
import Lorentz.Constraints
import Lorentz.Entrypoints
import Lorentz.Polymorphic
import Lorentz.Run (Contract, compileLorentzContract)
import Lorentz.Value
import Lorentz.Zip
import Michelson.Typed
  (CommentType(..), ConstraintDIG, ConstraintDIG', ConstraintDIPN, ConstraintDIPN', ConstraintDUG,
  ConstraintDUG', ConstraintDUPN, ConstraintDUPN', ConstraintGetN, ConstraintUpdateN,
  EntrypointCallT(..), ExtInstr(..), GetN, Instr(..), RemFail(..), SomeEntrypointCallT(..), UpdateN,
  Value'(..), pattern CAR, pattern CDR, pattern LEFT, pattern PAIR, pattern RIGHT, sepcName, starNotes)
import Michelson.Typed.Arith
import Michelson.Typed.Haskell.Value
import Util.Peano
import Util.Type

nop :: s :-> s
nop = I Nop

justComment :: Text -> s :-> s
justComment = comment . JustComment

comment :: CommentType -> s :-> s
comment = I . Ext . COMMENT_ITEM

commentAroundFun :: Text -> (i :-> o) -> (i :-> o)
commentAroundFun funName funBody =
  comment (FunctionStarts funName) #
  funBody #
  comment (FunctionEnds funName)

commentAroundStmt :: Text -> (i :-> o) -> (i :-> o)
commentAroundStmt stmtName stmtBody =
  comment (StatementStarts stmtName) #
  stmtBody #
  comment (StatementEnds stmtName)


drop :: a : s :-> s
drop = I DROP

-- | Drop top @n@ elements from the stack.
dropN ::
  forall (n :: GHC.Nat) (s :: [Type]).
  -- Note: if we introduce `nPeano ~ ToPeano n` variable,
  -- GHC will complain that this constraint is redundant.
  ( SingI (ToPeano n), KnownPeano (ToPeano n)
  , RequireLongerOrSameLength (ToTs s) (ToPeano n)
  -- ↓ Kinda obvious, but not to GHC.
  , Drop (ToPeano n) (ToTs s) ~ ToTs (Drop (ToPeano n) s)
  ) => s :-> Drop (ToPeano n) s
dropN = I (DROPN $ peanoSing @n)
  where
    _example :: '[ Integer, Integer, Integer ] :-> '[]
    _example = dropN @3

dup :: a : s :-> a : a : s
dup = I DUP

type ConstraintDUPNLorentz (n :: Peano) (inp :: [Type]) (out :: [Type])
  (a :: Type) =
  ( ConstraintDUPN n (ToTs inp) (ToTs out) (ToT a)
  , ConstraintDUPN' Type n inp out a
  )

dupNPeano ::
  forall (n :: Peano) inp out a.
  ( ConstraintDUPNLorentz n inp out a
  ) => inp :-> out
dupNPeano = I (DUPN (sing @n))

dupN ::
  forall (n :: GHC.Nat) inp out a.
  ( ConstraintDUPNLorentz (ToPeano n) inp out a
  ) => inp :-> out
dupN = dupNPeano @(ToPeano n)
  where
    _example :: '[ Integer, (), Bool ] :-> '[ Bool, Integer, (), Bool ]
    _example = dupN @3

swap :: a : b : s :-> b : a : s
swap = I SWAP

-- See a comment about `ConstraintDIPNLorentz'.
type ConstraintDIGLorentz (n :: Peano) (inp :: [Type]) (out :: [Type])
  (a :: Type) =
  ( ConstraintDIG n (ToTs inp) (ToTs out) (ToT a)
  , ConstraintDIG' Type n inp out a
  )

type ConstraintDUGLorentz (n :: Peano) (inp :: [Type]) (out :: [Type])
  (a :: Type) =
  ( ConstraintDUG n (ToTs inp) (ToTs out) (ToT a)
  , ConstraintDUG' Type n inp out a
  )

-- | Version of `dig` which uses Peano number.
-- It is intended for internal usage in Lorentz.
digPeano ::
  forall (n :: Peano) inp out a.
  ( ConstraintDIGLorentz n inp out a
  ) => inp :-> out
digPeano = I (DIG $ sing @n)

dig ::
  forall (n :: GHC.Nat) inp out a.
  ( ConstraintDIGLorentz (ToPeano n) inp out a
  ) => inp :-> out
dig = digPeano @(ToPeano n)
  where
    _example ::
      '[ Integer, Integer, Integer, Bool ] :->
      '[ Bool, Integer, Integer, Integer ]
    _example = dig @3

-- | Version of `dug` which uses Peano number.
-- It is intended for internal usage in Lorentz.
dugPeano ::
  forall (n :: Peano) inp out a.
  ( ConstraintDUGLorentz n inp out a
  ) => inp :-> out
dugPeano = I (DUG $ sing @n)

dug ::
  forall (n :: GHC.Nat) inp out a.
  ( ConstraintDUGLorentz (ToPeano n) inp out a
  ) => inp :-> out
dug = dugPeano @(ToPeano n)
  where
    _example ::
      '[ Bool, Integer, Integer, Integer ] :->
      '[ Integer, Integer, Integer, Bool ]
    _example = dug @3

push :: forall t s . NiceConstant t => t -> (s :-> t : s)
push a = I $ PUSH (toVal a) \\ niceConstantEvi @t

some :: a : s :-> Maybe a : s
some = I SOME

none :: forall a s . KnownValue a => s :-> (Maybe a : s)
none = I NONE

unit :: s :-> () : s
unit = I UNIT

ifNone
  :: (s :-> s') -> (a : s :-> s') -> (Maybe a : s :-> s')
ifNone = iGenericIf IF_NONE

pair :: a : b : s :-> (a, b) : s
pair = I PAIR

car :: (a, b) : s :-> a : s
car = I CAR

cdr :: (a, b) : s :-> b : s
cdr = I CDR

left :: forall a b s. KnownValue b => a : s :-> Either a b : s
left = I LEFT

right :: forall a b s. KnownValue a => b : s :-> Either a b : s
right = I RIGHT

ifLeft
  :: (a : s :-> s') -> (b : s :-> s') -> (Either a b : s :-> s')
ifLeft = iGenericIf IF_LEFT

nil :: KnownValue p => s :-> List p : s
nil = I NIL

cons :: a : List a : s :-> List a : s
cons = I CONS

ifCons
  :: (a : List a : s :-> s') -> (s :-> s') -> (List a : s :-> s')
ifCons = iGenericIf IF_CONS

size :: SizeOpHs c => c : s :-> Natural : s
size = I SIZE

emptySet :: (NiceComparable e) => s :-> Set e : s
emptySet = I EMPTY_SET

emptyMap :: (NiceComparable k, KnownValue v)
         => s :-> Map k v : s
emptyMap = I EMPTY_MAP

emptyBigMap :: (NiceComparable k, KnownValue v)
            => s :-> BigMap k v : s
emptyBigMap = I EMPTY_BIG_MAP

map
  :: (MapOpHs c, IsoMapOpRes c b, KnownValue b, HasCallStack)
  => (MapOpInpHs c : s :-> b : s) -> (c : s :-> MapOpResHs c b : s)
map (iNonFailingCode -> action) = I (MAP action)

iter
  :: (IterOpHs c, HasCallStack)
  => (IterOpElHs c : s :-> s) -> (c : s :-> s)
iter (iNonFailingCode -> action) = I (ITER action)

mem :: MemOpHs c => MemOpKeyHs c : c : s :-> Bool : s
mem = I MEM

get
  :: (GetOpHs c, KnownValue (GetOpValHs c))
  => GetOpKeyHs c : c : s :-> Maybe (GetOpValHs c) : s
get = I GET

type ConstraintPairGetLorentz (n :: GHC.Nat) (pair :: Type) =
  ( ConstraintGetN (ToPeano n) (ToT pair)
  , ToT (PairGetHs (ToPeano n) pair) ~ GetN (ToPeano n) (ToT pair)
  )

type family PairGetHs (ix :: Peano) (pair :: Type) :: Type where
  PairGetHs 'Z val                 = val
  PairGetHs ('S 'Z) (left, _)      = left
  PairGetHs ('S ('S n)) (_, right) = PairGetHs n right

pairGet
  :: forall (n :: GHC.Nat) (pair :: Type) (s :: [Type]).
     ConstraintPairGetLorentz n pair
  => pair : s :-> PairGetHs (ToPeano n) pair : s
pairGet = I (GETN (peanoSing @n))
  where
    _example :: '[ (Integer, Natural), () ] :-> '[ Integer, () ]
    _example = pairGet @1

update :: UpdOpHs c => UpdOpKeyHs c : UpdOpParamsHs c : c : s :-> c : s
update = I UPDATE

type ConstraintPairUpdateLorentz (n :: GHC.Nat) (val :: Type) (pair :: Type) =
  ( ConstraintUpdateN (ToPeano n) (ToT pair)
  , ToT (PairUpdateHs (ToPeano n) val pair) ~ UpdateN (ToPeano n) (ToT val) (ToT pair)
  )

type family PairUpdateHs (ix :: Peano) (val :: Type) (pair :: Type) :: Type where
  PairUpdateHs 'Z          val _             = val
  PairUpdateHs ('S 'Z)     val (_, right)    = (val, right)
  PairUpdateHs ('S ('S n)) val (left, right) = (left, PairUpdateHs n val right)

pairUpdate
  :: forall (n :: GHC.Nat) (val :: Type) (pair :: Type) (s :: [Type]).
     ConstraintPairUpdateLorentz n val pair
  => val : pair : s :-> PairUpdateHs (ToPeano n) val pair : s
pairUpdate = I (UPDATEN (peanoSing @n))
  where
    _example :: '[ MText, (Integer, Natural) ] :-> '[ (MText, Natural) ]
    _example = pairUpdate @1

if_ :: (s :-> s') -> (s :-> s') -> (Bool : s :-> s')
if_ = iGenericIf IF

loop :: (s :-> Bool : s) -> (Bool : s :-> s)
loop (iAnyCode -> b) = I (LOOP b)

loopLeft
  :: (a : s :-> Either a b : s) -> (Either a b : s :-> b : s)
loopLeft (iAnyCode -> b) = I (LOOP_LEFT b)

lambda
  :: ZipInstrs [i, o]
  => (i :-> o) -> (s :-> (i :-> o) : s)
lambda instr = case zippingStack instr of
  I l -> I (LAMBDA . VLam $ RfNormal l)
  FI l -> I (LAMBDA . VLam $ RfAlwaysFails l)

exec :: a : Lambda a b : s :-> b : s
exec = I EXEC

-- | Similar to 'exec' but works for lambdas with arbitrary size of input
-- and output.
--
-- Note that this instruction has its arguments flipped, lambda goes first.
-- This seems to be the only reasonable way to achieve good inference.
execute
  :: forall i o s.
      (Each [KnownList, ZipInstr] [i, o])
  => ((i :-> o) : (i ++ s)) :-> (o ++ s)
execute = framed @s $
  dip (zipInstr @i) # swap # I EXEC # unzipInstr @o
  where
    _example
      :: ([Integer, Natural] :-> [(), ()]) : Integer : Natural : s
      :-> () : () : s
    _example = execute

apply
  :: forall a b c s. (NiceConstant a, KnownValue b)
  => a : Lambda (a, b) c : s :-> Lambda b c : s
apply = I $ APPLY \\ niceConstantEvi @a

-- | Version of 'apply' that works for lambdas with arbitrary length
-- input and output.
applicate
  :: forall a b c inp2nd inpTail s.
     (NiceConstant a, ZipInstr b, b ~ (inp2nd : inpTail))
  => a : (a : b :-> c) : s :-> (b :-> c) : s
applicate = I APPLY \\ niceConstantEvi @a

dip :: forall a s s'. HasCallStack => (s :-> s') -> (a : s :-> a : s')
dip (iNonFailingCode -> a) = I (DIP a)

-- Helper constraint we need for 'dipN'.
-- The first constraint here is sufficient to make 'dipN' compile.
-- However, it is not enough for good type inference. If we use only the first
-- constraint, '_example' below will not compile because GHC will not be able
-- to deduce type of the input stack for 'unit'.
-- It can only deduce that 'ToTs s0' is empty (where 's0' is input stack), but
-- 'ToTs' is not injective, hence 's0' is ambiguous.
-- So we need both and we merge them into one to avoid a warning about
-- a redundant constraint.
type ConstraintDIPNLorentz (n :: Peano) (inp :: [Type]) (out :: [Type])
  (s :: [Type]) (s' :: [Type]) =
  ( ConstraintDIPN n (ToTs inp) (ToTs out) (ToTs s) (ToTs s')
  , ConstraintDIPN' Type n inp out s s'
  )

-- | Version of `dipN` which uses Peano number.
-- It is intended for internal usage in Lorentz.
dipNPeano ::
  forall (n :: Peano) (inp :: [Type]) (out :: [Type]) (s :: [Type]) (s' :: [Type]).
  ( ConstraintDIPNLorentz n inp out s s'
  ) => s :-> s' -> inp :-> out
dipNPeano (iNonFailingCode -> a) = I (DIPN (sing @n) a)

dipN ::
  forall (n :: GHC.Nat) (inp :: [Type]) (out :: [Type]) (s :: [Type]) (s' :: [Type]).
  ( ConstraintDIPNLorentz (ToPeano n) inp out s s'
  ) => s :-> s' -> inp :-> out
dipN = dipNPeano @(ToPeano n)
  where
    _example :: '[ Integer, Integer, Integer ] :-> '[ Integer, Integer, Integer, () ]
    _example = dipN @3 unit

-- Since 008 it's prohibited to fail with non-packable values and with the
-- 'Contract t' type values, which is equivalent to our @NiceConstant@ constraint.
-- See https://gitlab.com/tezos/tezos/-/issues/1093#note_496066354 for more information.
failWith :: forall a s t. NiceConstant a => a : s :-> t
failWith = FI FAILWITH \\ niceConstantEvi @a

cast :: KnownValue a => (a : s :-> a : s)
cast = I CAST

pack
  :: forall a s. (NicePackedValue a)
  => a : s :-> Packed a : s
pack = I $ PACK \\ nicePackedValueEvi @a

unpack
  :: forall a s. (NiceUnpackedValue a)
  => Packed a : s :-> Maybe a : s
unpack = I $ UNPACK \\ niceUnpackedValueEvi @a

packRaw
  :: forall a s. (NicePackedValue a)
  => a : s :-> ByteString : s
packRaw = I $ PACK \\ nicePackedValueEvi @a

unpackRaw
  :: forall a s. (NiceUnpackedValue a)
  => ByteString : s :-> Maybe a : s
unpackRaw = I $ UNPACK \\ niceUnpackedValueEvi @a

concat :: ConcatOpHs c => c : c : s :-> c : s
concat = I CONCAT

concat' :: ConcatOpHs c => List c : s :-> c : s
concat' = I CONCAT'

slice
  :: (SliceOpHs c, KnownValue c)
  => Natural : Natural : c : s :-> Maybe c : s
slice = I SLICE

isNat :: Integer : s :-> Maybe Natural : s
isNat = I ISNAT

add
  :: ArithOpHs Add n m
  => n : m : s :-> ArithResHs Add n m : s
add = I ADD

sub
  :: ArithOpHs Sub n m
  => n : m : s :-> ArithResHs Sub n m : s
sub = I SUB

rsub
  :: ArithOpHs Sub n m
  => m : n : s :-> ArithResHs Sub n m : s
rsub = swap # sub

mul
  :: ArithOpHs Mul n m
  => n : m : s :-> ArithResHs Mul n m : s
mul = I MUL

ediv :: EDivOpHs n m
     => n : m : s
     :-> Maybe ((EDivOpResHs n m, EModOpResHs n m)) : s
ediv = I EDIV

abs :: UnaryArithOpHs Abs n => n : s :-> UnaryArithResHs Abs n : s
abs = I ABS

neg :: UnaryArithOpHs Neg n => n : s :-> UnaryArithResHs Neg n : s
neg = I NEG


lsl
  :: ArithOpHs Lsl n m
  => n : m : s :-> ArithResHs Lsl n m : s
lsl = I LSL

lsr
  :: ArithOpHs Lsr n m
  => n : m : s :-> ArithResHs Lsr n m : s
lsr = I LSR

or
  :: ArithOpHs Or n m
  => n : m : s :-> ArithResHs Or n m : s
or = I OR

and
  :: ArithOpHs And n m
  => n : m : s :-> ArithResHs And n m : s
and = I AND

xor
  :: (ArithOpHs Xor n m)
  => n : m : s :-> ArithResHs Xor n m : s
xor = I XOR

not :: UnaryArithOpHs Not n => n : s :-> UnaryArithResHs Not n : s
not = I NOT

compare :: NiceComparable n => n : n : s :-> Integer : s
compare = I COMPARE

eq0 :: UnaryArithOpHs Eq' n => n : s :-> UnaryArithResHs Eq' n : s
eq0 = I EQ

neq0 :: UnaryArithOpHs Neq n => n : s :-> UnaryArithResHs Neq n : s
neq0 = I NEQ

lt0 :: UnaryArithOpHs Lt n => n : s :-> UnaryArithResHs Lt n : s
lt0 = I LT

gt0 :: UnaryArithOpHs Gt n => n : s :-> UnaryArithResHs Gt n : s
gt0 = I GT

le0 :: UnaryArithOpHs Le n => n : s :-> UnaryArithResHs Le n : s
le0 = I LE

ge0 :: UnaryArithOpHs Ge n => n : s :-> UnaryArithResHs Ge n : s
ge0 = I GE

int :: (ToIntegerArithOpHs i) => i : s :-> Integer : s
int = I INT

-- | Get a reference to the current contract.
--
-- Note that, similar to 'CONTRACT' instruction, in Michelson 'SELF' instruction
-- can accept an entrypoint as field annotation, and without annotation specified
-- it creates a @contract@ value which calls the default entrypoint.
--
-- This particular function carries the behaviour of @SELF@ before introduction
-- of lightweight entrypoints feature.
-- Thus the contract must __not__ have explicit "default" entrypoint for this to
-- work.
--
-- If you are going to call a specific entrypoint of the contract, see 'selfCalling'.
self
  :: forall p s.
      (NiceParameterFull p, ForbidExplicitDefaultEntrypoint p)
  => s :-> ContractRef p : s
self = I (SELF $ sepcCallRootChecked @p) \\ niceParameterEvi @p

-- | Make a reference to the current contract, maybe a specific entrypoint.
--
-- Note that, since information about parameter of the current contract is not
-- carried around, in this function you need to specify parameter type @p@
-- explicitly.
selfCalling
  :: forall p mname s.
     (NiceParameterFull p)
  => EntrypointRef mname
  -> s :-> ContractRef (GetEntrypointArgCustom p mname) : s
selfCalling epRef = I $
  withDict (niceParameterEvi @p) $
  case parameterEntrypointCallCustom @p epRef of
    epc@EntrypointCall{} -> SELF (SomeEpc epc)

-- | Get a reference to a contract by its address.
--
-- This instruction carries the behaviour of @CONTRACT@ before introduction
-- of lightweight entrypoints feature.
-- The contract must __not__ have explicit "default" entrypoint for this to work.
--
-- If you are going to call a specific entrypoint of the contract, see 'contractCalling'.
contract
  :: forall p addr s.
      ( NiceParameterFull p, ForbidExplicitDefaultEntrypoint p
      , ToTAddress_ p addr
      )
  => addr : s :-> Maybe (ContractRef p) : s
contract = I (CONTRACT starNotes epName) \\ niceParameterEvi @p
  where
    epName = sepcName (sepcCallRootChecked @p)

-- | Make a reference to a contract, maybe a specific entrypoint.
--
-- When calling this function, make sure that parameter type is known.
-- It's recommended that you supply 'TAddress' with a concrete parameter as the
-- stack argument.
contractCalling
  :: forall cp epRef epArg addr s.
     (HasEntrypointArg cp epRef epArg, ToTAddress_ cp addr)
  => epRef
  -> addr : s :-> Maybe (ContractRef epArg) : s
contractCalling epRef = I $
  case useHasEntrypointArg @cp @epRef @epArg epRef of
    (Dict, epName) -> CONTRACT starNotes epName

-- | Specialized version of 'contractCalling' for the case when you do
-- not have compile-time evidence of appropriate 'HasEntrypointArg'.
-- For instance, if you have untyped 'EpName' you can not have this
-- evidence (the value is only available in runtime).
-- If you have typed 'EntrypointRef', use 'eprName' to construct 'EpName'.
contractCallingUnsafe
  :: forall arg s.
     (NiceParameter arg)
  => EpName
  -> Address : s :-> Maybe (ContractRef arg) : s
contractCallingUnsafe epName = contractCalling (TrustEpName epName)

-- | Version of 'contract' instruction which may accept address with already
-- specified entrypoint name.
--
-- Also you cannot specify entrypoint name here because this could result in
-- conflict.
runFutureContract
  :: forall p s. (NiceParameter p)
  => FutureContract p : s :-> Maybe (ContractRef p) : s
runFutureContract =
  I Nop # epAddressToContract

-- | Similar to 'runFutureContract', works with 'EpAddress'.
--
-- Validity of such operation cannot be ensured at compile time.
epAddressToContract
  :: forall p s. (NiceParameter p)
  => EpAddress : s :-> Maybe (ContractRef p) : s
epAddressToContract =
  I (CONTRACT starNotes DefEpName) \\ niceParameterEvi @p

transferTokens
  :: forall p s. (NiceParameter p)
  => p : Mutez : ContractRef p : s :-> Operation : s
transferTokens = I $ TRANSFER_TOKENS \\ niceParameterEvi @p

setDelegate :: Maybe KeyHash : s :-> Operation : s
setDelegate = I SET_DELEGATE

createContract
  :: forall p g s. (NiceStorage g, NiceParameterFull p)
  => Contract p g
  -> Maybe KeyHash : Mutez : g : s
  :-> Operation : Address : s
createContract cntrc =
  I $ CREATE_CONTRACT (compileLorentzContract cntrc)
    \\ niceParameterEvi @p
    \\ niceStorageEvi @g

implicitAccount :: KeyHash : s :-> ContractRef () : s
implicitAccount = I IMPLICIT_ACCOUNT

now :: s :-> Timestamp : s
now = I NOW

amount :: s :-> Mutez : s
amount = I AMOUNT

balance :: s :-> Mutez : s
balance = I BALANCE

votingPower :: KeyHash : s :-> Natural : s
votingPower = I VOTING_POWER

totalVotingPower :: s :-> Natural : s
totalVotingPower = I TOTAL_VOTING_POWER

checkSignature :: BytesLike bs => PublicKey : TSignature bs : bs : s :-> Bool : s
checkSignature = I CHECK_SIGNATURE

sha256 :: BytesLike bs => bs : s :-> Hash Sha256 bs : s
sha256 = I SHA256

sha512 :: BytesLike bs => bs : s :-> Hash Sha512 bs : s
sha512 = I SHA512

blake2B :: BytesLike bs => bs : s :-> Hash Blake2b bs : s
blake2B = I BLAKE2B

sha3 :: BytesLike bs => bs : s :-> Hash Sha3 bs : s
sha3 = I SHA3

keccak :: BytesLike bs => bs : s :-> Hash Keccak bs : s
keccak = I KECCAK

hashKey :: PublicKey : s :-> KeyHash : s
hashKey = I HASH_KEY

pairingCheck :: [(Bls12381G1, Bls12381G2)] : s :-> Bool : s
pairingCheck = I PAIRING_CHECK

{-# WARNING source
    "Using `source` is considered a bad practice.\n\
\    Consider using `sender` instead until further investigation" #-}
source :: s :-> Address : s
source = I SOURCE

sender :: s :-> Address : s
sender = I SENDER

address :: ContractRef a : s :-> Address : s
address = I ADDRESS

chainId :: s :-> ChainId : s
chainId = I CHAIN_ID

level :: s :-> Natural : s
level = I LEVEL

selfAddress :: s :-> Address : s
selfAddress = I SELF_ADDRESS

never :: Never : s :-> s'
never = FI NEVER

-- | Execute given instruction on truncated stack.
--
-- This instruction requires you to specify the piece of stack to truncate
-- as type argument.
framed
  :: forall s i o.
      (KnownList i, KnownList o)
  => (i :-> o) -> ((i ++ s) :-> (o ++ s))
framed (iNonFailingCode -> i) =
  I $ FrameInstr (Proxy @(ToTs s)) i
    \\ totsKnownLemma @i
    \\ totsKnownLemma @o
    \\ totsAppendLemma @i @s
    \\ totsAppendLemma @o @s

----------------------------------------------------------------------------
-- Non-canonical instructions
----------------------------------------------------------------------------

-- | Helper instruction.
--
-- Checks whether given key present in the storage and fails if it is.
-- This instruction leaves stack intact.
failingWhenPresent
  :: forall c k s v st e.
     ( MemOpHs c, k ~ MemOpKeyHs c
     , NiceConstant e
     , st ~ (k : v : c : s)
     )
  => (forall s0. k : s0 :-> e : s0)
  -> st :-> st
failingWhenPresent mkErr =
  dupN @3 # dupN @2 # mem #
  if_ (mkErr # failWith) nop

-- | Like 'update', but throw an error on attempt to overwrite existing entry.
updateNew
  :: forall c k s e.
     ( UpdOpHs c, MemOpHs c, k ~ UpdOpKeyHs c, k ~ MemOpKeyHs c
     , NiceConstant e
     )
  => (forall s0. k : s0 :-> e : s0)
  -> k : UpdOpParamsHs c : c : s :-> c : s
updateNew mkErr = failingWhenPresent mkErr # update

class LorentzFunctor (c :: Type -> Type) where
  lmap :: KnownValue b => (a : s :-> b : s) -> (c a : s :-> c b : s)

instance LorentzFunctor Maybe where
  lmap f = ifNone none (f # some)

class NonZero t where
  -- | Retain the value only if it is not zero.
  nonZero :: t : s :-> Maybe t : s

instance NonZero Integer where
  nonZero = dup # eq0 # if_ (drop # none) some

instance NonZero Natural where
  nonZero = dup # int # eq0 # if_ (drop # none) some