module Michelson.TypeCheck.Instr
( typeCheckContract
, typeCheckValue
, typeVerifyValue
, typeCheckList
, typeVerifyTopLevelType
, typeCheckTopLevelType
) 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
import Util.Peano
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)
withUType mParam $ \(paramS :: Sing param, paramNote :: Notes param) ->
withUType mStorage $ \(storageS :: Sing st, storageNote :: Notes st) -> do
(Dict, Dict) <-
note (hasTypeError "parameter" paramS) $
(,) <$> opAbsense paramS
<*> nestedBigMapsAbsense paramS
(Dict, Dict, Dict) <-
note (hasTypeError "storage" storageS) $
(,,) <$> opAbsense storageS
<*> nestedBigMapsAbsense storageS
<*> contractTypeAbsense storageS
let inpNote = NTPair def def def paramNote storageNote
let inp = (STPair paramS storageS, inpNote, def) ::& SNil
inp' :/ instrOut <- typeCheckNE code inp
let (paramNotesRaw, fcStoreNotes) = case inp' of
(_, NTPair _ _ _ cpNotes stNotes, _) ::& SNil -> (cpNotes, stNotes)
fcParamNotesSafe <-
liftEither $
mkParamNotes paramNotesRaw `onLeft`
(TCContractError "invalid parameter declaration: " . Just . IllegalParamDecl)
case instrOut of
instr ::: out -> liftEither $ do
case eqHST1 @(ContractOut1 st) out of
Right Refl -> do
let (_, outN, _) ::& SNil = out
_ <- converge outN (NTPair def def def starNotes storageNote)
`onLeft`
((TCContractError "contract output type violates convention:") . Just . AnnError)
pure $ SomeContract FullContract
{ fcCode = instr
, fcParamNotesSafe, fcStoreNotes
}
Left err -> Left $ TCContractError "contract output type violates convention:" $ Just err
AnyOutInstr instr ->
pure $ SomeContract FullContract
{ fcCode = instr
, fcParamNotesSafe, fcStoreNotes
}
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 SomeNotedValue
typeCheckValue = typeCheckValImpl typeCheckInstr
typeVerifyValue
:: forall t.
(Typeable t, SingI t)
=> U.Value -> TypeCheckInstr (Value t)
typeVerifyValue uval =
typeCheckValue uval (sing @t, starNotes) <&> \case
val :::: _ -> gcast val ?: error "Typechecker produced value of wrong type"
typeVerifyTopLevelType
:: (Typeable t, SingI t, HasCallStack)
=> TcOriginatedContracts -> U.Value -> Either TCError (Value t)
typeVerifyTopLevelType originatedContracts valueU =
runTypeCheck param originatedContracts $ usingReaderT (def :: InstrCallStack) $
typeVerifyValue valueU
where
param = error "parameter type touched during top-level type typecheck"
typeCheckTopLevelType
:: HasCallStack
=> TcOriginatedContracts -> U.Type -> U.Value -> Either TCError SomeValue
typeCheckTopLevelType originatedContracts typeU valueU =
withSomeSingT (fromUType typeU) $ \(_ :: Sing t) ->
SomeValue <$> typeVerifyTopLevelType @t originatedContracts valueU
data TCDropHelper inp where
TCDropHelper ::
forall (n :: Peano) inp out.
(Typeable out, SingI n, KnownPeano n, LongerOrSameLength inp n, Drop n inp ~ out) =>
Sing n -> HST out -> TCDropHelper inp
data TCDigHelper inp where
TCDigHelper ::
forall (n :: Peano) inp out a.
(Typeable out, ConstraintDIG n inp out a) =>
Sing n -> HST out -> TCDigHelper inp
data TCDugHelper inp where
TCDugHelper ::
forall (n :: Peano) inp out a.
(Typeable out, ConstraintDUG n inp out a) =>
Sing n -> HST out -> TCDugHelper inp
typeCheckInstr :: TcInstrHandler
typeCheckInstr uInstr inp = case (uInstr, inp) of
(U.EXT ext, si) ->
typeCheckExt typeCheckList ext si
(U.DROP, _ ::& rs) -> pure (inp :/ DROP ::: rs)
(U.DROPN nTotal, inputHST) ->
go nTotal inputHST <&> \case
TCDropHelper s out -> inputHST :/ DROPN s ::: out
where
go :: forall inp. Typeable inp
=> Word
-> HST inp
-> TypeCheckInstr (TCDropHelper inp)
go n i = case (n, i) of
(0, _) -> pure (TCDropHelper SZ i)
(_, SNil) -> onTypeCheckInstrErr uInstr
(SomeHST SNil) "" (Left (NotEnoughItemsOnStack nTotal NotEnoughDrop))
(_, (_ ::& iTail)) -> do
go (n - 1) iTail <&> \case TCDropHelper s out -> TCDropHelper (SS s) out
(U.DUP _vn, a ::& rs) ->
pure (inp :/ DUP ::: (a ::& a::& rs))
(U.SWAP, a ::& b ::& rs) ->
pure (inp :/ SWAP ::: (b ::& a ::& rs))
(U.DIG nTotal, inputHST) ->
go nTotal inputHST <&> \case
TCDigHelper s out -> inputHST :/ DIG s ::: out
where
go :: forall inp. Typeable inp
=> Word
-> HST inp
-> TypeCheckInstr (TCDigHelper inp)
go n i = case (n, i) of
(_, SNil) -> onTypeCheckInstrErr uInstr
(SomeHST SNil) "" (Left (NotEnoughItemsOnStack nTotal NotEnoughDig))
(0, (_ ::& _)) -> pure (TCDigHelper SZ i)
(_, (b ::& iTail)) ->
go (n - 1) iTail <&> \case
TCDigHelper s (a ::& resTail) -> TCDigHelper (SS s) (a ::& b ::& resTail)
(U.DUG nTotal, inputHST) ->
go nTotal inputHST <&> \case
TCDugHelper s out -> inputHST :/ DUG s ::: out
where
go :: forall inp. Typeable inp
=> Word
-> HST inp
-> TypeCheckInstr (TCDugHelper inp)
go n i = case (n, i) of
(0, (_ ::& _)) -> pure (TCDugHelper SZ i)
(_, (a ::& b ::& iTail)) ->
go (n - 1) (a ::& iTail) <&> \case
TCDugHelper s resTail -> TCDugHelper (SS s) (b ::& resTail)
_ -> onTypeCheckInstrErr uInstr
(SomeHST i) "" (Left (NotEnoughItemsOnStack nTotal NotEnoughDug))
(U.PUSH vn mt mval, i) ->
withUType mt $ \(t' :: Sing t', nt' :: Notes t') -> do
val :::: (t :: Sing t, nt) <- typeCheckValue mval (t', nt')
proofOp <-
maybe (onTypeCheckInstrErr uInstr (SomeHST i)
"Operations in constant are not allowed"
$ Left $ UnsupportedTypes [demote @t])
pure (opAbsense t)
proofBigMap <-
maybe (onTypeCheckInstrErr uInstr (SomeHST i)
"BigMaps in constant are not allowed"
$ Left $ UnsupportedTypes [demote @t])
pure (bigMapAbsense t)
proofContract <-
maybe (onTypeCheckInstrErr uInstr (SomeHST i)
"Contract type in constant is not allowed"
$ Left $ UnsupportedTypes [demote @t])
pure (contractTypeAbsense t)
case (proofOp, proofBigMap, proofContract) of
(Dict, Dict, Dict) -> pure $ i :/ PUSH val ::: ((t, nt, vn) ::& i)
(U.SOME tn vn, (at, an, _) ::& rs) -> do
pure (inp :/ SOME ::: ((STOption at, NTOption tn an, vn) ::& rs))
(U.NONE tn vn elMt, _) ->
withUType elMt $ \(elSing :: Sing t, elNotes :: Notes t) ->
pure $ inp :/ NONE ::: ((STOption elSing, NTOption tn elNotes, vn) ::& inp)
(U.UNIT tn vn, _) ->
pure $ inp :/ UNIT ::: ((STUnit, NTUnit tn, vn) ::& inp)
(U.IF_NONE mp mq, (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) inp
(U.PAIR tn vn pfn qfn, (a, an, avn) ::& (b, bn, bvn) ::& rs) -> do
let (vn', pfn', qfn') = deriveSpecialFNs pfn qfn avn bvn
ns = NTPair tn pfn' qfn' an bn
pure (inp :/ PAIR ::: ((STPair a b, ns, vn `orAnn` vn') ::& rs))
(U.CAR vn fn, ( STPair a b
, NTPair pairTN pfn qfn pns qns
, pairVN ) ::& rs) -> do
pfn' <- onTypeCheckInstrAnnErr uInstr inp "wrong car type:" (convergeAnns fn pfn)
let vn' = deriveSpecialVN vn pfn' pairVN
i' = ( STPair a b
, NTPair pairTN pfn' qfn pns qns
, pairVN ) ::& rs
pure $ i' :/ AnnCAR fn ::: ((a, pns, vn') ::& rs)
(U.CDR vn fn, ( STPair a b
, NTPair pairTN pfn qfn pns qns
, pairVN ) ::& rs) -> do
qfn' <- onTypeCheckInstrAnnErr uInstr inp "wrong cdr type:" (convergeAnns fn qfn)
let vn' = deriveSpecialVN vn qfn' pairVN
i' = ( STPair a b
, NTPair pairTN pfn qfn' pns qns
, pairVN ) ::& rs
pure $ i' :/ AnnCDR fn ::: ((b, qns, vn') ::& rs)
(U.LEFT tn vn pfn qfn bMt, (a, an, _) ::& rs) ->
withUType bMt $ \(b :: Sing b, bn :: Notes b) -> do
let ns = NTOr tn pfn qfn an bn
pure (inp :/ LEFT ::: ((STOr a b, ns, vn) ::& rs))
(U.RIGHT tn vn pfn qfn aMt, (b, bn, _) ::& rs) ->
withUType aMt $ \(a :: Sing a, an :: Notes a) -> do
let ns = NTOr tn pfn qfn an bn
pure (inp :/ RIGHT ::: ((STOr a b, ns, vn) ::& rs))
(U.IF_LEFT mp mq, (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 inp
(U.NIL tn vn elMt, i) ->
withUType elMt $ \(elT :: Sing elT, elNotes :: Notes elT) ->
pure $ i :/ NIL ::: ((STList elT, NTList tn elNotes, vn) ::& i)
(U.CONS vn, ((at :: Sing a), an, _)
::& (STList (_ :: Sing a'), ln, _) ::& rs) ->
case eqType @a @a' of
Right Refl -> do
n <- onTypeCheckInstrAnnErr uInstr inp "wrong cons type:" (converge ln (NTList def an))
pure $ inp :/ CONS ::: ((STList at, n, vn) ::& rs)
Left m -> onTypeCheckInstrErr uInstr (SomeHST inp)
("list element type is different from one "
<> "that is being CONSed:") (Left m)
(U.IF_CONS mp mq, (STList a, ns, vn) ::& rs) -> do
let NTList _ an = ns
ait = (a, an, vn <> "hd") ::& (STList a, ns, vn <> "tl") ::& rs
genericIf IF_CONS U.IF_CONS mp mq ait rs inp
(U.SIZE vn, (STList _, _, _) ::& _) -> sizeImpl inp vn
(U.SIZE vn, (STSet _, _, _) ::& _) -> sizeImpl inp vn
(U.SIZE vn, (STMap _ _, _, _) ::& _) -> sizeImpl inp vn
(U.SIZE vn, (STc SCString, _, _) ::& _) -> sizeImpl inp vn
(U.SIZE vn, (STc SCBytes, _, _) ::& _) -> sizeImpl inp vn
(U.EMPTY_SET tn vn (U.Comparable mk ktn), i) ->
withSomeSingCT mk $ \k ->
pure $ i :/ EMPTY_SET ::: ((STSet k, NTSet tn ktn, vn) ::& inp)
(U.EMPTY_MAP tn vn (U.Comparable mk ktn) mv, i) ->
withUType mv $ \(v :: Sing v, vns :: Notes v) ->
withSomeSingCT mk $ \k -> do
let ns = NTMap tn ktn vns
pure $ i :/ EMPTY_MAP ::: ((STMap k v, ns, vn) ::& i)
(U.EMPTY_BIG_MAP tn vn (U.Comparable mk ktn) mv, i) ->
withUType mv $ \(v :: Sing v, vns :: Notes v) ->
withSomeSingCT mk $ \k -> do
let ns = NTBigMap tn ktn vns
pure $ i :/ EMPTY_BIG_MAP ::: ((STBigMap k v, ns, vn) ::& i)
(U.MAP vn mp, (STList _, NTList _ vns, _vn) ::& _) -> do
mapImpl vns uInstr mp inp
(\rt rn -> (::&) (STList rt, NTList def rn, vn))
(U.MAP vn mp, (STMap k _, NTMap _ kns vns, _vn) ::& _) -> do
let pns = NTPair def def def (NTc kns) vns
mapImpl pns uInstr mp inp
(\rt rn -> (::&) (STMap k rt, NTMap def kns rn, vn))
(U.ITER (i1 : ir), (STSet _, NTSet _ en, _) ::& _) -> do
iterImpl (NTc en) uInstr (i1 :| ir) inp
(U.ITER (i1 : ir), (STList _, NTList _ en, _) ::& _) -> do
iterImpl en uInstr (i1 :| ir) inp
(U.ITER (i1 : ir), (STMap _ _, NTMap _ kns vns, _) ::& _) -> do
let en = NTPair def def def (NTc kns) vns
iterImpl en uInstr (i1 :| ir) inp
(U.MEM vn, (STc _, _, _) ::& (STSet _, _, _) ::& _) ->
memImpl uInstr inp vn
(U.MEM vn, (STc _, _, _) ::& (STMap _ _, _, _) ::& _) ->
memImpl uInstr inp vn
(U.MEM vn, (STc _, _, _) ::& (STBigMap _ _, _, _) ::& _) ->
memImpl uInstr inp vn
(U.GET vn, _ ::& (STMap _ vt, NTMap _ _ v, _) ::& _) ->
getImpl uInstr inp vt v vn
(U.GET vn, _ ::& (STBigMap _ vt, NTBigMap _ _ v, _) ::& _) ->
getImpl uInstr inp vt v vn
(U.UPDATE vn, _ ::& _ ::& (STMap _ _, _, _) ::& _) ->
updImpl uInstr inp vn
(U.UPDATE vn, _ ::& _ ::& (STBigMap _ _, _, _) ::& _) ->
updImpl uInstr inp vn
(U.UPDATE vn, _ ::& _ ::& (STSet _, _, _) ::& _) ->
updImpl uInstr inp vn
(U.IF mp mq, (STc SCBool, _, _) ::& rs) ->
genericIf IF U.IF mp mq rs rs inp
(U.LOOP is, (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 $ inp :/ LOOP subI ::: rs'
Left m -> onTypeCheckInstrErr uInstr (SomeHST inp)
"iteration expression has wrong output stack type:" (Left m)
AnyOutInstr subI ->
pure $ inp :/ LOOP subI ::: rs
(U.LOOP_LEFT is, (STOr (at :: Sing a) (bt :: Sing b), ons, ovn) ::& 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 uInstr inp "wrong LOOP_LEFT input type:" $
convergeHSTEl (bt, bn, bvn) (bt', bn', bvn')
pure $ inp :/ LOOP_LEFT subI ::: (br ::& rs')
(Left m, _) -> onTypeCheckInstrErr uInstr (SomeHST inp)
"iteration expression has wrong output stack type:" (Left m)
AnyOutInstr subI -> do
let br = (bt, bn, bvn)
pure $ inp :/ LOOP_LEFT subI ::: (br ::& rs)
(U.LAMBDA vn imt omt is, i) -> do
withUType imt $ \(it :: Sing it, ins :: Notes ins) ->
withUType omt $ \(ot :: Sing ot, ons :: Notes ons) ->
lamImpl uInstr is vn it ins ot ons i
(U.EXEC vn, ((_ :: Sing t1), _, _)
::& ( STLambda (_ :: Sing t1') t2
, NTLambda _ _ t2n
, _
)
::& rs) -> do
Refl <- onTypeCheckInstrErr uInstr (SomeHST inp)
"lambda is given argument with wrong type:" (eqType @t1 @t1')
pure $ inp :/ EXEC ::: ((t2, t2n, vn) ::& rs)
(U.APPLY vn, ((_ :: Sing a'), _, _)
::& (STLambda (STPair (sa :: Sing a) (sb :: Sing b)) sc, ln, _)
::& rs) -> do
let
l2n = case ln of
NTLambda vann (NTPair _ _ _ _ bn) cn ->
NTLambda vann bn cn
proofArgEq <- onTypeCheckInstrErr uInstr (SomeHST inp)
"lambda is given argument with wrong type:" (eqType @a' @a)
proofOp <-
maybe (onTypeCheckInstrErr uInstr (SomeHST inp)
"Operations in argument of partially applied lambda are not allowed"
$ Left $ UnsupportedTypes [demote @a])
pure (opAbsense sa)
proofBigMap <-
maybe (onTypeCheckInstrErr uInstr (SomeHST inp)
"BigMaps in argument of partially applied lambda are not allowed"
$ Left $ UnsupportedTypes [demote @a])
pure (bigMapAbsense sa)
proofContract <-
maybe (onTypeCheckInstrErr uInstr (SomeHST inp)
"Contract type in constant is not allowed"
$ Left $ UnsupportedTypes [demote @a])
pure (contractTypeAbsense sa)
case (proofArgEq, proofOp, proofBigMap, proofContract) of
(Refl, Dict, Dict, Dict) ->
pure $ inp :/ (APPLY @a) ::: ((STLambda sb sc, l2n, vn) ::& rs)
(U.DIP is, a ::& s) -> do
typeCheckDipBody uInstr is s $
\subI t -> pure $ inp :/ DIP subI ::: (a ::& t)
(U.DIPN nTotal instructions, inputHST) ->
go nTotal inputHST <&> \case
TCDipHelper s subI out -> inputHST :/ DIPN s subI ::: out
where
go :: forall inp. Typeable inp
=> Word
-> HST inp
-> TypeCheckInstr (TCDipHelper inp)
go n curHST = case (n, curHST) of
(0, _) -> typeCheckDipBody uInstr instructions curHST $ \subI t ->
pure (TCDipHelper SZ subI t)
(_, SNil) -> onTypeCheckInstrErr uInstr
(SomeHST SNil) "" (Left (NotEnoughItemsOnStack nTotal NotEnoughDip))
(_, hstHead ::& hstTail) ->
go (n - 1) hstTail <&> \case
TCDipHelper s subI out -> TCDipHelper (SS s) subI (hstHead ::& out)
(U.FAILWITH, (_ ::& _)) ->
pure $ inp :/ AnyOutInstr FAILWITH
(U.CAST vn (AsUType _ castToNotes), (e, en, evn) ::& rs) -> do
(Refl, _) <- errM $ matchTypes en castToNotes
pure $ inp :/ CAST ::: ((e, castToNotes, vn `orAnn` evn) ::& rs)
where
errM :: (MonadReader InstrCallStack m, MonadError TCError m) => Either TCTypeError a -> m a
errM = onTypeCheckInstrErr uInstr (SomeHST inp) "cast to incompatible type:"
(U.RENAME vn, (at, an, _) ::& rs) ->
pure $ inp :/ RENAME ::: ((at, an, vn) ::& rs)
(U.UNPACK tn vn mt, (STc SCBytes, _, _) ::& rs) ->
withUType mt $ \(t, tns) -> do
let ns = NTOption tn tns
proofOp <-
maybe (typeCheckInstrErr uInstr (SomeHST inp)
"Operation cannot appear in serialized data")
pure (opAbsense t)
proofBigMap <-
maybe (typeCheckInstrErr uInstr (SomeHST inp)
"BigMap cannot appear in serialized data")
pure (bigMapAbsense t)
proofContract <-
maybe (typeCheckInstrErr uInstr (SomeHST inp)
"UNPACK should not contain 'contract' type")
pure (contractTypeAbsense t)
case (proofOp, proofBigMap, proofContract) of
(Dict, Dict, Dict) ->
pure $ inp :/ UNPACK ::: ((STOption t, ns, vn) ::& rs)
(U.PACK vn, (a, _, _) ::& rs) -> do
proofOp <-
maybe (onTypeCheckInstrErr uInstr (SomeHST inp)
"Operations cannot appear in serialized data"
$ Left $ UnsupportedTypes [fromSingT a])
pure (opAbsense a)
proofBigMap <-
maybe (onTypeCheckInstrErr uInstr (SomeHST inp)
"BigMap cannot appear in serialized data"
$ Left $ UnsupportedTypes [fromSingT a])
pure (bigMapAbsense a)
case (proofOp, proofBigMap) of
(Dict, Dict) ->
pure $ inp :/ PACK ::: ((STc SCBytes, starNotes, vn) ::& rs)
(U.CONCAT vn, (STc SCBytes, _, _) ::& (STc SCBytes, _, _) ::& _) ->
concatImpl inp vn
(U.CONCAT vn, (STc SCString, _, _) ::& (STc SCString, _, _) ::& _) ->
concatImpl inp vn
(U.CONCAT vn, (STList (STc SCBytes), _, _) ::& _) ->
concatImpl' inp vn
(U.CONCAT vn, (STList (STc SCString), _, _) ::& _) ->
concatImpl' inp vn
(U.SLICE vn, (STc SCNat, _, _) ::&
(STc SCNat, _, _) ::&
(STc SCString, _, _) ::& _) -> sliceImpl inp vn
(U.SLICE vn, (STc SCNat, _, _) ::&
(STc SCNat, _, _) ::&
(STc SCBytes, _, _) ::& _) -> sliceImpl inp vn
(U.ISNAT vn', (STc SCInt, _, oldVn) ::& rs) -> do
let vn = vn' `orAnn` oldVn
pure $ inp :/ ISNAT ::: ((STOption (STc SCNat), starNotes, vn) ::& rs)
(U.ADD vn, (STc a, _, _) ::& (STc b, _, _) ::& _) -> addImpl a b inp vn
(U.SUB vn, (STc a, _, _) ::& (STc b, _, _) ::& _) -> subImpl a b inp vn
(U.MUL vn, (STc a, _, _) ::& (STc b, _, _) ::& _) -> mulImpl a b inp vn
(U.EDIV vn, (STc a, _, _) ::& (STc b, _, _) ::& _) -> edivImpl a b inp vn
(U.ABS vn, (STc SCInt, _, _) ::& _) -> unaryArithImpl @Abs ABS inp vn
(U.NEG vn, (STc SCInt, _, _) ::& _) -> unaryArithImpl @Neg NEG inp vn
(U.NEG vn, (STc SCNat, _, _) ::& _) -> unaryArithImpl @Neg NEG inp vn
(U.LSL vn, (STc SCNat, _, _) ::&
(STc SCNat, _, _) ::& _) -> arithImpl @Lsl LSL inp vn
(U.LSR vn, (STc SCNat, _, _) ::&
(STc SCNat, _, _) ::& _) -> arithImpl @Lsr LSR inp vn
(U.OR vn, (STc SCBool, _, _) ::&
(STc SCBool, _, _) ::& _) -> arithImpl @Or OR inp vn
(U.OR vn, (STc SCNat, _, _) ::&
(STc SCNat, _, _) ::& _) -> arithImpl @Or OR inp vn
(U.AND vn, (STc SCInt, _, _) ::&
(STc SCNat, _, _) ::& _) -> arithImpl @And AND inp vn
(U.AND vn, (STc SCNat, _, _) ::&
(STc SCNat, _, _) ::& _) -> arithImpl @And AND inp vn
(U.AND vn, (STc SCBool, _, _) ::&
(STc SCBool, _, _) ::& _) -> arithImpl @And AND inp vn
(U.XOR vn, (STc SCBool, _, _) ::&
(STc SCBool, _, _) ::& _) -> arithImpl @Xor XOR inp vn
(U.XOR vn, (STc SCNat, _, _) ::&
(STc SCNat, _, _) ::& _) -> arithImpl @Xor XOR inp vn
(U.NOT vn, (STc SCNat, _, _) ::& _) -> unaryArithImpl @Not NOT inp vn
(U.NOT vn, (STc SCBool, _, _) ::& _) -> unaryArithImpl @Not NOT inp vn
(U.NOT vn, (STc SCInt, _, _) ::& _) -> unaryArithImpl @Not NOT inp vn
(U.COMPARE vn,
(a :: Sing aT, an :: Notes aT, _)
::& (_ :: Sing bT, bn :: Notes bT, _)
::& rs
)
-> do
case eqType @aT @bT of
Right Refl -> do
void . errConv $ converge an bn
proof <-
maybe (onTypeCheckInstrErr (U.COMPARE vn) (SomeHST inp)
"comparison is given incomparable arguments"
$ Left $ UnsupportedTypes [demote @aT, demote @bT])
pure (comparabilityPresence a)
case proof of
Dict -> do
pure $ inp :/ COMPARE ::: ((sing, starNotes, vn) ::& rs)
Left err -> do
typeCheckInstrErr' uInstr (SomeHST inp) "comparing different types:" err
where
errConv :: (MonadReader InstrCallStack m, MonadError TCError m) => Either AnnConvergeError a -> m a
errConv = onTypeCheckInstrAnnErr uInstr inp "comparing types with different annotations:"
(U.EQ vn, (STc SCInt, _, _) ::& _) -> unaryArithImpl @Eq' EQ inp vn
(U.NEQ vn, (STc SCInt, _, _) ::& _) -> unaryArithImpl @Neq NEQ inp vn
(U.LT vn, (STc SCInt, _, _) ::& _) -> unaryArithImpl @Lt LT inp vn
(U.GT vn, (STc SCInt, _, _) ::& _) -> unaryArithImpl @Gt GT inp vn
(U.LE vn, (STc SCInt, _, _) ::& _) -> unaryArithImpl @Le LE inp vn
(U.GE vn, (STc SCInt, _, _) ::& _) -> unaryArithImpl @Ge GE inp vn
(U.INT vn, (STc SCNat, _, _) ::& rs) ->
pure $ inp :/ INT ::: ((STc SCInt, starNotes, vn) ::& rs)
(U.SELF vn fn, _) -> do
cpType <- gets tcContractParam
let t = fromUType cpType
withUType cpType $ \(singcp :: Sing cp, (ParamNotesUnsafe -> notescp)) -> do
proofOp <-
maybe (onTypeCheckInstrErr uInstr (SomeHST inp)
"contract param type cannot contain operation"
$ Left $ UnsupportedTypes [t])
pure (opAbsense singcp)
proofBigMap <-
maybe (onTypeCheckInstrErr uInstr (SomeHST inp)
"contract param type cannot contain nested big_map"
$ Left $ UnsupportedTypes [t])
pure (nestedBigMapsAbsense singcp)
case (proofOp, proofBigMap) of
(Dict, Dict) -> do
epName <- onTypeCheckInstrErr uInstr (SomeHST inp) "Bad annotation:" $
epNameFromRefAnn fn `onLeft` IllegalEntryPoint
MkEntryPointCallRes (argNotes :: Notes arg) epc <-
mkEntryPointCall epName (singcp, notescp)
& maybeToRight (EntryPointNotFound epName)
& onTypeCheckInstrErr uInstr (SomeHST inp) "entrypoint not found"
let ntRes = NTContract U.noAnn argNotes
pure $ inp :/ SELF @arg (SomeEpc epc)
::: ((sing @('TContract arg), ntRes, vn) ::& inp)
(U.CONTRACT vn fn mt, (STc SCAddress, _, _) ::& rs) ->
withUType mt $ \(t :: Sing t, tns :: Notes t) -> do
proofOp <-
maybe (onTypeCheckInstrErr uInstr (SomeHST inp)
"contract param type cannot contain operation"
$ Left $ UnsupportedTypes [fromUType mt])
pure (opAbsense t)
proofBigMap <-
maybe (onTypeCheckInstrErr uInstr (SomeHST inp)
"contract param type cannot contain nested big_map"
$ Left $ UnsupportedTypes [fromUType mt])
pure (nestedBigMapsAbsense t)
let ns = NTOption def $ NTContract def tns
epName <- onTypeCheckInstrErr uInstr (SomeHST inp) "Bad annotation:" $
epNameFromRefAnn fn `onLeft` IllegalEntryPoint
case (proofOp, proofBigMap) of
(Dict, Dict) ->
pure $ inp :/ CONTRACT tns epName ::: ((STOption $ STContract t, ns, vn) ::& rs)
(U.TRANSFER_TOKENS vn, ((_ :: Sing p'), _, _)
::& (STc SCMutez, _, _) ::& (STContract (p :: Sing p), _, _) ::& rs) -> do
proofOp <-
maybe (onTypeCheckInstrErr uInstr (SomeHST inp)
"contract param type cannot contain operation"
$ Left $ UnsupportedTypes [demote @p])
pure (opAbsense p)
proofBigMap <-
maybe (onTypeCheckInstrErr uInstr (SomeHST inp)
"contract param type cannot contain big_map"
$ Left $ UnsupportedTypes [demote @p])
pure (nestedBigMapsAbsense p)
case (eqType @p @p', proofOp, proofBigMap) of
(Right Refl, Dict, Dict) ->
pure $ inp :/ TRANSFER_TOKENS ::: ((STOperation, starNotes, vn) ::& rs)
(Left m, _, _) ->
onTypeCheckInstrErr uInstr (SomeHST inp)
"mismatch of contract param type:" (Left m)
(U.SET_DELEGATE vn, (STOption (STc SCKeyHash), _, _) ::& rs) -> do
pure $ inp :/ SET_DELEGATE ::: ((STOperation, starNotes, vn) ::& rs)
(U.CREATE_CONTRACT ovn avn contract,
(STOption (STc SCKeyHash), _, _)
::& (STc SCMutez, _, _)
::& ((_ :: Sing g), gn, _) ::& rs) -> do
(SomeContract (FullContract (contr :: Contract p' g') paramNotes storeNotes))
<- lift $ typeCheckContractImpl contract
Refl <- checkEqT @g @g' uInstr inp "contract storage type mismatch"
void $ onTypeCheckInstrAnnErr uInstr inp "contract storage type mismatch" (converge gn storeNotes)
pure $ inp :/ CREATE_CONTRACT (FullContract contr paramNotes storeNotes) :::
((STOperation, starNotes, ovn) ::& (STc SCAddress, starNotes, avn) ::& rs)
(U.IMPLICIT_ACCOUNT vn, (STc SCKeyHash, _, _) ::& rs) ->
pure $ inp :/ IMPLICIT_ACCOUNT ::: ((STContract STUnit, starNotes, vn) ::& rs)
(U.NOW vn, _) ->
pure $ inp :/ NOW ::: ((STc SCTimestamp, starNotes, vn) ::& inp)
(U.AMOUNT vn, _) ->
pure $ inp :/ AMOUNT ::: ((STc SCMutez, starNotes, vn) ::& inp)
(U.BALANCE vn, _) ->
pure $ inp :/ BALANCE ::: ((STc SCMutez, starNotes, vn) ::& inp)
(U.CHECK_SIGNATURE vn,
(STKey, _, _)
::& (STSignature, _, _) ::& (STc SCBytes, _, _) ::& rs) ->
pure $ inp :/ CHECK_SIGNATURE ::: ((STc SCBool, starNotes, vn) ::& rs)
(U.SHA256 vn, (STc SCBytes, _, _) ::& rs) ->
pure $ inp :/ SHA256 ::: ((STc SCBytes, starNotes, vn) ::& rs)
(U.SHA512 vn, (STc SCBytes, _, _) ::& rs) ->
pure $ inp :/ SHA512 ::: ((STc SCBytes, starNotes, vn) ::& rs)
(U.BLAKE2B vn, (STc SCBytes, _, _) ::& rs) ->
pure $ inp :/ BLAKE2B ::: ((STc SCBytes, starNotes, vn) ::& rs)
(U.HASH_KEY vn, (STKey, _, _) ::& rs) ->
pure $ inp :/ HASH_KEY ::: ((STc SCKeyHash, starNotes, vn) ::& rs)
(U.STEPS_TO_QUOTA vn, _) ->
pure $ inp :/ STEPS_TO_QUOTA ::: ((STc SCNat, starNotes, vn) ::& inp)
(U.SOURCE vn, _) ->
pure $ inp :/ SOURCE ::: ((STc SCAddress, starNotes, vn) ::& inp)
(U.SENDER vn, _) ->
pure $ inp :/ SENDER ::: ((STc SCAddress, starNotes, vn) ::& inp)
(U.ADDRESS vn, (STContract _, _, _) ::& rs) ->
pure $ inp :/ ADDRESS ::: ((STc SCAddress, starNotes, vn) ::& rs)
(U.CHAIN_ID vn, _) ->
pure $ inp :/ CHAIN_ID ::: ((STChainId, starNotes, vn) ::& inp)
_ ->
typeCheckInstrErr uInstr (SomeHST inp) "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 = 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 $ RfNormal lam) ::: lamSt onsr)
Left m -> onTypeCheckInstrErr instr (SomeHST i)
"wrong output type of lambda's expression:" (Left m)
AnyOutInstr lam ->
pure (LAMBDA (VLam $ RfAlwaysFails lam) ::: lamSt ons)
where
hasSelf :: U.ExpandedOp -> Bool
hasSelf = everything (||)
(mkQ False
(\case
(U.SELF{} :: U.InstrAbstract U.ExpandedOp) -> True
_ -> False
)
)
data TCDipHelper inp where
TCDipHelper ::
forall (n :: Peano) inp out s s'.
(Typeable out, ConstraintDIPN n inp out s s') =>
Sing n -> Instr s s' -> HST out -> TCDipHelper inp
typeCheckDipBody ::
forall inp r. Typeable inp
=> U.ExpandedInstr
-> [U.ExpandedOp]
-> HST inp
-> (forall out. Typeable out =>
Instr inp out -> HST out -> TypeCheckInstr r)
-> TypeCheckInstr r
typeCheckDipBody mainInstr instructions inputHST callback = do
_ :/ tp <- lift (typeCheckList instructions inputHST)
case tp of
AnyOutInstr _ ->
typeCheckInstrErr mainInstr (SomeHST inputHST)
"Code within DIP instruction always fails, which is not allowed"
subI ::: t -> callback subI t