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

-- | Module, containing some boilerplate for support of
-- arithmetic operations in Michelson language.

module Morley.Michelson.Typed.Arith
  ( ArithOp (..)
  , UnaryArithOp (..)
  , ToIntArithOp (..)
  , ToBytesArithOp (..)
  , evalToNatOp
  , ArithError (..)
  , ShiftArithErrorType (..)
  , MutezArithErrorType (..)
  , Add
  , Sub
  , SubMutez
  , Mul
  , EDiv
  , Abs
  , Neg
  , Or
  , And
  , Xor
  , Not
  , Lsl
  , Lsr
  , Compare
  , Eq'
  , Neq
  , Lt
  , Gt
  , Le
  , Ge
  , compareOp

  -- * Misc
  , Bls12381MulBadOrder
  ) where

import Crypto.Number.Basic (numBits)
import Crypto.Number.Serialize (i2osp, os2ip)
import Data.Bits (complement, setBit, shift, zeroBits, (.&.), (.|.))
import Data.ByteString qualified as BS
import Data.Constraint (Bottom(..), Dict(..))
import Fmt (Buildable(build), (+|), (|+))
import Type.Errors (DelayError)
import Unsafe qualified (fromIntegral)

import Morley.Michelson.Typed.Polymorphic
import Morley.Michelson.Typed.Scope (Comparable)
import Morley.Michelson.Typed.T (T(..))
import Morley.Michelson.Typed.Value (Value'(..))
import Morley.Tezos.Core (addMutez, mulMutez, subMutez, timestampFromSeconds, timestampToSeconds)
import Morley.Tezos.Crypto.BLS12381 qualified as BLS
import Morley.Util.TypeLits

-- | Class for binary arithmetic operation.
--
-- Takes binary operation marker as @op@ parameter,
-- types of left operand @n@ and right operand @m@.
--
-- 'Typeable' constraints in superclass are necessary for error messages.
class (Typeable n, Typeable m) =>
      ArithOp aop (n :: T) (m :: T) where

  -- | Type family @ArithRes@ denotes the type resulting from
  -- computing operation @op@ from operands of types @n@ and @m@.
  --
  -- For instance, adding integer to natural produces integer,
  -- which is reflected in following instance of type family:
  -- @ArithRes Add CNat CInt = CInt@.
  type ArithRes aop n m :: T

  -- | Evaluate arithmetic operation on given operands.
  evalOp
    :: proxy aop
    -> Value' instr n
    -> Value' instr m
    -> Either (ArithError (Value' instr n) (Value' instr m)) (Value' instr (ArithRes aop n m))

  -- | An operation can marked as commutative, it does not affect its
  -- runtime behavior, but enables certain optimization in the optimizer.
  -- We conservatively consider operations non-commutative by default.
  --
  -- Note that there is one unusual case: @AND@ works with @int : nat@
  -- but not with @nat : int@. That's how it's specified in Michelson.
  commutativityProof :: Maybe $ Dict (ArithRes aop n m ~ ArithRes aop m n, ArithOp aop m n)
  commutativityProof = Maybe $ Dict (ArithRes aop n m ~ ArithRes aop m n, ArithOp aop m n)
forall a. Maybe a
Nothing

-- | Denotes the error type occurred in the arithmetic shift operation.
data ShiftArithErrorType
  = LslOverflow
  | LsrUnderflow
  deriving stock (Int -> ShiftArithErrorType -> ShowS
[ShiftArithErrorType] -> ShowS
ShiftArithErrorType -> String
(Int -> ShiftArithErrorType -> ShowS)
-> (ShiftArithErrorType -> String)
-> ([ShiftArithErrorType] -> ShowS)
-> Show ShiftArithErrorType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ShiftArithErrorType -> ShowS
showsPrec :: Int -> ShiftArithErrorType -> ShowS
$cshow :: ShiftArithErrorType -> String
show :: ShiftArithErrorType -> String
$cshowList :: [ShiftArithErrorType] -> ShowS
showList :: [ShiftArithErrorType] -> ShowS
Show, ShiftArithErrorType -> ShiftArithErrorType -> Bool
(ShiftArithErrorType -> ShiftArithErrorType -> Bool)
-> (ShiftArithErrorType -> ShiftArithErrorType -> Bool)
-> Eq ShiftArithErrorType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ShiftArithErrorType -> ShiftArithErrorType -> Bool
== :: ShiftArithErrorType -> ShiftArithErrorType -> Bool
$c/= :: ShiftArithErrorType -> ShiftArithErrorType -> Bool
/= :: ShiftArithErrorType -> ShiftArithErrorType -> Bool
Eq, Eq ShiftArithErrorType
Eq ShiftArithErrorType
-> (ShiftArithErrorType -> ShiftArithErrorType -> Ordering)
-> (ShiftArithErrorType -> ShiftArithErrorType -> Bool)
-> (ShiftArithErrorType -> ShiftArithErrorType -> Bool)
-> (ShiftArithErrorType -> ShiftArithErrorType -> Bool)
-> (ShiftArithErrorType -> ShiftArithErrorType -> Bool)
-> (ShiftArithErrorType
    -> ShiftArithErrorType -> ShiftArithErrorType)
-> (ShiftArithErrorType
    -> ShiftArithErrorType -> ShiftArithErrorType)
-> Ord ShiftArithErrorType
ShiftArithErrorType -> ShiftArithErrorType -> Bool
ShiftArithErrorType -> ShiftArithErrorType -> Ordering
ShiftArithErrorType -> ShiftArithErrorType -> ShiftArithErrorType
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: ShiftArithErrorType -> ShiftArithErrorType -> Ordering
compare :: ShiftArithErrorType -> ShiftArithErrorType -> Ordering
$c< :: ShiftArithErrorType -> ShiftArithErrorType -> Bool
< :: ShiftArithErrorType -> ShiftArithErrorType -> Bool
$c<= :: ShiftArithErrorType -> ShiftArithErrorType -> Bool
<= :: ShiftArithErrorType -> ShiftArithErrorType -> Bool
$c> :: ShiftArithErrorType -> ShiftArithErrorType -> Bool
> :: ShiftArithErrorType -> ShiftArithErrorType -> Bool
$c>= :: ShiftArithErrorType -> ShiftArithErrorType -> Bool
>= :: ShiftArithErrorType -> ShiftArithErrorType -> Bool
$cmax :: ShiftArithErrorType -> ShiftArithErrorType -> ShiftArithErrorType
max :: ShiftArithErrorType -> ShiftArithErrorType -> ShiftArithErrorType
$cmin :: ShiftArithErrorType -> ShiftArithErrorType -> ShiftArithErrorType
min :: ShiftArithErrorType -> ShiftArithErrorType -> ShiftArithErrorType
Ord, (forall x. ShiftArithErrorType -> Rep ShiftArithErrorType x)
-> (forall x. Rep ShiftArithErrorType x -> ShiftArithErrorType)
-> Generic ShiftArithErrorType
forall x. Rep ShiftArithErrorType x -> ShiftArithErrorType
forall x. ShiftArithErrorType -> Rep ShiftArithErrorType x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ShiftArithErrorType -> Rep ShiftArithErrorType x
from :: forall x. ShiftArithErrorType -> Rep ShiftArithErrorType x
$cto :: forall x. Rep ShiftArithErrorType x -> ShiftArithErrorType
to :: forall x. Rep ShiftArithErrorType x -> ShiftArithErrorType
Generic)

instance NFData ShiftArithErrorType

-- | Denotes the error type occurred in the arithmetic operation involving mutez.
data MutezArithErrorType
  = AddOverflow
  | MulOverflow
  deriving stock (Int -> MutezArithErrorType -> ShowS
[MutezArithErrorType] -> ShowS
MutezArithErrorType -> String
(Int -> MutezArithErrorType -> ShowS)
-> (MutezArithErrorType -> String)
-> ([MutezArithErrorType] -> ShowS)
-> Show MutezArithErrorType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> MutezArithErrorType -> ShowS
showsPrec :: Int -> MutezArithErrorType -> ShowS
$cshow :: MutezArithErrorType -> String
show :: MutezArithErrorType -> String
$cshowList :: [MutezArithErrorType] -> ShowS
showList :: [MutezArithErrorType] -> ShowS
Show, MutezArithErrorType -> MutezArithErrorType -> Bool
(MutezArithErrorType -> MutezArithErrorType -> Bool)
-> (MutezArithErrorType -> MutezArithErrorType -> Bool)
-> Eq MutezArithErrorType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: MutezArithErrorType -> MutezArithErrorType -> Bool
== :: MutezArithErrorType -> MutezArithErrorType -> Bool
$c/= :: MutezArithErrorType -> MutezArithErrorType -> Bool
/= :: MutezArithErrorType -> MutezArithErrorType -> Bool
Eq, Eq MutezArithErrorType
Eq MutezArithErrorType
-> (MutezArithErrorType -> MutezArithErrorType -> Ordering)
-> (MutezArithErrorType -> MutezArithErrorType -> Bool)
-> (MutezArithErrorType -> MutezArithErrorType -> Bool)
-> (MutezArithErrorType -> MutezArithErrorType -> Bool)
-> (MutezArithErrorType -> MutezArithErrorType -> Bool)
-> (MutezArithErrorType
    -> MutezArithErrorType -> MutezArithErrorType)
-> (MutezArithErrorType
    -> MutezArithErrorType -> MutezArithErrorType)
-> Ord MutezArithErrorType
MutezArithErrorType -> MutezArithErrorType -> Bool
MutezArithErrorType -> MutezArithErrorType -> Ordering
MutezArithErrorType -> MutezArithErrorType -> MutezArithErrorType
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: MutezArithErrorType -> MutezArithErrorType -> Ordering
compare :: MutezArithErrorType -> MutezArithErrorType -> Ordering
$c< :: MutezArithErrorType -> MutezArithErrorType -> Bool
< :: MutezArithErrorType -> MutezArithErrorType -> Bool
$c<= :: MutezArithErrorType -> MutezArithErrorType -> Bool
<= :: MutezArithErrorType -> MutezArithErrorType -> Bool
$c> :: MutezArithErrorType -> MutezArithErrorType -> Bool
> :: MutezArithErrorType -> MutezArithErrorType -> Bool
$c>= :: MutezArithErrorType -> MutezArithErrorType -> Bool
>= :: MutezArithErrorType -> MutezArithErrorType -> Bool
$cmax :: MutezArithErrorType -> MutezArithErrorType -> MutezArithErrorType
max :: MutezArithErrorType -> MutezArithErrorType -> MutezArithErrorType
$cmin :: MutezArithErrorType -> MutezArithErrorType -> MutezArithErrorType
min :: MutezArithErrorType -> MutezArithErrorType -> MutezArithErrorType
Ord, (forall x. MutezArithErrorType -> Rep MutezArithErrorType x)
-> (forall x. Rep MutezArithErrorType x -> MutezArithErrorType)
-> Generic MutezArithErrorType
forall x. Rep MutezArithErrorType x -> MutezArithErrorType
forall x. MutezArithErrorType -> Rep MutezArithErrorType x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. MutezArithErrorType -> Rep MutezArithErrorType x
from :: forall x. MutezArithErrorType -> Rep MutezArithErrorType x
$cto :: forall x. Rep MutezArithErrorType x -> MutezArithErrorType
to :: forall x. Rep MutezArithErrorType x -> MutezArithErrorType
Generic)

instance NFData MutezArithErrorType

-- | Represents an arithmetic error of the operation.
data ArithError n m
  = MutezArithError MutezArithErrorType n m
  | ShiftArithError ShiftArithErrorType n m
  deriving stock (Int -> ArithError n m -> ShowS
[ArithError n m] -> ShowS
ArithError n m -> String
(Int -> ArithError n m -> ShowS)
-> (ArithError n m -> String)
-> ([ArithError n m] -> ShowS)
-> Show (ArithError n m)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall n m. (Show n, Show m) => Int -> ArithError n m -> ShowS
forall n m. (Show n, Show m) => [ArithError n m] -> ShowS
forall n m. (Show n, Show m) => ArithError n m -> String
$cshowsPrec :: forall n m. (Show n, Show m) => Int -> ArithError n m -> ShowS
showsPrec :: Int -> ArithError n m -> ShowS
$cshow :: forall n m. (Show n, Show m) => ArithError n m -> String
show :: ArithError n m -> String
$cshowList :: forall n m. (Show n, Show m) => [ArithError n m] -> ShowS
showList :: [ArithError n m] -> ShowS
Show, ArithError n m -> ArithError n m -> Bool
(ArithError n m -> ArithError n m -> Bool)
-> (ArithError n m -> ArithError n m -> Bool)
-> Eq (ArithError n m)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall n m.
(Eq n, Eq m) =>
ArithError n m -> ArithError n m -> Bool
$c== :: forall n m.
(Eq n, Eq m) =>
ArithError n m -> ArithError n m -> Bool
== :: ArithError n m -> ArithError n m -> Bool
$c/= :: forall n m.
(Eq n, Eq m) =>
ArithError n m -> ArithError n m -> Bool
/= :: ArithError n m -> ArithError n m -> Bool
Eq, Eq (ArithError n m)
Eq (ArithError n m)
-> (ArithError n m -> ArithError n m -> Ordering)
-> (ArithError n m -> ArithError n m -> Bool)
-> (ArithError n m -> ArithError n m -> Bool)
-> (ArithError n m -> ArithError n m -> Bool)
-> (ArithError n m -> ArithError n m -> Bool)
-> (ArithError n m -> ArithError n m -> ArithError n m)
-> (ArithError n m -> ArithError n m -> ArithError n m)
-> Ord (ArithError n m)
ArithError n m -> ArithError n m -> Bool
ArithError n m -> ArithError n m -> Ordering
ArithError n m -> ArithError n m -> ArithError n m
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {n} {m}. (Ord n, Ord m) => Eq (ArithError n m)
forall n m.
(Ord n, Ord m) =>
ArithError n m -> ArithError n m -> Bool
forall n m.
(Ord n, Ord m) =>
ArithError n m -> ArithError n m -> Ordering
forall n m.
(Ord n, Ord m) =>
ArithError n m -> ArithError n m -> ArithError n m
$ccompare :: forall n m.
(Ord n, Ord m) =>
ArithError n m -> ArithError n m -> Ordering
compare :: ArithError n m -> ArithError n m -> Ordering
$c< :: forall n m.
(Ord n, Ord m) =>
ArithError n m -> ArithError n m -> Bool
< :: ArithError n m -> ArithError n m -> Bool
$c<= :: forall n m.
(Ord n, Ord m) =>
ArithError n m -> ArithError n m -> Bool
<= :: ArithError n m -> ArithError n m -> Bool
$c> :: forall n m.
(Ord n, Ord m) =>
ArithError n m -> ArithError n m -> Bool
> :: ArithError n m -> ArithError n m -> Bool
$c>= :: forall n m.
(Ord n, Ord m) =>
ArithError n m -> ArithError n m -> Bool
>= :: ArithError n m -> ArithError n m -> Bool
$cmax :: forall n m.
(Ord n, Ord m) =>
ArithError n m -> ArithError n m -> ArithError n m
max :: ArithError n m -> ArithError n m -> ArithError n m
$cmin :: forall n m.
(Ord n, Ord m) =>
ArithError n m -> ArithError n m -> ArithError n m
min :: ArithError n m -> ArithError n m -> ArithError n m
Ord, (forall x. ArithError n m -> Rep (ArithError n m) x)
-> (forall x. Rep (ArithError n m) x -> ArithError n m)
-> Generic (ArithError n m)
forall x. Rep (ArithError n m) x -> ArithError n m
forall x. ArithError n m -> Rep (ArithError n m) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall n m x. Rep (ArithError n m) x -> ArithError n m
forall n m x. ArithError n m -> Rep (ArithError n m) x
$cfrom :: forall n m x. ArithError n m -> Rep (ArithError n m) x
from :: forall x. ArithError n m -> Rep (ArithError n m) x
$cto :: forall n m x. Rep (ArithError n m) x -> ArithError n m
to :: forall x. Rep (ArithError n m) x -> ArithError n m
Generic)

instance (NFData n, NFData m) => NFData (ArithError n m)

-- | Class for unary arithmetic operation.
class UnaryArithOp aop (n :: T) where
  type UnaryArithRes aop n :: T
  evalUnaryArithOp :: proxy aop -> Value' instr n -> Value' instr (UnaryArithRes aop n)

-- | Class for conversions to an integer value.
class ToIntArithOp (n :: T) where
  evalToIntOp :: Value' instr n -> Value' instr 'TInt

-- | Class for conversions to bytes.
class ToBytesArithOp (n :: T) where
  evalToBytesOp :: Value' instr n -> Value' instr 'TBytes

data Add
data Sub
data SubMutez
data Mul
data EDiv
data Abs
data Neg

data Or
data And
data Xor
data Not
data Lsl
data Lsr

data Compare
data Eq'
data Neq
data Lt
data Gt
data Le
data Ge

-- For implementation hints see the reference implementation:
-- (note that you may need to change the branch)
-- https://gitlab.com/metastatedev/tezos/blob/master/src/proto_alpha/lib_protocol/script_ir_translator.ml#L4601

instance ArithOp Add 'TNat 'TInt where
  type ArithRes Add 'TNat 'TInt = 'TInt
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Add
-> Value' instr 'TNat
-> Value' instr 'TInt
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TInt))
     (Value' instr (ArithRes Add 'TNat 'TInt))
evalOp proxy Add
_ (VNat Natural
i) (VInt Integer
j) = Value' instr (ArithRes Add 'TNat 'TInt)
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TInt))
     (Value' instr (ArithRes Add 'TNat 'TInt))
forall a b. b -> Either a b
Right (Value' instr (ArithRes Add 'TNat 'TInt)
 -> Either
      (ArithError (Value' instr 'TNat) (Value' instr 'TInt))
      (Value' instr (ArithRes Add 'TNat 'TInt)))
-> Value' instr (ArithRes Add 'TNat 'TInt)
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TInt))
     (Value' instr (ArithRes Add 'TNat 'TInt))
forall a b. (a -> b) -> a -> b
$ Integer -> Value' instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
j)
  commutativityProof :: Maybe
$ Dict
    (ArithRes Add 'TNat 'TInt ~ ArithRes Add 'TInt 'TNat,
     ArithOp Add 'TInt 'TNat)
commutativityProof = Dict ('TInt ~ 'TInt, ArithOp Add 'TInt 'TNat)
-> Maybe (Dict ('TInt ~ 'TInt, ArithOp Add 'TInt 'TNat))
forall a. a -> Maybe a
Just Dict ('TInt ~ 'TInt, ArithOp Add 'TInt 'TNat)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Add 'TInt 'TNat where
  type ArithRes Add 'TInt 'TNat = 'TInt
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Add
-> Value' instr 'TInt
-> Value' instr 'TNat
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TNat))
     (Value' instr (ArithRes Add 'TInt 'TNat))
evalOp proxy Add
_ (VInt Integer
i) (VNat Natural
j) = Value' instr (ArithRes Add 'TInt 'TNat)
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TNat))
     (Value' instr (ArithRes Add 'TInt 'TNat))
forall a b. b -> Either a b
Right (Value' instr (ArithRes Add 'TInt 'TNat)
 -> Either
      (ArithError (Value' instr 'TInt) (Value' instr 'TNat))
      (Value' instr (ArithRes Add 'TInt 'TNat)))
-> Value' instr (ArithRes Add 'TInt 'TNat)
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TNat))
     (Value' instr (ArithRes Add 'TInt 'TNat))
forall a b. (a -> b) -> a -> b
$ Integer -> Value' instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
j)
  commutativityProof :: Maybe
$ Dict
    (ArithRes Add 'TInt 'TNat ~ ArithRes Add 'TNat 'TInt,
     ArithOp Add 'TNat 'TInt)
commutativityProof = Dict ('TInt ~ 'TInt, ArithOp Add 'TNat 'TInt)
-> Maybe (Dict ('TInt ~ 'TInt, ArithOp Add 'TNat 'TInt))
forall a. a -> Maybe a
Just Dict ('TInt ~ 'TInt, ArithOp Add 'TNat 'TInt)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Add 'TNat 'TNat where
  type ArithRes Add 'TNat 'TNat = 'TNat
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Add
-> Value' instr 'TNat
-> Value' instr 'TNat
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes Add 'TNat 'TNat))
evalOp proxy Add
_ (VNat Natural
i) (VNat Natural
j) = Value' instr (ArithRes Add 'TNat 'TNat)
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes Add 'TNat 'TNat))
forall a b. b -> Either a b
Right (Value' instr (ArithRes Add 'TNat 'TNat)
 -> Either
      (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
      (Value' instr (ArithRes Add 'TNat 'TNat)))
-> Value' instr (ArithRes Add 'TNat 'TNat)
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes Add 'TNat 'TNat))
forall a b. (a -> b) -> a -> b
$ Natural -> Value' instr 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat (Natural
i Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
j)
  commutativityProof :: Maybe
