module Michelson.TypeCheck.Instr
( typeCheckContract
, typeCheckValue
, typeVerifyValue
, typeCheckList
) where
import Prelude hiding (EQ, GT, LT)
import Control.Monad.Except (MonadError, liftEither, throwError)
import Data.Constraint (Dict(..))
import Data.Default (def)
import Data.Generics (everything, mkQ)
import Data.Singletons (SingI(sing), demote)
import Data.Typeable ((:~:)(..), gcast)
import Michelson.ErrorPos
import Michelson.TypeCheck.Error
import Michelson.TypeCheck.Ext
import Michelson.TypeCheck.Helpers
import Michelson.TypeCheck.TypeCheck
import Michelson.TypeCheck.Types
import Michelson.TypeCheck.Value
import Michelson.Typed
(Abs, And, CT(..), Contract, ContractOut1, Eq', Ge, Gt, Instr(..), IterOp(..), Le, Lsl, Lsr, Lt,
MapOp(..), Neg, Neq, Not, Notes(..), Notes'(..), Or, Sing(..), T(..), Value, Value'(..), Xor,
bigMapAbsense, bigMapConstrained, converge, convergeAnns, extractNotes, fromUType, mkNotes,
notesCase, opAbsense, orAnn, withSomeSingCT, withSomeSingT)
import qualified Michelson.Untyped as U
import Michelson.Untyped.Annotation (VarAnn)
typeCheckContract
:: TcOriginatedContracts
-> U.Contract
-> Either TCError SomeContract
typeCheckContract cs c = runTypeCheck (U.para c) cs $ typeCheckContractImpl c
typeCheckContractImpl
:: U.Contract
-> TypeCheck SomeContract
typeCheckContractImpl (U.Contract mParam mStorage pCode) = do
code <- maybe (throwError $ TCContractError "no instructions in contract code" Nothing)
pure (nonEmpty pCode)
withSomeSingT (fromUType mParam) $ \(paramS :: Sing param) ->
withSomeSingT (fromUType mStorage) $ \(storageS :: Sing st) -> do
storageNote <-
liftEither $ extractNotes mStorage storageS `onLeft`
(TCContractError "failed to extract annotations for storage:" . Just . ExtractionTypeMismatch)
paramNote <-
liftEither $ extractNotes mParam paramS `onLeft`
(TCContractError "failed to extract annotations for parameter:" . Just . ExtractionTypeMismatch)
Dict <-
note (hasTypeError "parameter" (Proxy @'TOperation)) $
opAbsense paramS
Dict <-
note (hasTypeError "storage" (Proxy @'TOperation)) $
opAbsense storageS
Dict <-
note (hasTypeError "parameter" (Proxy @param)) $
bigMapAbsense paramS
Dict <-
note (hasTypeError "storage" (Proxy @st)) $
bigMapConstrained storageS
let inpNote = mkNotes (NTPair def def def paramNote storageNote)
let inp = (STPair paramS storageS, inpNote, def) ::& SNil
inp' :/ instrOut <- typeCheckNE code inp
case instrOut of
instr ::: out -> liftEither $ do
case eqHST1 @(ContractOut1 st) out of
Right Refl -> do
let (_, outN, _) ::& SNil = out
_ <- converge outN (N $ NTPair def def def NStar storageNote)
`onLeft`
((TCContractError "contract output type violates convention:") . Just . AnnError)
pure $ SomeContract instr inp' out
Left err -> Left $ TCContractError "contract output type violates convention:" $ Just err
AnyOutInstr instr -> do
let outNote = mkNotes (NTPair def def def NStar storageNote)
let out = (STPair (STList STOperation) storageS, outNote, def)
::& SNil
pure $ SomeContract instr inp' out
where
hasTypeError name (_ :: Proxy t) =
TCContractError ("contract " <> name <> " type error") $
Just $ UnsupportedTypes [demote @t]
typeCheckNE
:: (Typeable inp)
=> NonEmpty U.ExpandedOp
-> HST inp
-> TypeCheck (SomeInstr inp)
typeCheckNE (x :| xs) = usingReaderT def . typeCheckImpl typeCheckInstr (x : xs)
typeCheckList
:: (Typeable inp)
=> [U.ExpandedOp]
-> HST inp
-> TypeCheck (SomeInstr inp)
typeCheckList = usingReaderT def ... typeCheckImpl typeCheckInstr
typeCheckValue
:: U.Value
-> (Sing t, Notes t)
-> TypeCheckInstr SomeValue
typeCheckValue = typeCheckValImpl typeCheckInstr
typeVerifyValue
:: forall t.
(Typeable t, SingI t)
=> U.Value -> TypeCheckInstr (Value t)
typeVerifyValue uval =
typeCheckValue uval (sing @t, NStar) <&> \case
val :::: _ -> gcast val ?: error "Typechecker produced value of wrong type"
typeCheckInstr :: TcInstrHandler
typeCheckInstr (U.EXT ext) si =
typeCheckExt typeCheckList ext si
typeCheckInstr U.DROP i@(_ ::& rs) = pure (i :/ DROP ::: rs)
typeCheckInstr (U.DUP _vn) i@(a ::& rs) =
pure (i :/ DUP ::: (a ::& a::& rs))
typeCheckInstr U.SWAP (i@(a ::& b ::& rs)) =
pure (i :/ SWAP ::: (b ::& a ::& rs))
typeCheckInstr instr@(U.PUSH vn mt mval) i =
withSomeSingT (fromUType mt) $ \t' -> do
nt' <- onTypeCheckInstrTypeErr instr i "wrong push type:" (extractNotes mt t')
val :::: (t :: Sing t, nt) <- typeCheckValue mval (t', nt')
proofOp <-
maybe (onTypeCheckInstrErr instr (SomeHST i)
"Operations in constant are not allowed"
$ Left $ UnsupportedTypes [demote @t])
pure (opAbsense t)
proofBigMap <-
maybe (onTypeCheckInstrErr instr (SomeHST i)
"BigMaps in constant are not allowed"
$ Left $ UnsupportedTypes [demote @t])
pure (bigMapAbsense t)
case (proofOp, proofBigMap) of
(Dict, Dict) -> pure $ i :/ PUSH val ::: ((t, nt, vn) ::& i)
typeCheckInstr (U.SOME tn vn fn) i@((at, an, _) ::& rs) = do
let n = mkNotes (NTOption tn fn an)
pure (i :/ SOME ::: ((STOption at, n, vn) ::& rs))
typeCheckInstr instr@(U.NONE tn vn fn elMt) i =
withSomeSingT (fromUType elMt) $ \elT -> do
let t = STOption elT
notes <- onTypeCheckInstrTypeErr instr i "wrong none type:"
(extractNotes (U.Type (U.TOption fn elMt) tn) t)
pure $ i :/ NONE ::: ((t, notes, vn) ::& i)
typeCheckInstr (U.UNIT tn vn) i = do
let ns = mkNotes $ NTUnit tn
pure $ i :/ UNIT ::: ((STUnit, ns, vn) ::& i)
typeCheckInstr (U.IF_NONE mp mq) i@((STOption a, ons, ovn) ::& rs) = do
let (an, avn) = deriveNsOption ons ovn
genericIf IF_NONE U.IF_NONE mp mq rs ((a, an, avn) ::& rs) i
typeCheckInstr (U.PAIR tn vn pfn qfn) i@((a, an, avn) ::&
(b, bn, bvn) ::& rs) = do
let (vn', pfn', qfn') = deriveSpecialFNs pfn qfn avn bvn
ns = mkNotes $ NTPair tn pfn' qfn' an bn
pure (i :/ PAIR ::: ((STPair a b, ns, vn `orAnn` vn') ::& rs))
typeCheckInstr (U.CAR vn _) i@((STPair a _, NStar, _) ::& rs) =
pure (i :/ CAR ::: ((a, NStar, vn) ::& rs))
typeCheckInstr instr@(U.CAR vn fn)
(i@(( STPair a b
, N (NTPair pairTN pfn qfn pns qns)
, pairVN ) ::& rs)) = do
pfn' <- onTypeCheckInstrAnnErr instr i "wrong car type:" (convergeAnns fn pfn)
let vn' = deriveSpecialVN vn pfn' pairVN
i' = ( STPair a b
, N (NTPair pairTN pfn' qfn pns qns)
, pairVN ) ::& rs
pure $ i' :/ CAR ::: ((a, pns, vn') ::& rs)
typeCheckInstr (U.CDR vn _) i@((STPair _ b, NStar, _) ::& rs) =
pure (i :/ CDR ::: ((b, NStar, vn) ::& rs))
typeCheckInstr instr@(U.CDR vn fn)
(i@(( STPair a b
, N (NTPair pairTN pfn qfn pns qns)
, pairVN ) ::& rs)) = do
qfn' <- onTypeCheckInstrAnnErr instr i "wrong cdr type:" (convergeAnns fn qfn)
let vn' = deriveSpecialVN vn qfn' pairVN
i' = ( STPair a b
, N (NTPair pairTN pfn qfn' pns qns)
, pairVN ) ::& rs
pure $ i' :/ CDR ::: ((b, qns, vn') ::& rs)
typeCheckInstr instr@(U.LEFT tn vn pfn qfn bMt) i@((a, an, _) ::& rs) =
withSomeSingT (fromUType bMt) $ \b -> do
bn <- onTypeCheckInstrTypeErr instr i "wrong left type:" (extractNotes bMt b)
let ns = mkNotes $ NTOr tn pfn qfn an bn
pure (i :/ LEFT ::: ((STOr a b, ns, vn) ::& rs))
typeCheckInstr instr@(U.RIGHT tn vn pfn qfn aMt) i@((b, bn, _) ::& rs) =
withSomeSingT (fromUType aMt) $ \a -> do
an <- onTypeCheckInstrTypeErr instr i "wrong right type:" (extractNotes aMt a)
let ns = mkNotes $ NTOr tn pfn qfn an bn
pure (i :/ RIGHT ::: ((STOr a b, ns, vn) ::& rs))
typeCheckInstr (U.IF_LEFT mp mq) i@((STOr a b, ons, ovn) ::& rs) = do
let (an, bn, avn, bvn) = deriveNsOr ons ovn
ait = (a, an, avn) ::& rs
bit = (b, bn, bvn) ::& rs
genericIf IF_LEFT U.IF_LEFT mp mq ait bit i
typeCheckInstr instr@(U.NIL tn vn elMt) i =
withSomeSingT (fromUType elMt) $ \elT -> do
let t = STList elT
notes <- onTypeCheckInstrTypeErr instr i "wrong nil type:" (extractNotes (U.Type (U.TList elMt) tn) t)
pure $ i :/ NIL ::: ((t, notes, vn) ::& i)
typeCheckInstr instr@(U.CONS vn) i@((((at :: Sing a), an, _)
::& (STList (_ :: Sing a'), ln, _) ::& rs)) =
case eqType @a @a' of
Right Refl -> do
n <- onTypeCheckInstrAnnErr instr i "wrong cons type:" (converge ln (mkNotes $ NTList def an))
pure $ i :/ CONS ::: ((STList at, n, vn) ::& rs)
Left m -> onTypeCheckInstrErr instr (SomeHST i)
("list element type is different from one "
<> "that is being CONSed:") (Left m)
typeCheckInstr (U.IF_CONS mp mq) i@((STList a, ns, vn) ::& rs) = do
let an = notesCase NStar (\(NTList _ an_) -> an_) ns
ait =
(a, an, vn <> "hd") ::& (STList a, ns, vn <> "tl") ::& rs
genericIf IF_CONS U.IF_CONS mp mq ait rs i
typeCheckInstr (U.SIZE vn) i@((STList _, _, _) ::& _) = sizeImpl i vn
typeCheckInstr (U.SIZE vn) i@((STSet _, _, _) ::& _) = sizeImpl i vn
typeCheckInstr (U.SIZE vn) i@((STMap _ _, _, _) ::& _) = sizeImpl i vn
typeCheckInstr (U.SIZE vn) i@((STc SCString, _, _) ::& _) = sizeImpl i vn
typeCheckInstr (U.SIZE vn) i@((STc SCBytes, _, _) ::& _) = sizeImpl i vn
typeCheckInstr (U.EMPTY_SET tn vn (U.Comparable mk ktn)) i =
withSomeSingCT mk $ \k ->
pure $ i :/ EMPTY_SET ::: ((STSet k, mkNotes $ NTSet tn ktn, vn) ::& i)
typeCheckInstr instr@(U.EMPTY_MAP tn vn (U.Comparable mk ktn) mv) i =
withSomeSingT (fromUType mv) $ \v ->
withSomeSingCT mk $ \k -> do
vns <- onTypeCheckInstrTypeErr instr i "wrong empty_map type:" (extractNotes mv v)
let ns = mkNotes $ NTMap tn ktn vns
pure $ i :/ EMPTY_MAP ::: ((STMap k v, ns, vn) ::& i)
typeCheckInstr instr@(U.MAP vn mp) i@((STList _, ns, _vn) ::& _) = do
let vns = notesCase NStar (\(NTList _ v') -> v') ns
mapImpl vns instr mp i
(\rt rn -> (::&) (STList rt, mkNotes $ NTList def rn, vn))
typeCheckInstr instr@(U.MAP vn mp) i@((STMap k _, ns, _vn) ::& _) = do
let (kns, vns) = notesCase (def, NStar) (\(NTMap _ k' v') -> (k', v')) ns
pns = mkNotes $ NTPair def def def (mkNotes $ NTc kns) vns
mapImpl pns instr mp i
(\rt rn -> (::&) (STMap k rt, mkNotes $ NTMap def kns rn, vn))
typeCheckInstr instr@(U.ITER (i1 : ir)) i@((STSet _, n, _) ::& _) = do
let en = notesCase NStar (\(NTSet _ en_) -> mkNotes $ NTc en_) n
iterImpl en instr (i1 :| ir) i
typeCheckInstr instr@(U.ITER (i1 : ir)) (i@((STList _, n, _) ::& _)) = do
let en = notesCase NStar (\(NTList _ en_) -> en_) n
iterImpl en instr (i1 :| ir) i
typeCheckInstr instr@(U.ITER (i1 : ir)) (i@((STMap _ _, n, _) ::& _)) = do
let en = notesCase NStar (\(NTMap _ kns vns) ->
mkNotes $ NTPair def def def (mkNotes $ NTc kns) vns) n
iterImpl en instr (i1 :| ir) i
typeCheckInstr instr@(U.MEM vn)
i@((STc _, _, _) ::& (STSet _, _, _) ::& _) = memImpl instr i vn
typeCheckInstr instr@(U.MEM vn)
i@((STc _, _, _) ::& (STMap _ _, _, _) ::& _) = memImpl instr i vn
typeCheckInstr instr@(U.MEM vn)
i@((STc _, _, _) ::& (STBigMap _ _, _, _) ::& _) = memImpl instr i vn
typeCheckInstr instr@(U.GET vn) i@(_ ::& (STMap _ vt, cn, _) ::& _) =
getImpl instr i vt (notesCase NStar (\(NTMap _ _ v) -> v) cn) vn
typeCheckInstr instr@(U.GET vn) i@(_ ::& (STBigMap _ vt, cn, _) ::& _) =
getImpl instr i vt (notesCase NStar (\(NTBigMap _ _ v) -> v) cn) vn
typeCheckInstr instr@U.UPDATE i@(_ ::& _ ::& (STMap _ _, _, _) ::& _) =
updImpl instr i
typeCheckInstr instr@U.UPDATE i@(_ ::& _ ::& (STBigMap _ _, _, _)
::& _) = updImpl instr i
typeCheckInstr instr@U.UPDATE i@(_ ::& _ ::& (STSet _, _, _) ::& _) = updImpl instr i
typeCheckInstr (U.IF mp mq) i@((STc SCBool, _, _) ::& rs) =
genericIf IF U.IF mp mq rs rs i
typeCheckInstr instr@(U.LOOP is)
i@((STc SCBool, _, _) ::& (rs :: HST rs)) = do
_ :/ tp <- lift $ typeCheckList is rs
case tp of
subI ::: (o :: HST o) -> do
case eqHST o (sing @('Tc 'CBool) -:& rs) of
Right Refl -> do
let _ ::& rs' = o
pure $ i :/ LOOP subI ::: rs'
Left m -> onTypeCheckInstrErr instr (SomeHST i)
"iteration expression has wrong output stack type:" (Left m)
AnyOutInstr subI ->
pure $ i :/ LOOP subI ::: rs
typeCheckInstr instr@(U.LOOP_LEFT is)
i@((STOr (at :: Sing a) (bt :: Sing b), ons, ovn)
::& (rs :: HST rs)) = do
let (an, bn, avn, bvn) = deriveNsOr ons ovn
ait = (at, an, avn) ::& rs
_ :/ tp <- lift $ typeCheckList is ait
case tp of
subI ::: o -> do
case (eqHST o (sing @('TOr a b) -:& rs), o) of
(Right Refl, ((STOr _ bt', ons', ovn') ::& rs')) -> do
let (_, bn', _, bvn') = deriveNsOr ons' ovn'
br <- onTypeCheckInstrAnnErr instr i "wrong LOOP_LEFT input type:" $
convergeHSTEl (bt, bn, bvn) (bt', bn', bvn')
pure $ i :/ LOOP_LEFT subI ::: (br ::& rs')
(Left m, _) -> onTypeCheckInstrErr instr (SomeHST i)
"iteration expression has wrong output stack type:" (Left m)
AnyOutInstr subI -> do
let br = (bt, bn, bvn)
pure $ i :/ LOOP_LEFT subI ::: (br ::& rs)
typeCheckInstr instr@(U.LAMBDA vn imt omt is) i = do
withSomeSingT (fromUType imt) $ \(it :: Sing it) -> do
withSomeSingT (fromUType omt) $ \(ot :: Sing ot) -> do
ins <- onTypeCheckInstrTypeErr instr i "wrong lambda input type:" (extractNotes imt it)
ons <- onTypeCheckInstrTypeErr instr i "wrong lambda output type:" (extractNotes omt ot)
lamImpl instr is vn it ins ot ons i
typeCheckInstr instr@(U.EXEC vn) i@(((_ :: Sing t1), _, _)
::& (STLambda (_ :: Sing t1') t2, ln, _)
::& rs) = do
let t2n = notesCase NStar (\(NTLambda _ _ n) -> n) ln
Refl <- onTypeCheckInstrErr instr (SomeHST i)
"lambda is given argument with wrong type:" (eqType @t1 @t1')
pure $ i :/ EXEC ::: ((t2, t2n, vn) ::& rs)
typeCheckInstr instr@(U.DIP is) i@(a ::& (s :: HST s)) = do
_ :/ tp <- lift (typeCheckList is s)
case tp of
subI ::: t ->
pure $ i :/ DIP subI ::: (a ::& t)
AnyOutInstr _ -> do
typeCheckInstrErr instr (SomeHST i)
"Code within DIP instruction always fails, which is not allowed"
typeCheckInstr U.FAILWITH i@(_ ::& _) =
pure $ i :/ AnyOutInstr FAILWITH
typeCheckInstr instr@(U.CAST vn mt)
i@(((e :: Sing e), (en :: Notes e), evn) ::& rs) =
withSomeSingT (fromUType mt) $ \(_ :: Sing e') -> do
Refl <- errM (eqType @e @e')
en' <- errM (extractNotes mt e `onLeft` ExtractionTypeMismatch)
ns <- errM (converge en en' `onLeft` AnnError)
pure $ i :/ CAST ::: ((e, ns, vn `orAnn` evn) ::& rs)
where
errM :: (MonadReader InstrCallStack m, MonadError TCError m) => Either TCTypeError a -> m a
errM = onTypeCheckInstrErr instr (SomeHST i) "cast to incompatible type:"
typeCheckInstr (U.RENAME vn) i@((at, an, _) ::& rs) =
pure $ i :/ RENAME ::: ((at, an, vn) ::& rs)
typeCheckInstr instr@(U.UNPACK vn mt) i@((STc SCBytes, _, _) ::& rs) =
withSomeSingT (fromUType mt) $ \t -> do
tns <- onTypeCheckInstrTypeErr instr i "wrong unpack type" (extractNotes mt t)
let ns = mkNotes $ NTOption def def tns
proofOp <-
maybe (typeCheckInstrErr instr (SomeHST i)
"Operation cannot appear in serialized data")
pure (opAbsense t)
proofBigMap <-
maybe (typeCheckInstrErr instr (SomeHST i)
"BigMap cannot appear in serialized data")
pure (bigMapAbsense t)
case (proofOp, proofBigMap) of
(Dict, Dict) -> pure $ i :/ UNPACK ::: ((STOption t, ns, vn) ::& rs)
typeCheckInstr instr@(U.PACK vn) i@(((a :: Sing a), _, _) ::& rs) = do
proofOp <-
maybe (onTypeCheckInstrErr instr (SomeHST i)
"Operations cannot appear in serialized data"
$ Left $ UnsupportedTypes [demote @a])
pure (opAbsense a)
proofBigMap <-
maybe (onTypeCheckInstrErr instr (SomeHST i)
"BigMap cannot appear in serialized data"
$ Left $ UnsupportedTypes [demote @a])
pure (bigMapAbsense a)
case (proofOp, proofBigMap) of
(Dict, Dict) -> pure $ i :/ PACK ::: ((STc SCBytes, NStar, vn) ::& rs)
typeCheckInstr (U.CONCAT vn) i@((STc SCBytes, _, _) ::&
(STc SCBytes, _, _) ::& _) = concatImpl i vn
typeCheckInstr (U.CONCAT vn) i@((STc SCString, _, _) ::&
(STc SCString, _, _) ::& _) = concatImpl i vn
typeCheckInstr (U.CONCAT vn) i@((STList (STc SCBytes), _, _) ::& _) = concatImpl' i vn
typeCheckInstr (U.CONCAT vn) i@((STList (STc SCString), _, _) ::& _) = concatImpl' i vn
typeCheckInstr (U.SLICE vn) i@((STc SCNat, _, _) ::&
(STc SCNat, _, _) ::&
(STc SCString, _, _) ::& _) = sliceImpl i vn
typeCheckInstr (U.SLICE vn) i@((STc SCNat, _, _) ::&
(STc SCNat, _, _) ::&
(STc SCBytes, _, _) ::& _) = sliceImpl i vn
typeCheckInstr (U.ISNAT vn') i@((STc SCInt, _, oldVn) ::& rs) = do
let vn = vn' `orAnn` oldVn
pure $ i :/ ISNAT ::: ((STOption (STc SCNat), NStar, vn) ::& rs)
typeCheckInstr (U.ADD vn) i@((STc a, _, _) ::&
(STc b, _, _) ::& _) = addImpl a b i vn
typeCheckInstr (U.SUB vn) i@((STc a, _, _) ::&
(STc b, _, _) ::& _) = subImpl a b i vn
typeCheckInstr (U.MUL vn) i@((STc a, _, _) ::&
(STc b, _, _) ::& _) = mulImpl a b i vn
typeCheckInstr (U.EDIV vn) i@((STc a, _, _) ::&
(STc b, _, _) ::& _) = edivImpl a b i vn
typeCheckInstr (U.ABS vn) i@((STc SCInt, _, _) ::& _) = unaryArithImpl @Abs ABS i vn
typeCheckInstr U.NEG (i@((STc SCInt, _, _) ::& _)) = unaryArithImpl @Neg NEG i def
typeCheckInstr U.NEG (i@((STc SCNat, _, _) ::& _)) = unaryArithImpl @Neg NEG i def
typeCheckInstr (U.LSL vn) i@((STc SCNat, _, _) ::&
(STc SCNat, _, _) ::& _) = arithImpl @Lsl LSL i vn
typeCheckInstr (U.LSR vn) i@((STc SCNat, _, _) ::&
(STc SCNat, _, _) ::& _) = arithImpl @Lsr LSR i vn
typeCheckInstr (U.OR vn) i@((STc SCBool, _, _) ::&
(STc SCBool, _, _) ::& _) = arithImpl @Or OR i vn
typeCheckInstr (U.OR vn) i@((STc SCNat, _, _) ::&
(STc SCNat, _, _) ::& _) = arithImpl @Or OR i vn
typeCheckInstr (U.AND vn) i@((STc SCInt, _, _) ::&
(STc SCNat, _, _) ::& _) = arithImpl @And AND i vn
typeCheckInstr (U.AND vn) i@((STc SCNat, _, _) ::&
(STc SCNat, _, _) ::& _) = arithImpl @And AND i vn
typeCheckInstr (U.AND vn) i@((STc SCBool, _, _) ::&
(STc SCBool, _, _) ::& _) = arithImpl @And AND i vn
typeCheckInstr (U.XOR vn) i@((STc SCBool, _, _) ::&
(STc SCBool, _, _) ::& _) = arithImpl @Xor XOR i vn
typeCheckInstr (U.XOR vn) i@((STc SCNat, _, _) ::&
(STc SCNat, _, _) ::& _) = arithImpl @Xor XOR i vn
typeCheckInstr (U.NOT vn) i@((STc SCNat, _, _) ::& _) = unaryArithImpl @Not NOT i vn
typeCheckInstr (U.NOT vn) i@((STc SCBool, _, _) ::& _) = unaryArithImpl @Not NOT i vn
typeCheckInstr (U.NOT vn) i@((STc SCInt, _, _) ::& _) = unaryArithImpl @Not NOT i vn
typeCheckInstr (U.COMPARE vn) i@((STc a, _, _) ::&
(STc b, _, _) ::& _) = compareImpl a b i vn
typeCheckInstr (U.EQ vn) i@((STc SCInt, _, _) ::& _) = unaryArithImpl @Eq' EQ i vn
typeCheckInstr (U.NEQ vn) i@((STc SCInt, _, _) ::& _) = unaryArithImpl @Neq NEQ i vn
typeCheckInstr (U.LT vn) i@((STc SCInt, _, _) ::& _) = unaryArithImpl @Lt LT i vn
typeCheckInstr (U.GT vn) i@((STc SCInt, _, _) ::& _) = unaryArithImpl @Gt GT i vn
typeCheckInstr (U.LE vn) i@((STc SCInt, _, _) ::& _) = unaryArithImpl @Le LE i vn
typeCheckInstr (U.GE vn) i@((STc SCInt, _, _) ::& _) = unaryArithImpl @Ge GE i vn
typeCheckInstr (U.INT vn) i@((STc SCNat, _, _) ::& rs) =
pure $ i :/ INT ::: ((STc SCInt, NStar, vn) ::& rs)
typeCheckInstr instr@(U.SELF vn) shst@i = do
cpType <- gets tcContractParam
let t = fromUType cpType
withSomeSingT t $ \(singcp :: Sing cp) -> do
nt <- onTypeCheckInstrTypeErr instr shst "wrong self type" (extractNotes cpType singcp )
pure $ i :/ SELF @cp ::: ((sing @('TContract cp), N (NTContract U.noAnn nt), vn) ::& i)
typeCheckInstr instr@(U.CONTRACT vn mt)
i@((STc SCAddress, _, _) ::& rs) =
withSomeSingT (fromUType mt) $ \t -> do
tns <- onTypeCheckInstrTypeErr instr i "wrong contract command type" (extractNotes mt t)
let ns = mkNotes $ NTOption def def $ mkNotes $ NTContract def tns
pure $ i :/ CONTRACT tns ::: ((STOption $ STContract t, ns, vn) ::& rs)
typeCheckInstr instr@(U.TRANSFER_TOKENS vn) i@(((_ :: Sing p'), _, _)
::& (STc SCMutez, _, _) ::& (STContract (p :: Sing p), _, _) ::& rs) = do
proofOp <-
maybe (onTypeCheckInstrErr instr (SomeHST i)
"contract param type cannot contain operation"
$ Left $ UnsupportedTypes [demote @p])
pure (opAbsense p)
proofBigMap <-
maybe (onTypeCheckInstrErr instr (SomeHST i)
"contract param type cannot contain big_map"
$ Left $ UnsupportedTypes [demote @p])
pure (bigMapAbsense p)
case (eqType @p @p', proofOp, proofBigMap) of
(Right Refl, Dict, Dict) ->
pure $ i :/ TRANSFER_TOKENS ::: ((STOperation, NStar, vn) ::& rs)
(Left m, _, _) ->
onTypeCheckInstrErr instr (SomeHST i)
"mismatch of contract param type:" (Left m)
typeCheckInstr (U.SET_DELEGATE vn)
i@((STOption (STc SCKeyHash), _, _) ::& rs) = do
pure $ i :/ SET_DELEGATE ::: ((STOperation, NStar, vn) ::& rs)
typeCheckInstr (U.CREATE_ACCOUNT ovn avn)
i@((STc SCKeyHash, _, _)
::& (STOption (STc SCKeyHash), _, _) ::& (STc SCBool, _, _)
::& (STc SCMutez, _, _) ::& rs) =
pure $ i :/ CREATE_ACCOUNT ::: ((STOperation, NStar, ovn) ::&
(STc SCAddress, NStar, avn) ::& rs)
typeCheckInstr instr@(U.CREATE_CONTRACT ovn avn contract)
i@((STc SCKeyHash, _, _)
::& (STOption (STc SCKeyHash), _, _)
::& (STc SCBool, _, _)
::& (STc SCBool, _, _)
::& (STc SCMutez, _, _)
::& ((_ :: Sing g), gn, _) ::& rs) = do
(SomeContract (contr :: Contract p' g') _ out) <- lift $ typeCheckContractImpl contract
Refl <- checkEqT @g @g' instr i "contract storage type mismatch"
void $ onTypeCheckInstrAnnErr instr i "contract storage type mismatch" (converge gn (outNotes out) )
pure $ i :/ CREATE_CONTRACT contr ::: ((STOperation, NStar, ovn) ::&
(STc SCAddress, NStar, avn) ::& rs)
where
outNotes :: HST '[ 'TPair ('TList 'TOperation) g' ] -> Notes g'
outNotes ((_, n, _) ::& SNil) =
notesCase NStar (\(NTPair _ _ _ _ n') -> n') n
typeCheckInstr (U.IMPLICIT_ACCOUNT vn)
i@((STc SCKeyHash, _, _) ::& rs) =
pure $ i :/ IMPLICIT_ACCOUNT ::: ((STContract STUnit, NStar, vn) ::& rs)
typeCheckInstr (U.NOW vn) i =
pure $ i :/ NOW ::: ((STc SCTimestamp, NStar, vn) ::& i)
typeCheckInstr (U.AMOUNT vn) i =
pure $ i :/ AMOUNT ::: ((STc SCMutez, NStar, vn) ::& i)
typeCheckInstr (U.BALANCE vn) i =
pure $ i :/ BALANCE ::: ((STc SCMutez, NStar, vn) ::& i)
typeCheckInstr (U.CHECK_SIGNATURE vn)
i@((STKey, _, _)
::& (STSignature, _, _) ::& (STc SCBytes, _, _) ::& rs) =
pure $ i :/ CHECK_SIGNATURE ::: ((STc SCBool, NStar, vn) ::& rs)
typeCheckInstr (U.SHA256 vn)
i@((STc SCBytes, _, _) ::& rs) =
pure $ i :/ SHA256 ::: ((STc SCBytes, NStar, vn) ::& rs)
typeCheckInstr (U.SHA512 vn)
i@((STc SCBytes, _, _) ::& rs) =
pure $ i :/ SHA512 ::: ((STc SCBytes, NStar, vn) ::& rs)
typeCheckInstr (U.BLAKE2B vn)
i@((STc SCBytes, _, _) ::& rs) =
pure $ i :/ BLAKE2B ::: ((STc SCBytes, NStar, vn) ::& rs)
typeCheckInstr (U.HASH_KEY vn)
i@((STKey, _, _) ::& rs) =
pure $ i :/ HASH_KEY ::: ((STc SCKeyHash, NStar, vn) ::& rs)
typeCheckInstr (U.STEPS_TO_QUOTA vn) i =
pure $ i :/ STEPS_TO_QUOTA ::: ((STc SCNat, NStar, vn) ::& i)
typeCheckInstr (U.SOURCE vn) i =
pure $ i :/ SOURCE ::: ((STc SCAddress, NStar, vn) ::& i)
typeCheckInstr (U.SENDER vn) i =
pure $ i :/ SENDER ::: ((STc SCAddress, NStar, vn) ::& i)
typeCheckInstr (U.ADDRESS vn) i@((STContract _, _, _) ::& rs) =
pure $ i :/ ADDRESS ::: ((STc SCAddress, NStar, vn) ::& rs)
typeCheckInstr instr sit = typeCheckInstrErr instr (SomeHST sit) "unknown expression"
genericIf
:: forall bti bfi cond rs .
(Typeable bti, Typeable bfi)
=> (forall s'.
Instr bti s' ->
Instr bfi s' ->
Instr (cond ': rs) s'
)
-> ([U.ExpandedOp] -> [U.ExpandedOp] -> U.ExpandedInstr)
-> [U.ExpandedOp]
-> [U.ExpandedOp]
-> HST bti
-> HST bfi
-> HST (cond ': rs)
-> TypeCheckInstr (SomeInstr (cond ': rs))
genericIf cons mCons mbt mbf bti bfi i@(_ ::& _) = do
_ :/ pinstr <- lift $ typeCheckList mbt bti
_ :/ qinstr <- lift $ typeCheckList mbf bfi
fmap (i :/) $ case (pinstr, qinstr) of
(p ::: po, q ::: qo) -> do
let instr = mCons mbt mbf
Refl <- checkEqHST qo po instr i
"branches have different output stack types:"
o <- onTypeCheckInstrAnnErr instr i "branches have different output stack types:" (convergeHST po qo)
pure $ cons p q ::: o
(AnyOutInstr p, q ::: qo) -> do
pure $ cons p q ::: qo
(p ::: po, AnyOutInstr q) -> do
pure $ cons p q ::: po
(AnyOutInstr p, AnyOutInstr q) ->
pure $ AnyOutInstr (cons p q)
mapImpl
:: forall c rs .
( MapOp c
, SingI (MapOpInp c)
, Typeable (MapOpInp c)
, Typeable (MapOpRes c)
)
=> Notes (MapOpInp c)
-> U.ExpandedInstr
-> [U.ExpandedOp]
-> HST (c ': rs)
-> (forall v' . (Typeable v', SingI v') =>
Sing v' -> Notes v' -> HST rs -> HST (MapOpRes c v' ': rs))
-> TypeCheckInstr (SomeInstr (c ': rs))
mapImpl vn instr mp i@(_ ::& rs) mkRes = do
_ :/ subp <- lift $ typeCheckList mp ((sing, vn, def) ::& rs)
case subp of
sub ::: subo ->
case subo of
(b, bn, _bvn) ::& rs' -> do
Refl <- checkEqHST rs rs' instr i $
"map expression has changed not only top of the stack"
pure $ i :/ MAP sub ::: mkRes b bn rs'
_ -> typeCheckInstrErr instr (SomeHST i) "map expression has wrong output stack type (empty stack)"
AnyOutInstr _ ->
typeCheckInstrErr instr (SomeHST i) "MAP code block always fails, which is not allowed"
iterImpl
:: forall c rs .
( IterOp c
, SingI (IterOpEl c)
, Typeable (IterOpEl c)
)
=> Notes (IterOpEl c)
-> U.ExpandedInstr
-> NonEmpty U.ExpandedOp
-> HST (c ': rs)
-> TypeCheckInstr (SomeInstr (c ': rs))
iterImpl en instr mp i@((_, _, lvn) ::& rs) = do
let evn = deriveVN "elt" lvn
_ :/ subp <- lift $ typeCheckNE mp ((sing, en, evn) ::& rs)
case subp of
subI ::: o -> do
Refl <- checkEqHST o rs instr i
"iteration expression has wrong output stack type"
pure $ i :/ ITER subI ::: o
AnyOutInstr _ ->
typeCheckInstrErr instr (SomeHST i) "ITER code block always fails, which is not allowed"
lamImpl
:: forall it ot ts .
( Typeable it, Typeable ts, Typeable ot
, SingI it, SingI ot
)
=> U.ExpandedInstr
-> [U.ExpandedOp]
-> VarAnn
-> Sing it -> Notes it
-> Sing ot -> Notes ot
-> HST ts
-> TypeCheckInstr (SomeInstr ts)
lamImpl instr is vn it ins ot ons i = do
when (any hasSelf is) $
typeCheckInstrErr instr (SomeHST i) "The SELF instruction cannot appear in a lambda"
_ :/ lamI <- lift $ typeCheckList is ((it, ins, def) ::& SNil)
let lamNotes onsr = mkNotes $ NTLambda def ins onsr
let lamSt onsr = (STLambda it ot, lamNotes onsr, vn) ::& i
fmap (i :/) $ case lamI of
lam ::: lo -> do
case eqHST1 @ot lo of
Right Refl -> do
let (_, ons', _) ::& SNil = lo
onsr <- onTypeCheckInstrAnnErr instr i "wrong output type of lambda's expression:" (converge ons ons')
pure (LAMBDA (VLam lam) ::: lamSt onsr)
Left m -> onTypeCheckInstrErr instr (SomeHST i)
"wrong output type of lambda's expression:" (Left m)
AnyOutInstr lam ->
pure (LAMBDA (VLam lam) ::: lamSt ons)
where
hasSelf :: U.ExpandedOp -> Bool
hasSelf = everything (||)
(mkQ False
(\case
(U.SELF _ :: U.InstrAbstract U.ExpandedOp) -> True
_ -> False
)
)