$ Dict
    (ArithRes Add 'TNat 'TNat ~ ArithRes Add 'TNat 'TNat,
     ArithOp Add 'TNat 'TNat)
commutativityProof = Dict ('TNat ~ 'TNat, ArithOp Add 'TNat 'TNat)
-> Maybe (Dict ('TNat ~ 'TNat, ArithOp Add 'TNat 'TNat))
forall a. a -> Maybe a
Just Dict ('TNat ~ 'TNat, ArithOp Add 'TNat 'TNat)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Add 'TInt 'TInt where
  type ArithRes Add 'TInt 'TInt = 'TInt
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Add
-> Value' instr 'TInt
-> Value' instr 'TInt
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TInt))
     (Value' instr (ArithRes Add 'TInt 'TInt))
evalOp proxy Add
_ (VInt Integer
i) (VInt Integer
j) = Value' instr (ArithRes Add 'TInt 'TInt)
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TInt))
     (Value' instr (ArithRes Add 'TInt 'TInt))
forall a b. b -> Either a b
Right (Value' instr (ArithRes Add 'TInt 'TInt)
 -> Either
      (ArithError (Value' instr 'TInt) (Value' instr 'TInt))
      (Value' instr (ArithRes Add 'TInt 'TInt)))
-> Value' instr (ArithRes Add 'TInt 'TInt)
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TInt))
     (Value' instr (ArithRes Add 'TInt 'TInt))
forall a b. (a -> b) -> a -> b
$ Integer -> Value' instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
j)
  commutativityProof :: Maybe
$ Dict
    (ArithRes Add 'TInt 'TInt ~ ArithRes Add 'TInt 'TInt,
     ArithOp Add 'TInt 'TInt)
commutativityProof = Dict ('TInt ~ 'TInt, ArithOp Add 'TInt 'TInt)
-> Maybe (Dict ('TInt ~ 'TInt, ArithOp Add 'TInt 'TInt))
forall a. a -> Maybe a
Just Dict ('TInt ~ 'TInt, ArithOp Add 'TInt 'TInt)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Add 'TTimestamp 'TInt where
  type ArithRes Add 'TTimestamp 'TInt = 'TTimestamp
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Add
-> Value' instr 'TTimestamp
-> Value' instr 'TInt
-> Either
     (ArithError (Value' instr 'TTimestamp) (Value' instr 'TInt))
     (Value' instr (ArithRes Add 'TTimestamp 'TInt))
evalOp proxy Add
_ (VTimestamp Timestamp
i) (VInt Integer
j) =
    Value' instr (ArithRes Add 'TTimestamp 'TInt)
-> Either
     (ArithError (Value' instr 'TTimestamp) (Value' instr 'TInt))
     (Value' instr (ArithRes Add 'TTimestamp 'TInt))
forall a b. b -> Either a b
Right (Value' instr (ArithRes Add 'TTimestamp 'TInt)
 -> Either
      (ArithError (Value' instr 'TTimestamp) (Value' instr 'TInt))
      (Value' instr (ArithRes Add 'TTimestamp 'TInt)))
-> Value' instr (ArithRes Add 'TTimestamp 'TInt)
-> Either
     (ArithError (Value' instr 'TTimestamp) (Value' instr 'TInt))
     (Value' instr (ArithRes Add 'TTimestamp 'TInt))
forall a b. (a -> b) -> a -> b
$ Timestamp -> Value' instr 'TTimestamp
forall (instr :: [T] -> [T] -> *).
Timestamp -> Value' instr 'TTimestamp
VTimestamp (Timestamp -> Value' instr 'TTimestamp)
-> Timestamp -> Value' instr 'TTimestamp
forall a b. (a -> b) -> a -> b
$ Integer -> Timestamp
timestampFromSeconds (Integer -> Timestamp) -> Integer -> Timestamp
forall a b. (a -> b) -> a -> b
$ Timestamp -> Integer
forall a. Integral a => Timestamp -> a
timestampToSeconds Timestamp
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
j
  commutativityProof :: Maybe
$ Dict
    (ArithRes Add 'TTimestamp 'TInt ~ ArithRes Add 'TInt 'TTimestamp,
     ArithOp Add 'TInt 'TTimestamp)
commutativityProof = Dict ('TTimestamp ~ 'TTimestamp, ArithOp Add 'TInt 'TTimestamp)
-> Maybe
     (Dict ('TTimestamp ~ 'TTimestamp, ArithOp Add 'TInt 'TTimestamp))
forall a. a -> Maybe a
Just Dict ('TTimestamp ~ 'TTimestamp, ArithOp Add 'TInt 'TTimestamp)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Add 'TInt 'TTimestamp where
  type ArithRes Add 'TInt 'TTimestamp = 'TTimestamp
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Add
-> Value' instr 'TInt
-> Value' instr 'TTimestamp
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TTimestamp))
     (Value' instr (ArithRes Add 'TInt 'TTimestamp))
evalOp proxy Add
_ (VInt Integer
i) (VTimestamp Timestamp
j) =
    Value' instr (ArithRes Add 'TInt 'TTimestamp)
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TTimestamp))
     (Value' instr (ArithRes Add 'TInt 'TTimestamp))
forall a b. b -> Either a b
Right (Value' instr (ArithRes Add 'TInt 'TTimestamp)
 -> Either
      (ArithError (Value' instr 'TInt) (Value' instr 'TTimestamp))
      (Value' instr (ArithRes Add 'TInt 'TTimestamp)))
-> Value' instr (ArithRes Add 'TInt 'TTimestamp)
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TTimestamp))
     (Value' instr (ArithRes Add 'TInt 'TTimestamp))
forall a b. (a -> b) -> a -> b
$ Timestamp -> Value' instr 'TTimestamp
forall (instr :: [T] -> [T] -> *).
Timestamp -> Value' instr 'TTimestamp
VTimestamp (Timestamp -> Value' instr 'TTimestamp)
-> Timestamp -> Value' instr 'TTimestamp
forall a b. (a -> b) -> a -> b
$ Integer -> Timestamp
timestampFromSeconds (Integer -> Timestamp) -> Integer -> Timestamp
forall a b. (a -> b) -> a -> b
$ Timestamp -> Integer
forall a. Integral a => Timestamp -> a
timestampToSeconds Timestamp
j Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
i
  commutativityProof :: Maybe
$ Dict
    (ArithRes Add 'TInt 'TTimestamp ~ ArithRes Add 'TTimestamp 'TInt,
     ArithOp Add 'TTimestamp 'TInt)
commutativityProof = Dict ('TTimestamp ~ 'TTimestamp, ArithOp Add 'TTimestamp 'TInt)
-> Maybe
     (Dict ('TTimestamp ~ 'TTimestamp, ArithOp Add 'TTimestamp 'TInt))
forall a. a -> Maybe a
Just Dict ('TTimestamp ~ 'TTimestamp, ArithOp Add 'TTimestamp 'TInt)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Add 'TMutez 'TMutez where
  type ArithRes Add 'TMutez 'TMutez = 'TMutez
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Add
-> Value' instr 'TMutez
-> Value' instr 'TMutez
-> Either
     (ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
     (Value' instr (ArithRes Add 'TMutez 'TMutez))
evalOp proxy Add
_ n :: Value' instr 'TMutez
n@(VMutez Mutez
i) m :: Value' instr 'TMutez
m@(VMutez Mutez
j) = Either
  (ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
  (Value' instr 'TMutez)
Either
  (ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
  (Value' instr (ArithRes Add 'TMutez 'TMutez))
res
    where
      res :: Either
  (ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
  (Value' instr 'TMutez)
res = Either
  (ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
  (Value' instr 'TMutez)
-> (Mutez
    -> Either
         (ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
         (Value' instr 'TMutez))
-> Maybe Mutez
-> Either
     (ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
     (Value' instr 'TMutez)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (ArithError (Value' instr 'TMutez) (Value' instr 'TMutez)
-> Either
     (ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
     (Value' instr 'TMutez)
forall a b. a -> Either a b
Left (ArithError (Value' instr 'TMutez) (Value' instr 'TMutez)
 -> Either
      (ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
      (Value' instr 'TMutez))
-> ArithError (Value' instr 'TMutez) (Value' instr 'TMutez)
-> Either
     (ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
     (Value' instr 'TMutez)
forall a b. (a -> b) -> a -> b
$ MutezArithErrorType
-> Value' instr 'TMutez
-> Value' instr 'TMutez
-> ArithError (Value' instr 'TMutez) (Value' instr 'TMutez)
forall n m. MutezArithErrorType -> n -> m -> ArithError n m
MutezArithError MutezArithErrorType
AddOverflow Value' instr 'TMutez
n Value' instr 'TMutez
m) (Value' instr 'TMutez
-> Either
     (ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
     (Value' instr 'TMutez)
forall a b. b -> Either a b
Right (Value' instr 'TMutez
 -> Either
      (ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
      (Value' instr 'TMutez))
-> (Mutez -> Value' instr 'TMutez)
-> Mutez
-> Either
     (ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
     (Value' instr 'TMutez)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Mutez -> Value' instr 'TMutez
forall (instr :: [T] -> [T] -> *). Mutez -> Value' instr 'TMutez
VMutez) (Maybe Mutez
 -> Either
      (ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
      (Value' instr 'TMutez))
-> Maybe Mutez
-> Either
     (ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
     (Value' instr 'TMutez)
forall a b. (a -> b) -> a -> b
$ Mutez
i Mutez -> Mutez -> Maybe Mutez
`addMutez` Mutez
j
  commutativityProof :: Maybe
$ Dict
    (ArithRes Add 'TMutez 'TMutez ~ ArithRes Add 'TMutez 'TMutez,
     ArithOp Add 'TMutez 'TMutez)
commutativityProof = Dict ('TMutez ~ 'TMutez, ArithOp Add 'TMutez 'TMutez)
-> Maybe (Dict ('TMutez ~ 'TMutez, ArithOp Add 'TMutez 'TMutez))
forall a. a -> Maybe a
Just Dict ('TMutez ~ 'TMutez, ArithOp Add 'TMutez 'TMutez)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Add 'TBls12381Fr 'TBls12381Fr where
  type ArithRes Add 'TBls12381Fr 'TBls12381Fr = 'TBls12381Fr
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Add
-> Value' instr 'TBls12381Fr
-> Value' instr 'TBls12381Fr
-> Either
     (ArithError
        (Value' instr 'TBls12381Fr) (Value' instr 'TBls12381Fr))
     (Value' instr (ArithRes Add 'TBls12381Fr 'TBls12381Fr))
evalOp proxy Add
_ (VBls12381Fr Bls12381Fr
i) (VBls12381Fr Bls12381Fr
j) =
    Value' instr (ArithRes Add 'TBls12381Fr 'TBls12381Fr)
-> Either
     (ArithError
        (Value' instr 'TBls12381Fr) (Value' instr 'TBls12381Fr))
     (Value' instr (ArithRes Add 'TBls12381Fr 'TBls12381Fr))
forall a b. b -> Either a b
Right (Value' instr (ArithRes Add 'TBls12381Fr 'TBls12381Fr)
 -> Either
      (ArithError
         (Value' instr 'TBls12381Fr) (Value' instr 'TBls12381Fr))
      (Value' instr (ArithRes Add 'TBls12381Fr 'TBls12381Fr)))
-> Value' instr (ArithRes Add 'TBls12381Fr 'TBls12381Fr)
-> Either
     (ArithError
        (Value' instr 'TBls12381Fr) (Value' instr 'TBls12381Fr))
     (Value' instr (ArithRes Add 'TBls12381Fr 'TBls12381Fr))
forall a b. (a -> b) -> a -> b
$ Bls12381Fr -> Value' instr 'TBls12381Fr
forall (instr :: [T] -> [T] -> *).
Bls12381Fr -> Value' instr 'TBls12381Fr
VBls12381Fr (Bls12381Fr -> Bls12381Fr -> Bls12381Fr
forall a. CurveObject a => a -> a -> a
BLS.add Bls12381Fr
i Bls12381Fr
j)
  commutativityProof :: Maybe
$ Dict
    (ArithRes Add 'TBls12381Fr 'TBls12381Fr
     ~ ArithRes Add 'TBls12381Fr 'TBls12381Fr,
     ArithOp Add 'TBls12381Fr 'TBls12381Fr)
commutativityProof = Dict
  ('TBls12381Fr ~ 'TBls12381Fr,
   ArithOp Add 'TBls12381Fr 'TBls12381Fr)
-> Maybe
     (Dict
        ('TBls12381Fr ~ 'TBls12381Fr,
         ArithOp Add 'TBls12381Fr 'TBls12381Fr))
forall a. a -> Maybe a
Just Dict
  ('TBls12381Fr ~ 'TBls12381Fr,
   ArithOp Add 'TBls12381Fr 'TBls12381Fr)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Add 'TBls12381G1 'TBls12381G1 where
  type ArithRes Add 'TBls12381G1 'TBls12381G1 = 'TBls12381G1
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Add
-> Value' instr 'TBls12381G1
-> Value' instr 'TBls12381G1
-> Either
     (ArithError
        (Value' instr 'TBls12381G1) (Value' instr 'TBls12381G1))
     (Value' instr (ArithRes Add 'TBls12381G1 'TBls12381G1))
evalOp proxy Add
_ (VBls12381G1 Bls12381G1
i) (VBls12381G1 Bls12381G1
j) =
    Value' instr (ArithRes Add 'TBls12381G1 'TBls12381G1)
-> Either
     (ArithError
        (Value' instr 'TBls12381G1) (Value' instr 'TBls12381G1))
     (Value' instr (ArithRes Add 'TBls12381G1 'TBls12381G1))
forall a b. b -> Either a b
Right (Value' instr (ArithRes Add 'TBls12381G1 'TBls12381G1)
 -> Either
      (ArithError
         (Value' instr 'TBls12381G1) (Value' instr 'TBls12381G1))
      (Value' instr (ArithRes Add 'TBls12381G1 'TBls12381G1)))
-> Value' instr (ArithRes Add 'TBls12381G1 'TBls12381G1)
-> Either
     (ArithError
        (Value' instr 'TBls12381G1) (Value' instr 'TBls12381G1))
     (Value' instr (ArithRes Add 'TBls12381G1 'TBls12381G1))
forall a b. (a -> b) -> a -> b
$ Bls12381G1 -> Value' instr 'TBls12381G1
forall (instr :: [T] -> [T] -> *).
Bls12381G1 -> Value' instr 'TBls12381G1
VBls12381G1 (Bls12381G1 -> Bls12381G1 -> Bls12381G1
forall a. CurveObject a => a -> a -> a
BLS.add Bls12381G1
i Bls12381G1
j)
  commutativityProof :: Maybe
$ Dict
    (ArithRes Add 'TBls12381G1 'TBls12381G1
     ~ ArithRes Add 'TBls12381G1 'TBls12381G1,
     ArithOp Add 'TBls12381G1 'TBls12381G1)
commutativityProof = Dict
  ('TBls12381G1 ~ 'TBls12381G1,
   ArithOp Add 'TBls12381G1 'TBls12381G1)
-> Maybe
     (Dict
        ('TBls12381G1 ~ 'TBls12381G1,
         ArithOp Add 'TBls12381G1 'TBls12381G1))
forall a. a -> Maybe a
Just Dict
  ('TBls12381G1 ~ 'TBls12381G1,
   ArithOp Add 'TBls12381G1 'TBls12381G1)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Add 'TBls12381G2 'TBls12381G2 where
  type ArithRes Add 'TBls12381G2 'TBls12381G2 = 'TBls12381G2
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Add
-> Value' instr 'TBls12381G2
-> Value' instr 'TBls12381G2
-> Either
     (ArithError
        (Value' instr 'TBls12381G2) (Value' instr 'TBls12381G2))
     (Value' instr (ArithRes Add 'TBls12381G2 'TBls12381G2))
evalOp proxy Add
_ (VBls12381G2 Bls12381G2
i) (VBls12381G2 Bls12381G2
j) =
    Value' instr (ArithRes Add 'TBls12381G2 'TBls12381G2)
-> Either
     (ArithError
        (Value' instr 'TBls12381G2) (Value' instr 'TBls12381G2))
     (Value' instr (ArithRes Add 'TBls12381G2 'TBls12381G2))
forall a b. b -> Either a b
Right (Value' instr (ArithRes Add 'TBls12381G2 'TBls12381G2)
 -> Either
      (ArithError
         (Value' instr 'TBls12381G2) (Value' instr 'TBls12381G2))
      (Value' instr (ArithRes Add 'TBls12381G2 'TBls12381G2)))
-> Value' instr (ArithRes Add 'TBls12381G2 'TBls12381G2)
-> Either
     (ArithError
        (Value' instr 'TBls12381G2) (Value' instr 'TBls12381G2))
     (Value' instr (ArithRes Add 'TBls12381G2 'TBls12381G2))
forall a b. (a -> b) -> a -> b
$ Bls12381G2 -> Value' instr 'TBls12381G2
forall (instr :: [T] -> [T] -> *).
Bls12381G2 -> Value' instr 'TBls12381G2
VBls12381G2 (Bls12381G2 -> Bls12381G2 -> Bls12381G2
forall a. CurveObject a => a -> a -> a
BLS.add Bls12381G2
i Bls12381G2
j)
  commutativityProof :: Maybe
$ Dict
    (ArithRes Add 'TBls12381G2 'TBls12381G2
     ~ ArithRes Add 'TBls12381G2 'TBls12381G2,
     ArithOp Add 'TBls12381G2 'TBls12381G2)
commutativityProof = Dict
  ('TBls12381G2 ~ 'TBls12381G2,
   ArithOp Add 'TBls12381G2 'TBls12381G2)
-> Maybe
     (Dict
        ('TBls12381G2 ~ 'TBls12381G2,
         ArithOp Add 'TBls12381G2 'TBls12381G2))
forall a. a -> Maybe a
Just Dict
  ('TBls12381G2 ~ 'TBls12381G2,
   ArithOp Add 'TBls12381G2 'TBls12381G2)
forall (a :: Constraint). a => Dict a
Dict

instance ArithOp Sub 'TNat 'TInt where
  type ArithRes Sub 'TNat 'TInt = 'TInt
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Sub
-> Value' instr 'TNat
-> Value' instr 'TInt
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TInt))
     (Value' instr (ArithRes Sub 'TNat 'TInt))
evalOp proxy Sub
_ (VNat Natural
i) (VInt Integer
j) = Value' instr (ArithRes Sub 'TNat 'TInt)
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TInt))
     (Value' instr (ArithRes Sub 'TNat 'TInt))
forall a b. b -> Either a b
Right (Value' instr (ArithRes Sub 'TNat 'TInt)
 -> Either
      (ArithError (Value' instr 'TNat) (Value' instr 'TInt))
      (Value' instr (ArithRes Sub 'TNat 'TInt)))
-> Value' instr (ArithRes Sub 'TNat 'TInt)
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TInt))
     (Value' instr (ArithRes Sub 'TNat 'TInt))
forall a b. (a -> b) -> a -> b
$ Integer -> Value' instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
j)
instance ArithOp Sub 'TInt 'TNat where
  type ArithRes Sub 'TInt 'TNat = 'TInt
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Sub
-> Value' instr 'TInt
-> Value' instr 'TNat
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TNat))
     (Value' instr (ArithRes Sub 'TInt 'TNat))
evalOp proxy Sub
_ (VInt Integer
i) (VNat Natural
j) = Value' instr (ArithRes Sub 'TInt 'TNat)
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TNat))
     (Value' instr (ArithRes Sub 'TInt 'TNat))
forall a b. b -> Either a b
Right (Value' instr (ArithRes Sub 'TInt 'TNat)
 -> Either
      (ArithError (Value' instr 'TInt) (Value' instr 'TNat))
      (Value' instr (ArithRes Sub 'TInt 'TNat)))
-> Value' instr (ArithRes Sub 'TInt 'TNat)
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TNat))
     (Value' instr (ArithRes Sub 'TInt 'TNat))
forall a b. (a -> b) -> a -> b
$ Integer -> Value' instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
j)
instance ArithOp Sub 'TNat 'TNat where
  type ArithRes Sub 'TNat 'TNat = 'TInt
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Sub
-> Value' instr 'TNat
-> Value' instr 'TNat
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes Sub 'TNat 'TNat))
evalOp proxy Sub
_ (VNat Natural
i) (VNat Natural
j) = Value' instr (ArithRes Sub 'TNat 'TNat)
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes Sub 'TNat 'TNat))
forall a b. b -> Either a b
Right (Value' instr (ArithRes Sub 'TNat 'TNat)
 -> Either
      (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
      (Value' instr (ArithRes Sub 'TNat 'TNat)))
-> Value' instr (ArithRes Sub 'TNat 'TNat)
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes Sub 'TNat 'TNat))
forall a b. (a -> b) -> a -> b
$ Integer -> Value' instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
j)
instance ArithOp Sub 'TInt 'TInt where
  type ArithRes Sub 'TInt 'TInt = 'TInt
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Sub
-> Value' instr 'TInt
-> Value' instr 'TInt
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TInt))
     (Value' instr (ArithRes Sub 'TInt 'TInt))
evalOp proxy Sub
_ (VInt Integer
i) (VInt Integer
j) = Value' instr (ArithRes Sub 'TInt 'TInt)
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TInt))
     (Value' instr (ArithRes Sub 'TInt 'TInt))
forall a b. b -> Either a b
Right (Value' instr (ArithRes Sub 'TInt 'TInt)
 -> Either
      (ArithError (Value' instr 'TInt) (Value' instr 'TInt))
      (Value' instr (ArithRes Sub 'TInt 'TInt)))
-> Value' instr (ArithRes Sub 'TInt 'TInt)
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TInt))
     (Value' instr (ArithRes Sub 'TInt 'TInt))
forall a b. (a -> b) -> a -> b
$ Integer -> Value' instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
j)
instance ArithOp Sub 'TTimestamp 'TInt where
  type ArithRes Sub 'TTimestamp 'TInt = 'TTimestamp
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Sub
-> Value' instr 'TTimestamp
-> Value' instr 'TInt
-> Either
     (ArithError (Value' instr 'TTimestamp) (Value' instr 'TInt))
     (Value' instr (ArithRes Sub 'TTimestamp 'TInt))
evalOp proxy Sub
_ (VTimestamp Timestamp
i) (VInt Integer
j) =
    Value' instr (ArithRes Sub 'TTimestamp 'TInt)
-> Either
     (ArithError (Value' instr 'TTimestamp) (Value' instr 'TInt))
     (Value' instr (ArithRes Sub 'TTimestamp 'TInt))
forall a b. b -> Either a b
Right (Value' instr (ArithRes Sub 'TTimestamp 'TInt)
 -> Either
      (ArithError (Value' instr 'TTimestamp) (Value' instr 'TInt))
      (Value' instr (ArithRes Sub 'TTimestamp 'TInt)))
-> Value' instr (ArithRes Sub 'TTimestamp 'TInt)
-> Either
     (ArithError (Value' instr 'TTimestamp) (Value' instr 'TInt))
     (Value' instr (ArithRes Sub 'TTimestamp 'TInt))
forall a b. (a -> b) -> a -> b
$ Timestamp -> Value' instr 'TTimestamp
forall (instr :: [T] -> [T] -> *).
Timestamp -> Value' instr 'TTimestamp
VTimestamp (Timestamp -> Value' instr 'TTimestamp)
-> Timestamp -> Value' instr 'TTimestamp
forall a b. (a -> b) -> a -> b
$ Integer -> Timestamp
timestampFromSeconds (Integer -> Timestamp) -> Integer -> Timestamp
forall a b. (a -> b) -> a -> b
$ Timestamp -> Integer
forall a. Integral a => Timestamp -> a
timestampToSeconds Timestamp
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
j
instance ArithOp Sub 'TTimestamp 'TTimestamp where
  type ArithRes Sub 'TTimestamp 'TTimestamp = 'TInt
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Sub
-> Value' instr 'TTimestamp
-> Value' instr 'TTimestamp
-> Either
     (ArithError (Value' instr 'TTimestamp) (Value' instr 'TTimestamp))
     (Value' instr (ArithRes Sub 'TTimestamp 'TTimestamp))
evalOp proxy Sub
_ (VTimestamp Timestamp
i) (VTimestamp Timestamp
j) =
    Value' instr (ArithRes Sub 'TTimestamp 'TTimestamp)
-> Either
     (ArithError (Value' instr 'TTimestamp) (Value' instr 'TTimestamp))
     (Value' instr (ArithRes Sub 'TTimestamp 'TTimestamp))
forall a b. b -> Either a b
Right (Value' instr (ArithRes Sub 'TTimestamp 'TTimestamp)
 -> Either
      (ArithError (Value' instr 'TTimestamp) (Value' instr 'TTimestamp))
      (Value' instr (ArithRes Sub 'TTimestamp 'TTimestamp)))
-> Value' instr (ArithRes Sub 'TTimestamp 'TTimestamp)
-> Either
     (ArithError (Value' instr 'TTimestamp) (Value' instr 'TTimestamp))
     (Value' instr (ArithRes Sub 'TTimestamp 'TTimestamp))
forall a b. (a -> b) -> a -> b
$ Integer -> Value' instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt (Integer -> Value' instr 'TInt) -> Integer -> Value' instr 'TInt
forall a b. (a -> b) -> a -> b
$ Timestamp -> Integer
forall a. Integral a => Timestamp -> a
timestampToSeconds Timestamp
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Timestamp -> Integer
forall a. Integral a => Timestamp -> a
timestampToSeconds Timestamp
j
instance ArithOp SubMutez 'TMutez 'TMutez where
  type ArithRes SubMutez 'TMutez 'TMutez = 'TOption 'TMutez
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy SubMutez
-> Value' instr 'TMutez
-> Value' instr 'TMutez
-> Either
     (ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
     (Value' instr (ArithRes SubMutez 'TMutez 'TMutez))
evalOp proxy SubMutez
_ (VMutez Mutez
i) (VMutez Mutez
j) =
    Value' instr (ArithRes SubMutez 'TMutez 'TMutez)
-> Either
     (ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
     (Value' instr (ArithRes SubMutez 'TMutez 'TMutez))
forall a b. b -> Either a b
Right (Value' instr (ArithRes SubMutez 'TMutez 'TMutez)
 -> Either
      (ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
      (Value' instr (ArithRes SubMutez 'TMutez 'TMutez)))
-> Value' instr (ArithRes SubMutez 'TMutez 'TMutez)
-> Either
     (ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
     (Value' instr (ArithRes SubMutez 'TMutez 'TMutez))
forall a b. (a -> b) -> a -> b
$ Maybe (Value' instr 'TMutez) -> Value' instr ('TOption 'TMutez)
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
Maybe (Value' instr t1) -> Value' instr ('TOption t1)
VOption (Maybe (Value' instr 'TMutez) -> Value' instr ('TOption 'TMutez))
-> Maybe (Value' instr 'TMutez) -> Value' instr ('TOption 'TMutez)
forall a b. (a -> b) -> a -> b
$ (Mutez -> Value' instr 'TMutez)
-> Maybe Mutez -> Maybe (Value' instr 'TMutez)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Mutez -> Value' instr 'TMutez
forall (instr :: [T] -> [T] -> *). Mutez -> Value' instr 'TMutez
VMutez (Maybe Mutez -> Maybe (Value' instr 'TMutez))
-> Maybe Mutez -> Maybe (Value' instr 'TMutez)
forall a b. (a -> b) -> a -> b
$ Mutez
i Mutez -> Mutez -> Maybe Mutez
`subMutez` Mutez
j

instance ArithOp Mul 'TNat 'TInt where
  type ArithRes Mul 'TNat 'TInt = 'TInt
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Mul
-> Value' instr 'TNat
-> Value' instr 'TInt
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TInt))
     (Value' instr (ArithRes Mul 'TNat 'TInt))
evalOp proxy Mul
_ (VNat Natural
i) (VInt Integer
j) = Value' instr (ArithRes Mul 'TNat 'TInt)
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TInt))
     (Value' instr (ArithRes Mul 'TNat 'TInt))
forall a b. b -> Either a b
Right (Value' instr (ArithRes Mul 'TNat 'TInt)
 -> Either
      (ArithError (Value' instr 'TNat) (Value' instr 'TInt))
      (Value' instr (ArithRes Mul 'TNat 'TInt)))
-> Value' instr (ArithRes Mul 'TNat 'TInt)
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TInt))
     (Value' instr (ArithRes Mul 'TNat 'TInt))
forall a b. (a -> b) -> a -> b
$ Integer -> Value' instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
j)
  commutativityProof :: Maybe
$ Dict
    (ArithRes Mul 'TNat 'TInt ~ ArithRes Mul 'TInt 'TNat,
     ArithOp Mul 'TInt 'TNat)
commutativityProof = Dict ('TInt ~ 'TInt, ArithOp Mul 'TInt 'TNat)
-> Maybe (Dict ('TInt ~ 'TInt, ArithOp Mul 'TInt 'TNat))
forall a. a -> Maybe a
Just Dict ('TInt ~ 'TInt, ArithOp Mul 'TInt 'TNat)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Mul 'TInt 'TNat where
  type ArithRes Mul 'TInt 'TNat = 'TInt
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Mul
-> Value' instr 'TInt
-> Value' instr 'TNat
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TNat))
     (Value' instr (ArithRes Mul 'TInt 'TNat))
evalOp proxy Mul
_ (VInt Integer
i) (VNat Natural
j) = Value' instr (ArithRes Mul 'TInt 'TNat)
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TNat))
     (Value' instr (ArithRes Mul 'TInt 'TNat))
forall a b. b -> Either a b
Right (Value' instr (ArithRes Mul 'TInt 'TNat)
 -> Either
      (ArithError (Value' instr 'TInt) (Value' instr 'TNat))
      (Value' instr (ArithRes Mul 'TInt 'TNat)))
-> Value' instr (ArithRes Mul 'TInt 'TNat)
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TNat))
     (Value' instr (ArithRes Mul 'TInt 'TNat))
forall a b. (a -> b) -> a -> b
$ Integer -> Value' instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
j)
  commutativityProof :: Maybe
$ Dict
    (ArithRes Mul 'TInt 'TNat ~ ArithRes Mul 'TNat 'TInt,
     ArithOp Mul 'TNat 'TInt)
commutativityProof = Dict ('TInt ~ 'TInt, ArithOp Mul 'TNat 'TInt)
-> Maybe (Dict ('TInt ~ 'TInt, ArithOp Mul 'TNat 'TInt))
forall a. a -> Maybe a
Just Dict ('TInt ~ 'TInt, ArithOp Mul 'TNat 'TInt)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Mul 'TNat 'TNat where
  type ArithRes Mul 'TNat 'TNat = 'TNat
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Mul
-> Value' instr 'TNat
-> Value' instr 'TNat
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes Mul 'TNat 'TNat))
evalOp proxy Mul
_ (VNat Natural
i) (VNat Natural
j) = Value' instr (ArithRes Mul 'TNat 'TNat)
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes Mul 'TNat 'TNat))
forall a b. b -> Either a b
Right (Value' instr (ArithRes Mul 'TNat 'TNat)
 -> Either
      (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
      (Value' instr (ArithRes Mul 'TNat 'TNat)))
-> Value' instr (ArithRes Mul 'TNat 'TNat)
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes Mul 'TNat 'TNat))
forall a b. (a -> b) -> a -> b
$ Natural -> Value' instr 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat (Natural
i Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
j)
  commutativityProof :: Maybe
$ Dict
    (ArithRes Mul 'TNat 'TNat ~ ArithRes Mul 'TNat 'TNat,
     ArithOp Mul 'TNat 'TNat)
commutativityProof = Dict ('TNat ~ 'TNat, ArithOp Mul 'TNat 'TNat)
-> Maybe (Dict ('TNat ~ 'TNat, ArithOp Mul 'TNat 'TNat))
forall a. a -> Maybe a
Just Dict ('TNat ~ 'TNat, ArithOp Mul 'TNat 'TNat)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Mul 'TInt 'TInt where
  type ArithRes Mul 'TInt 'TInt = 'TInt
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Mul
-> Value' instr 'TInt
-> Value' instr 'TInt
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TInt))
     (Value' instr (ArithRes Mul 'TInt 'TInt))
evalOp proxy Mul
_ (VInt Integer
i) (VInt Integer
j) = Value' instr (ArithRes Mul 'TInt 'TInt)
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TInt))
     (Value' instr (ArithRes Mul 'TInt 'TInt))
forall a b. b -> Either a b
Right (Value' instr (ArithRes Mul 'TInt 'TInt)
 -> Either
      (ArithError (Value' instr 'TInt) (Value' instr 'TInt))
      (Value' instr (ArithRes Mul 'TInt 'TInt)))
-> Value' instr (ArithRes Mul 'TInt 'TInt)
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TInt))
     (Value' instr (ArithRes Mul 'TInt 'TInt))
forall a b. (a -> b) -> a -> b
$ Integer -> Value' instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
j)
  commutativityProof :: Maybe
$ Dict
    (ArithRes Mul 'TInt 'TInt ~ ArithRes Mul 'TInt 'TInt,
     ArithOp Mul 'TInt 'TInt)
commutativityProof = Dict ('TInt ~ 'TInt, ArithOp Mul 'TInt 'TInt)
-> Maybe (Dict ('TInt ~ 'TInt, ArithOp Mul 'TInt 'TInt))
forall a. a -> Maybe a
Just Dict ('TInt ~ 'TInt, ArithOp Mul 'TInt 'TInt)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Mul 'TNat 'TMutez where
  type ArithRes Mul 'TNat 'TMutez = 'TMutez
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Mul
-> Value' instr 'TNat
-> Value' instr 'TMutez
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TMutez))
     (Value' instr (ArithRes Mul 'TNat 'TMutez))
evalOp proxy Mul
_ n :: Value' instr 'TNat
n@(VNat Natural
i) m :: Value' instr 'TMutez
m@(VMutez Mutez
j) = Either
  (ArithError (Value' instr 'TNat) (Value' instr 'TMutez))
  (Value' instr 'TMutez)
Either
  (ArithError (Value' instr 'TNat) (Value' instr 'TMutez))
  (Value' instr (ArithRes Mul 'TNat 'TMutez))
res
    where
      res :: Either
  (ArithError (Value' instr 'TNat) (Value' instr 'TMutez))
  (Value' instr 'TMutez)
res = Either
  (ArithError (Value' instr 'TNat) (Value' instr 'TMutez))
  (Value' instr 'TMutez)
-> (Mutez
    -> Either
         (ArithError (Value' instr 'TNat) (Value' instr 'TMutez))
         (Value' instr 'TMutez))
-> Maybe Mutez
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TMutez))
     (Value' instr 'TMutez)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (ArithError (Value' instr 'TNat) (Value' instr 'TMutez)
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TMutez))
     (Value' instr 'TMutez)
forall a b. a -> Either a b
Left (ArithError (Value' instr 'TNat) (Value' instr 'TMutez)
 -> Either
      (ArithError (Value' instr 'TNat) (Value' instr 'TMutez))
      (Value' instr 'TMutez))
-> ArithError (Value' instr 'TNat) (Value' instr 'TMutez)
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TMutez))
     (Value' instr 'TMutez)
forall a b. (a -> b) -> a -> b
$ MutezArithErrorType
-> Value' instr 'TNat
-> Value' instr 'TMutez
-> ArithError (Value' instr 'TNat) (Value' instr 'TMutez)
forall n m. MutezArithErrorType -> n -> m -> ArithError n m
MutezArithError MutezArithErrorType
MulOverflow Value' instr 'TNat
n Value' instr 'TMutez
m) (Value' instr 'TMutez
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TMutez))
     (Value' instr 'TMutez)
forall a b. b -> Either a b
Right (Value' instr 'TMutez
 -> Either
      (ArithError (Value' instr 'TNat) (Value' instr 'TMutez))
      (Value' instr 'TMutez))
-> (Mutez -> Value' instr 'TMutez)
-> Mutez
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TMutez))
     (Value' instr 'TMutez)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Mutez -> Value' instr 'TMutez
forall (instr :: [T] -> [T] -> *). Mutez -> Value' instr 'TMutez
VMutez) (Maybe Mutez
 -> Either
      (ArithError (Value' instr 'TNat) (Value' instr 'TMutez))
      (Value' instr 'TMutez))
-> Maybe Mutez
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TMutez))
     (Value' instr 'TMutez)
forall a b. (a -> b) -> a -> b
$ Mutez
j Mutez -> Natural -> Maybe Mutez
forall a. Integral a => Mutez -> a -> Maybe Mutez
`mulMutez` Natural
i
  commutativityProof :: Maybe
$ Dict
    (ArithRes Mul 'TNat 'TMutez ~ ArithRes Mul 'TMutez 'TNat,
     ArithOp Mul 'TMutez 'TNat)
commutativityProof = Dict ('TMutez ~ 'TMutez, ArithOp Mul 'TMutez 'TNat)
-> Maybe (Dict ('TMutez ~ 'TMutez, ArithOp Mul 'TMutez 'TNat))
forall a. a -> Maybe a
Just Dict ('TMutez ~ 'TMutez, ArithOp Mul 'TMutez 'TNat)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Mul 'TMutez 'TNat where
  type ArithRes Mul 'TMutez 'TNat = 'TMutez
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Mul
-> Value' instr 'TMutez
-> Value' instr 'TNat
-> Either
     (ArithError (Value' instr 'TMutez) (Value' instr 'TNat))
     (Value' instr (ArithRes Mul 'TMutez 'TNat))
evalOp proxy Mul
_ n :: Value' instr 'TMutez
n@(VMutez Mutez
i) m :: Value' instr 'TNat
m@(VNat Natural
j) = Either
  (ArithError (Value' instr 'TMutez) (Value' instr 'TNat))
  (Value' instr 'TMutez)
Either
  (ArithError (Value' instr 'TMutez) (Value' instr 'TNat))
  (Value' instr (ArithRes Mul 'TMutez 'TNat))
res
    where
      res :: Either
  (ArithError (Value' instr 'TMutez) (Value' instr 'TNat))
  (Value' instr 'TMutez)
res = Either
  (ArithError (Value' instr 'TMutez) (Value' instr 'TNat))
  (Value' instr 'TMutez)
-> (Mutez
    -> Either
         (ArithError (Value' instr 'TMutez) (Value' instr 'TNat))
         (Value' instr 'TMutez))
-> Maybe Mutez
-> Either
     (ArithError (Value' instr 'TMutez) (Value' instr 'TNat))
     (Value' instr 'TMutez)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (ArithError (Value' instr 'TMutez) (Value' instr 'TNat)
-> Either
     (ArithError (Value' instr 'TMutez) (Value' instr 'TNat))
     (Value' instr 'TMutez)
forall a b. a -> Either a b
Left (ArithError (Value' instr 'TMutez) (Value' instr 'TNat)
 -> Either
      (ArithError (Value' instr 'TMutez) (Value' instr 'TNat))
      (Value' instr 'TMutez))
-> ArithError (Value' instr 'TMutez) (Value' instr 'TNat)
-> Either
     (ArithError (Value' instr 'TMutez) (Value' instr 'TNat))
     (Value' instr 'TMutez)
forall a b. (a -> b) -> a -> b
$ MutezArithErrorType
-> Value' instr 'TMutez
-> Value' instr 'TNat
-> ArithError (Value' instr 'TMutez) (Value' instr 'TNat)
forall n m. MutezArithErrorType -> n -> m -> ArithError n m
MutezArithError MutezArithErrorType
MulOverflow Value' instr 'TMutez
n Value' instr 'TNat
m) (Value' instr 'TMutez
-> Either
     (ArithError (Value' instr 'TMutez) (Value' instr 'TNat))
     (Value' instr 'TMutez)
forall a b. b -> Either a b
Right (Value' instr 'TMutez
 -> Either
      (ArithError (Value' instr 'TMutez) (Value' instr 'TNat))
      (Value' instr 'TMutez))
-> (Mutez -> Value' instr 'TMutez)
-> Mutez
-> Either
     (ArithError (Value' instr 'TMutez) (Value' instr 'TNat))
     (Value' instr 'TMutez)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Mutez -> Value' instr 'TMutez
forall (instr :: [T] -> [T] -> *). Mutez -> Value' instr 'TMutez
VMutez) (Maybe Mutez
 -> Either
      (ArithError (Value' instr 'TMutez) (Value' instr 'TNat))
      (Value' instr 'TMutez))
-> Maybe Mutez
-> Either
     (ArithError (Value' instr 'TMutez) (Value' instr 'TNat))
     (Value' instr 'TMutez)
forall a b. (a -> b) -> a -> b
$ Mutez
i Mutez -> Natural -> Maybe Mutez
forall a. Integral a => Mutez -> a -> Maybe Mutez
`mulMutez` Natural
j
  commutativityProof :: Maybe
$ Dict
    (ArithRes Mul 'TMutez 'TNat ~ ArithRes Mul 'TNat 'TMutez,
     ArithOp Mul 'TNat 'TMutez)
commutativityProof = Dict ('TMutez ~ 'TMutez, ArithOp Mul 'TNat 'TMutez)
-> Maybe (Dict ('TMutez ~ 'TMutez, ArithOp Mul 'TNat 'TMutez))
forall a. a -> Maybe a
Just Dict ('TMutez ~ 'TMutez, ArithOp Mul 'TNat 'TMutez)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Mul 'TInt 'TBls12381Fr where
  type ArithRes Mul 'TInt 'TBls12381Fr = 'TBls12381Fr
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Mul
-> Value' instr 'TInt
-> Value' instr 'TBls12381Fr
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TBls12381Fr))
     (Value' instr (ArithRes Mul 'TInt 'TBls12381Fr))
evalOp proxy Mul
_ (VInt Integer
i) (VBls12381Fr Bls12381Fr
j) = Value' instr (ArithRes Mul 'TInt 'TBls12381Fr)
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TBls12381Fr))
     (Value' instr (ArithRes Mul 'TInt 'TBls12381Fr))
forall a b. b -> Either a b
Right (Value' instr (ArithRes Mul 'TInt 'TBls12381Fr)
 -> Either
      (ArithError (Value' instr 'TInt) (Value' instr 'TBls12381Fr))
      (Value' instr (ArithRes Mul 'TInt 'TBls12381Fr)))
-> Value' instr (ArithRes Mul 'TInt 'TBls12381Fr)
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TBls12381Fr))
     (Value' instr (ArithRes Mul 'TInt 'TBls12381Fr))
forall a b. (a -> b) -> a -> b
$ Bls12381Fr -> Value' instr 'TBls12381Fr
forall (instr :: [T] -> [T] -> *).
Bls12381Fr -> Value' instr 'TBls12381Fr
VBls12381Fr (forall a b. (Integral a, Num b) => a -> b
fromIntegralOverflowing @Integer @BLS.Bls12381Fr Integer
i Bls12381Fr -> Bls12381Fr -> Bls12381Fr
forall a. Num a => a -> a -> a
* Bls12381Fr
j)
  commutativityProof :: Maybe
$ Dict
    (ArithRes Mul 'TInt 'TBls12381Fr ~ ArithRes Mul 'TBls12381Fr 'TInt,
     ArithOp Mul 'TBls12381Fr 'TInt)
commutativityProof = Dict ('TBls12381Fr ~ 'TBls12381Fr, ArithOp Mul 'TBls12381Fr 'TInt)
-> Maybe
     (Dict
        ('TBls12381Fr ~ 'TBls12381Fr, ArithOp Mul 'TBls12381Fr 'TInt))
forall a. a -> Maybe a
Just Dict ('TBls12381Fr ~ 'TBls12381Fr, ArithOp Mul 'TBls12381Fr 'TInt)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Mul 'TNat 'TBls12381Fr where
  type ArithRes Mul 'TNat 'TBls12381Fr = 'TBls12381Fr
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Mul
-> Value' instr 'TNat
-> Value' instr 'TBls12381Fr
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TBls12381Fr))
     (Value' instr (ArithRes Mul 'TNat 'TBls12381Fr))
evalOp proxy Mul
_ (VNat Natural
i) (VBls12381Fr Bls12381Fr
j) = Value' instr (ArithRes Mul 'TNat 'TBls12381Fr)
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TBls12381Fr))
     (Value' instr (ArithRes Mul 'TNat 'TBls12381Fr))
forall a b. b -> Either a b
Right (Value' instr (ArithRes Mul 'TNat 'TBls12381Fr)
 -> Either
      (ArithError (Value' instr 'TNat) (Value' instr 'TBls12381Fr))
      (Value' instr (ArithRes Mul 'TNat 'TBls12381Fr)))
-> Value' instr (ArithRes Mul 'TNat 'TBls12381Fr)
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TBls12381Fr))
     (Value' instr (ArithRes Mul 'TNat 'TBls12381Fr))
forall a b. (a -> b) -> a -> b
$ Bls12381Fr -> Value' instr 'TBls12381Fr
forall (instr :: [T] -> [T] -> *).
Bls12381Fr -> Value' instr 'TBls12381Fr
VBls12381Fr (forall a b. (Integral a, Num b) => a -> b
fromIntegralOverflowing @Natural @BLS.Bls12381Fr Natural
i Bls12381Fr -> Bls12381Fr -> Bls12381Fr
forall a. Num a => a -> a -> a
* Bls12381Fr
j)
  commutativityProof :: Maybe
$ Dict
    (ArithRes Mul 'TNat 'TBls12381Fr ~ ArithRes Mul 'TBls12381Fr 'TNat,
     ArithOp Mul 'TBls12381Fr 'TNat)
commutativityProof = Dict ('TBls12381Fr ~ 'TBls12381Fr, ArithOp Mul 'TBls12381Fr 'TNat)
-> Maybe
     (Dict
        ('TBls12381Fr ~ 'TBls12381Fr, ArithOp Mul 'TBls12381Fr 'TNat))
forall a. a -> Maybe a
Just Dict ('TBls12381Fr ~ 'TBls12381Fr, ArithOp Mul 'TBls12381Fr 'TNat)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Mul 'TBls12381Fr 'TInt where
  type ArithRes Mul 'TBls12381Fr 'TInt = 'TBls12381Fr
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Mul
-> Value' instr 'TBls12381Fr
-> Value' instr 'TInt
-> Either
     (ArithError (Value' instr 'TBls12381Fr) (Value' instr 'TInt))
     (Value' instr (ArithRes Mul 'TBls12381Fr 'TInt))
evalOp proxy Mul
_ (VBls12381Fr Bls12381Fr
i) (VInt Integer
j) = Value' instr (ArithRes Mul 'TBls12381Fr 'TInt)
-> Either
     (ArithError (Value' instr 'TBls12381Fr) (Value' instr 'TInt))
     (Value' instr (ArithRes Mul 'TBls12381Fr 'TInt))
forall a b. b -> Either a b
Right (Value' instr (ArithRes Mul 'TBls12381Fr 'TInt)
 -> Either
      (ArithError (Value' instr 'TBls12381Fr) (Value' instr 'TInt))
      (Value' instr (ArithRes Mul 'TBls12381Fr 'TInt)))
-> Value' instr (ArithRes Mul 'TBls12381Fr 'TInt)
-> Either
     (ArithError (Value' instr 'TBls12381Fr) (Value' instr 'TInt))
     (Value' instr (ArithRes Mul 'TBls12381Fr 'TInt))
forall a b. (a -> b) -> a -> b
$ Bls12381Fr -> Value' instr 'TBls12381Fr
forall (instr :: [T] -> [T] -> *).
Bls12381Fr -> Value' instr 'TBls12381Fr
VBls12381Fr (Bls12381Fr
i Bls12381Fr -> Bls12381Fr -> Bls12381Fr
forall a. Num a => a -> a -> a
* forall a b. (Integral a, Num b) => a -> b
fromIntegralOverflowing @Integer @BLS.Bls12381Fr Integer
j)
  commutativityProof :: Maybe
$ Dict
    (ArithRes Mul 'TBls12381Fr 'TInt ~ ArithRes Mul 'TInt 'TBls12381Fr,
     ArithOp Mul 'TInt 'TBls12381Fr)
commutativityProof = Dict ('TBls12381Fr ~ 'TBls12381Fr, ArithOp Mul 'TInt 'TBls12381Fr)
-> Maybe
     (Dict
        ('TBls12381Fr ~ 'TBls12381Fr, ArithOp Mul 'TInt 'TBls12381Fr))
forall a. a -> Maybe a
Just Dict ('TBls12381Fr ~ 'TBls12381Fr, ArithOp Mul 'TInt 'TBls12381Fr)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Mul 'TBls12381Fr 'TNat where
  type ArithRes Mul 'TBls12381Fr 'TNat = 'TBls12381Fr
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Mul
-> Value' instr 'TBls12381Fr
-> Value' instr 'TNat
-> Either
     (ArithError (Value' instr 'TBls12381Fr) (Value' instr 'TNat))
     (Value' instr (ArithRes Mul 'TBls12381Fr 'TNat))
evalOp proxy Mul
_ (VBls12381Fr Bls12381Fr
i) (VNat Natural
j) = Value' instr (ArithRes Mul 'TBls12381Fr 'TNat)
-> Either
     (ArithError (Value' instr 'TBls12381Fr) (Value' instr 'TNat))
     (Value' instr (ArithRes Mul 'TBls12381Fr 'TNat))
forall a b. b -> Either a b
Right (Value' instr (ArithRes Mul 'TBls12381Fr 'TNat)
 -> Either
      (ArithError (Value' instr 'TBls12381Fr) (Value' instr 'TNat))
      (Value' instr (ArithRes Mul 'TBls12381Fr 'TNat)))
-> Value' instr (ArithRes Mul 'TBls12381Fr 'TNat)
-> Either
     (ArithError (Value' instr 'TBls12381Fr) (Value' instr 'TNat))
     (Value' instr (ArithRes Mul 'TBls12381Fr 'TNat))
forall a b. (a -> b) -> a -> b
$ Bls12381Fr -> Value' instr 'TBls12381Fr
forall (instr :: [T] -> [T] -> *).
Bls12381Fr -> Value' instr 'TBls12381Fr
VBls12381Fr (Bls12381Fr
i Bls12381Fr -> Bls12381Fr -> Bls12381Fr
forall a. Num a => a -> a -> a
* forall a b. (Integral a, Num b) => a -> b
fromIntegralOverflowing @Natural @BLS.Bls12381Fr Natural
j)
  commutativityProof :: Maybe
$ Dict
    (ArithRes Mul 'TBls12381Fr 'TNat ~ ArithRes Mul 'TNat 'TBls12381Fr,
     ArithOp Mul 'TNat 'TBls12381Fr)
commutativityProof = Dict ('TBls12381Fr ~ 'TBls12381Fr, ArithOp Mul 'TNat 'TBls12381Fr)
-> Maybe
     (Dict
        ('TBls12381Fr ~ 'TBls12381Fr, ArithOp Mul 'TNat 'TBls12381Fr))
forall a. a -> Maybe a
Just Dict ('TBls12381Fr ~ 'TBls12381Fr, ArithOp Mul 'TNat 'TBls12381Fr)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Mul 'TBls12381Fr 'TBls12381Fr where
  type ArithRes Mul 'TBls12381Fr 'TBls12381Fr = 'TBls12381Fr
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Mul
-> Value' instr 'TBls12381Fr
-> Value' instr 'TBls12381Fr
-> Either
     (ArithError
        (Value' instr 'TBls12381Fr) (Value' instr 'TBls12381Fr))
     (Value' instr (ArithRes Mul 'TBls12381Fr 'TBls12381Fr))
evalOp proxy Mul
_ (VBls12381Fr Bls12381Fr
i) (VBls12381Fr Bls12381Fr
j) = Value' instr (ArithRes Mul 'TBls12381Fr 'TBls12381Fr)
-> Either
     (ArithError
        (Value' instr 'TBls12381Fr) (Value' instr 'TBls12381Fr))
     (Value' instr (ArithRes Mul 'TBls12381Fr 'TBls12381Fr))
forall a b. b -> Either a b
Right (Value' instr (ArithRes Mul 'TBls12381Fr 'TBls12381Fr)
 -> Either
      (ArithError
         (Value' instr 'TBls12381Fr) (Value' instr 'TBls12381Fr))
      (Value' instr (ArithRes Mul 'TBls12381Fr 'TBls12381Fr)))
-> Value' instr (ArithRes Mul 'TBls12381Fr 'TBls12381Fr)
-> Either
     (ArithError
        (Value' instr 'TBls12381Fr) (Value' instr 'TBls12381Fr))
     (Value' instr (ArithRes Mul 'TBls12381Fr 'TBls12381Fr))
forall a b. (a -> b) -> a -> b
$ Bls12381Fr -> Value' instr 'TBls12381Fr
forall (instr :: [T] -> [T] -> *).
Bls12381Fr -> Value' instr 'TBls12381Fr
VBls12381Fr (Bls12381Fr
i Bls12381Fr -> Bls12381Fr -> Bls12381Fr
forall a. Num a => a -> a -> a
* Bls12381Fr
j)
  commutativityProof :: Maybe
$ Dict
    (ArithRes Mul 'TBls12381Fr 'TBls12381Fr
     ~ ArithRes Mul 'TBls12381Fr 'TBls12381Fr,
     ArithOp Mul 'TBls12381Fr 'TBls12381Fr)
commutativityProof = Dict
  ('TBls12381Fr ~ 'TBls12381Fr,
   ArithOp Mul 'TBls12381Fr 'TBls12381Fr)
-> Maybe
     (Dict
        ('TBls12381Fr ~ 'TBls12381Fr,
         ArithOp Mul 'TBls12381Fr 'TBls12381Fr))
forall a. a -> Maybe a
Just Dict
  ('TBls12381Fr ~ 'TBls12381Fr,
   ArithOp Mul 'TBls12381Fr 'TBls12381Fr)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Mul 'TBls12381G1 'TBls12381Fr where
  type ArithRes Mul 'TBls12381G1 'TBls12381Fr = 'TBls12381G1
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Mul
-> Value' instr 'TBls12381G1
-> Value' instr 'TBls12381Fr
-> Either
     (ArithError
        (Value' instr 'TBls12381G1) (Value' instr 'TBls12381Fr))
     (Value' instr (ArithRes Mul 'TBls12381G1 'TBls12381Fr))
evalOp proxy Mul
_ (VBls12381G1 Bls12381G1
i) (VBls12381Fr Bls12381Fr
j) = Value' instr (ArithRes Mul 'TBls12381G1 'TBls12381Fr)
-> Either
     (ArithError
        (Value' instr 'TBls12381G1) (Value' instr 'TBls12381Fr))
     (Value' instr (ArithRes Mul 'TBls12381G1 'TBls12381Fr))
forall a b. b -> Either a b
Right (Value' instr (ArithRes Mul 'TBls12381G1 'TBls12381Fr)
 -> Either
      (ArithError
         (Value' instr 'TBls12381G1) (Value' instr 'TBls12381Fr))
      (Value' instr (ArithRes Mul 'TBls12381G1 'TBls12381Fr)))
-> Value' instr (ArithRes Mul 'TBls12381G1 'TBls12381Fr)
-> Either
     (ArithError
        (Value' instr 'TBls12381G1) (Value' instr 'TBls12381Fr))
     (Value' instr (ArithRes Mul 'TBls12381G1 'TBls12381Fr))
forall a b. (a -> b) -> a -> b
$ Bls12381G1 -> Value' instr 'TBls12381G1
forall (instr :: [T] -> [T] -> *).
Bls12381G1 -> Value' instr 'TBls12381G1
VBls12381G1 (Bls12381Fr -> Bls12381G1 -> Bls12381G1
forall scalar point.
MultiplyPoint scalar point =>
scalar -> point -> point
BLS.multiply Bls12381Fr
j Bls12381G1
i)
  commutativityProof :: Maybe
$ Dict
    (ArithRes Mul 'TBls12381G1 'TBls12381Fr
     ~ ArithRes Mul 'TBls12381Fr 'TBls12381G1,
     ArithOp Mul 'TBls12381Fr 'TBls12381G1)
commutativityProof = Maybe
  (Dict
     ('TBls12381G1 ~ 'TBls12381G1,
      ArithOp Mul 'TBls12381Fr 'TBls12381G1))
Maybe
$ Dict
    (ArithRes Mul 'TBls12381G1 'TBls12381Fr
     ~ ArithRes Mul 'TBls12381Fr 'TBls12381G1,
     ArithOp Mul 'TBls12381Fr 'TBls12381G1)
forall a. Maybe a
Nothing
instance ArithOp Mul 'TBls12381G2 'TBls12381Fr where
  type ArithRes Mul 'TBls12381G2 'TBls12381Fr = 'TBls12381G2
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Mul
-> Value' instr 'TBls12381G2
-> Value' instr 'TBls12381Fr
-> Either
     (ArithError
        (Value' instr 'TBls12381G2) (Value' instr 'TBls12381Fr))
     (Value' instr (ArithRes Mul 'TBls12381G2 'TBls12381Fr))
evalOp proxy Mul
_ (VBls12381G2 Bls12381G2
i) (VBls12381Fr Bls12381Fr
j) = Value' instr (ArithRes Mul 'TBls12381G2 'TBls12381Fr)
-> Either
     (ArithError
        (Value' instr 'TBls12381G2) (Value' instr 'TBls12381Fr))
     (Value' instr (ArithRes Mul 'TBls12381G2 'TBls12381Fr))
forall a b. b -> Either a b
Right (Value' instr (ArithRes Mul 'TBls12381G2 'TBls12381Fr)
 -> Either
      (ArithError
         (Value' instr 'TBls12381G2) (Value' instr 'TBls12381Fr))
      (Value' instr (ArithRes Mul 'TBls12381G2 'TBls12381Fr)))
-> Value' instr (ArithRes Mul 'TBls12381G2 'TBls12381Fr)
-> Either
     (ArithError
        (Value' instr 'TBls12381G2) (Value' instr 'TBls12381Fr))
     (Value' instr (ArithRes Mul 'TBls12381G2 'TBls12381Fr))
forall a b. (a -> b) -> a -> b
$ Bls12381G2 -> Value' instr 'TBls12381G2
forall (instr :: [T] -> [T] -> *).
Bls12381G2 -> Value' instr 'TBls12381G2
VBls12381G2 (Bls12381Fr -> Bls12381G2 -> Bls12381G2
forall scalar point.
MultiplyPoint scalar point =>
scalar -> point -> point
BLS.multiply Bls12381Fr
j Bls12381G2
i)
  commutativityProof :: Maybe
$ Dict
    (ArithRes Mul 'TBls12381G2 'TBls12381Fr
     ~ ArithRes Mul 'TBls12381Fr 'TBls12381G2,
     ArithOp Mul 'TBls12381Fr 'TBls12381G2)
commutativityProof = Maybe
  (Dict
     ('TBls12381G2 ~ 'TBls12381G2,
      ArithOp Mul 'TBls12381Fr 'TBls12381G2))
Maybe
$ Dict
    (ArithRes Mul 'TBls12381G2 'TBls12381Fr
     ~ ArithRes Mul 'TBls12381Fr 'TBls12381G2,
     ArithOp Mul 'TBls12381Fr 'TBls12381G2)
forall a. Maybe a
Nothing
instance (Bottom, Bls12381MulBadOrder BLS.Bls12381Fr BLS.Bls12381G1) =>
         ArithOp Mul 'TBls12381Fr 'TBls12381G1 where
  type ArithRes Mul 'TBls12381Fr 'TBls12381G1 = 'TBls12381G1
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Mul
-> Value' instr 'TBls12381Fr
-> Value' instr 'TBls12381G1
-> Either
     (ArithError
        (Value' instr 'TBls12381Fr) (Value' instr 'TBls12381G1))
     (Value' instr (ArithRes Mul 'TBls12381Fr 'TBls12381G1))
evalOp = proxy Mul
-> Value' instr 'TBls12381Fr
-> Value' instr 'TBls12381G1
-> Either
     (ArithError
        (Value' instr 'TBls12381Fr) (Value' instr 'TBls12381G1))
     (Value' instr 'TBls12381G1)
proxy Mul
-> Value' instr 'TBls12381Fr
-> Value' instr 'TBls12381G1
-> Either
     (ArithError
        (Value' instr 'TBls12381Fr) (Value' instr 'TBls12381G1))
     (Value' instr (ArithRes Mul 'TBls12381Fr 'TBls12381G1))
forall a. Bottom => a
forall a. a
no
  commutativityProof :: Maybe
$ Dict
    (ArithRes Mul 'TBls12381Fr 'TBls12381G1
     ~ ArithRes Mul 'TBls12381G1 'TBls12381Fr,
     ArithOp Mul 'TBls12381G1 'TBls12381Fr)
commutativityProof = Maybe
$ Dict
    ('TBls12381G1 ~ 'TBls12381G1,
     ArithOp Mul 'TBls12381G1 'TBls12381Fr)
Maybe
$ Dict
    (ArithRes Mul 'TBls12381Fr 'TBls12381G1
     ~ ArithRes Mul 'TBls12381G1 'TBls12381Fr,
     ArithOp Mul 'TBls12381G1 'TBls12381Fr)
forall a. Bottom => a
forall a. a
no
instance (Bottom, Bls12381MulBadOrder BLS.Bls12381Fr BLS.Bls12381G2) =>
         ArithOp Mul 'TBls12381Fr 'TBls12381G2 where
  type ArithRes Mul 'TBls12381Fr 'TBls12381G2 = 'TBls12381G2
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Mul
-> Value' instr 'TBls12381Fr
-> Value' instr 'TBls12381G2
-> Either
     (ArithError
        (Value' instr 'TBls12381Fr) (Value' instr 'TBls12381G2))
     (Value' instr (ArithRes Mul 'TBls12381Fr 'TBls12381G2))
evalOp = proxy Mul
-> Value' instr 'TBls12381Fr
-> Value' instr 'TBls12381G2
-> Either
     (ArithError
        (Value' instr 'TBls12381Fr) (Value' instr 'TBls12381G2))
     (Value' instr 'TBls12381G2)
proxy Mul
-> Value' instr 'TBls12381Fr
-> Value' instr 'TBls12381G2
-> Either
     (ArithError
        (Value' instr 'TBls12381Fr) (Value' instr 'TBls12381G2))
     (Value' instr (ArithRes Mul 'TBls12381Fr 'TBls12381G2))
forall a. Bottom => a
forall a. a
no
  commutativityProof :: Maybe
$ Dict
    (ArithRes Mul 'TBls12381Fr 'TBls12381G2
     ~ ArithRes Mul 'TBls12381G2 'TBls12381Fr,
     ArithOp Mul 'TBls12381G2 'TBls12381Fr)
commutativityProof = Maybe
$ Dict
    ('TBls12381G2 ~ 'TBls12381G2,
     ArithOp Mul 'TBls12381G2 'TBls12381Fr)
Maybe
$ Dict
    (ArithRes Mul 'TBls12381Fr 'TBls12381G2
     ~ ArithRes Mul 'TBls12381G2 'TBls12381Fr,
     ArithOp Mul 'TBls12381G2 'TBls12381Fr)
forall a. Bottom => a
forall a. a
no

instance ArithOp EDiv 'TNat 'TInt where
  type ArithRes EDiv 'TNat 'TInt = 'TOption ('TPair (EDivOpRes 'TNat 'TInt) (EModOpRes 'TNat 'TInt))
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy EDiv
-> Value' instr 'TNat
-> Value' instr 'TInt
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TInt))
     (Value' instr (ArithRes EDiv 'TNat 'TInt))
evalOp proxy EDiv
_ Value' instr 'TNat
i Value' instr 'TInt
j = Value' instr (ArithRes EDiv 'TNat 'TInt)
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TInt))
     (Value' instr (ArithRes EDiv 'TNat 'TInt))
forall a b. b -> Either a b
Right (Value' instr (ArithRes EDiv 'TNat 'TInt)
 -> Either
      (ArithError (Value' instr 'TNat) (Value' instr 'TInt))
      (Value' instr (ArithRes EDiv 'TNat 'TInt)))
-> Value' instr (ArithRes EDiv 'TNat 'TInt)
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TInt))
     (Value' instr (ArithRes EDiv 'TNat 'TInt))
forall a b. (a -> b) -> a -> b
$ Value' instr 'TNat
-> Value' instr 'TInt
-> Value'
     instr
     ('TOption ('TPair (EDivOpRes 'TNat 'TInt) (EModOpRes 'TNat 'TInt)))
forall (n :: T) (m :: T) (instr :: [T] -> [T] -> *).
EDivOp n m =>
Value' instr n
-> Value' instr m
-> Value' instr ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)))
forall (instr :: [T] -> [T] -> *).
Value' instr 'TNat
-> Value' instr 'TInt
-> Value'
     instr
     ('TOption ('TPair (EDivOpRes 'TNat 'TInt) (EModOpRes 'TNat 'TInt)))
evalEDivOp Value' instr 'TNat
i Value' instr 'TInt
j
instance ArithOp EDiv 'TInt 'TNat where
  type ArithRes EDiv 'TInt 'TNat = 'TOption ('TPair (EDivOpRes 'TInt 'TNat) (EModOpRes 'TInt 'TNat))
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy EDiv
-> Value' instr 'TInt
-> Value' instr 'TNat
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TNat))
     (Value' instr (ArithRes EDiv 'TInt 'TNat))
evalOp proxy EDiv
_ Value' instr 'TInt
i Value' instr 'TNat
j = Value' instr (ArithRes EDiv 'TInt 'TNat)
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TNat))
     (Value' instr (ArithRes EDiv 'TInt 'TNat))
forall a b. b -> Either a b
Right (Value' instr (ArithRes EDiv 'TInt 'TNat)
 -> Either
      (ArithError (Value' instr 'TInt) (Value' instr 'TNat))
      (Value' instr (ArithRes EDiv 'TInt 'TNat)))
-> Value' instr (ArithRes EDiv 'TInt 'TNat)
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TNat))
     (Value' instr (ArithRes EDiv 'TInt 'TNat))
forall a b. (a -> b) -> a -> b
$ Value' instr 'TInt
-> Value' instr 'TNat
-> Value'
     instr
     ('TOption ('TPair (EDivOpRes 'TInt 'TNat) (EModOpRes 'TInt 'TNat)))
forall (n :: T) (m :: T) (instr :: [T] -> [T] -> *).
EDivOp n m =>
Value' instr n
-> Value' instr m
-> Value' instr ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)))
forall (instr :: [T] -> [T] -> *).
Value' instr 'TInt
-> Value' instr 'TNat
-> Value'
     instr
     ('TOption ('TPair (EDivOpRes 'TInt 'TNat) (EModOpRes 'TInt 'TNat)))
evalEDivOp Value' instr 'TInt
i Value' instr 'TNat
j
instance ArithOp EDiv 'TNat 'TNat where
  type ArithRes EDiv 'TNat 'TNat = 'TOption ('TPair (EDivOpRes 'TNat 'TNat) (EModOpRes 'TNat 'TNat))
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy EDiv
-> Value' instr 'TNat
-> Value' instr 'TNat
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes EDiv 'TNat 'TNat))
evalOp proxy EDiv
_ Value' instr 'TNat
i Value' instr 'TNat
j = Value' instr (ArithRes EDiv 'TNat 'TNat)
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes EDiv 'TNat 'TNat))
forall a b. b -> Either a b
Right (Value' instr (ArithRes EDiv 'TNat 'TNat)
 -> Either
      (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
      (Value' instr (ArithRes EDiv 'TNat 'TNat)))
-> Value' instr (ArithRes EDiv 'TNat 'TNat)
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes EDiv 'TNat 'TNat))
forall a b. (a -> b) -> a -> b
$ Value' instr 'TNat
-> Value' instr 'TNat
-> Value'
     instr
     ('TOption ('TPair (EDivOpRes 'TNat 'TNat) (EModOpRes 'TNat 'TNat)))
forall (n :: T) (m :: T) (instr :: [T] -> [T] -> *).
EDivOp n m =>
Value' instr n
-> Value' instr m
-> Value' instr ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)))
forall (instr :: [T] -> [T] -> *).
Value' instr 'TNat
-> Value' instr 'TNat
-> Value'
     instr
     ('TOption ('TPair (EDivOpRes 'TNat 'TNat) (EModOpRes 'TNat 'TNat)))
evalEDivOp Value' instr 'TNat
i Value' instr 'TNat
j
instance ArithOp EDiv 'TInt 'TInt where
  type ArithRes EDiv 'TInt 'TInt = 'TOption ('TPair (EDivOpRes 'TInt 'TInt) (EModOpRes 'TInt 'TInt))
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy EDiv
-> Value' instr 'TInt
-> Value' instr 'TInt
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TInt))
     (Value' instr (ArithRes EDiv 'TInt 'TInt))
evalOp proxy EDiv
_ Value' instr 'TInt
i Value' instr 'TInt
j = Value' instr (ArithRes EDiv 'TInt 'TInt)
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TInt))
     (Value' instr (ArithRes EDiv 'TInt 'TInt))
forall a b. b -> Either a b
Right (Value' instr (ArithRes EDiv 'TInt 'TInt)
 -> Either
      (ArithError (Value' instr 'TInt) (Value' instr 'TInt))
      (Value' instr (ArithRes EDiv 'TInt 'TInt)))
-> Value' instr (ArithRes EDiv 'TInt 'TInt)
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TInt))
     (Value' instr (ArithRes EDiv 'TInt 'TInt))
forall a b. (a -> b) -> a -> b
$ Value' instr 'TInt
-> Value' instr 'TInt
-> Value'
     instr
     ('TOption ('TPair (EDivOpRes 'TInt 'TInt) (EModOpRes 'TInt 'TInt)))
forall (n :: T) (m :: T) (instr :: [T] -> [T] -> *).
EDivOp n m =>
Value' instr n
-> Value' instr m
-> Value' instr ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)))
forall (instr :: [T] -> [T] -> *).
Value' instr 'TInt
-> Value' instr 'TInt
-> Value'
     instr
     ('TOption ('TPair (EDivOpRes 'TInt 'TInt) (EModOpRes 'TInt 'TInt)))
evalEDivOp Value' instr 'TInt
i Value' instr 'TInt
j
instance ArithOp EDiv 'TMutez 'TMutez where
  type ArithRes EDiv 'TMutez 'TMutez = 'TOption ('TPair (EDivOpRes 'TMutez 'TMutez) (EModOpRes 'TMutez 'TMutez))
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy EDiv
-> Value' instr 'TMutez
-> Value' instr 'TMutez
-> Either
     (ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
     (Value' instr (ArithRes EDiv 'TMutez 'TMutez))
evalOp proxy EDiv
_ Value' instr 'TMutez
i Value' instr 'TMutez
j = Value' instr (ArithRes EDiv 'TMutez 'TMutez)
-> Either
     (ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
     (Value' instr (ArithRes EDiv 'TMutez 'TMutez))
forall a b. b -> Either a b
Right (Value' instr (ArithRes EDiv 'TMutez 'TMutez)
 -> Either
      (ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
      (Value' instr (ArithRes EDiv 'TMutez 'TMutez)))
-> Value' instr (ArithRes EDiv 'TMutez 'TMutez)
-> Either
     (ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
     (Value' instr (ArithRes EDiv 'TMutez 'TMutez))
forall a b. (a -> b) -> a -> b
$ Value' instr 'TMutez
-> Value' instr 'TMutez
-> Value'
     instr
     ('TOption
        ('TPair (EDivOpRes 'TMutez 'TMutez) (EModOpRes 'TMutez 'TMutez)))
forall (n :: T) (m :: T) (instr :: [T] -> [T] -> *).
EDivOp n m =>
Value' instr n
-> Value' instr m
-> Value' instr ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)))
forall (instr :: [T] -> [T] -> *).
Value' instr 'TMutez
-> Value' instr 'TMutez
-> Value'
     instr
     ('TOption
        ('TPair (EDivOpRes 'TMutez 'TMutez) (EModOpRes 'TMutez 'TMutez)))
evalEDivOp Value' instr 'TMutez
i Value' instr 'TMutez
j
instance ArithOp EDiv 'TMutez 'TNat where
  type ArithRes EDiv 'TMutez 'TNat = 'TOption ('TPair (EDivOpRes 'TMutez 'TNat) (EModOpRes 'TMutez 'TNat))
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy EDiv
-> Value' instr 'TMutez
-> Value' instr 'TNat
-> Either
     (ArithError (Value' instr 'TMutez) (Value' instr 'TNat))
     (Value' instr (ArithRes EDiv 'TMutez 'TNat))
evalOp proxy EDiv
_ Value' instr 'TMutez
i Value' instr 'TNat
j = Value' instr (ArithRes EDiv 'TMutez 'TNat)
-> Either
     (ArithError (Value' instr 'TMutez) (Value' instr 'TNat))
     (Value' instr (ArithRes EDiv 'TMutez 'TNat))
forall a b. b -> Either a b
Right (Value' instr (ArithRes EDiv 'TMutez 'TNat)
 -> Either
      (ArithError (Value' instr 'TMutez) (Value' instr 'TNat))
      (Value' instr (ArithRes EDiv 'TMutez 'TNat)))
-> Value' instr (ArithRes EDiv 'TMutez 'TNat)
-> Either
     (ArithError (Value' instr 'TMutez) (Value' instr 'TNat))
     (Value' instr (ArithRes EDiv 'TMutez 'TNat))
forall a b. (a -> b) -> a -> b
$ Value' instr 'TMutez
-> Value' instr 'TNat
-> Value'
     instr
     ('TOption
        ('TPair (EDivOpRes 'TMutez 'TNat) (EModOpRes 'TMutez 'TNat)))
forall (n :: T) (m :: T) (instr :: [T] -> [T] -> *).
EDivOp n m =>
Value' instr n
-> Value' instr m
-> Value' instr ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)))
forall (instr :: [T] -> [T] -> *).
Value' instr 'TMutez
-> Value' instr 'TNat
-> Value'
     instr
     ('TOption
        ('TPair (EDivOpRes 'TMutez 'TNat) (EModOpRes 'TMutez 'TNat)))
evalEDivOp Value' instr 'TMutez
i Value' instr 'TNat
j

type Bls12381MulBadOrder a1 a2 = DelayError
  ('Text "Multiplication of "
      ':<>: 'ShowType a2 ':<>: 'Text " and "
      ':<>: 'ShowType a1 ':<>: 'Text " works only other way around"
  )

instance UnaryArithOp Abs 'TInt where
  type UnaryArithRes Abs 'TInt = 'TNat
  evalUnaryArithOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Abs
-> Value' instr 'TInt -> Value' instr (UnaryArithRes Abs 'TInt)
evalUnaryArithOp proxy Abs
_ (VInt Integer
i) = Natural -> Value' instr 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat (Integer -> Natural
forall a. (HasCallStack, Integral a) => Integer -> a
fromInteger (Integer -> Natural) -> Integer -> Natural
forall a b. (a -> b) -> a -> b
$ Integer -> Integer
forall a. Num a => a -> a
abs Integer
i)

instance UnaryArithOp Neg 'TInt where
  type UnaryArithRes Neg 'TInt = 'TInt
  evalUnaryArithOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Neg
-> Value' instr 'TInt -> Value' instr (UnaryArithRes Neg 'TInt)
evalUnaryArithOp proxy Neg
_ (VInt Integer
i) = Integer -> Value' instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt (-Integer
i)
instance UnaryArithOp Neg 'TNat where
  type UnaryArithRes Neg 'TNat = 'TInt
  evalUnaryArithOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Neg
-> Value' instr 'TNat -> Value' instr (UnaryArithRes Neg 'TNat)
evalUnaryArithOp proxy Neg
_ (VNat Natural
i) = Integer -> Value' instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt (- Natural -> Integer
forall a b. (Integral a, Integral b, CheckIntSubType a b) => a -> b
fromIntegral Natural
i)
instance UnaryArithOp Neg 'TBls12381Fr where
  type UnaryArithRes Neg 'TBls12381Fr = 'TBls12381Fr
  evalUnaryArithOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Neg
-> Value' instr 'TBls12381Fr
-> Value' instr (UnaryArithRes Neg 'TBls12381Fr)
evalUnaryArithOp proxy Neg
_ (VBls12381Fr Bls12381Fr
i) = Bls12381Fr -> Value' instr 'TBls12381Fr
forall (instr :: [T] -> [T] -> *).
Bls12381Fr -> Value' instr 'TBls12381Fr
VBls12381Fr (Bls12381Fr -> Bls12381Fr
forall a. CurveObject a => a -> a
BLS.negate Bls12381Fr
i)
instance UnaryArithOp Neg 'TBls12381G1 where
  type UnaryArithRes Neg 'TBls12381G1 = 'TBls12381G1
  evalUnaryArithOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Neg
-> Value' instr 'TBls12381G1
-> Value' instr (UnaryArithRes Neg 'TBls12381G1)
evalUnaryArithOp proxy Neg
_ (VBls12381G1 Bls12381G1
i) = Bls12381G1 -> Value' instr 'TBls12381G1
forall (instr :: [T] -> [T] -> *).
Bls12381G1 -> Value' instr 'TBls12381G1
VBls12381G1 (Bls12381G1 -> Bls12381G1
forall a. CurveObject a => a -> a
BLS.negate Bls12381G1
i)
instance UnaryArithOp Neg 'TBls12381G2 where
  type UnaryArithRes Neg 'TBls12381G2 = 'TBls12381G2
  evalUnaryArithOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Neg
-> Value' instr 'TBls12381G2
-> Value' instr (UnaryArithRes Neg 'TBls12381G2)
evalUnaryArithOp proxy Neg
_ (VBls12381G2 Bls12381G2
i) = Bls12381G2 -> Value' instr 'TBls12381G2
forall (instr :: [T] -> [T] -> *).
Bls12381G2 -> Value' instr 'TBls12381G2
VBls12381G2 (Bls12381G2 -> Bls12381G2
forall a. CurveObject a => a -> a
BLS.negate Bls12381G2
i)

bitwiseWithByteStringsEnd
  :: (Int -> Int -> Int) -- ^ Length comparator
  -> (Word8 -> Word8 -> Word8) -- ^ Zipper
  -> ByteString -> ByteString -> ByteString
bitwiseWithByteStringsEnd :: (Int -> Int -> Int)
-> (Word8 -> Word8 -> Word8)
-> ByteString
-> ByteString
-> ByteString
bitwiseWithByteStringsEnd Int -> Int -> Int
comp Word8 -> Word8 -> Word8
op ByteString
i ByteString
j = (Word8 -> Word8 -> Word8) -> ByteString -> ByteString -> ByteString
BS.packZipWith Word8 -> Word8 -> Word8
op ByteString
i' ByteString
j'
  where
    resultLen :: Int
resultLen = Int -> Int -> Int
comp Int
lenI Int
lenJ
    lenI :: Int
lenI = ByteString -> Int
forall i a.
(Integral i, Container a,
 DefaultToInt (IsIntSubType Length i) i) =>
a -> i
length ByteString
i
    lenJ :: Int
lenJ = ByteString -> Int
forall i a.
(Integral i, Container a,
 DefaultToInt (IsIntSubType Length i) i) =>
a -> i
length ByteString
j
    normalize :: Int -> ByteString -> ByteString
normalize Int
len = -- see Note [resultLen and normalize]
      (Int -> Word8 -> ByteString
BS.replicate (Int
resultLen Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
len) Word8
0 ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<>) (ByteString -> ByteString)
-> (ByteString -> ByteString) -> ByteString -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ByteString -> ByteString
BS.takeEnd Int
resultLen
    i' :: ByteString
i' = Int -> ByteString -> ByteString
normalize Int
lenI ByteString
i
    j' :: ByteString
j' = Int -> ByteString -> ByteString
normalize Int
lenJ ByteString
j

{-
Note [resultLen and normalize]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

The idea with 'normalize' is to take exactly 'resultLen' bytes and left-pad with
zero bytes to the same length, so that 'packZipWith' is aligned correctly.

Note that depending on whether 'comp' is 'min' or 'max', either 'replicate' or
'takeEnd' is a no-op, respectively.

'takeEnd' is O(1), and replicate is O(1) for arguments <= 0, hence we do both
instead of making two functions or checking some condition.

-- @lierdakil
-}

instance ArithOp Or 'TNat 'TNat where
  type ArithRes Or 'TNat 'TNat = 'TNat
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Or
-> Value' instr 'TNat
-> Value' instr 'TNat
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes Or 'TNat 'TNat))
evalOp proxy Or
_ (VNat Natural
i) (VNat Natural
j) = Value' instr (ArithRes Or 'TNat 'TNat)
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes Or 'TNat 'TNat))
forall a b. b -> Either a b
Right (Value' instr (ArithRes Or 'TNat 'TNat)
 -> Either
      (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
      (Value' instr (ArithRes Or 'TNat 'TNat)))
-> Value' instr (ArithRes Or 'TNat 'TNat)
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes Or 'TNat 'TNat))
forall a b. (a -> b) -> a -> b
$ Natural -> Value' instr 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat (Natural
i Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
.|. Natural
j)
  commutativityProof :: Maybe
$ Dict
    (ArithRes Or 'TNat 'TNat ~ ArithRes Or 'TNat 'TNat,
     ArithOp Or 'TNat 'TNat)
commutativityProof = Dict ('TNat ~ 'TNat, ArithOp Or 'TNat 'TNat)
-> Maybe (Dict ('TNat ~ 'TNat, ArithOp Or 'TNat 'TNat))
forall a. a -> Maybe a
Just Dict ('TNat ~ 'TNat, ArithOp Or 'TNat 'TNat)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Or 'TBool 'TBool where
  type ArithRes Or 'TBool 'TBool = 'TBool
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Or
-> Value' instr 'TBool
-> Value' instr 'TBool
-> Either
     (ArithError (Value' instr 'TBool) (Value' instr 'TBool))
     (Value' instr (ArithRes Or 'TBool 'TBool))
evalOp proxy Or
_ (VBool Bool
i) (VBool Bool
j) = Value' instr (ArithRes Or 'TBool 'TBool)
-> Either
     (ArithError (Value' instr 'TBool) (Value' instr 'TBool))
     (Value' instr (ArithRes Or 'TBool 'TBool))
forall a b. b -> Either a b
Right (Value' instr (ArithRes Or 'TBool 'TBool)
 -> Either
      (ArithError (Value' instr 'TBool) (Value' instr 'TBool))
      (Value' instr (ArithRes Or 'TBool 'TBool)))
-> Value' instr (ArithRes Or 'TBool 'TBool)
-> Either
     (ArithError (Value' instr 'TBool) (Value' instr 'TBool))
     (Value' instr (ArithRes Or 'TBool 'TBool))
forall a b. (a -> b) -> a -> b
$ Bool -> Value' instr 'TBool
forall (instr :: [T] -> [T] -> *). Bool -> Value' instr 'TBool
VBool (Bool
i Bool -> Bool -> Bool
forall a. Bits a => a -> a -> a
.|. Bool
j)
  commutativityProof :: Maybe
$ Dict
    (ArithRes Or 'TBool 'TBool ~ ArithRes Or 'TBool 'TBool,
     ArithOp Or 'TBool 'TBool)
commutativityProof = Dict ('TBool ~ 'TBool, ArithOp Or 'TBool 'TBool)
-> Maybe (Dict ('TBool ~ 'TBool, ArithOp Or 'TBool 'TBool))
forall a. a -> Maybe a
Just Dict ('TBool ~ 'TBool, ArithOp Or 'TBool 'TBool)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Or 'TBytes 'TBytes where
  type ArithRes Or 'TBytes 'TBytes = 'TBytes
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Or
-> Value' instr 'TBytes
-> Value' instr 'TBytes
-> Either
     (ArithError (Value' instr 'TBytes) (Value' instr 'TBytes))
     (Value' instr (ArithRes Or 'TBytes 'TBytes))
evalOp proxy Or
_ (VBytes ByteString
i) (VBytes ByteString
j) = Value' instr (ArithRes Or 'TBytes 'TBytes)
-> Either
     (ArithError (Value' instr 'TBytes) (Value' instr 'TBytes))
     (Value' instr (ArithRes Or 'TBytes 'TBytes))
forall a b. b -> Either a b
Right (Value' instr (ArithRes Or 'TBytes 'TBytes)
 -> Either
      (ArithError (Value' instr 'TBytes) (Value' instr 'TBytes))
      (Value' instr (ArithRes Or 'TBytes 'TBytes)))
-> Value' instr (ArithRes Or 'TBytes 'TBytes)
-> Either
     (ArithError (Value' instr 'TBytes) (Value' instr 'TBytes))
     (Value' instr (ArithRes Or 'TBytes 'TBytes))
forall a b. (a -> b) -> a -> b
$ ByteString -> Value' instr 'TBytes
forall (instr :: [T] -> [T] -> *).
ByteString -> Value' instr 'TBytes
VBytes (ByteString -> Value' instr 'TBytes)
-> ByteString -> Value' instr 'TBytes
forall a b. (a -> b) -> a -> b
$ (Int -> Int -> Int)
-> (Word8 -> Word8 -> Word8)
-> ByteString
-> ByteString
-> ByteString
bitwiseWithByteStringsEnd Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Word8 -> Word8 -> Word8
forall a. Bits a => a -> a -> a
(.|.) ByteString
i ByteString
j
  commutativityProof :: Maybe
$ Dict
    (ArithRes Or 'TBytes 'TBytes ~ ArithRes Or 'TBytes 'TBytes,
     ArithOp Or 'TBytes 'TBytes)
commutativityProof = Dict ('TBytes ~ 'TBytes, ArithOp Or 'TBytes 'TBytes)
-> Maybe (Dict ('TBytes ~ 'TBytes, ArithOp Or 'TBytes 'TBytes))
forall a. a -> Maybe a
Just Dict ('TBytes ~ 'TBytes, ArithOp Or 'TBytes 'TBytes)
forall (a :: Constraint). a => Dict a
Dict

instance ArithOp And 'TInt 'TNat where
  type ArithRes And 'TInt 'TNat = 'TNat
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy And
-> Value' instr 'TInt
-> Value' instr 'TNat
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TNat))
     (Value' instr (ArithRes And 'TInt 'TNat))
evalOp proxy And
_ (VInt Integer
i) (VNat Natural
j) = Value' instr (ArithRes And 'TInt 'TNat)
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TNat))
     (Value' instr (ArithRes And 'TInt 'TNat))
forall a b. b -> Either a b
Right (Value' instr (ArithRes And 'TInt 'TNat)
 -> Either
      (ArithError (Value' instr 'TInt) (Value' instr 'TNat))
      (Value' instr (ArithRes And 'TInt 'TNat)))
-> Value' instr (ArithRes And 'TInt 'TNat)
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TNat))
     (Value' instr (ArithRes And 'TInt 'TNat))
forall a b. (a -> b) -> a -> b
$ Natural -> Value' instr 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat (Integer -> Natural
forall a. (HasCallStack, Integral a) => Integer -> a
fromInteger (Integer
i Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
j))
instance ArithOp And 'TNat 'TNat where
  type ArithRes And 'TNat 'TNat = 'TNat
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy And
-> Value' instr 'TNat
-> Value' instr 'TNat
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes And 'TNat 'TNat))
evalOp proxy And
_ (VNat Natural
i) (VNat Natural
j) = Value' instr (ArithRes And 'TNat 'TNat)
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes And 'TNat 'TNat))
forall a b. b -> Either a b
Right (Value' instr (ArithRes And 'TNat 'TNat)
 -> Either
      (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
      (Value' instr (ArithRes And 'TNat 'TNat)))
-> Value' instr (ArithRes And 'TNat 'TNat)
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes And 'TNat 'TNat))
forall a b. (a -> b) -> a -> b
$ Natural -> Value' instr 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat (Natural
i Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
.&. Natural
j)
  commutativityProof :: Maybe
$ Dict
    (ArithRes And 'TNat 'TNat ~ ArithRes And 'TNat 'TNat,
     ArithOp And 'TNat 'TNat)
commutativityProof = Dict ('TNat ~ 'TNat, ArithOp And 'TNat 'TNat)
-> Maybe (Dict ('TNat ~ 'TNat, ArithOp And 'TNat 'TNat))
forall a. a -> Maybe a
Just Dict ('TNat ~ 'TNat, ArithOp And 'TNat 'TNat)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp And 'TBool 'TBool where
  type ArithRes And 'TBool 'TBool = 'TBool
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy And
-> Value' instr 'TBool
-> Value' instr 'TBool
-> Either
     (ArithError (Value' instr 'TBool) (Value' instr 'TBool))
     (Value' instr (ArithRes And 'TBool 'TBool))
evalOp proxy And
_ (VBool Bool
i) (VBool Bool
j) = Value' instr (ArithRes And 'TBool 'TBool)
-> Either
     (ArithError (Value' instr 'TBool) (Value' instr 'TBool))
     (Value' instr (ArithRes And 'TBool 'TBool))
forall a b. b -> Either a b
Right (Value' instr (ArithRes And 'TBool 'TBool)
 -> Either
      (ArithError (Value' instr 'TBool) (Value' instr 'TBool))
      (Value' instr (ArithRes And 'TBool 'TBool)))
-> Value' instr (ArithRes And 'TBool 'TBool)
-> Either
     (ArithError (Value' instr 'TBool) (Value' instr 'TBool))
     (Value' instr (ArithRes And 'TBool 'TBool))
forall a b. (a -> b) -> a -> b
$ Bool -> Value' instr 'TBool
forall (instr :: [T] -> [T] -> *). Bool -> Value' instr 'TBool
VBool (Bool
i Bool -> Bool -> Bool
forall a. Bits a => a -> a -> a
.&. Bool
j)
  commutativityProof :: Maybe
$ Dict
    (ArithRes And 'TBool 'TBool ~ ArithRes And 'TBool 'TBool,
     ArithOp And 'TBool 'TBool)
commutativityProof = Dict ('TBool ~ 'TBool, ArithOp And 'TBool 'TBool)
-> Maybe (Dict ('TBool ~ 'TBool, ArithOp And 'TBool 'TBool))
forall a. a -> Maybe a
Just Dict ('TBool ~ 'TBool, ArithOp And 'TBool 'TBool)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp And 'TBytes 'TBytes where
  type ArithRes And 'TBytes 'TBytes = 'TBytes
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy And
-> Value' instr 'TBytes
-> Value' instr 'TBytes
-> Either
     (ArithError (Value' instr 'TBytes) (Value' instr 'TBytes))
     (Value' instr (ArithRes And 'TBytes 'TBytes))
evalOp proxy And
_ (VBytes ByteString
i) (VBytes ByteString
j) = Value' instr (ArithRes And 'TBytes 'TBytes)
-> Either
     (ArithError (Value' instr 'TBytes) (Value' instr 'TBytes))
     (Value' instr (ArithRes And 'TBytes 'TBytes))
forall a b. b -> Either a b
Right (Value' instr (ArithRes And 'TBytes 'TBytes)
 -> Either
      (ArithError (Value' instr 'TBytes) (Value' instr 'TBytes))
      (Value' instr (ArithRes And 'TBytes 'TBytes)))
-> Value' instr (ArithRes And 'TBytes 'TBytes)
-> Either
     (ArithError (Value' instr 'TBytes) (Value' instr 'TBytes))
     (Value' instr (ArithRes And 'TBytes 'TBytes))
forall a b. (a -> b) -> a -> b
$ ByteString -> Value' instr 'TBytes
forall (instr :: [T] -> [T] -> *).
ByteString -> Value' instr 'TBytes
VBytes (ByteString -> Value' instr 'TBytes)
-> ByteString -> Value' instr 'TBytes
forall a b. (a -> b) -> a -> b
$ (Int -> Int -> Int)
-> (Word8 -> Word8 -> Word8)
-> ByteString
-> ByteString
-> ByteString
bitwiseWithByteStringsEnd Int -> Int -> Int
forall a. Ord a => a -> a -> a
min Word8 -> Word8 -> Word8
forall a. Bits a => a -> a -> a
(.&.) ByteString
i ByteString
j
  commutativityProof :: Maybe
$ Dict
    (ArithRes And 'TBytes 'TBytes ~ ArithRes And 'TBytes 'TBytes,
     ArithOp And 'TBytes 'TBytes)
commutativityProof = Dict ('TBytes ~ 'TBytes, ArithOp And 'TBytes 'TBytes)
-> Maybe (Dict ('TBytes ~ 'TBytes, ArithOp And 'TBytes 'TBytes))
forall a. a -> Maybe a
Just Dict ('TBytes ~ 'TBytes, ArithOp And 'TBytes 'TBytes)
forall (a :: Constraint). a => Dict a
Dict

instance ArithOp Xor 'TNat 'TNat where
  type ArithRes Xor 'TNat 'TNat = 'TNat
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Xor
-> Value' instr 'TNat
-> Value' instr 'TNat
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes Xor 'TNat 'TNat))
evalOp proxy Xor
_ (VNat Natural
i) (VNat Natural
j) = Value' instr (ArithRes Xor 'TNat 'TNat)
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes Xor 'TNat 'TNat))
forall a b. b -> Either a b
Right (Value' instr (ArithRes Xor 'TNat 'TNat)
 -> Either
      (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
      (Value' instr (ArithRes Xor 'TNat 'TNat)))
-> Value' instr (ArithRes Xor 'TNat 'TNat)
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes Xor 'TNat 'TNat))
forall a b. (a -> b) -> a -> b
$ Natural -> Value' instr 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat (Natural
i Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
`xor` Natural
j)
  commutativityProof :: Maybe
$ Dict
    (ArithRes Xor 'TNat 'TNat ~ ArithRes Xor 'TNat 'TNat,
     ArithOp Xor 'TNat 'TNat)
commutativityProof = Dict ('TNat ~ 'TNat, ArithOp Xor 'TNat 'TNat)
-> Maybe (Dict ('TNat ~ 'TNat, ArithOp Xor 'TNat 'TNat))
forall a. a -> Maybe a
Just Dict ('TNat ~ 'TNat, ArithOp Xor 'TNat 'TNat)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Xor 'TBool 'TBool where
  type ArithRes Xor 'TBool 'TBool = 'TBool
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Xor
-> Value' instr 'TBool
-> Value' instr 'TBool
-> Either
     (ArithError (Value' instr 'TBool) (Value' instr 'TBool))
     (Value' instr (ArithRes Xor 'TBool 'TBool))
evalOp proxy Xor
_ (VBool Bool
i) (VBool Bool
j) = Value' instr (ArithRes Xor 'TBool 'TBool)
-> Either
     (ArithError (Value' instr 'TBool) (Value' instr 'TBool))
     (Value' instr (ArithRes Xor 'TBool 'TBool))
forall a b. b -> Either a b
Right (Value' instr (ArithRes Xor 'TBool 'TBool)
 -> Either
      (ArithError (Value' instr 'TBool) (Value' instr 'TBool))
      (Value' instr (ArithRes Xor 'TBool 'TBool)))
-> Value' instr (ArithRes Xor 'TBool 'TBool)
-> Either
     (ArithError (Value' instr 'TBool) (Value' instr 'TBool))
     (Value' instr (ArithRes Xor 'TBool 'TBool))
forall a b. (a -> b) -> a -> b
$ Bool -> Value' instr 'TBool
forall (instr :: [T] -> [T] -> *). Bool -> Value' instr 'TBool
VBool (Bool
i Bool -> Bool -> Bool
forall a. Bits a => a -> a -> a
`xor` Bool
j)
  commutativityProof :: Maybe
$ Dict
    (ArithRes Xor 'TBool 'TBool ~ ArithRes Xor 'TBool 'TBool,
     ArithOp Xor 'TBool 'TBool)
commutativityProof = Dict ('TBool ~ 'TBool, ArithOp Xor 'TBool 'TBool)
-> Maybe (Dict ('TBool ~ 'TBool, ArithOp Xor 'TBool 'TBool))
forall a. a -> Maybe a
Just Dict ('TBool ~ 'TBool, ArithOp Xor 'TBool 'TBool)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Xor 'TBytes 'TBytes where
  type ArithRes Xor 'TBytes 'TBytes = 'TBytes
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Xor
-> Value' instr 'TBytes
-> Value' instr 'TBytes
-> Either
     (ArithError (Value' instr 'TBytes) (Value' instr 'TBytes))
     (Value' instr (ArithRes Xor 'TBytes 'TBytes))
evalOp proxy Xor
_ (VBytes ByteString
i) (VBytes ByteString
j) = Value' instr (ArithRes Xor 'TBytes 'TBytes)
-> Either
     (ArithError (Value' instr 'TBytes) (Value' instr 'TBytes))
     (Value' instr (ArithRes Xor 'TBytes 'TBytes))
forall a b. b -> Either a b
Right (Value' instr (ArithRes Xor 'TBytes 'TBytes)
 -> Either
      (ArithError (Value' instr 'TBytes) (Value' instr 'TBytes))
      (Value' instr (ArithRes Xor 'TBytes 'TBytes)))
-> Value' instr (ArithRes Xor 'TBytes 'TBytes)
-> Either
     (ArithError (Value' instr 'TBytes) (Value' instr 'TBytes))
     (Value' instr (ArithRes Xor 'TBytes 'TBytes))
forall a b. (a -> b) -> a -> b
$ ByteString -> Value' instr 'TBytes
forall (instr :: [T] -> [T] -> *).
ByteString -> Value' instr 'TBytes
VBytes (ByteString -> Value' instr 'TBytes)
-> ByteString -> Value' instr 'TBytes
forall a b. (a -> b) -> a -> b
$ (Int -> Int -> Int)
-> (Word8 -> Word8 -> Word8)
-> ByteString
-> ByteString
-> ByteString
bitwiseWithByteStringsEnd Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Word8 -> Word8 -> Word8
forall a. Bits a => a -> a -> a
xor ByteString
i ByteString
j
  commutativityProof :: Maybe
$ Dict
    (ArithRes Xor 'TBytes 'TBytes ~ ArithRes Xor 'TBytes 'TBytes,
     ArithOp Xor 'TBytes 'TBytes)
commutativityProof = Dict ('TBytes ~ 'TBytes, ArithOp Xor 'TBytes 'TBytes)
-> Maybe (Dict ('TBytes ~ 'TBytes, ArithOp Xor 'TBytes 'TBytes))
forall a. a -> Maybe a
Just Dict ('TBytes ~ 'TBytes, ArithOp Xor 'TBytes 'TBytes)
forall (a :: Constraint). a => Dict a
Dict

instance ArithOp Lsl 'TNat 'TNat where
  type ArithRes Lsl 'TNat 'TNat = 'TNat
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Lsl
-> Value' instr 'TNat
-> Value' instr 'TNat
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes Lsl 'TNat 'TNat))
evalOp proxy Lsl
_ n :: Value' instr 'TNat
n@(VNat Natural
i) m :: Value' instr 'TNat
m@(VNat Natural
j) =
    if Natural
j Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
> Natural
256
    then ArithError (Value' instr 'TNat) (Value' instr 'TNat)
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes Lsl 'TNat 'TNat))
forall a b. a -> Either a b
Left (ArithError (Value' instr 'TNat) (Value' instr 'TNat)
 -> Either
      (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
      (Value' instr (ArithRes Lsl 'TNat 'TNat)))
-> ArithError (Value' instr 'TNat) (Value' instr 'TNat)
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes Lsl 'TNat 'TNat))
forall a b. (a -> b) -> a -> b
$ ShiftArithErrorType
-> Value' instr 'TNat
-> Value' instr 'TNat
-> ArithError (Value' instr 'TNat) (Value' instr 'TNat)
forall n m. ShiftArithErrorType -> n -> m -> ArithError n m
ShiftArithError ShiftArithErrorType
LslOverflow Value' instr 'TNat
n Value' instr 'TNat
m
    else Value' instr (ArithRes Lsl 'TNat 'TNat)
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes Lsl 'TNat 'TNat))
forall a b. b -> Either a b
Right (Value' instr (ArithRes Lsl 'TNat 'TNat)
 -> Either
      (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
      (Value' instr (ArithRes Lsl 'TNat 'TNat)))
-> Value' instr (ArithRes Lsl 'TNat 'TNat)
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes Lsl 'TNat 'TNat))
forall a b. (a -> b) -> a -> b
$ Natural -> Value' instr 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat (Integer -> Natural
forall a. (HasCallStack, Integral a) => Integer -> a
fromInteger (Integer -> Natural) -> Integer -> Natural
forall a b. (a -> b) -> a -> b
$ Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shift (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
i) (forall a b. (HasCallStack, Integral a, Integral b) => a -> b
Unsafe.fromIntegral @Natural @Int Natural
j))
instance ArithOp Lsl 'TBytes 'TNat where
  type ArithRes Lsl 'TBytes 'TNat = 'TBytes
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Lsl
-> Value' instr 'TBytes
-> Value' instr 'TNat
-> Either
     (ArithError (Value' instr 'TBytes) (Value' instr 'TNat))
     (Value' instr (ArithRes Lsl 'TBytes 'TNat))
evalOp proxy Lsl
_ n :: Value' instr 'TBytes
n@(VBytes ByteString
i) m :: Value' instr 'TNat
m@(VNat Natural
j) =
    if Natural
j Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
> Natural
64000
    then ArithError (Value' instr 'TBytes) (Value' instr 'TNat)
-> Either
     (ArithError (Value' instr 'TBytes) (Value' instr 'TNat))
     (Value' instr (ArithRes Lsl 'TBytes 'TNat))
forall a b. a -> Either a b
Left (ArithError (Value' instr 'TBytes) (Value' instr 'TNat)
 -> Either
      (ArithError (Value' instr 'TBytes) (Value' instr 'TNat))
      (Value' instr (ArithRes Lsl 'TBytes 'TNat)))
-> ArithError (Value' instr 'TBytes) (Value' instr 'TNat)
-> Either
     (ArithError (Value' instr 'TBytes) (Value' instr 'TNat))
     (Value' instr (ArithRes Lsl 'TBytes 'TNat))
forall a b. (a -> b) -> a -> b
$ ShiftArithErrorType
-> Value' instr 'TBytes
-> Value' instr 'TNat
-> ArithError (Value' instr 'TBytes) (Value' instr 'TNat)
forall n m. ShiftArithErrorType -> n -> m -> ArithError n m
ShiftArithError ShiftArithErrorType
LslOverflow Value' instr 'TBytes
n Value' instr 'TNat
m
    else Value' instr (ArithRes Lsl 'TBytes 'TNat)
-> Either
     (ArithError (Value' instr 'TBytes) (Value' instr 'TNat))
     (Value' instr (ArithRes Lsl 'TBytes 'TNat))
forall a b. b -> Either a b
Right (Value' instr (ArithRes Lsl 'TBytes 'TNat)
 -> Either
      (ArithError (Value' instr 'TBytes) (Value' instr 'TNat))
      (Value' instr (ArithRes Lsl 'TBytes 'TNat)))
-> Value' instr (ArithRes Lsl 'TBytes 'TNat)
-> Either
     (ArithError (Value' instr 'TBytes) (Value' instr 'TNat))
     (Value' instr (ArithRes Lsl 'TBytes 'TNat))
forall a b. (a -> b) -> a -> b
$ ByteString -> Value' instr 'TBytes
forall (instr :: [T] -> [T] -> *).
ByteString -> Value' instr 'TBytes
VBytes (ByteString -> Value' instr 'TBytes)
-> ByteString -> Value' instr 'TBytes
forall a b. (a -> b) -> a -> b
$
      let -- according to the docs, the result is left-padded to this number of bytes
          len :: Int
len = ByteString -> Int
forall i a.
(Integral i, Container a,
 DefaultToInt (IsIntSubType Length i) i) =>
a -> i
length ByteString
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ forall a b. (HasCallStack, Integral a, Integral b) => a -> b
Unsafe.fromIntegral @Natural @Int ((Natural
j Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
7) Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`div` Natural
8)
          bs :: ByteString
bs = Integer -> ByteString
forall ba. ByteArray ba => Integer -> ba
i2osp (Integer -> ByteString) -> Integer -> ByteString
forall a b. (a -> b) -> a -> b
$ Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shift (ByteString -> Integer
forall ba. ByteArrayAccess ba => ba -> Integer
os2ip ByteString
i) (forall a b. (HasCallStack, Integral a, Integral b) => a -> b
Unsafe.fromIntegral @Natural @Int Natural
j)
      in Int -> Word8 -> ByteString
BS.replicate (Int
len Int -> Int -> Int
forall a. Num a => a -> a -> a
- ByteString -> Int
forall i a.
(Integral i, Container a,
 DefaultToInt (IsIntSubType Length i) i) =>
a -> i
length ByteString
bs) Word8
0 ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> ByteString
bs

instance ArithOp Lsr 'TNat 'TNat where
  type ArithRes Lsr 'TNat 'TNat = 'TNat
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Lsr
-> Value' instr 'TNat
-> Value' instr 'TNat
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes Lsr 'TNat 'TNat))
evalOp proxy Lsr
_ n :: Value' instr 'TNat
n@(VNat Natural
i) m :: Value' instr 'TNat
m@(VNat Natural
j) =
    if Natural
j Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
> Natural
256
    then ArithError (Value' instr 'TNat) (Value' instr 'TNat)
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes Lsr 'TNat 'TNat))
forall a b. a -> Either a b
Left (ArithError (Value' instr 'TNat) (Value' instr 'TNat)
 -> Either
      (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
      (Value' instr (ArithRes Lsr 'TNat 'TNat)))
-> ArithError (Value' instr 'TNat) (Value' instr 'TNat)
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes Lsr 'TNat 'TNat))
forall a b. (a -> b) -> a -> b
$ ShiftArithErrorType
-> Value' instr 'TNat
-> Value' instr 'TNat
-> ArithError (Value' instr 'TNat) (Value' instr 'TNat)
forall n m. ShiftArithErrorType -> n -> m -> ArithError n m
ShiftArithError ShiftArithErrorType
LsrUnderflow Value' instr 'TNat
n Value' instr 'TNat
m
    else Value' instr (ArithRes Lsr 'TNat 'TNat)
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes Lsr 'TNat 'TNat))
forall a b. b -> Either a b
Right (Value' instr (ArithRes Lsr 'TNat 'TNat)
 -> Either
      (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
      (Value' instr (ArithRes Lsr 'TNat 'TNat)))
-> Value' instr (ArithRes Lsr 'TNat 'TNat)
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes Lsr 'TNat 'TNat))
forall a b. (a -> b) -> a -> b
$ Natural -> Value' instr 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat (Integer -> Natural
forall a. (HasCallStack, Integral a) => Integer -> a
fromInteger (Integer -> Natural) -> Integer -> Natural
forall a b. (a -> b) -> a -> b
$ Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shift (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
i) (-(forall a b. (HasCallStack, Integral a, Integral b) => a -> b
Unsafe.fromIntegral @Natural @Int Natural
j)))
instance ArithOp Lsr 'TBytes 'TNat where
  type ArithRes Lsr 'TBytes 'TNat = 'TBytes
  evalOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Lsr
-> Value' instr 'TBytes
-> Value' instr 'TNat
-> Either
     (ArithError (Value' instr 'TBytes) (Value' instr 'TNat))
     (Value' instr (ArithRes Lsr 'TBytes 'TNat))
evalOp proxy Lsr
_ (VBytes ByteString
i) (VNat Natural
j)
    -- Michelson docs claim there's a limit of 256, but actually there isn't.
    -- https://gitlab.com/tezos/tezos/-/issues/5018
    -- Very large shifts just return empty byte string
    -- https://gitlab.com/tezos/tezos/-/blob/b2a49caf2e6d4b34c4fd226996d3637e19397401/src/proto_alpha/lib_protocol/script_bytes.ml#L48
    | Natural
j Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
> forall a b. (Integral a, Num b) => a -> b
fromIntegralOverflowing @Int @Natural Int
forall a. Bounded a => a
maxBound = Value' instr (ArithRes Lsr 'TBytes 'TNat)
-> Either
     (ArithError (Value' instr 'TBytes) (Value' instr 'TNat))
     (Value' instr (ArithRes Lsr 'TBytes 'TNat))
forall a b. b -> Either a b
Right (Value' instr (ArithRes Lsr 'TBytes 'TNat)
 -> Either
      (ArithError (Value' instr 'TBytes) (Value' instr 'TNat))
      (Value' instr (ArithRes Lsr 'TBytes 'TNat)))
-> Value' instr (ArithRes Lsr 'TBytes 'TNat)
-> Either
     (ArithError (Value' instr 'TBytes) (Value' instr 'TNat))
     (Value' instr (ArithRes Lsr 'TBytes 'TNat))
forall a b. (a -> b) -> a -> b
$ ByteString -> Value' instr 'TBytes
forall (instr :: [T] -> [T] -> *).
ByteString -> Value' instr 'TBytes
VBytes ByteString
forall a. Monoid a => a
mempty
    | Bool
otherwise = Value' instr (ArithRes Lsr 'TBytes 'TNat)
-> Either
     (ArithError (Value' instr 'TBytes) (Value' instr 'TNat))
     (Value' instr (ArithRes Lsr 'TBytes 'TNat))
forall a b. b -> Either a b
Right (Value' instr (ArithRes Lsr 'TBytes 'TNat)
 -> Either
      (ArithError (Value' instr 'TBytes) (Value' instr 'TNat))
      (Value' instr (ArithRes Lsr 'TBytes 'TNat)))
-> Value' instr (ArithRes Lsr 'TBytes 'TNat)
-> Either
     (ArithError (Value' instr 'TBytes) (Value' instr 'TNat))
     (Value' instr (ArithRes Lsr 'TBytes 'TNat))
forall a b. (a -> b) -> a -> b
$ ByteString -> Value' instr 'TBytes
forall (instr :: [T] -> [T] -> *).
ByteString -> Value' instr 'TBytes
VBytes (ByteString -> Value' instr 'TBytes)
-> ByteString -> Value' instr 'TBytes
forall a b. (a -> b) -> a -> b
$
        let k :: Int
k = forall a b. (HasCallStack, Integral a, Integral b) => a -> b
Unsafe.fromIntegral @Natural @Int Natural
j -- safe, we just checked bounds above
            -- empirical number of bytes to match octez impl
            -- this is inverse to LSL in some sense
            len :: Int
len = ByteString -> Int
forall i a.
(Integral i, Container a,
 DefaultToInt (IsIntSubType Length i) i) =>
a -> i
length ByteString
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- (Int
k Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
8)
            bs :: ByteString
bs = Integer -> ByteString
forall ba. ByteArray ba => Integer -> ba
i2osp (Integer -> ByteString) -> Integer -> ByteString
forall a b. (a -> b) -> a -> b
$ Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shift (ByteString -> Integer
forall ba. ByteArrayAccess ba => ba -> Integer
os2ip ByteString
i) (-Int
k)
            finalLenDiff :: Int
finalLenDiff = Int
len Int -> Int -> Int
forall a. Num a => a -> a -> a
- ByteString -> Int
forall i a.
(Integral i, Container a,
 DefaultToInt (IsIntSubType Length i) i) =>
a -> i
length ByteString
bs
        in Int -> Word8 -> ByteString
BS.replicate Int
finalLenDiff Word8
0 ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> Int -> ByteString -> ByteString
BS.drop (-Int
finalLenDiff) ByteString
bs

instance UnaryArithOp Not 'TInt where
  type UnaryArithRes Not 'TInt = 'TInt
  evalUnaryArithOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Not
-> Value' instr 'TInt -> Value' instr (UnaryArithRes Not 'TInt)
evalUnaryArithOp proxy Not
_ (VInt Integer
i) = Integer -> Value' instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt (Integer -> Integer
forall a. Bits a => a -> a
complement Integer
i)
instance UnaryArithOp Not 'TNat where
  type UnaryArithRes Not 'TNat = 'TInt
  evalUnaryArithOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Not
-> Value' instr 'TNat -> Value' instr (UnaryArithRes Not 'TNat)
evalUnaryArithOp proxy Not
_ (VNat Natural
i) = Integer -> Value' instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt (Integer -> Integer
forall a. Bits a => a -> a
complement (Integer -> Integer) -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
i)
instance UnaryArithOp Not 'TBool where
  type UnaryArithRes Not 'TBool = 'TBool
  evalUnaryArithOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Not
-> Value' instr 'TBool -> Value' instr (UnaryArithRes Not 'TBool)
evalUnaryArithOp proxy Not
_ (VBool Bool
i) = Bool -> Value' instr 'TBool
forall (instr :: [T] -> [T] -> *). Bool -> Value' instr 'TBool
VBool (Bool -> Bool
forall a. Boolean a => a -> a
not Bool
i)
instance UnaryArithOp Not 'TBytes where
  type UnaryArithRes Not 'TBytes = 'TBytes
  evalUnaryArithOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Not
-> Value' instr 'TBytes -> Value' instr (UnaryArithRes Not 'TBytes)
evalUnaryArithOp proxy Not
_ (VBytes ByteString
i) = ByteString -> Value' instr 'TBytes
forall (instr :: [T] -> [T] -> *).
ByteString -> Value' instr 'TBytes
VBytes ((Word8 -> Word8) -> ByteString -> ByteString
BS.map Word8 -> Word8
forall a. Bits a => a -> a
complement ByteString
i)

-- | Implementation for @COMPARE@ instruction.
compareOp :: Comparable t => Value' i t -> Value' i t -> Integer
compareOp :: forall (t :: T) (i :: [T] -> [T] -> *).
Comparable t =>
Value' i t -> Value' i t -> Integer
compareOp Value' i t
a Value' i t
b =
  -- If at some point we need to return a number outside of [-1; 1] range,
  -- let's extend 'tcompare' respectively and use it here.
  -- Such situation seems unlikely to happen though, our previous communication
  -- with the Tezos developers shows that even if in Tezos 'COMPARE' returns
  -- something unusual, that is probably a bug.
  Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int -> Integer) -> Int -> Integer
forall a b. (a -> b) -> a -> b
$ Ordering -> Int
forall a. Enum a => a -> Int
fromEnum (Value' i t -> Value' i t -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Value' i t
a Value' i t
b) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1

instance UnaryArithOp Eq' 'TInt where
  type UnaryArithRes Eq' 'TInt = 'TBool
  evalUnaryArithOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Eq'
-> Value' instr 'TInt -> Value' instr (UnaryArithRes Eq' 'TInt)
evalUnaryArithOp proxy Eq'
_ (VInt Integer
i) = Bool -> Value' instr 'TBool
forall (instr :: [T] -> [T] -> *). Bool -> Value' instr 'TBool
VBool (Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0)

instance UnaryArithOp Neq 'TInt where
  type UnaryArithRes Neq 'TInt = 'TBool
  evalUnaryArithOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Neq
-> Value' instr 'TInt -> Value' instr (UnaryArithRes Neq 'TInt)
evalUnaryArithOp proxy Neq
_ (VInt Integer
i) = Bool -> Value' instr 'TBool
forall (instr :: [T] -> [T] -> *). Bool -> Value' instr 'TBool
VBool (Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0)


instance UnaryArithOp Lt 'TInt where
  type UnaryArithRes Lt 'TInt = 'TBool
  evalUnaryArithOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Lt
-> Value' instr 'TInt -> Value' instr (UnaryArithRes Lt 'TInt)
evalUnaryArithOp proxy Lt
_ (VInt Integer
i) = Bool -> Value' instr 'TBool
forall (instr :: [T] -> [T] -> *). Bool -> Value' instr 'TBool
VBool (Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0)

instance UnaryArithOp Gt 'TInt where
  type UnaryArithRes Gt 'TInt = 'TBool
  evalUnaryArithOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Gt
-> Value' instr 'TInt -> Value' instr (UnaryArithRes Gt 'TInt)
evalUnaryArithOp proxy Gt
_ (VInt Integer
i) = Bool -> Value' instr 'TBool
forall (instr :: [T] -> [T] -> *). Bool -> Value' instr 'TBool
VBool (Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0)

instance UnaryArithOp Le 'TInt where
  type UnaryArithRes Le 'TInt = 'TBool
  evalUnaryArithOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Le
-> Value' instr 'TInt -> Value' instr (UnaryArithRes Le 'TInt)
evalUnaryArithOp proxy Le
_ (VInt Integer
i) = Bool -> Value' instr 'TBool
forall (instr :: [T] -> [T] -> *). Bool -> Value' instr 'TBool
VBool (Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
0)

instance UnaryArithOp Ge 'TInt where
  type UnaryArithRes Ge 'TInt = 'TBool
  evalUnaryArithOp :: forall (proxy :: * -> *) (instr :: [T] -> [T] -> *).
proxy Ge
-> Value' instr 'TInt -> Value' instr (UnaryArithRes Ge 'TInt)
evalUnaryArithOp proxy Ge
_ (VInt Integer
i) = Bool -> Value' instr 'TBool
forall (instr :: [T] -> [T] -> *). Bool -> Value' instr 'TBool
VBool (Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0)

instance ToIntArithOp 'TNat where
  evalToIntOp :: forall (instr :: [T] -> [T] -> *).
Value' instr 'TNat -> Value' instr 'TInt
evalToIntOp (VNat Natural
i) = Integer -> Value' instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
i)

instance ToIntArithOp 'TBls12381Fr where
  evalToIntOp :: forall (instr :: [T] -> [T] -> *).
Value' instr 'TBls12381Fr -> Value' instr 'TInt
evalToIntOp (VBls12381Fr Bls12381Fr
i) = Integer -> Value' instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt (Bls12381Fr -> Integer
forall a. Integral a => a -> Integer
toInteger Bls12381Fr
i)

instance ToIntArithOp 'TBytes where
  evalToIntOp :: forall (instr :: [T] -> [T] -> *).
Value' instr 'TBytes -> Value' instr 'TInt
evalToIntOp (VBytes ByteString
i) = Integer -> Value' instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt (Integer -> Value' instr 'TInt) -> Integer -> Value' instr 'TInt
forall a b. (a -> b) -> a -> b
$ case ByteString -> Maybe (Word8, ByteString)
BS.uncons ByteString
i of
    Maybe (Word8, ByteString)
Nothing -> Integer
0
    Just (Word8
msb, ByteString
_)
      -- positive, msbit not set
      | Word8
msb Word8 -> Word8 -> Word8
forall a. Bits a => a -> a -> a
.&. Word8
0x80 Word8 -> Word8 -> Bool
forall a. Eq a => a -> a -> Bool
== Word8
0 -> Integer
x
      -- negative
      | Bool
otherwise -> Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
comp
      where
        x :: Integer
x = ByteString -> Integer
forall ba. ByteArrayAccess ba => ba -> Integer
os2ip ByteString
i
        nbytes :: Int
nbytes = ByteString -> Int
forall i a.
(Integral i, Container a,
 DefaultToInt (IsIntSubType Length i) i) =>
a -> i
length ByteString
i
        comp :: Integer
comp = Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
setBit Integer
forall a. Bits a => a
zeroBits (Int
nbytes Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
8)

instance ToBytesArithOp 'TNat where
  evalToBytesOp :: forall (instr :: [T] -> [T] -> *).
Value' instr 'TNat -> Value' instr 'TBytes
evalToBytesOp (VNat Natural
i)
    | Natural
0 <- Natural
i = ByteString -> Value' instr 'TBytes
forall (instr :: [T] -> [T] -> *).
ByteString -> Value' instr 'TBytes
VBytes ByteString
forall a. Monoid a => a
mempty
    | Bool
otherwise = ByteString -> Value' instr 'TBytes
forall (instr :: [T] -> [T] -> *).
ByteString -> Value' instr 'TBytes
VBytes (ByteString -> Value' instr 'TBytes)
-> ByteString -> Value' instr 'TBytes
forall a b. (a -> b) -> a -> b
$ Integer -> ByteString
forall ba. ByteArray ba => Integer -> ba
i2osp (Integer -> ByteString) -> Integer -> ByteString
forall a b. (a -> b) -> a -> b
$ Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
i

instance ToBytesArithOp 'TInt where
  evalToBytesOp :: forall (instr :: [T] -> [T] -> *).
Value' instr 'TInt -> Value' instr 'TBytes
evalToBytesOp (VInt Integer
i)
    | Integer
0 <- Integer
i = ByteString -> Value' instr 'TBytes
forall (instr :: [T] -> [T] -> *).
ByteString -> Value' instr 'TBytes
VBytes ByteString
forall a. Monoid a => a
mempty
    | Bool
otherwise = ByteString -> Value' instr 'TBytes
forall (instr :: [T] -> [T] -> *).
ByteString -> Value' instr 'TBytes
VBytes (ByteString -> Value' instr 'TBytes)
-> ByteString -> Value' instr 'TBytes
forall a b. (a -> b) -> a -> b
$ Int -> Word8 -> ByteString
BS.replicate (Int
nbytes Int -> Int -> Int
forall a. Num a => a -> a -> a
- ByteString -> Int
forall i a.
(Integral i, Container a,
 DefaultToInt (IsIntSubType Length i) i) =>
a -> i
length ByteString
bs) Word8
0 ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> ByteString
bs
    where
      x :: Integer
x = Integer -> Integer
forall a. Num a => a -> a
abs Integer
i
      nbits :: Int
nbits = case Integer -> Int
numBits Integer
x of
        Int
n | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0, Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
setBit Integer
forall a. Bits a => a
zeroBits (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
x
          -- exactly 0b10…0, by convention it's a negative, so doesn't need an extra bit
          -> Int
n
          | Bool
otherwise -> Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 -- extra bit for sign.
      nbytes :: Int
nbytes = (Int
nbits Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
7) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
8
      bs :: ByteString
bs
        | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 = Integer -> ByteString
forall ba. ByteArray ba => Integer -> ba
i2osp Integer
i
        | Bool
otherwise = Integer -> ByteString
forall ba. ByteArray ba => Integer -> ba
i2osp (Integer -> ByteString) -> Integer -> ByteString
forall a b. (a -> b) -> a -> b
$ Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
setBit Integer
forall a. Bits a => a
zeroBits (Int
nbytes Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
8) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
x -- two's complement

evalToNatOp :: Value' instr 'TBytes -> Value' instr 'TNat
evalToNatOp :: forall (instr :: [T] -> [T] -> *).
Value' instr 'TBytes -> Value' instr 'TNat
evalToNatOp (VBytes ByteString
a)
  | ByteString -> Bool
forall t. Container t => t -> Bool
null ByteString
a = Natural -> Value' instr 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat Natural
0
  | Bool
otherwise = Natural -> Value' instr 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat (Natural -> Value' instr 'TNat)
-> (Integer -> Natural) -> Integer -> Value' instr 'TNat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (HasCallStack, Integral a, Integral b) => a -> b
Unsafe.fromIntegral @Integer @Natural (Integer -> Value' instr 'TNat) -> Integer -> Value' instr 'TNat
forall a b. (a -> b) -> a -> b
$ ByteString -> Integer
forall ba. ByteArrayAccess ba => ba -> Integer
os2ip ByteString
a

instance Buildable ShiftArithErrorType where
  build :: ShiftArithErrorType -> Doc
build = \case
    ShiftArithErrorType
LslOverflow -> Doc
"lsl overflow"
    ShiftArithErrorType
LsrUnderflow -> Doc
"lsr underflow"

instance Buildable MutezArithErrorType where
  build :: MutezArithErrorType -> Doc
build = \case
    MutezArithErrorType
AddOverflow -> Doc
"add overflow"
    MutezArithErrorType
MulOverflow -> Doc
"mul overflow"

instance (Buildable n, Buildable m) => Buildable (ArithError n m) where
  build :: ArithError n m -> Doc
build (MutezArithError MutezArithErrorType
errType n
n m
m) = Doc
"Mutez "
    Doc -> Doc -> Doc
forall b. FromDoc b => Doc -> Doc -> b
+| MutezArithErrorType
errType MutezArithErrorType -> Doc -> Doc
forall a b. (Buildable a, FromDoc b) => a -> Doc -> b
|+ Doc
" with " Doc -> Doc -> Doc
forall b. FromDoc b => Doc -> Doc -> b
+| n
n n -> Doc -> Doc
forall a b. (Buildable a, FromDoc b) => a -> Doc -> b
|+ Doc
", " Doc -> Doc -> Doc
forall b. FromDoc b => Doc -> Doc -> b
+| m
m m -> Doc -> Doc
forall a b. (Buildable a, FromDoc b) => a -> Doc -> b
|+ Doc
""
  build (ShiftArithError ShiftArithErrorType
errType n
n m
m) = Doc
""
    Doc -> Doc -> Doc
forall b. FromDoc b => Doc -> Doc -> b
+| ShiftArithErrorType
errType ShiftArithErrorType -> Doc -> Doc
forall a b. (Buildable a, FromDoc b) => a -> Doc -> b
|+ Doc
" with " Doc -> Doc -> Doc
forall b. FromDoc b => Doc -> Doc -> b
+| n
n n -> Doc -> Doc
forall a b. (Buildable a, FromDoc b) => a -> Doc -> b
|+ Doc
", " Doc -> Doc -> Doc
forall b. FromDoc b => Doc -> Doc -> b
+| m
m m -> Doc -> Doc
forall a b. (Buildable a, FromDoc b) => a -> Doc -> b
|+ Doc
""