diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,3 +1,24 @@ +1.8.0 +===== + +* [!610](https://gitlab.com/morley-framework/morley/-/merge_requests/610) + Remove `Arbitrary` instances and everything else that depends on `QuickCheck`. +* [!616](https://gitlab.com/morley-framework/morley/-/merge_requests/616) + Make `RootAnn` a mere type alias of `FieldAnn`. +* [!615](https://gitlab.com/morley-framework/morley/-/merge_requests/615) + Make `mkEntrypointsMap` accept `ParameterType` instead of `Type`. +* [!567](https://gitlab.com/morley-framework/morley/-/merge_requests/567) + Add `DConversionInfo` that describes Haskell <-> Michelson conversion + mechanism. +* [!585](https://gitlab.com/morley-framework/morley/-/merge_requests/585) + Add `Exception` instance for `ParseChainIdError`. +* [!598](https://gitlab.com/morley-framework/morley/-/merge_requests/598) + Fix bug: correct processing of `EDIV` of negative `Integer` and `Natural`. +* [!574](https://gitlab.com/morley-framework/morley/-/merge_requests/574) + Implement a verbose switch for `morley typecheck`. It allows to + print a stack type after every well-typed instruction, even if a + contract as a whole is ill-typed. + 1.7.1 ===== * [!549](https://gitlab.com/morley-framework/morley/-/merge_requests/549) diff --git a/app/Main.hs b/app/Main.hs --- a/app/Main.hs +++ b/app/Main.hs @@ -6,6 +6,7 @@ ( main ) where +import Data.Default (def) import qualified Data.Text.Lazy.IO.Utf8 as Utf8 (writeFile) import Data.Version (showVersion) import Fmt (pretty) @@ -26,7 +27,7 @@ import Michelson.Runtime (TxData(..), originateContract, prepareContract, readAndParseContract, runContract, transfer) import Michelson.Runtime.GState (genesisAddress) -import Michelson.TypeCheck (typeCheckContract) +import Michelson.TypeCheck (tcVerbose, typeCheckContract) import Michelson.TypeCheck.Types (SomeContract(..), mapSomeContract) import Michelson.Typed (Contract(..)) import qualified Michelson.Untyped as U @@ -287,17 +288,21 @@ write $ printUntypedContract forceSingleLine contract Optimize OptimizeOptions{..} -> do untypedContract <- prepareContract optoContractFile - checkedContract <- either throwM pure $ typeCheckContract untypedContract + checkedContract <- + either throwM pure $ typeCheckContract untypedContract def let optimizedContract = mapSomeContract optimize checkedContract let write = maybe putStrLn Utf8.writeFile optoOutput write $ printSomeContract optoSingleLine optimizedContract Analyze AnalyzeOptions{..} -> do untypedContract <- prepareContract aoContractFile - SomeContract contract <- either throwM pure $ typeCheckContract untypedContract + SomeContract contract <- + either throwM pure $ typeCheckContract untypedContract def putTextLn $ pretty $ analyze (cCode contract) TypeCheck TypeCheckOptions{..} -> do morleyContract <- prepareContract tcoContractFile - either throwM (const pass) $ typeCheckContract morleyContract + contract <- either throwM pure + $ typeCheckContract morleyContract def{ tcVerbose = tcoVerbose } + when tcoVerbose (putStrLn $ printSomeContract False contract) putTextLn "Contract is well-typed" Run RunOptions {..} -> do michelsonContract <- prepareContract roContractFile diff --git a/app/REPL.hs b/app/REPL.hs --- a/app/REPL.hs +++ b/app/REPL.hs @@ -230,7 +230,7 @@ T.Dict -> case T.checkOpPresence (T.sing @a) of T.OpAbsent -> -- print nice if value has no operations addSuffix (toText $ printTypedValue True v) - T.OpPresent -> -- else just call show, and indicate value has operation inside + _ -> -- else just call show, and indicate value has operation inside case (v, T.sing @a) of (T.VList [], T.STList T.STOperation) -> "{ } :: list operation\n" <> showStack rst rHst _ -> addSuffix $ "(operations container:" <> show v <> ")" diff --git a/docs/language/morleyInstructions.md b/docs/language/morleyInstructions.md --- a/docs/language/morleyInstructions.md +++ b/docs/language/morleyInstructions.md @@ -71,6 +71,6 @@ PUSH int 2; PUSH int 10; TEST_ASSERT Test1 "%[0] + %[1] > 10" {ADD; PUSH int 10; COMPARE;LT;}; - DROP; UNIT; NIL operation; PAIR; }; + DROP; DROP; UNIT; NIL operation; PAIR; }; ``` diff --git a/docs/morleyTypechecker.md b/docs/morleyTypechecker.md --- a/docs/morleyTypechecker.md +++ b/docs/morleyTypechecker.md @@ -6,26 +6,43 @@ # Morley Typechecker -In Morley, we have a typechecker for the core Michelson language, i. e. without macros. -It is located in `Michelson.TypeCheck` and designed in the following way: -* It takes a core Michelson contract extended with `EXT` instruction to support additional instructions described in the [`morleyInstructions.md`](language/morleyInstructions.md) document. -* The contract passed to the typechecker uses [untyped representation](./michelsonTypes.md). -* During typechecking, we verify that instructions are well-typed and provide evidence to the compiler that allows us to convert instructions into [typed representation](./michelsonTypes.md). If the contract is ill-typed, the typechecking process fails with an error. -* The typechecker can check a whole contract or a standalone value (for example, a lambda). -In the former case it needs to know the parameter type of the contract (to check `SELF`). +In Morley, we have a typechecker for the core Michelson language, +i. e. without macros. It is located in `Michelson.TypeCheck` and +designed in the following way: +* It takes a core Michelson contract extended with `EXT` instruction + to support additional instructions described in the + [`morleyInstructions.md`](language/morleyInstructions.md) document. +* The contract passed to the typechecker uses [untyped + representation](./michelsonTypes.md). +* During typechecking, we verify that instructions are well-typed and + provide evidence to the compiler that allows us to convert + instructions into [typed representation](./michelsonTypes.md). If + the contract is ill-typed, the typechecking process fails with an + error. +* The typechecker can check a whole contract or a standalone value +(for example, a lambda). In the former case it needs to know the +parameter type of the contract (to check `SELF`). ## CLI End users can use the `typecheck` command to execute the typechecker. -It parses the contract, performs macro expansion, and passes it to the typechecker which says that the contract is well-typed or produces an error message. +It parses the contract, performs macro expansion, and passes it to the +typechecker which says that the contract is well-typed or produces an +error message. Additionally, one can specify a `--verbose` option to +print stack types between instructions which is useful for debugging. -Example: `morley typecheck --contract auction.tz`. +Example: `morley typecheck --contract auction.tz --verbose`. ## Internals -An internal structure of the typechecker is pretty well described in Haddock comments. -Two main modules are: -* [`Michelson.TypeCheck.Value`](/code/morley/src/Michelson/TypeCheck/Value.hs) contains logic for checking Michelson values. -* [`Michelson.TypeCheck.Instr`](/code/morley/src/Michelson/TypeCheck/Instr.hs) contains logic for checking Michelson instructions and the whole contract. +An internal structure of the typechecker is pretty well described in +Haddock comments. Two main modules are: +* [`Michelson.TypeCheck.Value`](/code/morley/src/Michelson/TypeCheck/Value.hs) + contains logic for checking Michelson values. +* [`Michelson.TypeCheck.Instr`](/code/morley/src/Michelson/TypeCheck/Instr.hs) + contains logic for checking Michelson instructions and the whole + contract. -Their functionality is re-exported from the [`Michelson.TypeCheck`](/code/morley/src/Michelson/TypeCheck.hs) module along with some auxiliary types and functions. +Their functionality is re-exported from the +[`Michelson.TypeCheck`](/code/morley/src/Michelson/TypeCheck.hs) +module along with some auxiliary types and functions. diff --git a/morley.cabal b/morley.cabal --- a/morley.cabal +++ b/morley.cabal @@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack name: morley -version: 1.7.1 +version: 1.8.0 synopsis: Developer tools for the Michelson Language description: A library to make writing smart contracts in Michelson — the smart contract language of the Tezos blockchain — pleasant and effective. category: Language @@ -73,6 +73,8 @@ Michelson.TypeCheck.Helpers Michelson.TypeCheck.Instr Michelson.TypeCheck.TypeCheck + Michelson.TypeCheck.TypeCheckedOp + Michelson.TypeCheck.TypeCheckedSeq Michelson.TypeCheck.Types Michelson.TypeCheck.Value Michelson.Typed @@ -138,9 +140,9 @@ Util.Lens Util.Markdown Util.Named + Util.Num Util.Peano Util.Positive - Util.Test.Arbitrary Util.Text Util.TH Util.Type @@ -157,8 +159,7 @@ default-extensions: AllowAmbiguousTypes ApplicativeDo BangPatterns BlockArguments ConstraintKinds DataKinds DefaultSignatures DeriveAnyClass DeriveDataTypeable DeriveFoldable DeriveFunctor DeriveGeneric DeriveTraversable DerivingStrategies DerivingVia EmptyCase FlexibleContexts FlexibleInstances GADTs GeneralizedNewtypeDeriving LambdaCase MultiParamTypeClasses MultiWayIf NamedFieldPuns NegativeLiterals NumDecimals OverloadedLabels OverloadedStrings PatternSynonyms PolyKinds QuasiQuotes RankNTypes RecordWildCards RecursiveDo ScopedTypeVariables StandaloneDeriving StrictData TemplateHaskell TupleSections TypeApplications TypeFamilies TypeOperators UndecidableInstances UndecidableSuperClasses ViewPatterns ghc-options: -Weverything -Wno-missing-exported-signatures -Wno-missing-import-lists -Wno-missed-specialisations -Wno-all-missed-specialisations -Wno-unsafe -Wno-safe -Wno-missing-local-signatures -Wno-monomorphism-restriction -Wno-implicit-prelude build-depends: - QuickCheck - , aeson + aeson , aeson-casing , aeson-pretty , base >=4.7 && <5 @@ -183,8 +184,6 @@ , named , optparse-applicative , parser-combinators >=1.0.0 - , quickcheck-arbitrary-adt - , quickcheck-instances , semigroups >=0.19.1 , show-type , singletons @@ -220,6 +219,7 @@ aeson , base >=4.7 && <5 , bytestring + , data-default , fmt , haskeline , megaparsec >=7.0.0 diff --git a/src/Michelson/Doc.hs b/src/Michelson/Doc.hs --- a/src/Michelson/Doc.hs +++ b/src/Michelson/Doc.hs @@ -47,6 +47,7 @@ , DComment (..) , DAnchor (..) , DToc (..) + , DConversionInfo (..) ) where import Control.Lens.Cons (_head) @@ -665,3 +666,34 @@ docItemPos = 4 docItemSectionName = Nothing docItemToMarkdown _ (DAnchor a) = mdAnchor a + +data DConversionInfo = DConversionInfo + +-- TODO: we should also recommend using morley-client when +-- it'll become good enough +instance DocItem DConversionInfo where + docItemPos = 15 + docItemSectionName = Just "Haskell ⇄ Michelson conversion" + docItemToMarkdown _ _ = + "This smart contract is developed in Haskell using the \ + \[Morley framework](https://gitlab.com/morley-framework/morley). \ + \Documentation mentions Haskell types that can be used for interaction with \ + \this contract from Haskell, but for each Haskell type we also mention its \ + \Michelson representation to make interactions outside of Haskell possible.\n\n\ + \There are multiple ways to interact with this contract:\n\n\ + \* Use this contract in your Haskell application, thus all operation submission\ + \should be handled separately, e.g. via calling `tezos-client`, which will communicate \ + \with the `tezos-node`. In order to be able to call `tezos-client` you'll need to be able \ + \to construct Michelson values from Haskell.\n\n\ + \ The easiest way to do that is to serialize Haskell value using `lPackValue` function \ + \from [`Lorentz.Pack`](https://gitlab.com/morley-framework/morley/-/blob/2441e26bebd22ac4b30948e8facbb698d3b25c6d/code/lorentz/src/Lorentz/Pack.hs) \ + \module, encode resulting bytestring to hexadecimal representation using `encodeHex` function. \ + \Resulting hexadecimal encoded bytes sequence can be decoded back to Michelson value via \ + \`tezos-client unpack michelson data`.\n\n\ + \ Reverse conversion from Michelson value to the \ + \Haskell value can be done by serializing Michelson value using `tezos-client hash data` command, \ + \resulting `Raw packed data` should be decoded from the hexadecimal representation using `decodeHex` \ + \and deserialized to the Haskell value via `lUnpackValue` function from \ + \[`Lorentz.Pack`](https://gitlab.com/morley-framework/morley/-/blob/2441e26bebd22ac4b30948e8facbb698d3b25c6d/code/lorentz/src/Lorentz/Pack.hs).\n\n\ + \* Contruct values for this contract directly on Michelson level using types provided in the \ + \documentation." diff --git a/src/Michelson/ErrorPos.hs b/src/Michelson/ErrorPos.hs --- a/src/Michelson/ErrorPos.hs +++ b/src/Michelson/ErrorPos.hs @@ -4,6 +4,7 @@ module Michelson.ErrorPos ( mkPos + , unsafeMkPos , Pos (..) , SrcPos (..) , srcPos @@ -16,22 +17,33 @@ import Data.Data (Data(..)) import Data.Default (Default(..)) import qualified Data.Text as T -import Fmt (Buildable) +import Fmt (Buildable (..)) import Util.Aeson -newtype Pos = Pos Word +newtype Pos = Pos {unPos :: Word} deriving stock (Eq, Ord, Show, Generic, Data) instance NFData Pos -mkPos :: Int -> Pos -mkPos x +unsafeMkPos :: Int -> Pos +unsafeMkPos x | x < 0 = error $ "negative pos: " <> show x | otherwise = Pos $ fromIntegral x -data SrcPos = SrcPos Pos Pos - deriving stock (Eq, Ord, Show, Generic, Data) +mkPos :: Int -> Maybe Pos +mkPos x + | x < 0 = Nothing + | otherwise = Just $ Pos $ fromIntegral x + +data SrcPos = + SrcPos + { srcLine :: Pos + , srcCol :: Pos + } deriving stock (Eq, Ord, Show, Generic, Data) + +instance Buildable SrcPos where + build (SrcPos (Pos l) (Pos c)) = build l <> ":" <> build c instance NFData SrcPos diff --git a/src/Michelson/FailPattern.hs b/src/Michelson/FailPattern.hs --- a/src/Michelson/FailPattern.hs +++ b/src/Michelson/FailPattern.hs @@ -2,6 +2,12 @@ -- -- SPDX-License-Identifier: LicenseRef-MIT-TQ +-- NOTE this pragmas. +-- We disable some wargnings for the sake of speed up. +-- Write code with care. +{-# OPTIONS_GHC -Wno-incomplete-patterns #-} +{-# OPTIONS_GHC -Wno-overlapping-patterns #-} + -- | Typical usages of FAILWITH instruction. module Michelson.FailPattern @@ -45,25 +51,22 @@ -- passed to other instructions. -- -- The instruction MUST be linearized to the left (see 'linearizeLeft'). --- --- *IMPORTANT* be careful if you want to rewrite this function. --- It took GHC about 30 seconds to compile this function previously. --- The clause @isTypicalPreFailWith (Seq x PAIR) = ..@ is crucial, so please --- don't move these two case branches in this clause outside of it: --- either in different patten matching or in case or \case clause, --- I usually experienced a regression for any of these options. isTypicalFailWith :: Instr inp out -> Maybe TypicalFailWith -isTypicalFailWith (Seq i1 FAILWITH) = isTypicalPreFailWith i1 +isTypicalFailWith = \case + Seq i1 FAILWITH -> isTypicalPreFailWith i1 + _ -> Nothing where - isTypicalPreFailWith :: Instr inp (a ': out) -> Maybe TypicalFailWith - isTypicalPreFailWith (Seq x PAIR) = case x of - Seq _ (PUSH v) -> FailWithStackValue <$> isStringValue v - PUSH v -> FailWithStackValue <$> isStringValue v - _ -> Nothing - isTypicalPreFailWith (Seq _ (PUSH v)) = isTypicalErrorConstant v - isTypicalPreFailWith (PUSH v) = isTypicalErrorConstant v - isTypicalPreFailWith _ = Nothing -isTypicalFailWith _ = Nothing + isTypicalPreFailWith :: + Instr inp (a ': out) -> Maybe TypicalFailWith + isTypicalPreFailWith = + \case + PUSH v -> isTypicalErrorConstant v + Seq _ (PUSH v) -> isTypicalErrorConstant v + + Seq (PUSH v) PAIR -> FailWithStackValue <$> isStringValue v + Seq (Seq _ (PUSH v)) PAIR -> FailWithStackValue <$> isStringValue v + + _ -> Nothing isTypicalErrorConstant :: forall t. ConstantScope t => Value t -> Maybe TypicalFailWith diff --git a/src/Michelson/Interpret/Pack.hs b/src/Michelson/Interpret/Pack.hs --- a/src/Michelson/Interpret/Pack.hs +++ b/src/Michelson/Interpret/Pack.hs @@ -34,7 +34,7 @@ import Michelson.Text import Michelson.Typed import Michelson.Untyped.Annotation - (Annotation(..), FieldAnn, TypeAnn, VarAnn, convAnn, fullAnnSet, isNoAnnSet, noAnn) + (Annotation(..), FieldAnn, TypeAnn, VarAnn, fullAnnSet, isNoAnnSet, noAnn) import Tezos.Address (Address(..), ContractHash(..)) import Tezos.Core (ChainId(..), Mutez(..), timestampToSeconds) import Tezos.Crypto (KeyHash(..), KeyHashTag(..), PublicKey(..), signatureToBytes) @@ -461,7 +461,7 @@ encodeParamNotes' :: forall (t :: T). SingI t => ParamNotes t -> LByteString -encodeParamNotes' ParamNotesUnsafe{..} = encodeNotedST (sing @t) (convAnn pnRootAnn) pnNotes +encodeParamNotes' ParamNotesUnsafe{..} = encodeNotedST (sing @t) pnRootAnn pnNotes -- Note: to encode field annotations we have to accept them as an additional -- parameter because they are stored in the parent's `Notes t`, e.g. see STPair. diff --git a/src/Michelson/Interpret/Unpack.hs b/src/Michelson/Interpret/Unpack.hs --- a/src/Michelson/Interpret/Unpack.hs +++ b/src/Michelson/Interpret/Unpack.hs @@ -57,6 +57,7 @@ import Tezos.Core import Tezos.Crypto import Util.Binary +import Util.Num ---------------------------------------------------------------------------- -- Helpers @@ -279,10 +280,9 @@ -- One more reason to go with just 'Int' for now is that we need to be able to -- deserialize byte arrays, and 'BS.ByteString' keeps length of type 'Int' -- inside. - let len' = fromIntegral @_ @Int len - unless (fromIntegral len' == len && len' >= 0) $ - fail "Length overflow" - return len' + fromIntegralChecked len + & either (fail . toString) pure + ? "Length" decodeAsListRaw :: Get a -> Get a decodeAsListRaw getElems = do @@ -375,7 +375,7 @@ => [ExpandedOp] -> m (RemFail T.Instr '[inp] '[out]) decodeTypeCheckLam uinstr = - either tcErrToFail pure . evaluatingState tcInitEnv . runExceptT $ do + either tcErrToFail pure . run $ do let inp = (starNotes, Dict, noAnn) ::& SNil _ :/ instr' <- typeCheckList uinstr inp case instr' of @@ -394,6 +394,7 @@ AnyOutInstr instr -> return $ RfAlwaysFails instr where + run = evaluatingState tcInitEnv . runExceptT . usingReaderT def tcErrToFail err = fail $ "Type check failed: " +| err |+ "" tcInitEnv = TypeCheckEnv @@ -627,7 +628,7 @@ expectTag "Pre contract parameter" 0x05 expectTag "Contract parameter" 0x00 (t, ta, root) <- decodeTWithAnns - pure $ ParameterType (Type t ta) (convAnn root) + pure $ ParameterType (Type t ta) root decodeStorageBlock = CBStorage <$> do expectTag "Pre contract storage" 0x05 expectTag "Contract storage" 0x01 diff --git a/src/Michelson/OpSize.hs b/src/Michelson/OpSize.hs --- a/src/Michelson/OpSize.hs +++ b/src/Michelson/OpSize.hs @@ -156,7 +156,7 @@ contractOpSize :: Contract -> OpSize contractOpSize (Contract (ParameterType cp rootAnn) st is _) = - OpSize 16 <> typeOpSize' [convAnn rootAnn] cp <> typeOpSize st <> expandedInstrsOpSize is + OpSize 16 <> typeOpSize' [rootAnn] cp <> typeOpSize st <> expandedInstrsOpSize is numOpSize :: Integral i => i -> OpSize numOpSize = OpSize . fromIntegral . length . encodeIntPayload . fromIntegral diff --git a/src/Michelson/Optimizer.hs b/src/Michelson/Optimizer.hs --- a/src/Michelson/Optimizer.hs +++ b/src/Michelson/Optimizer.hs @@ -2,6 +2,12 @@ -- -- SPDX-License-Identifier: LicenseRef-MIT-TQ +-- NOTE this pragmas. +-- We disable some wargnings for the sake of speed up. +-- Write code with care. +{-# OPTIONS_GHC -Wno-incomplete-patterns #-} +{-# OPTIONS_GHC -Wno-overlapping-patterns #-} + -- | Optimizer for typed instructions. -- -- It's quite experimental and incomplete. diff --git a/src/Michelson/Parser.hs b/src/Michelson/Parser.hs --- a/src/Michelson/Parser.hs +++ b/src/Michelson/Parser.hs @@ -35,6 +35,7 @@ -- * Quoters , utypeQ + , uparamTypeQ -- * Re-exports , errorBundlePretty @@ -42,12 +43,14 @@ import Prelude hiding (try) +import qualified Language.Haskell.TH.Lift as TH import qualified Language.Haskell.TH.Quote as TH -import Text.Megaparsec (Parsec, choice, customFailure, eitherP, eof, errorBundlePretty, - getSourcePos, lookAhead, parse, try) +import Text.Megaparsec + (Parsec, choice, customFailure, eitherP, eof, errorBundlePretty, getSourcePos, lookAhead, parse, + try) import Text.Megaparsec.Pos (SourcePos(..), unPos) -import Michelson.ErrorPos (SrcPos(..), mkPos) +import Michelson.ErrorPos (SrcPos(..), unsafeMkPos) import Michelson.Macro (LetMacro, Macro(..), ParsedInstr, ParsedOp(..), ParsedValue, expandValue) import Michelson.Parser.Annotations (noteF) import Michelson.Parser.Error @@ -92,8 +95,10 @@ local (const env) contract cbParameter :: Parser ParameterType -cbParameter = do - symbol "parameter" +cbParameter = symbol "parameter" *> cbParameterBare + +cbParameterBare :: Parser ParameterType +cbParameterBare = do prefixRootAnn <- optional noteF (inTypeRootAnn, t) <- field rootAnn <- case (prefixRootAnn, inTypeRootAnn) of @@ -103,7 +108,7 @@ (Just a, "") -> pure a (Nothing, b) -> pure b (Just _, _) -> customFailure MultiRootAnnotationException - pure $ ParameterType t (convAnn rootAnn) + pure $ ParameterType t rootAnn cbStorage :: Parser Type cbStorage = symbol "storage" *> type_ @@ -219,7 +224,7 @@ let l = unPos $ sourceLine sp let c = unPos $ sourceColumn sp -- reindexing starting from 0 - pure $ SrcPos (mkPos $ l - 1) (mkPos $ c - 1) + pure $ SrcPos (unsafeMkPos $ l - 1) (unsafeMkPos $ c - 1) primWithPos :: Parser ParsedInstr -> Parser ParsedOp primWithPos act = do @@ -260,17 +265,25 @@ -- Safe construction of Haskell values ------------------------------------------------------------------------------- --- | Creates 'U.Type' by its Morley representation. --- --- >>> [utypeQ| (int :a | nat :b) |] --- Type (TOr % % (Type (Tc CInt) :a) (Type (Tc CNat) :b)) : -utypeQ :: TH.QuasiQuoter -utypeQ = TH.QuasiQuoter +parserToQuasiQuoter :: TH.Lift a => Parser a -> TH.QuasiQuoter +parserToQuasiQuoter parser = TH.QuasiQuoter { TH.quoteExp = \s -> - case parseNoEnv (mSpace *> type_) "QuasiQuoter" (toText s) of + case parseNoEnv (mSpace *> parser) "QuasiQuoter" (toText s) of Left err -> fail $ errorBundlePretty err Right res -> [e| res |] , TH.quotePat = \_ -> fail "Cannot be used as pattern" , TH.quoteType = \_ -> fail "Cannot be used as type" , TH.quoteDec = \_ -> fail "Cannot be used as declaration" } + + +-- | Creates 'U.Type' by its Morley representation. +-- +-- >>> [utypeQ| (int :a | nat :b) |] +-- Type (TOr % % (Type (Tc CInt) :a) (Type (Tc CNat) :b)) : +utypeQ :: TH.QuasiQuoter +utypeQ = parserToQuasiQuoter type_ + +-- | Creates 'U.ParameterType' by its Morley representation. +uparamTypeQ :: TH.QuasiQuoter +uparamTypeQ = parserToQuasiQuoter cbParameterBare diff --git a/src/Michelson/Printer/Util.hs b/src/Michelson/Printer/Util.hs --- a/src/Michelson/Printer/Util.hs +++ b/src/Michelson/Printer/Util.hs @@ -10,6 +10,7 @@ , printDocS , renderOps , renderOpsList + , renderOpsListNoBraces , spaces , wrapInParens , buildRenderDoc @@ -81,10 +82,12 @@ renderOpsList :: (RenderDoc op) => Bool -> [op] -> Doc renderOpsList oneLine ops = - braces $ - enclose space space $ - cat' $ punctuate semi $ - renderDoc doesntNeedParens <$> filter isRenderable ops + braces $ enclose space space $ renderOpsListNoBraces oneLine ops + +renderOpsListNoBraces :: RenderDoc op => Bool -> [op] -> Doc +renderOpsListNoBraces oneLine ops = + cat' $ punctuate semi $ + renderDoc doesntNeedParens <$> filter isRenderable ops where cat' = if oneLine then maybe "" spacecat . nonEmpty else align . vcat diff --git a/src/Michelson/Text.hs b/src/Michelson/Text.hs --- a/src/Michelson/Text.hs +++ b/src/Michelson/Text.hs @@ -44,7 +44,6 @@ import Fmt (Buildable) import qualified Language.Haskell.TH as TH import qualified Language.Haskell.TH.Quote as TH -import Test.QuickCheck (Arbitrary(..), choose, listOf) import Util.CLI import Util.Label (Label(..), labelToText) @@ -129,11 +128,6 @@ instance ToText MText where toText = unMText - -instance Arbitrary MText where - arbitrary = - mkMTextUnsafe . toText <$> - listOf (choose @Char (toEnum minBoundMChar, toEnum maxBoundMChar)) instance ToJSON MText where toJSON = toJSON . unMText diff --git a/src/Michelson/TypeCheck.hs b/src/Michelson/TypeCheck.hs --- a/src/Michelson/TypeCheck.hs +++ b/src/Michelson/TypeCheck.hs @@ -5,13 +5,15 @@ module Michelson.TypeCheck ( typeCheckContract , typeCheckContractAndStorage - , typeCheckStorage + , typeCheckExt + , typeCheckInstr + , typeCheckList + , typeCheckListNoExcept , typeCheckParameter - , typeVerifyStorage - , typeVerifyParameter + , typeCheckStorage , typeCheckValue - , typeCheckList - , typeCheckExt + , typeVerifyParameter + , typeVerifyStorage , module E , module M , module T diff --git a/src/Michelson/TypeCheck/Error.hs b/src/Michelson/TypeCheck/Error.hs --- a/src/Michelson/TypeCheck/Error.hs +++ b/src/Michelson/TypeCheck/Error.hs @@ -17,6 +17,8 @@ import qualified Text.Show (show) import Michelson.ErrorPos (InstrCallStack(..), Pos(..), SrcPos(..)) +import Michelson.Printer.Util (doesntNeedParens, printDocB, renderDoc) +import Michelson.TypeCheck.TypeCheckedOp (TypeCheckedOp) import Michelson.TypeCheck.Types (SomeHST(..)) import qualified Michelson.Typed as T import Michelson.Typed.Annotation (AnnConvergeError(..)) @@ -242,6 +244,7 @@ | TCContractError Text (Maybe TCTypeError) | TCUnreachableCode InstrCallStack (NonEmpty U.ExpandedOp) | TCExtError SomeHST InstrCallStack ExtError + | TCIncompletelyTyped TCError (U.Contract' TypeCheckedOp) deriving stock (Eq, Generic) instance NFData TCError @@ -270,6 +273,10 @@ "Error occurred during Morley extension typecheck: " +| e |+ " on stack " +| t |+ ". " +| buildCallStack ics + TCIncompletelyTyped err contract -> + "\n" + +| printDocB False (renderDoc doesntNeedParens contract) |+ "\n" + +| build err where buildTruncated k l | null (drop k l) = build l @@ -280,10 +287,10 @@ [] -> "." _ -> " inside these let defenitions: " +| listF icsCallStack |+ "." -instance Buildable U.ExpandedInstr => Show TCError where +instance Show TCError where show = pretty -instance Buildable U.ExpandedInstr => Exception TCError +instance Exception TCError newtype StackSize = StackSize Natural deriving stock (Show, Eq, Generic) diff --git a/src/Michelson/TypeCheck/Ext.hs b/src/Michelson/TypeCheck/Ext.hs --- a/src/Michelson/TypeCheck/Ext.hs +++ b/src/Michelson/TypeCheck/Ext.hs @@ -8,8 +8,8 @@ ) where import Control.Lens ((%=)) -import Data.Constraint (Dict(..)) import Control.Monad.Except (MonadError, liftEither, throwError) +import Data.Constraint (Dict(..)) import Data.Map.Lazy (insert, lookup) import Data.Typeable ((:~:)(..)) @@ -17,6 +17,7 @@ import Michelson.TypeCheck.Error import Michelson.TypeCheck.Helpers import Michelson.TypeCheck.TypeCheck +import Michelson.TypeCheck.TypeCheckedSeq (IllTypedInstr(..), TypeCheckedSeq(..)) import Michelson.TypeCheck.Types import Michelson.Typed (Notes(..), converge, mkUType, notesT, withUType) import qualified Michelson.Typed as T @@ -26,44 +27,52 @@ import qualified Michelson.Untyped as U import Util.Peano (SingNat(SS, SZ)) -type TypeCheckListHandler inp = - [U.ExpandedOp] - -> HST inp - -> TypeCheck (SomeInstr inp) +-- | Perform some, possibly throwing, action presumably making use of a supplied +-- external instruction. In case of an error, return @IllTypedSeq@ wrapping the +-- thrown error and the instruction. If the action successfully returns +-- @SomeInstr@, wrap it in a @WellTypedSeq@. +workOnInstr + :: U.ExpandedExtInstr + -> TypeCheckInstr (SomeInstr s) + -> TypeCheckInstrNoExcept (TypeCheckedSeq s) +workOnInstr ext = tcEither + (\err -> pure $ IllTypedSeq err [NonTypedInstr $ U.PrimEx $ U.EXT ext]) + (pure . WellTypedSeq) typeCheckExt - :: forall s. - (Typeable s) - => TypeCheckListHandler s + :: forall s. Typeable s + => TcInstrHandler -> U.ExpandedExtInstr -> HST s - -> TypeCheckInstr (SomeInstr s) -typeCheckExt typeCheckListH ext hst = do + -> TypeCheckInstrNoExcept (TypeCheckedSeq s) +typeCheckExt tcInstr ext hst = do instrPos <- ask case ext of - U.STACKTYPE s -> liftExtError hst $ nopSomeInstr <$ checkStackType noBoundVars s hst - U.FN t sf op -> checkFn typeCheckListH t sf op hst - U.UPRINT pc -> verifyPrint pc <&> \tpc -> toSomeInstr (T.PRINT tpc) + U.STACKTYPE s -> workOnInstr ext $ + liftExtError hst $ nopSomeInstr <$ checkStackType noBoundVars s hst + U.FN t sf op -> checkFn tcInstr t sf op hst + U.UPRINT pc -> workOnInstr ext $ + verifyPrint pc <&> \tpc -> toSomeInstr (T.PRINT tpc) U.UTEST_ASSERT U.TestAssert{..} -> do - verifyPrint tassComment - _ :/ si <- lift $ typeCheckListH tassInstrs hst - case si of + let cons = U.EXT . U.UTEST_ASSERT . U.TestAssert tassName tassComment + preserving (typeCheckImpl tcInstr tassInstrs hst) cons $ \(_ :/ si) -> case si of AnyOutInstr _ -> throwError $ TCExtError (SomeHST hst) instrPos $ TestAssertError "TEST_ASSERT has to return Bool, but it always fails" - instr ::: (((_ :: (T.Notes b, Dict (T.WellTyped b), VarAnn)) ::& (_ :: HST out1))) -> do - Refl <- liftEither $ - first (const $ TCExtError (SomeHST hst) instrPos $ - TestAssertError "TEST_ASSERT has to return Bool, but returned something else") $ - eqType @b @'T.TBool + instr ::: (((_ :: (T.Notes b, Dict (T.WellTyped b), VarAnn)) ::& _)) -> do + Refl <- liftEither $ first + (const $ TCExtError (SomeHST hst) instrPos $ + TestAssertError "TEST_ASSERT has to return Bool, but returned something else") + (eqType @b @'T.TBool) tcom <- verifyPrint tassComment pure . toSomeInstr $ T.TEST_ASSERT $ T.TestAssert tassName tcom instr _ -> throwError $ TCExtError (SomeHST hst) instrPos $ TestAssertError "TEST_ASSERT has to return Bool, but the stack is empty" + U.UCOMMENT t -> -- TODO if we are going to analyze/parse programs from files, -- there should be parsing of string and creation of FunctionStarted/FunctionFinished/etc - pure $ toSomeInstr $ T.COMMENT_ITEM $ T.JustComment t + pure $ WellTypedSeq $ toSomeInstr $ T.COMMENT_ITEM $ T.JustComment t where verifyPrint :: U.PrintComment -> TypeCheckInstr (T.PrintComment s) verifyPrint (U.PrintComment pc) = do @@ -90,19 +99,18 @@ -- the pattern in @FN@. checkFn :: Typeable inp - => TypeCheckListHandler inp + => TcInstrHandler -> Text -> StackFn -> [ExpandedOp] -> HST inp - -> TypeCheckInstr (SomeInstr inp) -checkFn typeCheckListH t sf body inp = do - vars <- checkStart inp - res@(_ :/ instr) <- lift $ typeCheckListH body inp - case instr of - _ ::: out -> checkEnd vars out - AnyOutInstr _ -> pass - return res + -> TypeCheckInstrNoExcept (TypeCheckedSeq inp) +checkFn tcInstr t sf body inp = do + guarding (con body) (checkStart inp) $ \vars -> + preserving (typeCheckImplStripped tcInstr body inp) con $ \someI@(_ :/ instrAndOut) -> + case instrAndOut of + _ ::: out -> checkEnd vars out $> someI + AnyOutInstr{} -> pure someI where checkStart hst = do liftExtError hst $ checkVars t sf @@ -113,6 +121,9 @@ checkEnd :: Typeable out => BoundVars -> HST out -> TypeCheckInstr () checkEnd vars out = liftExtError out $ void $ checkStackType vars (sfnOutPattern sf) out + + con :: [op] -> U.InstrAbstract op + con = U.EXT . U.FN t sf -- | Check that a @StackTypePattern@ matches the type of the current stack checkStackType diff --git a/src/Michelson/TypeCheck/Helpers.hs b/src/Michelson/TypeCheck/Helpers.hs --- a/src/Michelson/TypeCheck/Helpers.hs +++ b/src/Michelson/TypeCheck/Helpers.hs @@ -24,6 +24,7 @@ , typeCheckInstrErr , typeCheckInstrErr' , typeCheckImpl + , typeCheckImplStripped , matchTypes , memImpl @@ -56,9 +57,11 @@ import Michelson.TypeCheck.Error (TCError(..), TCTypeError(..), TypeContext(..)) import Michelson.TypeCheck.TypeCheck import Michelson.TypeCheck.Types +import Michelson.TypeCheck.TypeCheckedSeq (IllTypedInstr(..), TypeCheckedSeq(..)) import Michelson.Typed - (BadTypeForScope(..), Comparable, Instr(..), KnownT, Notes(..), PackedNotes(..), SingT(..), - T(..), WellTyped, converge, getComparableProofS, notesT, orAnn, starNotes) + (BadTypeForScope(..), CommentType(StackTypeComment), Comparable, ExtInstr(COMMENT_ITEM), + Instr(..), KnownT, Notes(..), PackedNotes(..), SingT(..), T(..), WellTyped, converge, + getComparableProofS, notesT, orAnn, starNotes) import Michelson.Typed.Annotation (AnnConvergeError, isStar) import Michelson.Typed.Arith (Add, ArithOp(..), Mul, Sub, UnaryArithOp(..)) import Michelson.Typed.Polymorphic @@ -254,73 +257,171 @@ Just d@Dict -> pure $ withDict d act Nothing -> typeCheckInstrErr instr (SomeHST i) $ Just ComparisonArguments -typeCheckImpl - :: forall inp . Typeable inp +typeCheckOpImpl + :: forall inp. Typeable inp => TcInstrHandler - -> [Un.ExpandedOp] + -> Un.ExpandedOp -> HST inp - -> TypeCheckInstr (SomeInstr inp) -typeCheckImpl tcInstr instrs t@(a :: HST a) = - case instrs of - Un.WithSrcEx _ (i@(Un.WithSrcEx _ _)) : rs -> typeCheckImpl tcInstr (i : rs) t - Un.WithSrcEx cs (Un.PrimEx i) : rs -> typeCheckPrim (Just cs) i rs - Un.WithSrcEx cs (Un.SeqEx sq) : rs -> typeCheckSeq (Just cs) sq rs - Un.PrimEx i : rs -> typeCheckPrim Nothing i rs - Un.SeqEx sq : rs -> typeCheckSeq Nothing sq rs - [] -> pure $ a :/ Nop ::: a + -> TypeCheckInstrNoExcept (TypeCheckedSeq inp) +typeCheckOpImpl tcInstr op' inputStack = case op' of + Un.WithSrcEx _ op@Un.WithSrcEx{} -> typeCheckOpImpl tcInstr op inputStack + Un.WithSrcEx loc (Un.PrimEx op) -> typeCheckPrimWithLoc loc op + Un.WithSrcEx loc (Un.SeqEx sq) -> typeCheckSeqWithLoc loc sq + Un.PrimEx op -> typeCheckPrim op + Un.SeqEx sq -> typeCheckSeq sq where -- If we know source location from the untyped instruction, keep it in the typed one. - typeCheckPrim (Just cs) i [] = local (const cs) $ (tcInstr i t <&> wrapWithLoc cs) - typeCheckPrim (Just cs) i rs = local (const cs) $ typeCheckImplDo (tcInstr i t <&> wrapWithLoc cs) id rs - typeCheckPrim Nothing i [] = tcInstr i t - typeCheckPrim Nothing i rs = typeCheckImplDo (tcInstr i t) id rs + typeCheckPrimWithLoc loc op = local (const loc) + (wrapWithLoc loc <$> typeCheckPrim op) - typeCheckSeq (Just cs) sq = local (const cs) . typeCheckImplDo (typeCheckImpl tcInstr sq t) Nested - typeCheckSeq Nothing sq = typeCheckImplDo (typeCheckImpl tcInstr sq t) Nested + typeCheckPrim op = tcInstr op inputStack <&> mapSeq addNotes - wrapWithLoc :: InstrCallStack -> SomeInstr inp -> SomeInstr inp - wrapWithLoc _ si@(_ :/ (WithLoc _ _) ::: _) = si - wrapWithLoc cs (inp :/ instr ::: out) = inp :/ WithLoc cs instr ::: out - wrapWithLoc _ si = si + typeCheckSeqWithLoc loc = local (const loc) . typeCheckSeq - typeCheckImplDo - :: TypeCheckInstr (SomeInstr inp) - -> (forall inp' out . Instr inp' out -> Instr inp' out) - -> [Un.ExpandedOp] - -> TypeCheckInstr (SomeInstr inp) - typeCheckImplDo f wrap rs = do - _ :/ pi' <- f - case pi' of - p ::: b -> do - _ :/ qi <- typeCheckImpl tcInstr rs b - case qi of - q ::: c -> case q of - Seq _ _ -> - pure $ a :/ Seq (wrapWithNotes b (wrap p)) q ::: c - -- Wrap the RHS if it is a single instruction and not a - -- sequence - _ -> - pure $ a :/ Seq (wrapWithNotes b (wrap p)) (wrapWithNotes c q) ::: c - AnyOutInstr q -> - pure $ a :/ AnyOutInstr (Seq (wrapWithNotes b (wrap p)) q) + typeCheckSeq sq = typeCheckImpl tcInstr sq inputStack + <&> mapSeq (addNotes . mapSomeInstr Nested) - AnyOutInstr instr -> - case rs of - [] -> - pure $ a :/ AnyOutInstr instr - r : rr -> - throwError $ TCUnreachableCode (extractInstrPos r) (r :| rr) + addNotes (inp :/ i ::: out) = inp :/ wrapWithNotes out i ::: out + addNotes i = i wrapWithNotes :: HST d -> Instr c d -> Instr c d - wrapWithNotes h ins = case h of + wrapWithNotes outputStack instr = case outputStack of -- do not wrap in notes if the notes are "star" - ((n, _, _) ::& _) | isStar n -> ins - ((n, _, _) ::& _) -> InstrWithNotes (PackedNotes n) ins - SNil -> ins + ((n, _, _) ::& _) | isStar n -> instr + ((n, _, _) ::& _) -> InstrWithNotes (PackedNotes n) instr + SNil -> instr - extractInstrPos :: Un.ExpandedOp -> InstrCallStack - extractInstrPos (Un.WithSrcEx cs _) = cs - extractInstrPos _ = def +-- | Like 'typeCheckImpl' but doesn't add a stack type comment after the +-- sequence. +typeCheckImplNoLastTypeComment + :: forall inp . Typeable inp + => TcInstrHandler + -> [Un.ExpandedOp] + -> HST inp + -> TypeCheckInstrNoExcept (TypeCheckedSeq inp) +typeCheckImplNoLastTypeComment _ [] inputStack + = pure (WellTypedSeq (inputStack :/ Nop ::: inputStack)) +typeCheckImplNoLastTypeComment tcInstr (op : ops) inputStack = do + done <- typeCheckOpImpl tcInstr op inputStack + >>= mapMSeq prependStackTypeComment + continueTypeChecking tcInstr done ops + +continueTypeChecking + :: forall inp. () + => TcInstrHandler + -> TypeCheckedSeq inp + -> [Un.ExpandedOp] + -> TypeCheckInstrNoExcept (TypeCheckedSeq inp) +continueTypeChecking tcInstr done rest = case done of + WellTypedSeq instr -> handleFirst instr + MixedSeq i e left -> pure (MixedSeq i e (left <> map NonTypedInstr rest)) + IllTypedSeq e left -> pure (IllTypedSeq e (left <> map NonTypedInstr rest)) + where + handleFirst :: SomeInstr inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp) + handleFirst packedInstr@(inputStack :/ instrAndOutputStack) = do + case instrAndOutputStack of + instr ::: outputStack -> do + nextPiece <- typeCheckImplNoLastTypeComment tcInstr rest outputStack + let combiner = combine inputStack instr + pure case nextPiece of + WellTypedSeq nextInstr -> WellTypedSeq (combiner nextInstr) + MixedSeq nextInstr err left -> MixedSeq (combiner nextInstr) err left + IllTypedSeq err left -> MixedSeq packedInstr err left + AnyOutInstr{} -> pure case rest of + [] -> WellTypedSeq packedInstr + op : ops -> (MixedSeq + packedInstr + (TCUnreachableCode (extractOpPos op) (op :| ops)) + (map NonTypedInstr ops)) + + combine inp i1 (_ :/ nextPart) = inp :/ mapSomeInstrOut (Seq i1) nextPart + + extractOpPos :: Un.ExpandedOp -> InstrCallStack + extractOpPos (Un.WithSrcEx loc _) = loc + extractOpPos _ = def + +-- | Like 'typeCheckImpl' but without the first and the last stack type +-- comments. Useful to reduce duplication of stack type comments. +typeCheckImplStripped + :: forall inp . Typeable inp + => TcInstrHandler + -> [Un.ExpandedOp] + -> HST inp + -> TypeCheckInstrNoExcept (TypeCheckedSeq inp) +typeCheckImplStripped tcInstr [] inp + = typeCheckImplNoLastTypeComment tcInstr [] inp +typeCheckImplStripped tcInstr (op : ops) inp = do + done <- typeCheckOpImpl tcInstr op inp + continueTypeChecking tcInstr done ops + +typeCheckImpl + :: forall inp . Typeable inp + => TcInstrHandler + -> [Un.ExpandedOp] + -> HST inp + -> TypeCheckInstrNoExcept (TypeCheckedSeq inp) +typeCheckImpl tcInstr ops inputStack = do + tcSeq <- typeCheckImplNoLastTypeComment tcInstr ops inputStack + mapMSeq appendTypeComment tcSeq + where + appendTypeComment packedI@(inp :/ iAndOut) = do + verbose <- lift (asks tcVerbose) + pure case (verbose, iAndOut) of + (True, i ::: out) -> inp :/ Seq i (stackTypeComment out) ::: out + (True, AnyOutInstr i) -> inp :/ AnyOutInstr (Seq i noStackTypeComment) + _ -> packedI + + +prependStackTypeComment + :: SomeInstr inp -> TypeCheckInstrNoExcept (SomeInstr inp) +prependStackTypeComment packedInstr@(inp :/ _) = do + verbose <- lift (asks tcVerbose) + pure if verbose && (not (isNop' packedInstr)) + then mapSomeInstr (Seq (stackTypeComment inp)) packedInstr + else packedInstr + +isNop' :: SomeInstr inp -> Bool +isNop' (_ :/ i ::: _) = isNop i +isNop' (_ :/ AnyOutInstr i) = isNop i + +isNop :: Instr inp out -> Bool +isNop (WithLoc _ i) = isNop i +isNop (InstrWithNotes _ i) = isNop i +isNop (InstrWithVarNotes _ i) = isNop i +isNop (FrameInstr _ i) = isNop i +isNop (Seq i1 i2) = isNop i1 && isNop i2 +isNop (Nested i) = isNop i +isNop Nop = True +isNop (Ext _) = True +isNop _ = False + +mapMSeq + :: Applicative f + => (SomeInstr inp -> f (SomeInstr inp')) + -> TypeCheckedSeq inp + -> f (TypeCheckedSeq inp') +mapMSeq f v = case v of + WellTypedSeq instr -> f instr <&> WellTypedSeq + MixedSeq instr err tail' -> f instr <&> \instr' -> MixedSeq instr' err tail' + IllTypedSeq err tail' -> pure $ IllTypedSeq err tail' + +mapSeq + :: (SomeInstr inp -> SomeInstr inp') + -> TypeCheckedSeq inp + -> TypeCheckedSeq inp' +mapSeq f = runIdentity . mapMSeq (Identity . f) + +stackTypeComment :: HST st -> Instr st st +stackTypeComment = Ext . COMMENT_ITEM . StackTypeComment . Just . hstToTs + +noStackTypeComment :: Instr st st +noStackTypeComment = Ext (COMMENT_ITEM (StackTypeComment Nothing)) + +wrapWithLoc :: InstrCallStack -> TypeCheckedSeq inp -> TypeCheckedSeq inp +wrapWithLoc loc = mapSeq $ \someInstr -> case someInstr of + (_ :/ WithLoc{} ::: _) -> someInstr + (inp :/ instr ::: out) -> inp :/ WithLoc loc instr ::: out + _ -> someInstr -- | Check whether given types are structurally equal and annotations converge. matchTypes diff --git a/src/Michelson/TypeCheck/Instr.hs b/src/Michelson/TypeCheck/Instr.hs --- a/src/Michelson/TypeCheck/Instr.hs +++ b/src/Michelson/TypeCheck/Instr.hs @@ -31,17 +31,19 @@ module Michelson.TypeCheck.Instr ( typeCheckContract , typeCheckContractAndStorage - , typeCheckValue + , typeCheckInstr , typeCheckList - , typeVerifyStorage - , typeVerifyParameter - , typeCheckStorage + , typeCheckListNoExcept , typeCheckParameter + , typeCheckStorage + , typeCheckValue + , typeVerifyParameter + , typeVerifyStorage ) where import Prelude hiding (EQ, GT, LT) -import Control.Monad.Except (MonadError, liftEither, throwError) +import Control.Monad.Except (MonadError, liftEither, throwError, catchError) import Data.Default (def) import Data.Generics (everything, mkQ) import Data.Singletons (Sing, demote) @@ -52,6 +54,8 @@ import Michelson.TypeCheck.Ext import Michelson.TypeCheck.Helpers import Michelson.TypeCheck.TypeCheck +import Michelson.TypeCheck.TypeCheckedSeq + (IllTypedInstr(..), TypeCheckedInstr, TypeCheckedOp(..), TypeCheckedSeq(..), tcsEither, someInstrToOp) import Michelson.TypeCheck.Types import Michelson.TypeCheck.Value import Michelson.Typed.Value @@ -66,16 +70,17 @@ -- is of the type expected by the contract. typeCheckContractAndStorage :: U.Contract -> U.Value -> Either TCError SomeContractAndStorage typeCheckContractAndStorage uContract uStorage = do - SomeContract (contract@Contract{} :: Contract cp st) <- typeCheckContract uContract + SomeContract (contract@Contract{} :: Contract cp st) <- typeCheckContract uContract def storage <- typeVerifyStorage @st uStorage Right $ SomeContractAndStorage contract storage typeCheckContract :: U.Contract + -> TypeCheckOptions -> Either TCError SomeContract -typeCheckContract c = do +typeCheckContract c options = do paramType <- mkSomeParamType (U.contractParameter c) - runTypeCheck (TypeCheckContract paramType) $ typeCheckContractImpl c + runTypeCheck (TypeCheckContract paramType) options $ typeCheckContractImpl c withWTP :: forall t a. SingI t => (WellTyped t => TypeCheck a) -> TypeCheck a withWTP fn = case getWTP @t of @@ -89,10 +94,24 @@ loc <- ask throwError $ TCFailedOnInstr v t loc Nothing (Just $ UnsupportedTypeForScope badType BtNotComparable) +withWTPInstr'_ + :: forall t inp. SingI t + => U.ExpandedInstr + -> SomeHST + -> (WellTyped t => TypeCheckInstrNoExcept (TypeCheckedSeq inp)) + -> TypeCheckInstrNoExcept (TypeCheckedSeq inp) +withWTPInstr'_ v t fn = case getWTP @t of + Right Dict -> fn + Left (NotWellTyped badType) -> do + loc <- ask + let err = TCFailedOnInstr v t loc Nothing + (Just $ UnsupportedTypeForScope badType BtNotComparable) + pure $ IllTypedSeq err [NonTypedInstr $ U.PrimEx v] + typeCheckContractImpl :: U.Contract -> TypeCheck SomeContract -typeCheckContractImpl (U.Contract (U.ParameterType mParam rootAnn) mStorage pCode entriesOrder) = do +typeCheckContractImpl (U.Contract wholeParam@(U.ParameterType mParam rootAnn) mStorage pCode entriesOrder) = do _ <- maybe (throwError $ TCContractError "no instructions in contract code" $ Just EmptyCode) pure (nonEmpty pCode) withUType mParam $ \(paramNote :: Notes param) -> @@ -105,41 +124,71 @@ $ checkScope @(StorageScope st) let inpNote = NTPair def def def paramNote storageNote let inp = (inpNote, Dict, def) ::& SNil - inp' :/ instrOut <- usingReaderT def $ typeCheckImpl typeCheckInstr pCode inp - let (paramNotesRaw, cStoreNotes) = case inp' of - (NTPair _ _ _ cpNotes stNotes, _, _) ::& SNil -> (cpNotes, stNotes) - cParamNotes <- - liftEither $ - mkParamNotes paramNotesRaw rootAnn `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 Contract - { cCode = instr - , cParamNotes - , cStoreNotes - , cEntriesOrder = entriesOrder - } - Left err -> Left $ TCContractError "contract output type violates convention:" $ Just err - AnyOutInstr instr -> + + codeRes <- usingReaderT def $ + liftNoExcept $ + typeCheckImpl typeCheckInstr pCode inp + codeRes & tcsEither + (onFailedTypeCheck) + (onSuccessfulTypeCheck (NTPair def def def starNotes storageNote)) + where + hasTypeError :: forall (t :: T) a. SingI t => Text -> BadTypeForScope -> TypeCheck a + hasTypeError name reason = throwError $ + TCContractError ("contract " <> name <> " type error") $ + Just $ UnsupportedTypeForScope (demote @t) reason + + onFailedTypeCheck :: [TypeCheckedOp] -> TCError -> TypeCheck SomeContract + onFailedTypeCheck ops err = do + verbose <- asks tcVerbose + throwError if verbose + then TCIncompletelyTyped err U.Contract + { contractParameter = wholeParam + , contractStorage = mStorage + , contractCode = ops + , entriesOrder = entriesOrder + } + else err + + onSuccessfulTypeCheck + :: forall st param + . (ParameterScope param, StorageScope st, WellTyped st) + => Notes (ContractOut1 st) + -> SomeInstr (ContractInp param st) + -> TypeCheck SomeContract + onSuccessfulTypeCheck outNote i@(inp' :/ instrOut) = wrapErrorsIfVerbose i $ do + let (paramNotesRaw, cStoreNotes) = case inp' of + (NTPair _ _ _ cpNotes stNotes, _, _) ::& SNil -> (cpNotes, stNotes) + cParamNotes <- + liftEither $ + mkParamNotes paramNotesRaw rootAnn `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 outNote + `onLeft` + ((TCContractError "contract output type violates convention:") . Just . AnnError) pure $ SomeContract Contract { cCode = instr , cParamNotes , cStoreNotes , cEntriesOrder = entriesOrder } - where - hasTypeError :: forall (t :: T) a. SingI t => Text -> BadTypeForScope -> TypeCheck a - hasTypeError name reason = throwError $ - TCContractError ("contract " <> name <> " type error") $ - Just $ UnsupportedTypeForScope (demote @t) reason + Left err -> Left $ TCContractError "contract output type violates convention:" $ Just err + AnyOutInstr instr -> + pure $ SomeContract Contract + { cCode = instr + , cParamNotes + , cStoreNotes + , cEntriesOrder = entriesOrder + } + wrapErrorsIfVerbose :: SomeInstr inp -> TypeCheck SomeContract -> TypeCheck SomeContract + wrapErrorsIfVerbose instr action = + action `catchError` (onFailedTypeCheck [someInstrToOp instr]) + -- | Function @typeCheckList@ converts list of Michelson instructions -- given in representation from @Michelson.Type@ module to representation -- in strictly typed GADT. @@ -153,8 +202,19 @@ => [U.ExpandedOp] -> HST inp -> TypeCheck (SomeInstr inp) -typeCheckList = usingReaderT def ... typeCheckImpl typeCheckInstr +typeCheckList = throwingTCError' ... typeCheckListNoExcept +-- | Function @typeCheckListNoExcept@ converts list of Michelson instructions +-- given in representation from @Michelson.Type@ module to representation in a +-- partially typed tree. See @TypeCheckedSeq@ and @TypeCheckedOp@. +-- +-- Types are checked along the way. It is necessary to embed well typed node as +-- well as type checking errors into the tree. +typeCheckListNoExcept + :: (Typeable inp) + => [U.ExpandedOp] -> HST inp -> TypeCheckNoExcept (TypeCheckedSeq inp) +typeCheckListNoExcept = usingReaderT def ... typeCheckImpl typeCheckInstr + -- | Function @typeCheckValue@ converts a single Michelson value -- given in representation from @Michelson.Untyped@ module hierarchy to -- representation in strictly typed GADT. @@ -187,7 +247,7 @@ :: forall t. SingI t => Maybe TcOriginatedContracts -> U.Value -> Either TCError (Value t) typeVerifyTopLevelType mOriginatedContracts valueU = - runTypeCheck (TypeCheckValue (valueU, demote @t)) $ usingReaderT (def :: InstrCallStack) $ + runTypeCheck (TypeCheckValue (valueU, demote @t)) def $ usingReaderT def $ typeCheckValImpl mOriginatedContracts typeCheckInstr valueU -- | Like 'typeCheckValue', but for values to be used as parameter. @@ -230,6 +290,22 @@ (Typeable out, ConstraintDUG n inp out a) => Sing n -> HST out -> TCDugHelper inp +-- Helper function to convert a simple throwing typechecking action into a +-- non-throwing one, embedding possible errors into the type checking tree. +workOnInstr + :: U.ExpandedInstr + -> TypeCheckInstr (SomeInstr s) + -> TypeCheckInstrNoExcept (TypeCheckedSeq s) +workOnInstr instr = tcEither + (\err -> pure $ IllTypedSeq err [NonTypedInstr $ U.PrimEx instr]) + (pure . WellTypedSeq) + +-- Less verbose version of `lift ... typeCheckListNoExcept`. +tcList + :: (Typeable inp) + => [U.ExpandedOp] -> HST inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp) +tcList ops stack = lift $ typeCheckListNoExcept ops stack + -- | Function @typeCheckInstr@ converts a single Michelson instruction -- given in representation from @Michelson.Type@ module to representation -- in strictly typed GADT. @@ -246,13 +322,13 @@ typeCheckInstr :: TcInstrHandler typeCheckInstr uInstr inp = case (uInstr, inp) of (U.EXT ext, si) -> - typeCheckExt typeCheckList ext si + typeCheckExt typeCheckInstr ext si - (U.DROP, _ ::& rs) -> pure (inp :/ DROP ::: rs) + (U.DROP, _ ::& rs) -> workOnInstr uInstr $ pure $ inp :/ DROP ::: rs (U.DROP, SNil) -> notEnoughItemsOnStack - (U.DROPN nTotal, inputHST) -> + (U.DROPN nTotal, inputHST) -> workOnInstr uInstr $ go nTotal inputHST <&> \case TCDropHelper s out -> inputHST :/ DROPN s ::: out where @@ -263,22 +339,22 @@ go n i = case (n, i) of (0, _) -> pure (TCDropHelper SZ i) - (_, SNil) -> notEnoughItemsOnStack + (_, SNil) -> notEnoughItemsOnStack' (_, (_ ::& iTail)) -> do go (n - 1) iTail <&> \case TCDropHelper s out -> TCDropHelper (SS s) out - (U.DUP _vn, a ::& rs) -> + (U.DUP _vn, a ::& rs) -> workOnInstr uInstr $ pure (inp :/ DUP ::: (a ::& a::& rs)) (U.DUP _vn, SNil) -> notEnoughItemsOnStack - (U.SWAP, a ::& b ::& rs) -> + (U.SWAP, a ::& b ::& rs) -> workOnInstr uInstr $ pure (inp :/ SWAP ::: (b ::& a ::& rs)) (U.SWAP, _) -> notEnoughItemsOnStack - (U.DIG nTotal, inputHST) -> + (U.DIG nTotal, inputHST) -> workOnInstr uInstr $ go nTotal inputHST <&> \case TCDigHelper s out -> inputHST :/ DIG s ::: out where @@ -288,7 +364,7 @@ -> TypeCheckInstr (TCDigHelper inp) go n i = case (n, i) of -- Even 'DIG 0' is invalid on empty stack (so it is not strictly `Nop`). - (_, SNil) -> notEnoughItemsOnStack + (_, SNil) -> notEnoughItemsOnStack' (0, (_ ::& _)) -> pure (TCDigHelper SZ i) @@ -296,7 +372,7 @@ go (n - 1) iTail <&> \case TCDigHelper s (a ::& resTail) -> TCDigHelper (SS s) (a ::& b ::& resTail) - (U.DUG nTotal, inputHST) -> + (U.DUG nTotal, inputHST) -> workOnInstr uInstr $ go nTotal inputHST <&> \case TCDugHelper s out -> inputHST :/ DUG s ::: out where @@ -314,32 +390,32 @@ -- Two cases: -- 1. Input stack is empty. -- 2. n > 0 and input stack has exactly 1 item. - _ -> notEnoughItemsOnStack + _ -> notEnoughItemsOnStack' - (U.PUSH vn mt mval, i) -> + (U.PUSH vn mt mval, i) -> workOnInstr uInstr $ withUType mt $ \(nt :: Notes t) -> do val <- typeCheckValue @t mval proofScope <- onScopeCheckInstrErr @t uInstr (SomeHST i) Nothing $ checkScope @(ConstantScope t) case proofScope of - Dict -> withWTPInstr @t $ pure $ i :/ PUSH val ::: ((nt, Dict, vn) ::& i) + Dict -> withWTPInstr @t $ pure $ i :/ PUSH val ::: ((nt, Dict, vn) ::& i) - (U.SOME tn vn, (an, Dict, _) ::& rs) -> do + (U.SOME tn vn, (an, Dict, _) ::& rs) -> workOnInstr uInstr $ pure (inp :/ SOME ::: ((NTOption tn an, Dict, vn) ::& rs)) (U.SOME _ _, SNil) -> notEnoughItemsOnStack - (U.NONE tn vn elMt, _) -> + (U.NONE tn vn elMt, _) -> workOnInstr uInstr $ withUType elMt $ \(elNotes :: Notes t) -> withWTPInstr @t $ pure $ inp :/ NONE ::: ((NTOption tn elNotes, Dict, vn) ::& inp) - (U.UNIT tn vn, _) -> + (U.UNIT tn vn, _) -> workOnInstr uInstr $ pure $ inp :/ UNIT ::: ((NTUnit tn, Dict, vn) ::& inp) (U.IF_NONE mp mq, (STOption{}, (ons :: Notes ('TOption a)), Dict, ovn) ::&+ rs) -> do let (an, avn) = deriveNsOption ons ovn - withWTPInstr @a $ + withWTPInstr' @a $ genericIf IF_NONE U.IF_NONE mp mq rs ((an, Dict, avn) ::& rs) inp (U.IF_NONE _ _, _ ::& _) -> @@ -347,7 +423,7 @@ (U.IF_NONE _ _, SNil) -> notEnoughItemsOnStack - (U.PAIR tn vn pfn qfn, (an, _, avn) ::& (bn, _, bvn) ::& rs) -> do + (U.PAIR tn vn pfn qfn, (an, _, avn) ::& (bn, _, bvn) ::& rs) -> workOnInstr uInstr $ do let (vn', pfn', qfn') = deriveSpecialFNs pfn qfn avn bvn case NTPair tn pfn' qfn' an bn of (ns :: Notes ('TPair a b)) -> withWTPInstr @('TPair a b) $ @@ -355,7 +431,7 @@ (U.PAIR {}, _) -> notEnoughItemsOnStack - (U.CAR vn fn, (STPair{}, NTPair pairTN pfn qfn (pns :: Notes p) (qns :: Notes q), _, pairVN) ::&+ rs) -> do + (U.CAR vn fn, (STPair{}, NTPair pairTN pfn qfn (pns :: Notes p) (qns :: Notes q), _, pairVN) ::&+ rs) -> workOnInstr uInstr $ do pfn' <- onTypeCheckInstrAnnErr uInstr inp (Just CarArgument) (convergeAnns fn pfn) withWTPInstr @p $ withWTPInstr @('TPair p q) $ do @@ -368,7 +444,7 @@ (U.CAR _ _, SNil) -> notEnoughItemsOnStack - (U.CDR vn fn, (STPair{}, NTPair pairTN pfn qfn (pns :: Notes p) (qns :: Notes q), _, pairVN) ::&+ rs) -> do + (U.CDR vn fn, (STPair{}, NTPair pairTN pfn qfn (pns :: Notes p) (qns :: Notes q), _, pairVN) ::&+ rs) -> workOnInstr uInstr $ do qfn' <- onTypeCheckInstrAnnErr uInstr inp (Just CdrArgument) (convergeAnns fn qfn) withWTPInstr @q $ @@ -383,7 +459,7 @@ (U.CDR _ _, SNil) -> notEnoughItemsOnStack (U.LEFT tn vn pfn qfn bMt, (an :: Notes l, Dict, _) ::& rs) -> - withUType bMt $ \(bn :: Notes r) -> do + withUType bMt $ \(bn :: Notes r) -> workOnInstr uInstr $ do withWTPInstr @r $ do let ns = NTOr tn pfn qfn an bn pure (inp :/ LEFT ::: ((ns, Dict, vn) ::& rs)) @@ -391,7 +467,7 @@ (U.LEFT {}, SNil) -> notEnoughItemsOnStack (U.RIGHT tn vn pfn qfn aMt, (bn :: Notes r, Dict, _) ::& rs) -> - withUType aMt $ \(an :: Notes l) -> do + withUType aMt $ \(an :: Notes l) -> workOnInstr uInstr $ do withWTPInstr @l $ do let ns = NTOr tn pfn qfn an bn pure (inp :/ RIGHT ::: ((ns, Dict, vn) ::& rs)) @@ -401,8 +477,8 @@ (U.IF_LEFT mp mq, (STOr{}, ons, _, ovn) ::&+ rs) -> do case deriveNsOr ons ovn of (an :: Notes a, bn :: Notes b, avn, bvn) -> - withWTPInstr @a $ - withWTPInstr @b $ do + withWTPInstr' @a $ + withWTPInstr' @b $ do let ait = (an, Dict, avn) ::& rs bit = (bn, Dict, bvn) ::& rs @@ -413,13 +489,13 @@ (U.IF_LEFT _ _, SNil) -> notEnoughItemsOnStack - (U.NIL tn vn elMt, i) -> + (U.NIL tn vn elMt, i) -> workOnInstr uInstr $ withUType elMt $ \(elNotes :: Notes t) -> withWTPInstr @('TList t) $ pure $ i :/ NIL ::: ((NTList tn elNotes, Dict, vn) ::& i) (U.CONS vn, ((an :: Notes a), _, _) - ::& ((ln :: Notes l), _, _) ::& rs) -> + ::& ((ln :: Notes l), _, _) ::& rs) -> workOnInstr uInstr case eqType @('TList a) @l of Right Refl -> do (n :: Notes t) <- onTypeCheckInstrAnnErr uInstr inp (Just ConsArgument) (converge ln (NTList def an)) @@ -431,8 +507,8 @@ (U.IF_CONS mp mq, (STList{}, ns, Dict, vn) ::&+ rs) -> do case ns of - NTList _ (an :: Notes t1) -> do - ait <- withWTPInstr @t1 $ pure $ (an, Dict, vn <> "hd") ::& (ns, Dict, vn <> "tl") ::& rs + NTList _ (an :: Notes t1) -> withWTPInstr' @t1 $ do + let ait = (an, Dict, vn <> "hd") ::& (ns, Dict, vn <> "tl") ::& rs genericIf IF_CONS U.IF_CONS mp mq ait rs inp (U.IF_CONS _ _, _ ::& _) -> @@ -440,11 +516,11 @@ (U.IF_CONS _ _, SNil)-> notEnoughItemsOnStack - (U.SIZE vn, (NTList{}, _, _) ::& _) -> sizeImpl inp vn - (U.SIZE vn, (NTSet{}, _, _) ::& _) -> sizeImpl inp vn - (U.SIZE vn, (NTMap{}, _, _) ::& _) -> sizeImpl inp vn - (U.SIZE vn, (NTString{}, _, _) ::& _) -> sizeImpl inp vn - (U.SIZE vn, (NTBytes{}, _, _) ::& _) -> sizeImpl inp vn + (U.SIZE vn, (NTList{}, _, _) ::& _) -> workOnInstr uInstr $ sizeImpl inp vn + (U.SIZE vn, (NTSet{}, _, _) ::& _) -> workOnInstr uInstr $ sizeImpl inp vn + (U.SIZE vn, (NTMap{}, _, _) ::& _) -> workOnInstr uInstr $ sizeImpl inp vn + (U.SIZE vn, (NTString{}, _, _) ::& _) -> workOnInstr uInstr $ sizeImpl inp vn + (U.SIZE vn, (NTBytes{}, _, _) ::& _) -> workOnInstr uInstr $ sizeImpl inp vn (U.SIZE _, _ ::& _) -> failWithErr $ UnexpectedType $ (ExpectList Nothing :| []) :| @@ -456,33 +532,33 @@ (U.SIZE _, SNil) -> notEnoughItemsOnStack - (U.EMPTY_SET tn vn mv, i) -> + (U.EMPTY_SET tn vn mv, i) -> workOnInstr uInstr $ withUType mv $ \(vns :: Notes v) -> withWTPInstr @('TSet v) $ withCompareableCheck (notesSing vns) uInstr inp $ i :/ EMPTY_SET ::: ((STSet sing, NTSet tn vns, Dict, vn) ::&+ i) - (U.EMPTY_MAP tn vn mk mv, i) -> do + (U.EMPTY_MAP tn vn mk mv, i) -> workOnInstr uInstr $ do withUType mv $ \(vns :: Notes v) -> withUType mk $ \(ktn :: Notes k) -> withWTPInstr @('TMap k v) $ withCompareableCheck (notesSing ktn) uInstr inp $ i :/ EMPTY_MAP ::: ((STMap sing sing, NTMap tn ktn vns, Dict, vn) ::&+ i) - (U.EMPTY_BIG_MAP tn vn mk mv, i) -> + (U.EMPTY_BIG_MAP tn vn mk mv, i) -> workOnInstr uInstr $ withUType mv $ \(vns :: Notes v) -> withUType mk $ \(ktn :: Notes k) -> withWTPInstr @('TBigMap k v) $ withCompareableCheck (notesSing ktn) uInstr inp $ i :/ EMPTY_BIG_MAP ::: ((STBigMap sing sing, NTBigMap tn ktn vns, Dict, vn) ::&+ i) (U.MAP vn mp, (STList _, NTList _ (vns :: Notes t1), Dict, _vn) ::&+ _) -> do - withWTPInstr @t1 $ - mapImpl vns uInstr mp inp + withWTPInstr' @t1 $ + mapImpl (U.MAP vn) vns uInstr mp inp (\(rn :: Notes t) hst -> withWTPInstr @t $ pure $ (NTList def rn, Dict, vn) ::& hst) (U.MAP vn mp, (STMap{}, NTMap _ kns vns, Dict, _vn) ::&+ _) -> do case NTPair def def def kns vns of (pns :: Notes ('TPair k v1)) -> - withWTPInstr @('TPair k v1) $ - mapImpl pns uInstr mp inp + withWTPInstr' @('TPair k v1) $ + mapImpl (U.MAP vn) pns uInstr mp inp (\(rn :: Notes v) hst -> withWTPInstr @('TMap k v) $ pure $ (NTMap def kns rn, Dict, vn) ::& hst) (U.MAP _ _, _ ::& _) -> @@ -494,17 +570,17 @@ (U.MAP _ _, SNil) -> notEnoughItemsOnStack (U.ITER is, (STSet (_ :: Sing t1), NTSet _ en, _, _) ::&+ _) -> do - withWTPInstr @t1 $ + withWTPInstr' @t1 $ iterImpl en uInstr is inp (U.ITER is, (STList (_ :: Sing t1), NTList _ en, _, _) ::&+ _) -> do - withWTPInstr @t1 $ + withWTPInstr' @t1 $ iterImpl en uInstr is inp (U.ITER is, (STMap _ _, NTMap _ kns vns, _, _) ::&+ _) -> do case NTPair def def def kns vns of (en :: Notes ('TPair a b)) -> - withWTPInstr @('TPair a b) $ iterImpl en uInstr is inp + withWTPInstr' @('TPair a b) $ iterImpl en uInstr is inp (U.ITER _, _ ::& _) -> failWithErr $ UnexpectedType @@ -516,13 +592,13 @@ (U.ITER _, SNil) -> notEnoughItemsOnStack (U.MEM varNotes, - _ ::& (STSet{}, NTSet _ notesK, _, _) ::&+ _) -> + _ ::& (STSet{}, NTSet _ notesK, _, _) ::&+ _) -> workOnInstr uInstr $ memImpl notesK inp varNotes (U.MEM varNotes, - _ ::& (STMap{}, NTMap _ notesK _, _, _) ::&+ _) -> + _ ::& (STMap{}, NTMap _ notesK _, _, _) ::&+ _) -> workOnInstr uInstr $ memImpl notesK inp varNotes (U.MEM varNotes, - _ ::& (STBigMap{}, NTBigMap _ notesK _, _, _) ::&+ _) -> + _ ::& (STBigMap{}, NTBigMap _ notesK _, _, _) ::&+ _) -> workOnInstr uInstr $ memImpl notesK inp varNotes (U.MEM _, _ ::& _ ::& _) -> failWithErr $ UnexpectedType @@ -536,10 +612,12 @@ (U.GET varNotes, _ ::& (STMap{}, NTMap _ notesK (notesV :: Notes v), _, _) ::&+ _) -> - withWTPInstr @v $ getImpl notesK inp notesV varNotes + workOnInstr uInstr $ withWTPInstr @v $ + getImpl notesK inp notesV varNotes (U.GET varNotes, _ ::& (STBigMap{}, NTBigMap _ notesK (notesV :: Notes v), _, _) ::&+ _) -> - withWTPInstr @v $ getImpl notesK inp notesV varNotes + workOnInstr uInstr $ withWTPInstr @v $ + getImpl notesK inp notesV varNotes (U.GET _, _ ::& _ ::& _) -> failWithErr $ UnexpectedType @@ -551,13 +629,13 @@ (U.UPDATE varNotes, _ ::& _ ::& (STMap{}, (NTMap _ notesK (notesV :: Notes v)), _, _) ::&+ _) -> - updImpl notesK inp (NTOption U.noAnn notesV) varNotes + workOnInstr uInstr $ updImpl notesK inp (NTOption U.noAnn notesV) varNotes (U.UPDATE varNotes, _ ::& _ ::& (STBigMap{}, NTBigMap _ notesK (notesV :: Notes v), _, _) ::&+ _) -> - updImpl notesK inp (NTOption U.noAnn notesV) varNotes + workOnInstr uInstr $ updImpl notesK inp (NTOption U.noAnn notesV) varNotes (U.UPDATE varNotes, _ ::& _ ::& (STSet{}, NTSet _ (notesK :: Notes k), _, _) ::&+ _) -> - updImpl notesK inp (NTBool U.noAnn) varNotes + workOnInstr uInstr $ updImpl notesK inp (NTBool U.noAnn) varNotes (U.UPDATE _, _ ::& _ ::& _ ::& _) -> failWithErr $ UnexpectedType @@ -577,16 +655,16 @@ (U.IF _ _, SNil) -> notEnoughItemsOnStack (U.LOOP is, (NTBool{}, _, _) ::& (rs :: HST rs)) -> do - _ :/ tp <- lift $ typeCheckList is rs - case tp of - subI ::: (o :: HST o) -> do - case eqHST o (sing @('TBool) -:& rs) of - Right Refl -> do - let _ ::& rs' = o - pure $ inp :/ LOOP subI ::: rs' - Left m -> typeCheckInstrErr' uInstr (SomeHST inp) (Just Iteration) m - AnyOutInstr subI -> - pure $ inp :/ LOOP subI ::: rs + preserving (tcList is rs) U.LOOP $ \(_ :/ tp) -> + case tp of + subI ::: (o :: HST o) -> do + case eqHST o (sing @('TBool) -:& rs) of + Right Refl -> do + let _ ::& rs' = o + pure $ inp :/ LOOP subI ::: rs' + Left m -> typeCheckInstrErr' uInstr (SomeHST inp) (Just Iteration) m + AnyOutInstr subI -> + pure $ inp :/ LOOP subI ::: rs (U.LOOP _, _ ::& _ ::& _) -> failWithErr $ UnexpectedType @@ -597,22 +675,22 @@ (U.LOOP_LEFT is, (os@STOr{}, ons, Dict, ovn) ::&+ rs) -> do case deriveNsOr ons ovn of (an :: Notes t, bn :: Notes b, avn, bvn) -> do - withWTPInstr @t $ withWTPInstr @b $ do + withWTPInstr' @t $ withWTPInstr' @b $ do let ait = (an, Dict, avn) ::& rs - _ :/ tp <- lift $ typeCheckList is ait - case tp of - subI ::: o -> do - case (eqHST o (os -:& rs), o) of - (Right Refl, ((ons', Dict, ovn') ::& rs')) -> do - let (_, bn', _, bvn') = deriveNsOr ons' ovn' - br <- onTypeCheckInstrAnnErr uInstr inp - (Just Iteration) - (convergeHSTEl (bn, Dict, bvn) (bn', Dict, bvn')) - pure $ inp :/ LOOP_LEFT subI ::: (br ::& rs') - (Left m, _) -> typeCheckInstrErr' uInstr (SomeHST inp) (Just Iteration) m - AnyOutInstr subI -> do - let br = (bn, Dict, bvn) - pure $ inp :/ LOOP_LEFT subI ::: (br ::& rs) + preserving (tcList is ait) U.LOOP_LEFT $ \(_ :/ tp) -> + case tp of + subI ::: o -> do + case (eqHST o (os -:& rs), o) of + (Right Refl, ((ons', Dict, ovn') ::& rs')) -> do + let (_, bn', _, bvn') = deriveNsOr ons' ovn' + br <- onTypeCheckInstrAnnErr uInstr inp + (Just Iteration) + (convergeHSTEl (bn, Dict, bvn) (bn', Dict, bvn')) + pure $ inp :/ LOOP_LEFT subI ::: (br ::& rs') + (Left m, _) -> typeCheckInstrErr' uInstr (SomeHST inp) (Just Iteration) m + AnyOutInstr subI -> do + let br = (bn, Dict, bvn) + pure $ inp :/ LOOP_LEFT subI ::: (br ::& rs) (U.LOOP_LEFT _, _ ::& _) -> failWithErr $ UnexpectedType @@ -620,12 +698,12 @@ (U.LOOP_LEFT _, _) -> notEnoughItemsOnStack - (U.LAMBDA vn (AsUType (ins :: Notes t)) (AsUType (ons :: Notes u)) is, i) -> do + (U.LAMBDA vn p1@(AsUType (ins :: Notes t)) p2@(AsUType (ons :: Notes u)) is, i) -> do -- further processing is extracted into another function just not to -- litter our main typechecking logic - withWTPInstr @t $ - withWTPInstr @u $ - lamImpl uInstr is vn ins ons i + withWTPInstr' @t $ + withWTPInstr' @u $ + lamImpl (U.LAMBDA vn p1 p2) uInstr is vn ins ons i (U.EXEC vn, ((_ :: Notes t1), _, _) ::& ( STLambda _ _ @@ -633,7 +711,7 @@ , _ , _ ) - ::&+ rs) -> do + ::&+ rs) -> workOnInstr uInstr $ do Refl <- onTypeCheckInstrErr uInstr (SomeHST inp) (Just LambdaArgument) (eqType @t1 @t1') withWTPInstr @t2' $ pure $ inp :/ EXEC ::: ((t2n, Dict, vn) ::& rs) @@ -649,7 +727,7 @@ , NTLambda vann (NTPair _ _ _ (_ :: Notes a) (nb :: Notes b)) sc , _ , _) - ::&+ rs) -> do + ::&+ rs) -> workOnInstr uInstr $ do case NTLambda vann nb sc of (l2n :: Notes ('TLambda t1 t2)) -> withWTPInstr @('TLambda t1 t2) $ do @@ -668,48 +746,57 @@ (U.APPLY _, _) -> notEnoughItemsOnStack (U.DIP is, a ::& s) -> do - typeCheckDipBody uInstr is s $ - \subI t -> pure $ inp :/ DIP subI ::: (a ::& t) + typeCheckDipBody U.DIP uInstr is s + (IllTypedSeq) + (\subI t -> WellTypedSeq $ inp :/ DIP subI ::: (a ::& t)) (U.DIP _is, SNil) -> notEnoughItemsOnStack (U.DIPN nTotal instructions, inputHST) -> go nTotal inputHST <&> \case - TCDipHelper s subI out -> inputHST :/ DIPN s subI ::: out + TCDipHelperErr err rest -> IllTypedSeq err rest + TCDipHelperOk s subI out -> WellTypedSeq $ inputHST :/ DIPN s subI ::: out where go :: forall inp. Typeable inp => Word -> HST inp - -> TypeCheckInstr (TCDipHelper inp) + -> TypeCheckInstrNoExcept (TCDipHelper inp) go n curHST = case (n, curHST) of - (0, _) -> typeCheckDipBody uInstr instructions curHST $ \subI t -> - pure (TCDipHelper SZ subI t) - (_, SNil) -> notEnoughItemsOnStack + (0, _) -> typeCheckDipBody (U.DIPN nTotal) uInstr instructions curHST + (TCDipHelperErr) + (TCDipHelperOk SZ) + (_, SNil) -> do + pos <- ask + let err = TCFailedOnInstr uInstr (SomeHST inp) pos Nothing (Just NotEnoughItemsOnStack) + pure $ TCDipHelperErr err [NonTypedInstr $ U.PrimEx uInstr] (_, hstHead ::& hstTail) -> go (n - 1) hstTail <&> \case - TCDipHelper s subI out -> TCDipHelper (SS s) subI (hstHead ::& out) + TCDipHelperOk s subI out -> TCDipHelperOk (SS s) subI (hstHead ::& out) + TCDipHelperErr err rest -> TCDipHelperErr err rest + (u, v) -> case (u, v) of -- Workaround for not exceeding -fmax-pmcheck-iterations limit - (U.FAILWITH, (_ ::& _)) -> + (U.FAILWITH, (_ ::& _)) -> workOnInstr uInstr $ pure $ inp :/ AnyOutInstr FAILWITH (U.FAILWITH, _) -> notEnoughItemsOnStack - (U.CAST vn (AsUType (castToNotes :: Notes t)), (en, _, evn) ::& rs) -> do - (Refl, _) <- errM $ matchTypes en castToNotes - withWTPInstr @t $ - pure $ inp :/ CAST ::: ((castToNotes, Dict, vn `orAnn` evn) ::& rs) + (U.CAST vn (AsUType (castToNotes :: Notes t)), (en, _, evn) ::& rs) -> + workOnInstr uInstr $ do + (Refl, _) <- errM $ matchTypes en castToNotes + withWTPInstr @t $ + pure $ inp :/ CAST ::: ((castToNotes, Dict, vn `orAnn` evn) ::& rs) where errM :: (MonadReader InstrCallStack m, MonadError TCError m) => Either TCTypeError a -> m a errM = onTypeCheckInstrErr uInstr (SomeHST inp) (Just Cast) (U.CAST _ _, _) -> notEnoughItemsOnStack - (U.RENAME vn, (an, Dict, _) ::& rs) -> + (U.RENAME vn, (an, Dict, _) ::& rs) -> workOnInstr uInstr $ pure $ inp :/ RENAME ::: ((an, Dict, vn) ::& rs) (U.RENAME _, SNil) -> notEnoughItemsOnStack - (U.UNPACK tn vn mt, (NTBytes{}, _, _) ::& rs) -> + (U.UNPACK tn vn mt, (NTBytes{}, _, _) ::& rs) -> workOnInstr uInstr $ withUType mt $ \(tns :: Notes tn) -> do case NTOption tn tns of (ns :: Notes ('TOption t1)) -> withWTPInstr @('TOption t1) $ do @@ -722,7 +809,7 @@ (U.UNPACK {}, SNil) -> notEnoughItemsOnStack - (U.PACK vn, (_ :: Notes a, _, _) ::& rs) -> do + (U.PACK vn, (_ :: Notes a, _, _) ::& rs) -> workOnInstr uInstr $ do Dict <- onScopeCheckInstrErr @a uInstr (SomeHST inp) Nothing $ checkScope @(PackedValScope a) pure $ inp :/ PACK ::: ((starNotes, Dict, vn) ::& rs) @@ -730,13 +817,13 @@ (U.PACK _, SNil) -> notEnoughItemsOnStack (U.CONCAT vn, (NTBytes{}, _, _) ::& (NTBytes{}, _, _) ::& _) -> - concatImpl inp vn + workOnInstr uInstr $ concatImpl inp vn (U.CONCAT vn, (NTString{}, _, _) ::& (NTString{}, _, _) ::& _) -> - concatImpl inp vn + workOnInstr uInstr $ concatImpl inp vn (U.CONCAT vn, (STList STBytes, _, _, _) ::&+ _) -> - concatImpl' inp vn + workOnInstr uInstr $ concatImpl' inp vn (U.CONCAT vn, (STList STString, _, _, _) ::&+ _) -> - concatImpl' inp vn + workOnInstr uInstr $ concatImpl' inp vn (U.CONCAT _, _ ::& _ ::& _) -> failWithErr $ UnexpectedType $ (ExpectByte :| [ExpectByte]) :| @@ -751,10 +838,10 @@ (U.SLICE vn, (NTNat{}, _, _) ::& (NTNat{}, _, _) ::& - (NTString{}, _, _) ::& _) -> sliceImpl inp vn + (NTString{}, _, _) ::& _) -> workOnInstr uInstr $ sliceImpl inp vn (U.SLICE vn, (NTNat{}, _, _) ::& (NTNat{}, _, _) ::& - (NTBytes{}, _, _) ::& _) -> sliceImpl inp vn + (NTBytes{}, _, _) ::& _) -> workOnInstr uInstr $ sliceImpl inp vn (U.SLICE _, _ ::& _ ::& _ ::& _) -> failWithErr $ UnexpectedType @@ -763,7 +850,7 @@ ] (U.SLICE _, _) -> notEnoughItemsOnStack - (U.ISNAT vn', (NTInt{}, _, oldVn) ::& rs) -> do + (U.ISNAT vn', (NTInt{}, _, oldVn) ::& rs) -> workOnInstr uInstr $ do let vn = vn' `orAnn` oldVn pure $ inp :/ ISNAT ::: ((starNotes, Dict, vn) ::& rs) @@ -773,30 +860,37 @@ (U.ISNAT _, SNil)-> notEnoughItemsOnStack -- Type checking is already done inside `addImpl`. - (U.ADD vn, (a, _, _, _) ::&+ (b, _, _, _) ::&+ _) -> addImpl a b inp vn uInstr + (U.ADD vn, (a, _, _, _) ::&+ (b, _, _, _) ::&+ _) -> workOnInstr uInstr $ + addImpl a b inp vn uInstr (U.ADD _, _) -> notEnoughItemsOnStack - (U.SUB vn, (a, _, _, _) ::&+ (b, _, _, _) ::&+ _) -> subImpl a b inp vn uInstr + (U.SUB vn, (a, _, _, _) ::&+ (b, _, _, _) ::&+ _) -> workOnInstr uInstr $ + subImpl a b inp vn uInstr (U.SUB _, _) -> notEnoughItemsOnStack - (U.MUL vn, (a, _, _, _) ::&+ (b, _, _, _) ::&+ _) -> mulImpl a b inp vn uInstr + (U.MUL vn, (a, _, _, _) ::&+ (b, _, _, _) ::&+ _) -> workOnInstr uInstr $ + mulImpl a b inp vn uInstr (U.MUL _, _) -> notEnoughItemsOnStack - (U.EDIV vn, (a, _, _, _) ::&+ (b, _, _, _) ::&+ _) -> edivImpl a b inp vn uInstr + (U.EDIV vn, (a, _, _, _) ::&+ (b, _, _, _) ::&+ _) -> workOnInstr uInstr $ + edivImpl a b inp vn uInstr (U.EDIV _, _) -> notEnoughItemsOnStack - (U.ABS vn, (STInt, _, _, _) ::&+ _) -> unaryArithImpl @Abs ABS inp vn + (U.ABS vn, (STInt, _, _, _) ::&+ _) -> workOnInstr uInstr $ + unaryArithImpl @Abs ABS inp vn (U.ABS _, _ ::& _) -> failWithErr $ UnexpectedType $ (ExpectInt :| []) :| [] (U.ABS _, SNil) -> notEnoughItemsOnStack - (U.NEG vn, (STInt, _, _, _) ::&+ _) -> unaryArithImpl @Neg NEG inp vn - (U.NEG vn, (STNat, _, _, _) ::&+ _) -> unaryArithImpl @Neg NEG inp vn + (U.NEG vn, (STInt, _, _, _) ::&+ _) -> workOnInstr uInstr $ + unaryArithImpl @Neg NEG inp vn + (U.NEG vn, (STNat, _, _, _) ::&+ _) -> workOnInstr uInstr $ + unaryArithImpl @Neg NEG inp vn (U.NEG _, _ ::& _) -> failWithErr $ UnexpectedType $ (ExpectInt :| []) :| @@ -805,21 +899,25 @@ (U.NEG _, SNil) -> notEnoughItemsOnStack (U.LSL vn, (STNat, _, _, _) ::&+ - (STNat, _, _, _) ::&+ _) -> arithImpl @Lsl LSL inp vn uInstr + (STNat, _, _, _) ::&+ _) -> workOnInstr uInstr $ + arithImpl @Lsl LSL inp vn uInstr (U.LSL _, _ ::& _ ::& _) -> failWithErr $ UnexpectedType $ (ExpectNat :| [ExpectNat]) :| [] (U.LSL _, _) -> notEnoughItemsOnStack (U.LSR vn, (STNat, _, _, _) ::&+ - (STNat, _, _, _) ::&+ _) -> arithImpl @Lsr LSR inp vn uInstr + (STNat, _, _, _) ::&+ _) -> workOnInstr uInstr $ + arithImpl @Lsr LSR inp vn uInstr (U.LSR _, _ ::& _ ::& _) -> failWithErr $ UnexpectedType $ (ExpectNat :| [ExpectNat]) :| [] (U.LSR _, _) -> notEnoughItemsOnStack (U.OR vn, (STBool, _, _, _) ::&+ - (STBool, _, _, _) ::&+ _) -> arithImpl @Or OR inp vn uInstr + (STBool, _, _, _) ::&+ _) -> workOnInstr uInstr $ + arithImpl @Or OR inp vn uInstr (U.OR vn, (STNat, _, _, _) ::&+ - (STNat, _, _, _) ::&+ _) -> arithImpl @Or OR inp vn uInstr + (STNat, _, _, _) ::&+ _) -> workOnInstr uInstr $ + arithImpl @Or OR inp vn uInstr (U.OR _, _ ::& _ ::& _) -> failWithErr $ UnexpectedType $ (ExpectBool :| [ExpectBool]) :| @@ -828,11 +926,14 @@ (U.OR _, _) -> notEnoughItemsOnStack (U.AND vn, (STInt, _, _, _) ::&+ - (STNat, _, _, _) ::&+ _) -> arithImpl @And AND inp vn uInstr + (STNat, _, _, _) ::&+ _) -> workOnInstr uInstr $ + arithImpl @And AND inp vn uInstr (U.AND vn, (STNat, _, _, _) ::&+ - (STNat, _, _, _) ::&+ _) -> arithImpl @And AND inp vn uInstr + (STNat, _, _, _) ::&+ _) -> workOnInstr uInstr $ + arithImpl @And AND inp vn uInstr (U.AND vn, (STBool, _, _, _) ::&+ - (STBool, _, _, _) ::&+ _) -> arithImpl @And AND inp vn uInstr + (STBool, _, _, _) ::&+ _) -> workOnInstr uInstr $ + arithImpl @And AND inp vn uInstr (U.AND _, _ ::& _ ::& _) -> failWithErr $ UnexpectedType $ (ExpectInt :| [ExpectNat]) :| @@ -842,9 +943,11 @@ (U.AND _, _) -> notEnoughItemsOnStack (U.XOR vn, (STBool, _, _, _) ::&+ - (STBool, _, _, _) ::&+ _) -> arithImpl @Xor XOR inp vn uInstr + (STBool, _, _, _) ::&+ _) -> workOnInstr uInstr $ + arithImpl @Xor XOR inp vn uInstr (U.XOR vn, (STNat, _, _, _) ::&+ - (STNat, _, _, _) ::&+ _) -> arithImpl @Xor XOR inp vn uInstr + (STNat, _, _, _) ::&+ _) -> workOnInstr uInstr $ + arithImpl @Xor XOR inp vn uInstr (U.XOR _, _ ::& _ ::& _) -> failWithErr $ UnexpectedType $ (ExpectBool :| [ExpectBool]) :| @@ -852,9 +955,12 @@ ] (U.XOR _, _) -> notEnoughItemsOnStack - (U.NOT vn, (STNat, _, _, _) ::&+ _) -> unaryArithImpl @Not NOT inp vn - (U.NOT vn, (STBool, _, _, _) ::&+ _) -> unaryArithImpl @Not NOT inp vn - (U.NOT vn, (STInt, _, _, _) ::&+ _) -> unaryArithImpl @Not NOT inp vn + (U.NOT vn, (STNat, _, _, _) ::&+ _) -> workOnInstr uInstr $ + unaryArithImpl @Not NOT inp vn + (U.NOT vn, (STBool, _, _, _) ::&+ _) -> workOnInstr uInstr $ + unaryArithImpl @Not NOT inp vn + (U.NOT vn, (STInt, _, _, _) ::&+ _) -> workOnInstr uInstr $ + unaryArithImpl @Not NOT inp vn (U.NOT _, _ ::& _) -> failWithErr $ UnexpectedType $ (ExpectNat :| []) :| @@ -868,7 +974,7 @@ ::& (bn :: Notes bT, _, _) ::& rs ) - -> do + -> workOnInstr uInstr $ do case eqType @aT @bT of Right Refl -> do void . errConv $ converge an bn @@ -886,43 +992,49 @@ (U.COMPARE _, _) -> notEnoughItemsOnStack - (U.EQ vn, (NTInt{}, _, _) ::& _) -> unaryArithImpl @Eq' EQ inp vn + (U.EQ vn, (NTInt{}, _, _) ::& _) -> workOnInstr uInstr $ + unaryArithImpl @Eq' EQ inp vn (U.EQ _, _ ::& _) -> failWithErr $ UnexpectedType $ (ExpectInt :| []) :| [] (U.EQ _, SNil) -> notEnoughItemsOnStack - (U.NEQ vn, (NTInt{}, _, _) ::& _) -> unaryArithImpl @Neq NEQ inp vn + (U.NEQ vn, (NTInt{}, _, _) ::& _) -> workOnInstr uInstr $ + unaryArithImpl @Neq NEQ inp vn (U.NEQ _, _ ::& _) -> failWithErr $ UnexpectedType $ (ExpectInt :| []) :| [] (U.NEQ _, SNil) -> notEnoughItemsOnStack - (U.LT vn, (NTInt{}, _, _) ::& _) -> unaryArithImpl @Lt LT inp vn + (U.LT vn, (NTInt{}, _, _) ::& _) -> workOnInstr uInstr $ + unaryArithImpl @Lt LT inp vn (U.LT _, _ ::& _) -> failWithErr $ UnexpectedType $ (ExpectInt :| []) :| [] (U.LT _, SNil) -> notEnoughItemsOnStack - (U.GT vn, (NTInt{}, _, _) ::& _) -> unaryArithImpl @Gt GT inp vn + (U.GT vn, (NTInt{}, _, _) ::& _) -> workOnInstr uInstr $ + unaryArithImpl @Gt GT inp vn (U.GT _, _ ::& _) -> failWithErr $ UnexpectedType $ (ExpectInt :| []) :| [] (U.GT _, SNil) -> notEnoughItemsOnStack - (U.LE vn, (NTInt{}, _, _) ::& _) -> unaryArithImpl @Le LE inp vn + (U.LE vn, (NTInt{}, _, _) ::& _) -> workOnInstr uInstr $ + unaryArithImpl @Le LE inp vn (U.LE _, _ ::& _) -> failWithErr $ UnexpectedType $ (ExpectInt :| []) :| [] (U.LE _, SNil) -> notEnoughItemsOnStack - (U.GE vn, (NTInt{}, _, _) ::& _) -> unaryArithImpl @Ge GE inp vn + (U.GE vn, (NTInt{}, _, _) ::& _) -> workOnInstr uInstr $ + unaryArithImpl @Ge GE inp vn (U.GE _, _ ::& _) -> failWithErr $ UnexpectedType $ (ExpectInt :| []) :| [] (U.GE _, SNil) -> notEnoughItemsOnStack - (U.INT vn, (NTNat{}, _, _) ::& rs) -> + (U.INT vn, (NTNat{}, _, _) ::& rs) -> workOnInstr uInstr $ pure $ inp :/ INT ::: ((starNotes, Dict, vn) ::& rs) (U.INT _, _ ::& _) -> failWithErr $ UnexpectedType $ (ExpectNat :| []) :| [] (U.INT _, SNil) -> notEnoughItemsOnStack - (U.SELF vn fn, _) -> do + (U.SELF vn fn, _) -> workOnInstr uInstr $ do mode <- gets tcMode case mode of TypeCheckValue (value, ty) -> @@ -942,7 +1054,7 @@ error "'SELF' appears in test typechecking." TypeCheckPack -> error "'SELF' appears in packed data." - (U.CONTRACT vn fn mt, (NTAddress{}, _, _) ::& rs) -> + (U.CONTRACT vn fn mt, (NTAddress{}, _, _) ::& rs) -> workOnInstr uInstr $ withUType mt $ \(tns :: Notes t) -> do proofScope <- onScopeCheckInstrErr @t uInstr (SomeHST inp) (Just ContractParameter) $ checkScope @(ParameterScope t) @@ -959,7 +1071,7 @@ (U.TRANSFER_TOKENS vn, ((_ :: Notes p'), _, _) ::& (NTMutez{}, _, _) - ::& (STContract (_ :: Sing p), _, _, _) ::&+ rs) -> do + ::& (STContract (_ :: Sing p), _, _, _) ::&+ rs) -> workOnInstr uInstr $ do proofScope <- onScopeCheckInstrErr @p uInstr (SomeHST inp) (Just ContractParameter) $ checkScope @(ParameterScope p) case (eqType @p @p', proofScope) of @@ -975,7 +1087,7 @@ (U.SET_DELEGATE vn, (STOption STKeyHash, NTOption _ NTKeyHash{}, _, _) - ::&+ rs) -> do + ::&+ rs) -> workOnInstr uInstr $ do pure $ inp :/ SET_DELEGATE ::: ((starNotes, Dict, vn) ::& rs) (U.SET_DELEGATE _, _ ::& _) -> @@ -986,7 +1098,7 @@ (U.CREATE_CONTRACT ovn avn contract, (STOption STKeyHash, NTOption _ (_ :: Notes ('TKeyHash)), _, _) ::&+ (NTMutez{}, _, _) - ::& (gn :: Notes g, Dict, _) ::& rs) -> do + ::& (gn :: Notes g, Dict, _) ::& rs) -> workOnInstr uInstr $ do (SomeContract (Contract (contr :: ContractCode p' g') @@ -1006,69 +1118,70 @@ (U.CREATE_CONTRACT {}, _) -> notEnoughItemsOnStack - (U.IMPLICIT_ACCOUNT vn, (NTKeyHash{}, _, _) ::& rs) -> + (U.IMPLICIT_ACCOUNT vn, (NTKeyHash{}, _, _) ::& rs) -> workOnInstr uInstr $ pure $ inp :/ IMPLICIT_ACCOUNT ::: ((starNotes, Dict, vn) ::& rs) (U.IMPLICIT_ACCOUNT _, _ ::& _) -> failWithErr $ UnexpectedType $ (ExpectKeyHash :| []) :| [] (U.IMPLICIT_ACCOUNT _, SNil) -> notEnoughItemsOnStack - (U.NOW vn, _) -> + (U.NOW vn, _) -> workOnInstr uInstr $ pure $ inp :/ NOW ::: ((starNotes, Dict, vn) ::& inp) - (U.AMOUNT vn, _) -> + (U.AMOUNT vn, _) -> workOnInstr uInstr $ pure $ inp :/ AMOUNT ::: ((starNotes, Dict, vn) ::& inp) - (U.BALANCE vn, _) -> + (U.BALANCE vn, _) -> workOnInstr uInstr $ pure $ inp :/ BALANCE ::: ((starNotes, Dict, vn) ::& inp) (U.CHECK_SIGNATURE vn, (NTKey _, _, _) ::& (NTSignature _, _, _) ::& (NTBytes{}, _, _) ::& rs) -> - pure $ inp :/ CHECK_SIGNATURE ::: ((starNotes, Dict, vn) ::& rs) + workOnInstr uInstr $ + pure $ inp :/ CHECK_SIGNATURE ::: ((starNotes, Dict, vn) ::& rs) (U.CHECK_SIGNATURE _, _ ::& _ ::& _) -> failWithErr $ UnexpectedType $ (ExpectKey :| [ExpectSignature]) :| [] (U.CHECK_SIGNATURE _, _) -> notEnoughItemsOnStack - (U.SHA256 vn, (NTBytes{}, _, _) ::& rs) -> + (U.SHA256 vn, (NTBytes{}, _, _) ::& rs) -> workOnInstr uInstr $ pure $ inp :/ SHA256 ::: ((starNotes, Dict, vn) ::& rs) (U.SHA256 _, _ ::& _) -> failWithErr $ UnexpectedType $ (ExpectByte :| []) :| [] (U.SHA256 _, SNil) -> notEnoughItemsOnStack - (U.SHA512 vn, (NTBytes{}, _, _) ::& rs) -> + (U.SHA512 vn, (NTBytes{}, _, _) ::& rs) -> workOnInstr uInstr $ pure $ inp :/ SHA512 ::: ((starNotes, Dict, vn) ::& rs) (U.SHA512 _, _ ::& _) -> failWithErr $ UnexpectedType $ (ExpectByte :| []) :| [] (U.SHA512 _, SNil) -> notEnoughItemsOnStack - (U.BLAKE2B vn, (NTBytes{}, _, _) ::& rs) -> + (U.BLAKE2B vn, (NTBytes{}, _, _) ::& rs) -> workOnInstr uInstr $ pure $ inp :/ BLAKE2B ::: ((starNotes, Dict, vn) ::& rs) (U.BLAKE2B _, _ ::& _) -> failWithErr $ UnexpectedType $ (ExpectByte :| []) :| [] (U.BLAKE2B _, SNil) -> notEnoughItemsOnStack - (U.HASH_KEY vn, (NTKey{}, _, _) ::& rs) -> + (U.HASH_KEY vn, (NTKey{}, _, _) ::& rs) -> workOnInstr uInstr $ pure $ inp :/ HASH_KEY ::: ((starNotes, Dict, vn) ::& rs) (U.HASH_KEY _, _ ::& _) -> failWithErr $ UnexpectedType $ (ExpectKey :| []) :| [] (U.HASH_KEY _, SNil) -> notEnoughItemsOnStack - (U.SOURCE vn, _) -> + (U.SOURCE vn, _) -> workOnInstr uInstr $ pure $ inp :/ SOURCE ::: ((starNotes, Dict, vn) ::& inp) - (U.SENDER vn, _) -> + (U.SENDER vn, _) -> workOnInstr uInstr $ pure $ inp :/ SENDER ::: ((starNotes, Dict, vn) ::& inp) - (U.ADDRESS vn, (NTContract{}, _, _) ::& rs) -> + (U.ADDRESS vn, (NTContract{}, _, _) ::& rs) -> workOnInstr uInstr $ pure $ inp :/ ADDRESS ::: ((starNotes, Dict, vn) ::& rs) (U.ADDRESS _, _ ::& _) -> failWithErr $ UnexpectedType $ (ExpectContract :| []) :| [] (U.ADDRESS _, SNil) -> notEnoughItemsOnStack - (U.CHAIN_ID vn, _) -> + (U.CHAIN_ID vn, _) -> workOnInstr uInstr $ pure $ inp :/ CHAIN_ID ::: ((starNotes, Dict, vn) ::& inp) -- Could not get rid of the catch all clause due to this warning: @@ -1080,15 +1193,25 @@ i -> error $ "Pattern matches should be exhuastive, but instead got: " <> show i where - withWTPInstr :: forall t a. SingI t => (WellTyped t => TypeCheckInstr a) -> TypeCheckInstr a - withWTPInstr fn = withWTPInstr_ @t uInstr (SomeHST inp) fn + withWTPInstr' + :: forall t inp. SingI t + => (WellTyped t => TypeCheckInstrNoExcept (TypeCheckedSeq inp)) + -> TypeCheckInstrNoExcept (TypeCheckedSeq inp) + withWTPInstr' = withWTPInstr'_ @t uInstr (SomeHST inp) - failWithErr :: (MonadReader InstrCallStack m, MonadError TCError m) => TCTypeError -> m a - failWithErr = typeCheckInstrErr' uInstr (SomeHST inp) Nothing + withWTPInstr + :: forall t a. SingI t => (WellTyped t => TypeCheckInstr a) -> TypeCheckInstr a + withWTPInstr = withWTPInstr_ @t uInstr (SomeHST inp) - notEnoughItemsOnStack :: (MonadReader InstrCallStack m, MonadError TCError m) => m a + failWithErr :: TCTypeError -> TypeCheckInstrNoExcept (TypeCheckedSeq a) + failWithErr = workOnInstr uInstr . typeCheckInstrErr' uInstr (SomeHST inp) Nothing + + notEnoughItemsOnStack :: TypeCheckInstrNoExcept (TypeCheckedSeq a) notEnoughItemsOnStack = failWithErr NotEnoughItemsOnStack + notEnoughItemsOnStack' :: TypeCheckInstr a + notEnoughItemsOnStack' = typeCheckInstrErr' uInstr (SomeHST inp) Nothing NotEnoughItemsOnStack + -- | Helper function for two-branch if where each branch is given a single -- value. genericIf @@ -1099,29 +1222,31 @@ Instr bfi s' -> Instr (cond ': rs) s' ) - -> ([U.ExpandedOp] -> [U.ExpandedOp] -> U.ExpandedInstr) + -> (forall op. [op] -> [op] -> U.InstrAbstract op) -> [U.ExpandedOp] -> [U.ExpandedOp] -> HST bti -> HST bfi -> HST (cond ': rs) - -> TypeCheckInstr (SomeInstr (cond ': rs)) + -> TypeCheckInstrNoExcept (TypeCheckedSeq (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 <- onTypeCheckInstrErr instr (SomeHST i) (Just If) - $ eqHST po qo - o <- onTypeCheckInstrAnnErr instr i (Just If) (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) + let cons1 opsT = mCons opsT (map (IllTypedOp . NonTypedInstr) mbf) + preserving' (tcList mbt bti) cons1 $ \tInstr@(_ :/ pinstr) -> do + let cons2 opsF = mCons [someInstrToOp tInstr] opsF + preserving (tcList mbf bfi) cons2 $ \(_ :/ qinstr) -> do + fmap (i :/) $ case (pinstr, qinstr) of + (p ::: po, q ::: qo) -> do + let instr = mCons mbt mbf + Refl <- onTypeCheckInstrErr instr (SomeHST i) (Just If) + $ eqHST po qo + o <- onTypeCheckInstrAnnErr instr i (Just If) (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 . @@ -1129,26 +1254,27 @@ , WellTyped (MapOpInp c) , Typeable (MapOpRes c) ) - => Notes (MapOpInp c) + => ([TypeCheckedOp] -> TypeCheckedInstr) + -> Notes (MapOpInp c) -> U.ExpandedInstr -> [U.ExpandedOp] -> HST (c ': rs) -> (forall v' . (KnownT v') => Notes v' -> HST rs -> TypeCheckInstr (HST (MapOpRes c v' ': rs))) - -> TypeCheckInstr (SomeInstr (c ': rs)) -mapImpl vn instr mp i@(_ ::& rs) mkRes = do - _ :/ subp <- lift $ typeCheckList mp ((vn, Dict, def) ::& rs) - case subp of - sub ::: subo -> - case subo of - (bn, _, _bvn) ::& rs' -> do - Refl <- onTypeCheckInstrErr instr (SomeHST i) (Just Iteration) - $ eqHST rs rs' - x <- mkRes bn rs' - pure $ i :/ MAP sub ::: x - _ -> typeCheckInstrErr instr (SomeHST i) (Just Iteration) - AnyOutInstr _ -> - typeCheckInstrErr' instr (SomeHST i) (Just Iteration) CodeAlwaysFails + -> TypeCheckInstrNoExcept (TypeCheckedSeq (c ': rs)) +mapImpl cons vn instr mp i@(_ ::& rs) mkRes = do + preserving (tcList mp ((vn, Dict, def) ::& rs)) cons $ \(_ :/ subp) -> + case subp of + sub ::: subo -> + case subo of + (bn, _, _bvn) ::& rs' -> do + Refl <- onTypeCheckInstrErr instr (SomeHST i) (Just Iteration) + $ eqHST rs rs' + x <- mkRes bn rs' + pure $ i :/ MAP sub ::: x + _ -> typeCheckInstrErr instr (SomeHST i) (Just Iteration) + AnyOutInstr _ -> + typeCheckInstrErr' instr (SomeHST i) (Just Iteration) CodeAlwaysFails iterImpl :: forall c rs . @@ -1159,17 +1285,16 @@ -> U.ExpandedInstr -> [U.ExpandedOp] -> HST (c ': rs) - -> TypeCheckInstr (SomeInstr (c ': rs)) + -> TypeCheckInstrNoExcept (TypeCheckedSeq (c ': rs)) iterImpl en instr mp i@((_, _, lvn) ::& rs) = do let evn = deriveVN "elt" lvn - _ :/ subp <- - case mp of - [] -> typeCheckInstrErr' instr (SomeHST i) (Just Iteration) EmptyCode - _ -> typeCheckImpl typeCheckInstr mp ((en, Dict, evn) ::& rs) - case subp of + let tcAction = case mp of + [] -> workOnInstr instr + (typeCheckInstrErr' instr (SomeHST i) (Just Iteration) EmptyCode) + _ -> typeCheckImpl typeCheckInstr mp ((en, Dict, evn) ::& rs) + preserving tcAction U.ITER $ \(_ :/ subp) -> case subp of subI ::: o -> do - Refl <- onTypeCheckInstrErr instr (SomeHST i) (Just Iteration) - $ eqHST o rs + Refl <- onTypeCheckInstrErr instr (SomeHST i) (Just Iteration) $ eqHST o rs pure $ i :/ ITER subI ::: o AnyOutInstr _ -> typeCheckInstrErr' instr (SomeHST i) (Just Iteration) CodeAlwaysFails @@ -1179,29 +1304,31 @@ ( WellTyped it, WellTyped ot , Typeable ts ) - => U.ExpandedInstr + => ([TypeCheckedOp] -> TypeCheckedInstr) + -> U.ExpandedInstr -> [U.ExpandedOp] -> VarAnn -> Notes it -> Notes ot -> HST ts - -> TypeCheckInstr (SomeInstr ts) -lamImpl instr is vn ins ons i = do - whenJust (getFirst $ foldMap hasSelf is) $ \selfInstr -> - typeCheckInstrErr' instr (SomeHST i) (Just LambdaCode) $ InvalidInstruction selfInstr - _ :/ lamI <- lift $ typeCheckList is ((ins, Dict, def) ::& SNil) - let lamNotes onsr = NTLambda def ins onsr - let lamSt onsr = (lamNotes onsr, Dict, 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 (Just LambdaCode) (converge ons ons') - pure (LAMBDA (VLam $ RfNormal lam) ::: lamSt onsr) - Left m -> typeCheckInstrErr' instr (SomeHST i) (Just LambdaCode) m - AnyOutInstr lam -> - pure (LAMBDA (VLam $ RfAlwaysFails lam) ::: lamSt ons) + -> TypeCheckInstrNoExcept (TypeCheckedSeq ts) +lamImpl cons instr is vn ins ons i = + guarding_ instr + (whenJust (getFirst $ foldMap hasSelf is) $ \selfInstr -> + typeCheckInstrErr' instr (SomeHST i) (Just LambdaCode) $ InvalidInstruction selfInstr) $ + preserving (tcList is ((ins, Dict, def) ::& SNil)) cons $ \(_ :/ lamI) -> do + let lamNotes onsr = NTLambda def ins onsr + let lamSt onsr = (lamNotes onsr, Dict, 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 (Just LambdaCode) (converge ons ons') + pure (LAMBDA (VLam $ RfNormal lam) ::: lamSt onsr) + Left m -> typeCheckInstrErr' instr (SomeHST i) (Just LambdaCode) m + AnyOutInstr lam -> + pure (LAMBDA (VLam $ RfAlwaysFails lam) ::: lamSt ons) where hasSelf :: U.ExpandedOp -> First U.ExpandedInstr hasSelf = everything (<>) @@ -1218,27 +1345,37 @@ -- Helper data type we use to typecheck DIPN. data TCDipHelper inp where - TCDipHelper :: + TCDipHelperOk :: forall (n :: Peano) inp out s s'. (Typeable out, ConstraintDIPN n inp out s s') => Sing n -> Instr s s' -> HST out -> TCDipHelper inp + TCDipHelperErr :: TCError -> [IllTypedInstr] -> TCDipHelper inp -typeCheckDipBody :: - forall inp r. Typeable inp - => U.ExpandedInstr +typeCheckDipBody + :: Typeable inp + => ([TypeCheckedOp] -> TypeCheckedInstr) + -> 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 _ -> - -- This may seem like we throw error because of despair, but in fact, - -- the reference implementation seems to behave exactly in this way - - -- if output stack of code block within @DIP@ occurs to be any, an - -- error "FAILWITH must be at tail position" is raised. - -- It is not allowed even in `DIP 0`. - typeCheckInstrErr' mainInstr (SomeHST inputHST) (Just DipCode) CodeAlwaysFails - subI ::: t -> callback subI t + -> (TCError -> [IllTypedInstr] -> r) + -> (forall out. Typeable out => Instr inp out -> HST out -> r) + -> TypeCheckInstrNoExcept r +typeCheckDipBody cons mainInstr instructions inputHST onErr onOk = do + listRes <- lift $ typeCheckListNoExcept instructions inputHST + pos <- ask + pure $ listRes & tcsEither + (\tcOps err -> onErr err [SemiTypedInstr $ cons tcOps]) + (\someInstr@(_ :/ iAndOut) -> case iAndOut of + AnyOutInstr _ -> + -- This may seem like we throw error because of despair, but in fact, + -- the reference implementation seems to behave exactly in this way - + -- if output stack of code block within @DIP@ occurs to be any, an + -- error "FAILWITH must be at tail position" is raised. + -- It is not allowed even in `DIP 0`. + let err = TCFailedOnInstr mainInstr + (SomeHST inputHST) + pos + (Just DipCode) + (Just CodeAlwaysFails) + in onErr err [SemiTypedInstr $ cons [someInstrToOp someInstr]] + subI ::: t -> onOk subI t) diff --git a/src/Michelson/TypeCheck/TypeCheck.hs b/src/Michelson/TypeCheck/TypeCheck.hs --- a/src/Michelson/TypeCheck/TypeCheck.hs +++ b/src/Michelson/TypeCheck/TypeCheck.hs @@ -6,13 +6,24 @@ ( TcInstrHandler , TcOriginatedContracts , TcResult - , TypeCheckEnv (..) + , TypeCheckEnv(..) + , TypeCheckOptions(..) , TypeCheck + , TypeCheckNoExcept , runTypeCheck , TypeCheckInstr + , TypeCheckInstrNoExcept , runTypeCheckIsolated , runTypeCheckInstrIsolated - , mapTCError + , liftNoExcept + , liftNoExcept' + , throwingTCError + , throwingTCError' + , preserving + , preserving' + , guarding + , guarding_ + , tcEither , tcExtFramesL , tcModeL @@ -22,15 +33,18 @@ , mkSomeParamTypeUnsafe ) where -import Control.Monad.Except (withExceptT) -import Control.Monad.Reader (mapReaderT) -import Data.Default (def) + +import Control.Monad.Except (throwError) +import Data.Default (Default(..)) import Data.Singletons (Sing) import Fmt (Buildable, build, pretty) import qualified Text.Show import Michelson.ErrorPos (InstrCallStack) import Michelson.TypeCheck.Error (TCError(..), TCTypeError(..)) +import Michelson.TypeCheck.TypeCheckedSeq + (IllTypedInstr(..), TypeCheckedInstr, TypeCheckedOp(..), TypeCheckedSeq(..), someInstrToOp, + tcsEither) import Michelson.TypeCheck.Types import qualified Michelson.Typed as T import qualified Michelson.Untyped as U @@ -38,9 +52,16 @@ import Util.Lens type TypeCheck = - ExceptT TCError - (State TypeCheckEnv) + (ReaderT TypeCheckOptions + (ExceptT TCError + (State TypeCheckEnv))) +-- | A non-throwing alternative for @TypeCheck@. Mainly meant to be used for +-- construction of a partially typed tree (see @TypeCheckedSeq@). +type TypeCheckNoExcept = + (ReaderT TypeCheckOptions + (State TypeCheckEnv)) + data SomeParamType = forall t. (T.ParameterScope t) => SomeParamType (Sing t) (T.ParamNotes t) @@ -96,10 +117,20 @@ , tcMode :: ~TypeCheckMode } +data TypeCheckOptions = TypeCheckOptions + { tcVerbose :: Bool -- ^ Whether to add stack type comments after every + -- instruction a la tezos-client. + } + +instance Default TypeCheckOptions where + def = TypeCheckOptions{ tcVerbose = False } + makeLensesWith postfixLFields ''TypeCheckEnv -runTypeCheck :: TypeCheckMode -> TypeCheck a -> Either TCError a -runTypeCheck mode = evaluatingState (TypeCheckEnv [] mode) . runExceptT +runTypeCheck :: TypeCheckMode -> TypeCheckOptions -> TypeCheck a -> Either TCError a +runTypeCheck mode options = evaluatingState (TypeCheckEnv [] mode) + . runExceptT + . usingReaderT options -- | Run type checker as if it worked isolated from other world - -- no access to environment of the current contract is allowed. @@ -110,22 +141,108 @@ -- contract which is being typechecked (because there is no contract -- that we are typechecking). runTypeCheckIsolated :: TypeCheck a -> Either TCError a -runTypeCheckIsolated = runTypeCheck TypeCheckTest +runTypeCheckIsolated = runTypeCheck TypeCheckTest def type TcResult inp = Either TCError (SomeInstr inp) type TypeCheckInstr = - ReaderT InstrCallStack TypeCheck + ReaderT InstrCallStack TypeCheck +type TypeCheckInstrNoExcept = + ReaderT InstrCallStack TypeCheckNoExcept + -- | Similar to 'runTypeCheckIsolated', but for 'TypeCheckInstr.' runTypeCheckInstrIsolated :: TypeCheckInstr a -> Either TCError a -runTypeCheckInstrIsolated = - runTypeCheckIsolated . flip runReaderT def +runTypeCheckInstrIsolated = runTypeCheckIsolated . flip runReaderT def --- | Run 'TypeCheckInstr' and modify thrown errors using given functions. -mapTCError :: (TCError -> TCError) -> TypeCheckInstr a -> TypeCheckInstr a -mapTCError f = mapReaderT (withExceptT f) +liftNoExcept :: TypeCheckInstrNoExcept a -> TypeCheckInstr a +liftNoExcept action = (pure action) + <**> (usingReaderT <$> ask) + <**> (usingReaderT <$> lift ask) + <**> (evaluatingState <$> get) +liftNoExcept' :: TypeCheckNoExcept a -> TypeCheck a +liftNoExcept' action = (pure action) + <**> (usingReaderT <$> ask) + <**> (evaluatingState <$> get) + +throwingTCError + :: TypeCheckInstrNoExcept (TypeCheckedSeq inp) -> TypeCheckInstr (SomeInstr inp) +throwingTCError action = liftNoExcept action + >>= tcsEither (const throwError) (pure) + +throwingTCError' + :: TypeCheckNoExcept (TypeCheckedSeq inp) -> TypeCheck (SomeInstr inp) +throwingTCError' action = liftNoExcept' action + >>= tcsEither (const throwError) (pure) + +tcEither + :: (TCError -> TypeCheckInstrNoExcept a) -- ^ Call this if the action throws + -> (b -> TypeCheckInstrNoExcept a) -- ^ Call this if it doesn't + -> TypeCheckInstr b -- ^ The action to perform + -> TypeCheckInstrNoExcept a -- ^ A non-throwing action +tcEither onErr onOk action = do + res <- (pure action) + <**> (usingReaderT <$> ask) + <**> (usingReaderT <$> lift ask) + <**> (pure runExceptT) + <**> (evaluatingState <$> get) + either onErr onOk res + +-- | Perform a throwing action on an acquired instruction. Preserve the acquired +-- result by embedding it into a type checking tree with a specified parent +-- instruction. +preserving + :: TypeCheckInstrNoExcept (TypeCheckedSeq inp) + -- ^ Acquiring computation + -> ([TypeCheckedOp] -> TypeCheckedInstr) + -- ^ The parent instruction constructor + -> (SomeInstr inp -> TypeCheckInstr (SomeInstr inp')) + -- ^ The throwing action + -> TypeCheckInstrNoExcept (TypeCheckedSeq inp') +preserving acquire con action = preserving' acquire con + (\instr -> action instr & tcEither + (\err -> pure $ IllTypedSeq err [SemiTypedInstr $ con [someInstrToOp instr]]) + (pure . WellTypedSeq)) + +-- | Perform a non-throwing action on an acquired instruction. Preserve the +-- acquired result even if the action does not succeed. Embed the result into a +-- type checking tree with a specified parent instruction. +preserving' + :: TypeCheckInstrNoExcept (TypeCheckedSeq inp) + -- ^ Acquiring computation + -> ([TypeCheckedOp] -> TypeCheckedInstr) + -- ^ The parent instruction constructor + -> (SomeInstr inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp')) + -- ^ The action + -> TypeCheckInstrNoExcept (TypeCheckedSeq inp') +preserving' acquire con action = + acquire >>= tcsEither + (\tcOps err -> pure $ IllTypedSeq err [SemiTypedInstr $ con tcOps]) + (action) + +-- | Acquire a resource. If successfully, call a follow-up action on it, +-- otherwise embed the error into a type checking tree along with a specified +-- untyped instruction. +guarding + :: U.ExpandedInstr -- ^ Untyped instruction + -> TypeCheckInstr a -- ^ Acquiring computation + -> (a -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)) -- ^ Follow-up action + -> TypeCheckInstrNoExcept (TypeCheckedSeq inp) +guarding instr cond action = do + cond & tcEither + (\err -> pure $ IllTypedSeq err [NonTypedInstr $ U.PrimEx instr]) + (action) + +-- | Same as @guarding@ but doesn't pass an acquired result to a follow-up +-- action. +guarding_ + :: U.ExpandedInstr + -> TypeCheckInstr a + -> TypeCheckInstrNoExcept (TypeCheckedSeq inp) + -> TypeCheckInstrNoExcept (TypeCheckedSeq inp) +guarding_ instr cond action = guarding instr cond (const action) + -- pva701: it's really painful to add arguments to TcInstrHandler -- due to necessity to refactor @typeCheckInstr@. -- Also functions which are being called from @typeCheckInstr@ would @@ -135,4 +252,4 @@ = forall inp. (Typeable inp, HasCallStack) => U.ExpandedInstr -> HST inp - -> TypeCheckInstr (SomeInstr inp) + -> TypeCheckInstrNoExcept (TypeCheckedSeq inp) diff --git a/src/Michelson/TypeCheck/TypeCheckedOp.hs b/src/Michelson/TypeCheck/TypeCheckedOp.hs new file mode 100644 --- /dev/null +++ b/src/Michelson/TypeCheck/TypeCheckedOp.hs @@ -0,0 +1,62 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +-- This module provides data types for representing partially typed +-- instructions. +module Michelson.TypeCheck.TypeCheckedOp + ( TypeCheckedInstr + , TypeCheckedOp(..) + , IllTypedInstr(..) + , someInstrToOp + ) where + +import Data.Typeable (cast) + +import Michelson.Printer.Util (RenderDoc(..), renderOpsListNoBraces) +import Michelson.TypeCheck.Types (HST(..), SomeInstr(..), SomeInstrOut(..)) +import Michelson.Typed.Convert (instrToOps) +import Michelson.Typed.Instr (Instr) +import Michelson.Untyped.Instr (ExpandedOp, InstrAbstract(..)) +import Util.TH (deriveGADTNFData) + +-- | Represents a root of a partially typed operation tree. +type TypeCheckedInstr = InstrAbstract TypeCheckedOp + +-- | Represents nodes of a partially typed operation tree. +data TypeCheckedOp where + -- | Constructs well-typed node. + WellTypedOp :: (Typeable inp, Typeable out) => Instr inp out -> TypeCheckedOp + -- | Constructs ill-typed node which might in turn contain well-typed and + -- non-typed operations. + IllTypedOp :: IllTypedInstr -> TypeCheckedOp + +instance Eq TypeCheckedOp where + WellTypedOp i1 == WellTypedOp i2 = cast i1 == Just i2 + IllTypedOp i1 == IllTypedOp i2 = i1 == i2 + _ == _ = False + +-- | Represents a non-well-typed operation +data IllTypedInstr + = SemiTypedInstr TypeCheckedInstr -- ^ Constructs a partialy typed operation. + | NonTypedInstr ExpandedOp -- ^ Constructs a completely untyped operation. + deriving stock (Eq, Generic) + +deriving anyclass instance NFData TypeCheckedOp => NFData IllTypedInstr + +instance RenderDoc TypeCheckedOp where + renderDoc _ (WellTypedOp instr) = renderOpsListNoBraces False (instrToOps instr) + renderDoc pn (IllTypedOp (SemiTypedInstr instr)) = renderDoc pn instr + renderDoc pn (IllTypedOp (NonTypedInstr op)) = renderDoc pn op + +-- | Makes a well-typed node out of `SomeInstr` +someInstrToOp :: SomeInstr inp -> TypeCheckedOp +someInstrToOp (hst :/ rest) = case hst of + SNil -> go rest + (::&){} -> go rest + where + go :: forall inp. Typeable inp => SomeInstrOut inp -> TypeCheckedOp + go (i ::: _) = WellTypedOp i + go (AnyOutInstr i) = WellTypedOp (i @'[]) + +$(deriveGADTNFData ''TypeCheckedOp) diff --git a/src/Michelson/TypeCheck/TypeCheckedSeq.hs b/src/Michelson/TypeCheck/TypeCheckedSeq.hs new file mode 100644 --- /dev/null +++ b/src/Michelson/TypeCheck/TypeCheckedSeq.hs @@ -0,0 +1,51 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +-- | This module provides a data type for representing a partially typed +-- sequence of instructions. +-- +-- It is needed to represent the fact that there can only be one well-typed node +-- in a sequence and it is the first one. Also, it serves its role to remove +-- @TCError@ usage from @TypeCheckedOp@. +module Michelson.TypeCheck.TypeCheckedSeq + ( TypeCheckedInstr + , TypeCheckedOp(..) + , IllTypedInstr(..) + , TypeCheckedSeq(..) + , tcsEither + , seqToOps + , someInstrToOp + ) where + +import Michelson.TypeCheck.Error (TCError) +import Michelson.TypeCheck.TypeCheckedOp + (IllTypedInstr(..), TypeCheckedInstr, TypeCheckedOp(..), someInstrToOp) +import Michelson.TypeCheck.Types (SomeInstr(..)) + +-- | Represents a partiall typed sequence of instructions. +data TypeCheckedSeq inp + -- | A fully well-typed sequence. + = WellTypedSeq (SomeInstr inp) + -- | A well-typed prefix followed by some error and semi-typed instructions. + | MixedSeq (SomeInstr inp) TCError [IllTypedInstr] + -- | There is no well-typed prefix, only an error and semi-typed instructions. + | IllTypedSeq TCError [IllTypedInstr] + +seqToOps :: TypeCheckedSeq inp -> [TypeCheckedOp] +seqToOps = \case + WellTypedSeq instr -> [someInstrToOp instr] + MixedSeq instr _ tail' -> someInstrToOp instr : map IllTypedOp tail' + IllTypedSeq _ tail' -> map IllTypedOp tail' + +-- | Case analysis for @TypeCheckedSeq@. +tcsEither + :: ([TypeCheckedOp] -> TCError -> a) + -- ^ On error, with all already typechecked operations + -> (SomeInstr inp -> a) -- ^ On well-typed instruction + -> TypeCheckedSeq inp -- ^ The sequence to dispatch on + -> a +tcsEither onErr onInstr v = case v of + WellTypedSeq instr -> onInstr instr + MixedSeq _ err _ -> onErr (seqToOps v) err + IllTypedSeq err _ -> onErr (seqToOps v) err diff --git a/src/Michelson/TypeCheck/Types.hs b/src/Michelson/TypeCheck/Types.hs --- a/src/Michelson/TypeCheck/Types.hs +++ b/src/Michelson/TypeCheck/Types.hs @@ -18,13 +18,15 @@ , withWTPm , unsafeWithWTP , mapSomeContract + , mapSomeInstr + , mapSomeInstrOut , noBoundVars ) where import Data.Constraint (Dict(..)) import qualified Data.Map.Lazy as Map import Data.Singletons (Sing, SingI(..), demote) -import Fmt (Buildable(..), Builder, (+|), (|+)) +import Fmt (Buildable(..), Builder, (+|), (|+), pretty) import Prelude hiding (EQ, GT, LT) import qualified Text.Show @@ -164,6 +166,19 @@ (:/) :: HST inp -> SomeInstrOut inp -> SomeInstr inp infix 8 :/ +mapSomeInstrOut + :: (forall out. Instr inp out -> Instr inp' out) + -> SomeInstrOut inp + -> SomeInstrOut inp' +mapSomeInstrOut f (i ::: out) = f i ::: out +mapSomeInstrOut f (AnyOutInstr i) = AnyOutInstr (f i) + +mapSomeInstr + :: (forall out. Instr inp out -> Instr inp out) + -> SomeInstr inp + -> SomeInstr inp +mapSomeInstr f (inp :/ instrAndOut) = inp :/ mapSomeInstrOut f instrAndOut + instance Show (ExtInstr inp) => Show (SomeInstr inp) where show (inp :/ out) = show inp <> " -> " <> show out @@ -204,6 +219,11 @@ -- | Error type for when a value is not well-typed. data NotWellTyped = NotWellTyped T +instance Buildable NotWellTyped where + build (NotWellTyped t) = + "Given type is not well typed because it has an non-comparable type in it: \ + \'" <> (build t) <> "', where a comparable type is required" + fromEDict :: Either e (Dict a) -> (a => Either e (Dict b)) -> Either e (Dict b) fromEDict ma b = ma >>= (\Dict -> b) @@ -257,12 +277,10 @@ withWTPm :: forall t m a. (MonadFail m, SingI t) => (WellTyped t => m a) -> m a withWTPm a = case getWTP @t of Right Dict -> a - Left (NotWellTyped t) -> - fail ("This type is not well typed because it has an non-comparable type in it: '" <> (show t) <> - "', where a comparable type is required") + Left e -> fail (pretty e) -- | Similar to @withWTPm@ but is mean to be used within tests. unsafeWithWTP :: forall t a. SingI t => (WellTyped t => a) -> a unsafeWithWTP fn = case getWTP @t of Right Dict -> fn - Left (NotWellTyped t) -> error $ "Type is not well typed: " <> (show t) + Left e -> error $ pretty e diff --git a/src/Michelson/TypeCheck/Value.hs b/src/Michelson/TypeCheck/Value.hs --- a/src/Michelson/TypeCheck/Value.hs +++ b/src/Michelson/TypeCheck/Value.hs @@ -19,11 +19,11 @@ import Michelson.Text import Michelson.TypeCheck.Error (TCError(..), TCTypeError(..)) import Michelson.TypeCheck.Helpers -import Michelson.TypeCheck.TypeCheck (SomeParamType(..), TcInstrHandler, TcOriginatedContracts, TypeCheckInstr) +import Michelson.TypeCheck.TypeCheck + (SomeParamType(..), TcInstrHandler, TcOriginatedContracts, TypeCheckInstr, throwingTCError) import Michelson.TypeCheck.Types import Michelson.Typed - (EpAddress(..), KnownT, Notes(..), SingT(..), Value'(..), - fromSingT, starNotes) + (EpAddress(..), KnownT, Notes(..), SingT(..), Value'(..), fromSingT, starNotes) import qualified Michelson.Typed as T import qualified Michelson.Untyped as U import Tezos.Address (Address(..)) @@ -168,7 +168,9 @@ U.ValueNil -> pure [] U.ValueLambda mp -> pure $ toList mp _ -> tcFailedOnValue v (demote @ty) "unexpected value" Nothing - _ :/ instr <- withWTP @it uvalue $ typeCheckImpl tcDo mp ((starNotes @it, Dict, def) ::& SNil) + _ :/ instr <- + withWTP @it uvalue $ throwingTCError $ + typeCheckImpl tcDo mp ((starNotes @it, Dict, def) ::& SNil) case instr of lam ::: (lo :: HST lo) -> withWTP @ot uvalue $ do case eqHST1 @ot lo of diff --git a/src/Michelson/Typed/Annotation.hs b/src/Michelson/Typed/Annotation.hs --- a/src/Michelson/Typed/Annotation.hs +++ b/src/Michelson/Typed/Annotation.hs @@ -49,7 +49,7 @@ -- -- Each constructor corresponds to exactly one constructor of 'T' -- and holds all type and field annotations that can be attributed to a --- Michelson type corrspoding to @t@. +-- Michelson type corresponding to @t@. data Notes t where NTKey :: TypeAnn -> Notes 'TKey NTUnit :: TypeAnn -> Notes 'TUnit diff --git a/src/Michelson/Typed/Convert.hs b/src/Michelson/Typed/Convert.hs --- a/src/Michelson/Typed/Convert.hs +++ b/src/Michelson/Typed/Convert.hs @@ -5,20 +5,24 @@ {-# OPTIONS_GHC -fno-warn-orphans #-} module Michelson.Typed.Convert - ( convertContractCode + ( convertParamNotes + , convertContractCode , convertContract , instrToOps , untypeValue -- Helper for generating documentation , sampleValueFromUntype + + -- * Misc + , flattenEntrypoints ) where import Data.Constraint (Dict(..)) import qualified Data.Map as Map import qualified Data.Set as Set import Data.Singletons (Sing, demote) -import Fmt (Buildable(..), pretty) +import Fmt (Buildable(..), fmt, listF, pretty) import Michelson.Text import Michelson.Typed.Aliases @@ -31,12 +35,15 @@ import Michelson.Typed.T (T(..)) import Michelson.Typed.Value import qualified Michelson.Untyped as U -import Tezos.Core - (mformatChainId, parseChainId, timestampFromSeconds, unMutez, unsafeMkMutez) +import Tezos.Core (mformatChainId, parseChainId, timestampFromSeconds, unMutez, unsafeMkMutez) import Tezos.Crypto import Util.Peano import Util.Typeable +convertParamNotes :: SingI cp => ParamNotes cp -> U.ParameterType +convertParamNotes (ParamNotes notes rootAnn) = + U.ParameterType (mkUType notes) rootAnn + convertContractCode :: forall param store . (SingI param, SingI store) => ContractCode param store -> U.Contract @@ -53,8 +60,7 @@ => Contract param store -> U.Contract convertContract fc = let c = convertContractCode (cCode fc) - in c { U.contractParameter = U.ParameterType (mkUType (pnNotes $ cParamNotes fc)) - (pnRootAnn (cParamNotes fc)) + in c { U.contractParameter = convertParamNotes (cParamNotes fc) , U.contractStorage = mkUType (cStoreNotes fc) , U.entriesOrder = cEntriesOrder fc } @@ -318,7 +324,7 @@ U.SLICE _ -> U.SLICE va U.ISNAT _ -> U.ISNAT va U.ADD _ -> U.ADD va - U.SUB _ -> U.MUL va + U.SUB _ -> U.SUB va U.MUL _ -> U.MUL va U.EDIV _ -> U.EDIV va U.ABS _ -> U.ABS va @@ -332,9 +338,10 @@ U.COMPARE _ -> U.COMPARE va U.EQ _ -> U.EQ va U.NEQ _ -> U.NEQ va - U.LT _ -> U.GT va + U.LT _ -> U.LT va U.GT _ -> U.GT va - U.LE _ -> U.GE va + U.LE _ -> U.LE va + U.GE _ -> U.GE va U.INT _ -> U.INT va U.SELF _ fa -> U.SELF va fa U.CONTRACT _ fa t -> U.CONTRACT va fa t @@ -346,7 +353,8 @@ U.AMOUNT _ -> U.AMOUNT va U.BALANCE _ -> U.BALANCE va U.CHECK_SIGNATURE _ -> U.CHECK_SIGNATURE va - U.SHA256 _ -> U.SHA512 va + U.SHA256 _ -> U.SHA256 va + U.SHA512 _ -> U.SHA512 va U.BLAKE2B _ -> U.BLAKE2B va U.HASH_KEY _ -> U.HASH_KEY va U.SOURCE _ -> U.SOURCE va @@ -501,6 +509,8 @@ StatementStarts name -> one $ U.UCOMMENT $ "Statement starts: " <> name StatementEnds name -> one $ U.UCOMMENT $ "Statement ends: " <> name JustComment com -> one $ U.UCOMMENT com + StackTypeComment (Just stack) -> one $ U.UCOMMENT $ pretty (listF stack) + StackTypeComment Nothing -> one $ U.UCOMMENT $ fmt "any stack type" -- It's an orphan instance, but it's better than checking all cases manually. -- We can also move this convertion to the place where `Instr` is defined, @@ -604,3 +614,12 @@ sampleSignature = fromRight (error "impossible") $ parseSignature "edsigtrs8bK7vNfiR4Kd9dWasVa1bAWaQSu2ipnmLGZuwQa8ktCEMYVKqbWsbJ7zTS8dgYT9tiSUKorWCPFHosL5zPsiDwBQ6vb" sampleChainId = fromRight (error "impossible") $ parseChainId "NetXUdfLh6Gm88t" + +-- Misc +---------------------------------------------------------------------------- + +-- | Flatten a provided list of notes to a map of its entrypoints and its +-- corresponding utype. Please refer to 'mkEntrypointsMap' in regards to how +-- duplicate entrypoints are handled. +flattenEntrypoints :: SingI t => ParamNotes t -> Map EpName U.Type +flattenEntrypoints = U.mkEntrypointsMap . convertParamNotes diff --git a/src/Michelson/Typed/Entrypoints.hs b/src/Michelson/Typed/Entrypoints.hs --- a/src/Michelson/Typed/Entrypoints.hs +++ b/src/Michelson/Typed/Entrypoints.hs @@ -33,7 +33,6 @@ , mkEntrypointCall , tyImplicitAccountParam - , flattenEntrypoints -- * Re-exports , EpName (..) @@ -51,15 +50,12 @@ import qualified Data.List.NonEmpty as NE import qualified Data.Text as T import Fmt (Buildable(..), hexF, pretty, (+|), (|+)) -import Test.QuickCheck (Arbitrary(..)) import Michelson.Text import Michelson.Typed.Annotation -import Michelson.Typed.Extract import Michelson.Typed.Scope import Michelson.Typed.Sing import Michelson.Typed.T -import qualified Michelson.Untyped as U import Michelson.Untyped.Annotation import Michelson.Untyped.Entrypoints import Tezos.Address @@ -144,9 +140,6 @@ unsafeParseEpAddress :: HasCallStack => Text -> EpAddress unsafeParseEpAddress = either (error . pretty) id . parseEpAddress -instance Arbitrary FieldAnn => Arbitrary EpAddress where - arbitrary = EpAddress <$> arbitrary <*> arbitrary - -- | Parses byte representation of entrypoint address. -- -- For every address @@ -241,7 +234,7 @@ = mapMaybe (safeHead . tail) . NE.group . sort - $ maybe allEps (: allEps) (epNameFromParamAnn $ convAnn ra) + $ maybe allEps (: allEps) (epNameFromParamAnn ra) whenJust (nonEmpty duplicatedEps) $ \dups -> throwError $ ParamEpDuplicatedNames dups @@ -466,7 +459,7 @@ mkEntrypointCall epName (ParamNotes paramNotes root) = asum [ do - epName' <- epNameFromParamAnn $ convAnn root + epName' <- epNameFromParamAnn root guard (epName == epName') return $ MkEntrypointCallRes paramNotes @@ -492,12 +485,3 @@ -- | "Parameter" type of implicit account. tyImplicitAccountParam :: ParamNotes 'TUnit tyImplicitAccountParam = ParamNotesUnsafe starNotes noAnn - --- Misc ----------------------------------------------------------------------------- - --- | Flatten a provided list of notes to a map of its entrypoints and its --- corresponding utype. Please refer to 'mkEntrypointsMap' in regards to how --- duplicate entrypoints are handled. -flattenEntrypoints :: SingI t => ParamNotes t -> Map EpName U.Type -flattenEntrypoints (pnNotes -> notes) = mkEntrypointsMap (mkUType notes) diff --git a/src/Michelson/Typed/Haskell/Value.hs b/src/Michelson/Typed/Haskell/Value.hs --- a/src/Michelson/Typed/Haskell/Value.hs +++ b/src/Michelson/Typed/Haskell/Value.hs @@ -47,7 +47,6 @@ import GHC.Generics ((:*:)(..), (:+:)(..)) import qualified GHC.Generics as G import Named (NamedF(..)) -import Test.QuickCheck (Arbitrary(..)) import Michelson.Text import Michelson.Typed.Aliases @@ -270,12 +269,6 @@ toVal = VBigMap . Map.mapKeys toVal . Map.map toVal . unBigMap fromVal (VBigMap x) = BigMap $ Map.map fromVal $ Map.mapKeys fromVal x -instance - ( WellTypedToT k, WellTypedToT v, Comparable (ToT k), Arbitrary k - , Arbitrary v, Ord k - ) => Arbitrary (BigMap k v) where - arbitrary = BigMap <$> arbitrary - -- Generic magic ---------------------------------------------------------------------------- @@ -378,22 +371,34 @@ -- illegal as per Michelson typing rule. Using this class, we inductively -- enforce that a type and all types it contains are well typed as per -- Michelson's rules. -class KnownT t => WellTyped (t :: T) where +class (KnownT t, WellTypedSuperC t) => WellTyped (t :: T) where + -- | Constraints required for instance of a given type. + type WellTypedSuperC t :: Constraint + type WellTypedSuperC t = () instance WellTyped 'TKey where instance WellTyped 'TUnit where instance WellTyped 'TSignature where instance WellTyped 'TChainId where -instance (WellTyped t) => WellTyped ('TOption t) where -instance (WellTyped t) => WellTyped ('TList t) where +instance WellTyped t => WellTyped ('TOption t) where + type WellTypedSuperC ('TOption t) = WellTyped t +instance WellTyped t => WellTyped ('TList t) where + type WellTypedSuperC ('TList t) = WellTyped t instance (Comparable t, WellTyped t) => WellTyped ('TSet t) where + type WellTypedSuperC ('TSet t) = (Comparable t, WellTyped t) instance WellTyped 'TOperation where -instance (WellTyped t) => WellTyped ('TContract t) where -instance (WellTyped t1, WellTyped t2) => WellTyped ('TPair t1 t2) -instance (WellTyped t1, WellTyped t2) => WellTyped ('TOr t1 t2) -instance (WellTyped t1, WellTyped t2) => WellTyped ('TLambda t1 t2) -instance (Comparable k, WellTyped k, WellTyped v) => WellTyped ('TMap k v) -instance (Comparable k, WellTyped k, WellTyped v) => WellTyped ('TBigMap k v) +instance WellTyped t => WellTyped ('TContract t) where + type WellTypedSuperC ('TContract t) = WellTyped t +instance (WellTyped t1, WellTyped t2) => WellTyped ('TPair t1 t2) where + type WellTypedSuperC ('TPair t1 t2) = (WellTyped t1, WellTyped t2) +instance (WellTyped t1, WellTyped t2) => WellTyped ('TOr t1 t2) where + type WellTypedSuperC ('TOr t1 t2) = (WellTyped t1, WellTyped t2) +instance (WellTyped t1, WellTyped t2) => WellTyped ('TLambda t1 t2) where + type WellTypedSuperC ('TLambda t1 t2) = (WellTyped t1, WellTyped t2) +instance (Comparable k, WellTyped k, WellTyped v) => WellTyped ('TMap k v) where + type WellTypedSuperC ('TMap k v) = (Comparable k, WellTyped k, WellTyped v) +instance (Comparable k, WellTyped k, WellTyped v) => WellTyped ('TBigMap k v) where + type WellTypedSuperC ('TBigMap k v) = (Comparable k, WellTyped k, WellTyped v) instance WellTyped 'TInt instance WellTyped 'TNat instance WellTyped 'TString diff --git a/src/Michelson/Typed/Instr.hs b/src/Michelson/Typed/Instr.hs --- a/src/Michelson/Typed/Instr.hs +++ b/src/Michelson/Typed/Instr.hs @@ -47,7 +47,8 @@ import Michelson.Typed.Sing (KnownT) import Michelson.Typed.T (T(..)) import Michelson.Typed.Value (Comparable, ContractInp, ContractOut, Value'(..)) -import Michelson.Untyped (Annotation(..), EntriesOrder(..), FieldAnn, TypeAnn, VarAnn, entriesOrderToInt) +import Michelson.Untyped + (Annotation(..), EntriesOrder(..), FieldAnn, TypeAnn, VarAnn, entriesOrderToInt) import Util.Peano import Util.TH import Util.Type (type (++), KnownList) @@ -444,6 +445,7 @@ | StatementStarts Text | StatementEnds Text | JustComment Text + | StackTypeComment (Maybe [T]) -- ^ 'Nothing' for any stack type deriving stock (Show, Generic) instance NFData CommentType diff --git a/src/Michelson/Typed/Polymorphic.hs b/src/Michelson/Typed/Polymorphic.hs --- a/src/Michelson/Typed/Polymorphic.hs +++ b/src/Michelson/Typed/Polymorphic.hs @@ -15,6 +15,8 @@ , UpdOp (..) , SliceOp (..) , ConcatOp (..) + , divMich + , modMich ) where import qualified Data.ByteString as B @@ -201,7 +203,7 @@ if j == 0 then VOption $ Nothing else VOption $ Just $ - VPair (VInt (div i j), VNat $ fromInteger (abs $ mod i j)) + VPair (VInt (divMich i j), VNat $ fromInteger $ modMich i j) instance EDivOp 'TInt 'TNat where type EDivOpRes 'TInt 'TNat = 'TInt type EModOpRes 'TInt 'TNat = 'TNat @@ -211,7 +213,7 @@ if j == 0 then VOption $ Nothing else VOption $ Just $ - VPair (VInt (div i (toInteger j)), VNat $ (abs $ mod (fromInteger i) j)) + VPair (VInt (divMich i (toInteger j)), VNat $ fromInteger $ modMich i (toInteger j)) instance EDivOp 'TNat 'TInt where type EDivOpRes 'TNat 'TInt = 'TInt type EModOpRes 'TNat 'TInt = 'TNat @@ -221,7 +223,7 @@ if j == 0 then VOption $ Nothing else VOption $ Just $ - VPair (VInt (div (toInteger i) j), VNat $ (abs $ mod i (fromInteger j))) + VPair (VInt (divMich (toInteger i) j), VNat $ fromInteger $ modMich (toInteger i) j) instance EDivOp 'TNat 'TNat where type EDivOpRes 'TNat 'TNat = 'TNat type EModOpRes 'TNat 'TNat = 'TNat @@ -231,7 +233,7 @@ if j == 0 then VOption $ Nothing else VOption $ Just $ - VPair (VNat (div i j), VNat $ (mod i j)) + VPair (VNat (divMich i j), VNat $ (modMich i j)) instance EDivOp 'TMutez 'TMutez where type EDivOpRes 'TMutez 'TMutez = 'TNat type EModOpRes 'TMutez 'TMutez = 'TMutez @@ -252,3 +254,21 @@ i `divModMutezInt` j <&> \case (quotient, remainder) -> VPair (VMutez quotient, VMutez remainder) + +-- | Computing 'div' function in Michelson style. +-- When divisor is negative, Haskell gives x as integer part, +-- while Michelson gives x+1. +divMich :: Integral a => a -> a -> a +divMich divisible divisor = divisible `div` divisor + extra + where + extra = + if divisor > 0 + then 0 + else 1 + +-- | Computing 'mod' function in Michelson style. +-- When divisor is negative, Haskell gives a negative modulo, +-- while there is a positive modulo in Michelson. +modMich :: Integral a => a -> a -> a +modMich divisible divisor = divisible - divisor * intPart + where intPart = divMich divisible divisor diff --git a/src/Michelson/Typed/Value.hs b/src/Michelson/Typed/Value.hs --- a/src/Michelson/Typed/Value.hs +++ b/src/Michelson/Typed/Value.hs @@ -37,17 +37,17 @@ , eqValueExt ) where -import GHC.TypeLits (ErrorMessage(..), TypeError) -import Data.Singletons (SingI (..), Sing) -import Data.Constraint (Dict (..), (\\)) -import Data.Type.Bool (type (&&)) -import Fmt (Buildable(build), (+|), (|+), Builder) +import Data.Constraint (Dict(..), (\\)) import qualified Data.Kind as Kind +import Data.Singletons (Sing, SingI(..)) +import Data.Type.Bool (type (&&)) +import Fmt (Buildable(build), Builder, (+|), (|+)) +import GHC.TypeLits (ErrorMessage(..), TypeError) import Michelson.Text (MText) import Michelson.Typed.Entrypoints -import Michelson.Typed.Sing import Michelson.Typed.Scope (BadTypeForScope(..), CheckScope(..), ParameterScope, StorageScope) +import Michelson.Typed.Sing import Michelson.Typed.T (T(..)) import Tezos.Address (Address) import Tezos.Core (ChainId, Mutez, Timestamp) diff --git a/src/Michelson/Untyped/Annotation.hs b/src/Michelson/Untyped/Annotation.hs --- a/src/Michelson/Untyped/Annotation.hs +++ b/src/Michelson/Untyped/Annotation.hs @@ -171,17 +171,13 @@ data VarTag data SomeTag -data RootTag - type TypeAnn = Annotation TypeTag type FieldAnn = Annotation FieldTag type VarAnn = Annotation VarTag type SomeAnn = Annotation SomeTag --- | Root annotation was added in the Babylon, it looks the same as --- field annotation, but has slightly different semantic and can be used --- only in parameter 'ParameterType'. -type RootAnn = Annotation RootTag +-- | Field annotation for the entire parameter. +type RootAnn = Annotation FieldTag instance KnownAnnTag FieldTag where annPrefix = "%" @@ -189,8 +185,6 @@ annPrefix = "@" instance KnownAnnTag TypeTag where annPrefix = ":" -instance KnownAnnTag RootTag where - annPrefix = "%" instance KnownAnnTag tag => RenderDoc (Annotation tag) where renderDoc _ = renderAnn diff --git a/src/Michelson/Untyped/Entrypoints.hs b/src/Michelson/Untyped/Entrypoints.hs --- a/src/Michelson/Untyped/Entrypoints.hs +++ b/src/Michelson/Untyped/Entrypoints.hs @@ -20,7 +20,6 @@ import Data.Aeson.TH (deriveJSON) import qualified Data.Map as Map import Fmt (Buildable(..), pretty, (+|), (|+)) -import Test.QuickCheck (Arbitrary(..), suchThatMap) import Michelson.Untyped.Annotation import Michelson.Untyped.Type @@ -153,30 +152,28 @@ unsafeBuildEpName :: HasCallStack => Text -> EpName unsafeBuildEpName = either (error . pretty) id . buildEpName -instance Arbitrary FieldAnn => Arbitrary EpName where - arbitrary = arbitrary `suchThatMap` (rightToMaybe . epNameFromRefAnn) - instance HasCLReader EpName where getReader = eitherReader (buildEpName . toText) getMetavar = "ENTRYPOINT" --- | Given an untyped type, extract a map that maps entrypoint names to the --- their parameter types. If there are duplicate entrypoints in the given Type --- then the duplicate entrypoints at a deeper nesting level will get +-- | Given an untyped parameter type, extract a map that maps entrypoint names +-- to the their parameter types. If there are duplicate entrypoints in the +-- given Type then the duplicate entrypoints at a deeper nesting level will get -- overwritten with the ones that are on top. -mkEntrypointsMap :: Type -> Map EpName Type -mkEntrypointsMap (Type t _) = case t of - -- We are only interested in `Or` branches to extract entrypoint - -- annotations. - TOr f1 f2 t1 t2 -> extractSubmap f1 t1 <> extractSubmap f2 t2 - _ -> mempty +mkEntrypointsMap :: ParameterType -> Map EpName Type +mkEntrypointsMap (ParameterType ty rootAnn) = mkEntrypointsMapRec rootAnn ty + +-- | Version of 'mkEntrypointMaps' for plain untyped type. +mkEntrypointsMapRec :: FieldAnn -> Type -> Map EpName Type +mkEntrypointsMapRec curRootAnn ty = + accountRoot curRootAnn <> accountTree ty where - extractSubmap :: FieldAnn -> Type -> Map EpName Type - extractSubmap f1 t1 = let - -- If the field annotation is not empty then merge this field - -- annotation/type pair with the entrypoint map of inner type. Else - -- just fetch entrypoint map of inner type. - innerMap = mkEntrypointsMap t1 - in case epNameFromParamAnn f1 of - Just epName -> Map.singleton epName t1 <> innerMap - Nothing -> innerMap + accountRoot rootAnn = Map.fromList $ do + Just rootEp <- pure $ epNameFromParamAnn rootAnn + return (rootEp, ty) + + accountTree (Type t _) = case t of + -- We are only interested in `Or` branches to extract entrypoint + -- annotations. + TOr f1 f2 t1 t2 -> mkEntrypointsMapRec f1 t1 <> mkEntrypointsMapRec f2 t2 + _ -> mempty diff --git a/src/Michelson/Untyped/Type.hs b/src/Michelson/Untyped/Type.hs --- a/src/Michelson/Untyped/Type.hs +++ b/src/Michelson/Untyped/Type.hs @@ -46,8 +46,7 @@ (Prettier(..), RenderContext, RenderDoc(..), addParens, buildRenderDoc, doesntNeedParens, needsParens, wrapInParens) import Michelson.Untyped.Annotation - (AnnotationSet, FieldAnn, RootAnn, TypeAnn, convAnn, emptyAnnSet, fullAnnSet, noAnn, - singleAnnSet) + (AnnotationSet, FieldAnn, RootAnn, TypeAnn, emptyAnnSet, fullAnnSet, noAnn, singleAnnSet) import Util.Aeson -- Annotated type @@ -79,11 +78,11 @@ instance RenderDoc (Prettier ParameterType) where renderDoc pn (Prettier w) = case w of ParameterType (Type t ta) ra -> - renderType t False pn (fullAnnSet [ta] [convAnn ra] []) + renderType t False pn (fullAnnSet [ta] [ra] []) instance RenderDoc ParameterType where renderDoc pn (ParameterType (Type t ta) ra) = - renderType t True pn (fullAnnSet [ta] [convAnn ra] []) + renderType t True pn (fullAnnSet [ta] [ra] []) -- Ordering between different kinds of annotations is not significant, -- but ordering among annotations of the same kind is. Annotations diff --git a/src/Morley/Micheline/Class.hs b/src/Morley/Micheline/Class.hs --- a/src/Morley/Micheline/Class.hs +++ b/src/Morley/Micheline/Class.hs @@ -22,7 +22,7 @@ import Michelson.Typed.Instr (mapEntriesOrdered) import Michelson.Typed.Scope (UnpackedValScope) import qualified Michelson.Untyped as Untyped -import Michelson.Untyped.Annotation (RootAnn, convAnn, noAnn) +import Michelson.Untyped.Annotation (RootAnn, noAnn) import Michelson.Untyped.Instr (ExpandedOp) import Morley.Micheline.Binary (decodeExpression, encodeExpression) import Morley.Micheline.Expression @@ -72,8 +72,7 @@ addRootAnnToExpression rootAnn expr = case expr of ExpressionPrim p | rootAnn /= noAnn -> ExpressionPrim p - { mpaAnnots = mpaAnnots p |> - (AnnotationField $ convAnn rootAnn) + { mpaAnnots = mpaAnnots p |> AnnotationField rootAnn } | otherwise -> expr -- Currently this error can't happen because parameter type diff --git a/src/Morley/Micheline/Json.hs b/src/Morley/Micheline/Json.hs --- a/src/Morley/Micheline/Json.hs +++ b/src/Morley/Micheline/Json.hs @@ -9,6 +9,7 @@ ( StringEncode (..) , TezosBigNum , TezosInt64 + , parseMutezJson ) where import Data.Aeson (FromJSON, ToJSON, parseJSON, toEncoding, toJSON) @@ -19,6 +20,8 @@ import Fmt (Buildable(..)) import qualified Text.Show as T +import Tezos.Core (Mutez, mkMutez') + parseAsString :: forall a. (Read a, Typeable a) => Aeson.Value -> Aeson.Parser a parseAsString = Aeson.withText (T.show $ typeRep (Proxy :: Proxy a)) $ \txt -> maybe (fail "Failed to parse string") pure $ readMaybe (toString txt) @@ -50,3 +53,7 @@ instance ToJSON TezosInt64 where toJSON (StringEncode x) = Aeson.String $ show x toEncoding (StringEncode x) = AE.int64Text x + +parseMutezJson :: TezosInt64 -> Aeson.Parser Mutez +parseMutezJson (StringEncode i) = + either (fail . toString) pure $ mkMutez' i diff --git a/src/Tezos/Address.hs b/src/Tezos/Address.hs --- a/src/Tezos/Address.hs +++ b/src/Tezos/Address.hs @@ -38,7 +38,6 @@ import qualified Data.ByteString as BS import qualified Data.ByteString.Lazy as BSL import Fmt (Buildable(build), hexF, pretty) -import Test.QuickCheck (Arbitrary(..), oneof, vector) import Michelson.Text import Tezos.Crypto @@ -343,13 +342,3 @@ fromJSONKey = AesonTypes.FromJSONKeyTextParser (either (fail . pretty) pure . parseAddress) - ----------------------------------------------------------------------------- --- Arbitrary ----------------------------------------------------------------------------- - -instance Arbitrary Address where - arbitrary = oneof [genKeyAddress, genContractAddress] - where - genKeyAddress = KeyAddress <$> arbitrary - genContractAddress = ContractAddress . ContractHash . BS.pack <$> vector 20 diff --git a/src/Tezos/Core.hs b/src/Tezos/Core.hs --- a/src/Tezos/Core.hs +++ b/src/Tezos/Core.hs @@ -9,6 +9,7 @@ -- * Mutez Mutez (unMutez) , mkMutez + , mkMutez' , unsafeMkMutez , toMutez , addMutez @@ -48,7 +49,6 @@ import Data.Aeson (FromJSON(..), ToJSON(..)) import qualified Data.Aeson as Aeson import Data.Aeson.TH (deriveJSON) -import qualified Data.ByteString as BS import Data.Data (Data(..)) import qualified Data.Text as T import Data.Time.Clock (UTCTime) @@ -60,12 +60,12 @@ import qualified Language.Haskell.TH.Quote as TH import Language.Haskell.TH.Syntax (liftData) import qualified Options.Applicative as Opt -import Test.QuickCheck (Arbitrary(..), vector) import Michelson.Text import Tezos.Crypto import Util.Aeson import Util.CLI +import Util.Num ---------------------------------------------------------------------------- -- Mutez @@ -99,6 +99,13 @@ | otherwise = Nothing {-# INLINE mkMutez #-} +-- | Version of 'mkMutez' that accepts a number of any type. +mkMutez' :: Integral i => i -> Either Text Mutez +mkMutez' i = do + w :: Word64 <- fromIntegralChecked i + mkMutez w + & maybeToRight "Mutez overflow" + -- | Partial function for 'Mutez' creation, it's pre-condition is that -- the argument must not exceed the maximal 'Mutez' value. unsafeMkMutez :: HasCallStack => Word64 -> Mutez @@ -321,6 +328,9 @@ ParseChainIdWrongSize s -> "Wrong size for a chain id: " <> build s +instance Exception ParseChainIdError where + displayException = pretty + parseChainId :: Text -> Either ParseChainIdError ChainId parseChainId text = case decodeBase58CheckWithPrefix chainIdPrefix text of @@ -339,9 +349,6 @@ -- Corresponds to "Net" part. chainIdPrefix :: ByteString chainIdPrefix = "\87\82\0" - -instance Arbitrary ChainId where - arbitrary = ChainIdUnsafe . BS.pack <$> (vector 4) ---------------------------------------------------------------------------- -- JSON diff --git a/src/Tezos/Crypto.hs b/src/Tezos/Crypto.hs --- a/src/Tezos/Crypto.hs +++ b/src/Tezos/Crypto.hs @@ -93,7 +93,6 @@ import qualified Data.ByteString.Lazy as LBS import qualified Data.Text as T import Fmt (Buildable, build, hexF, pretty) -import Test.QuickCheck (Arbitrary(..), elements, oneof) import Michelson.Text import qualified Tezos.Crypto.Ed25519 as Ed25519 @@ -101,8 +100,8 @@ import qualified Tezos.Crypto.P256 as P256 import qualified Tezos.Crypto.Secp256k1 as Secp256k1 import Tezos.Crypto.Util -import Util.CLI import Util.Binary +import Util.CLI ---------------------------------------------------------------------------- -- Types, instances, conversions @@ -121,9 +120,6 @@ instance NFData PublicKey -instance Arbitrary PublicKey where - arbitrary = toPublic <$> arbitrary - -- | Secret cryptographic key used by Tezos. -- Constructors correspond to 'PublicKey' constructors. data SecretKey @@ -141,7 +137,6 @@ getReader = eitherReader (first pretty . parseSecretKey . toText) getMetavar = "SECRET_KEY" - -- | Deterministicaly generate a secret key from seed. -- Type of the key depends on seed length. detSecretKey :: HasCallStack => ByteString -> SecretKey @@ -151,13 +146,6 @@ 2 -> SecretKeyP256 . P256.detSecretKey _ -> error "detSecretKey: unexpected happened" -instance Arbitrary SecretKey where - arbitrary = oneof - [ SecretKeyEd25519 <$> arbitrary - , SecretKeySecp256k1 <$> arbitrary - , SecretKeyP256 <$> arbitrary - ] - -- | Create a public key from a secret key. toPublic :: SecretKey -> PublicKey toPublic = \case @@ -215,14 +203,6 @@ (SignatureP256 s1, SignatureP256 s2) -> s1 == s2 (SignatureP256 {}, _) -> False -instance Arbitrary Signature where - arbitrary = oneof - [ SignatureEd25519 <$> arbitrary - , SignatureSecp256k1 <$> arbitrary - , SignatureP256 <$> arbitrary - , SignatureGeneric . BS.replicate signatureLengthBytes <$> arbitrary - ] - ---------------------------------------------------------------------------- -- Signature ---------------------------------------------------------------------------- @@ -427,9 +407,6 @@ | KeyHashP256 deriving stock (Show, Eq, Ord, Bounded, Enum, Generic) -instance Arbitrary KeyHashTag where - arbitrary = elements [minBound .. ] - instance NFData KeyHashTag -- | Blake2b_160 hash of a public key. @@ -446,9 +423,6 @@ -- or anything). keyHashLengthBytes :: Integral n => n keyHashLengthBytes = 20 - -instance Arbitrary KeyHash where - arbitrary = hashKey <$> arbitrary -- | Compute the b58check of a public key hash. hashKey :: PublicKey -> KeyHash diff --git a/src/Tezos/Crypto/Ed25519.hs b/src/Tezos/Crypto/Ed25519.hs --- a/src/Tezos/Crypto/Ed25519.hs +++ b/src/Tezos/Crypto/Ed25519.hs @@ -38,9 +38,7 @@ import Crypto.Error (onCryptoFailure) import qualified Crypto.PubKey.Ed25519 as Ed25519 import Data.ByteArray (ByteArray, ByteArrayAccess, convert) -import qualified Data.ByteString as BS import Fmt (Buildable, build) -import Test.QuickCheck (Arbitrary(..), vector) import Michelson.Text import Tezos.Crypto.Hash @@ -55,9 +53,6 @@ { unPublicKey :: Ed25519.PublicKey } deriving stock (Show, Eq, Generic) -instance Arbitrary PublicKey where - arbitrary = toPublic <$> arbitrary - instance NFData PublicKey -- | ED25519 secret cryptographic key. @@ -71,9 +66,6 @@ detSecretKey :: ByteString -> SecretKey detSecretKey seed = SecretKey $ deterministic seed Ed25519.generateSecretKey -instance Arbitrary SecretKey where - arbitrary = detSecretKey . BS.pack <$> vector 32 - -- | Create a public key from a secret key. toPublic :: SecretKey -> PublicKey toPublic = PublicKey . Ed25519.toPublic . unSecretKey @@ -82,9 +74,6 @@ newtype Signature = Signature { unSignature :: Ed25519.Signature } deriving stock (Show, Eq, Generic) - -instance Arbitrary Signature where - arbitrary = sign <$> arbitrary <*> (encodeUtf8 @String <$> arbitrary) instance NFData Signature diff --git a/src/Tezos/Crypto/P256.hs b/src/Tezos/Crypto/P256.hs --- a/src/Tezos/Crypto/P256.hs +++ b/src/Tezos/Crypto/P256.hs @@ -40,11 +40,9 @@ import qualified Crypto.PubKey.ECC.ECDSA as ECDSA import qualified Crypto.PubKey.ECC.Generate as ECC.Generate import Crypto.PubKey.ECC.Types (Curve(..), CurveName(..), getCurveByName) -import Crypto.Random (MonadRandom, drgNewSeed, seedFromInteger, withDRG) +import Crypto.Random (MonadRandom) import Data.ByteArray (ByteArray, ByteArrayAccess) -import qualified Data.ByteString as BS import Fmt (Buildable, build) -import Test.QuickCheck (Arbitrary(..), vector) import Michelson.Text import Tezos.Crypto.Util @@ -61,9 +59,6 @@ { unPublicKey :: ECDSA.PublicKey } deriving stock (Eq, Show, Generic) -instance Arbitrary PublicKey where - arbitrary = toPublic <$> arbitrary - instance NFData PublicKey where rnf (PublicKey (ECDSA.PublicKey cu q)) = rnfCurve cu `seq` rnf q @@ -87,9 +82,6 @@ return $ ECDSA.KeyPair curve (ECDSA.public_q publicKey) (ECDSA.private_d privateKey) -instance Arbitrary SecretKey where - arbitrary = detSecretKey . BS.pack <$> vector 32 - -- | Create a public key from a secret key. toPublic :: SecretKey -> PublicKey toPublic = @@ -100,14 +92,6 @@ newtype Signature = Signature { unSignature :: ECDSA.Signature } deriving stock (Show, Eq, Generic) - -instance Arbitrary Signature where - arbitrary = do - seed <- drgNewSeed . seedFromInteger <$> arbitrary - byteToSign <- arbitrary - return $ fst $ withDRG seed $ do - sk <- detSecretKeyDo - sign sk (one byteToSign) instance NFData Signature where rnf (Signature (ECDSA.Signature a b)) = rnf a `seq` rnf b diff --git a/src/Tezos/Crypto/Secp256k1.hs b/src/Tezos/Crypto/Secp256k1.hs --- a/src/Tezos/Crypto/Secp256k1.hs +++ b/src/Tezos/Crypto/Secp256k1.hs @@ -40,11 +40,9 @@ import qualified Crypto.PubKey.ECC.ECDSA as ECDSA import qualified Crypto.PubKey.ECC.Generate as ECC.Generate import Crypto.PubKey.ECC.Types (Curve(..), CurveName(..), getCurveByName) -import Crypto.Random (MonadRandom, drgNewSeed, seedFromInteger, withDRG) +import Crypto.Random (MonadRandom) import Data.ByteArray (ByteArray, ByteArrayAccess) -import qualified Data.ByteString as BS import Fmt (Buildable, build) -import Test.QuickCheck (Arbitrary(..), vector) import Michelson.Text import Tezos.Crypto.Util @@ -61,9 +59,6 @@ { unPublicKey :: ECDSA.PublicKey } deriving stock (Eq, Show, Generic) -instance Arbitrary PublicKey where - arbitrary = toPublic <$> arbitrary - instance NFData PublicKey where rnf (PublicKey (ECDSA.PublicKey cu q)) = rnfCurve cu `seq` rnf q @@ -87,9 +82,6 @@ return $ ECDSA.KeyPair curve (ECDSA.public_q publicKey) (ECDSA.private_d privateKey) -instance Arbitrary SecretKey where - arbitrary = detSecretKey . BS.pack <$> vector 32 - -- | Create a public key from a secret key. toPublic :: SecretKey -> PublicKey toPublic = @@ -100,14 +92,6 @@ newtype Signature = Signature { unSignature :: ECDSA.Signature } deriving stock (Show, Eq, Generic) - -instance Arbitrary Signature where - arbitrary = do - seed <- drgNewSeed . seedFromInteger <$> arbitrary - byteToSign <- arbitrary - return $ fst $ withDRG seed $ do - sk <- detSecretKeyDo - sign sk (one byteToSign) instance NFData Signature where rnf (Signature (ECDSA.Signature a b)) = rnf a `seq` rnf b diff --git a/src/Util/Num.hs b/src/Util/Num.hs new file mode 100644 --- /dev/null +++ b/src/Util/Num.hs @@ -0,0 +1,19 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +-- | Utilities for numbers. +module Util.Num + ( fromIntegralChecked + ) where + +-- | Convert between integral types, checking for overflows/underflows. +fromIntegralChecked :: (Integral a, Integral b) => a -> Either Text b +fromIntegralChecked a = + let b = fromIntegral a + in if toInteger a == toInteger b + then Right b + else Left + if toInteger a > toInteger b + then "Numeric overflow" + else "Numeric underflow" diff --git a/src/Util/Test/Arbitrary.hs b/src/Util/Test/Arbitrary.hs deleted file mode 100644 --- a/src/Util/Test/Arbitrary.hs +++ /dev/null @@ -1,241 +0,0 @@ --- SPDX-FileCopyrightText: 2020 Tocqueville Group --- --- SPDX-License-Identifier: LicenseRef-MIT-TQ - -{-# OPTIONS_GHC -Wno-orphans #-} - -module Util.Test.Arbitrary - ( runGen - ) where - -import Prelude hiding (EQ, GT, LT) - -import Test.QuickCheck - (Arbitrary(..), Gen, choose, elements, frequency, oneof, resize, suchThatMap, vector) -import Test.QuickCheck.Arbitrary.ADT (ToADTArbitrary(..)) -import Test.QuickCheck.Gen (unGen) -import Test.QuickCheck.Instances.ByteString () -import Test.QuickCheck.Instances.Natural () -import Test.QuickCheck.Instances.Semigroup () -import Test.QuickCheck.Instances.Text () -import Test.QuickCheck.Random (mkQCGen) - -import Michelson.ErrorPos (InstrCallStack(..), LetName(..), Pos(..), SrcPos(..)) -import Michelson.Untyped - (Annotation, Contract'(..), Elt(..), EntriesOrder(..), ExpandedExtInstr, ExpandedOp(..), - ExtInstrAbstract(..), InstrAbstract(..), InternalByteString(..), ParameterType(..), - StackTypePattern(..), T(..), TyVar(..), Type(..), Value'(..), Var(..), mkAnnotation) -import Tezos.Core (Mutez(..)) - -instance Arbitrary InternalByteString where - arbitrary = InternalByteString <$> arbitrary - -instance Arbitrary Var where - arbitrary = Var <$> arbitrary - -instance Arbitrary TyVar where - arbitrary = oneof [VarID <$> arbitrary, TyCon <$> arbitrary] - -instance Arbitrary StackTypePattern where - arbitrary = oneof [pure StkEmpty, pure StkRest, StkCons <$> arbitrary <*> arbitrary] - --- TODO extend Arbitrary ExpandedExtInstr with other constructors -instance Arbitrary ExpandedExtInstr where - arbitrary = oneof [STACKTYPE <$> arbitrary] - -instance ToADTArbitrary Pos -instance Arbitrary Pos where - arbitrary = Pos <$> arbitrary - -instance ToADTArbitrary SrcPos -instance Arbitrary SrcPos where - arbitrary = liftA2 SrcPos arbitrary arbitrary - -instance ToADTArbitrary LetName -instance Arbitrary LetName where - arbitrary = LetName <$> resize 3 arbitrary - -instance ToADTArbitrary InstrCallStack -instance Arbitrary InstrCallStack where - arbitrary = liftA2 InstrCallStack genName arbitrary - where - genName = frequency [(80, pure []), (18, vector 1), (2, vector 2)] - -instance ToADTArbitrary ExpandedOp -instance Arbitrary ExpandedOp where - arbitrary = liftA2 WithSrcEx arbitrary (PrimEx <$> arbitrary) - -instance ToADTArbitrary Mutez - -instance ToADTArbitrary (Annotation tag) -instance Arbitrary (Annotation tag) where - arbitrary = resize 5 arbitrary `suchThatMap` (rightToMaybe . mkAnnotation) - -smallSize :: Gen Int -smallSize = choose (0, 3) - -smallList :: Arbitrary a => Gen [a] -smallList = smallSize >>= vector - -smallList1 :: Arbitrary a => Gen (NonEmpty a) -smallList1 = smallList `suchThatMap` nonEmpty - -instance Arbitrary EntriesOrder where - arbitrary = elements [minBound .. maxBound] - -instance (Arbitrary op, ToADTArbitrary op) => ToADTArbitrary (Contract' op) -instance (Arbitrary op) => Arbitrary (Contract' op) where - arbitrary = Contract <$> arbitrary <*> arbitrary <*> smallList <*> arbitrary - -instance (Arbitrary op, ToADTArbitrary op, Arbitrary (ExtInstrAbstract op)) => ToADTArbitrary (InstrAbstract op) -instance (Arbitrary op, Arbitrary (ExtInstrAbstract op)) => Arbitrary (InstrAbstract op) where - arbitrary = - oneof - [ EXT <$> arbitrary - , pure DROP - , DUP <$> arbitrary - , pure SWAP - , PUSH <$> arbitrary <*> arbitrary <*> arbitrary - , SOME <$> arbitrary <*> arbitrary - , NONE <$> arbitrary <*> arbitrary <*> arbitrary - , UNIT <$> arbitrary <*> arbitrary - , IF_NONE <$> smallList <*> smallList - , PAIR <$> arbitrary <*> arbitrary <*> arbitrary <*> arbitrary - , CAR <$> arbitrary <*> arbitrary - , CDR <$> arbitrary <*> arbitrary - , LEFT <$> arbitrary <*> arbitrary <*> arbitrary <*> arbitrary <*> arbitrary - , RIGHT <$> arbitrary <*> arbitrary <*> arbitrary <*> arbitrary <*> arbitrary - , IF_LEFT <$> smallList <*> smallList - , NIL <$> arbitrary <*> arbitrary <*> arbitrary - , CONS <$> arbitrary - , IF_CONS <$> smallList <*> smallList - , SIZE <$> arbitrary - , EMPTY_SET <$> arbitrary <*> arbitrary <*> arbitrary - , EMPTY_MAP <$> arbitrary <*> arbitrary <*> arbitrary <*> arbitrary - , EMPTY_BIG_MAP <$> arbitrary <*> arbitrary <*> arbitrary <*> arbitrary - , MAP <$> arbitrary <*> smallList - , ITER <$> smallList - , MEM <$> arbitrary - , GET <$> arbitrary - , UPDATE <$> arbitrary - , IF <$> smallList <*> smallList - , LOOP <$> smallList - , LOOP_LEFT <$> smallList - , LAMBDA <$> arbitrary <*> arbitrary <*> arbitrary <*> smallList - , EXEC <$> arbitrary - , APPLY <$> arbitrary - , DIP <$> smallList - , pure FAILWITH - , CAST <$> arbitrary <*> arbitrary - , RENAME <$> arbitrary - , PACK <$> arbitrary - , UNPACK <$> arbitrary <*> arbitrary <*> arbitrary - , CONCAT <$> arbitrary - , SLICE <$> arbitrary - , ISNAT <$> arbitrary - , ADD <$> arbitrary - , SUB <$> arbitrary - , MUL <$> arbitrary - , EDIV <$> arbitrary - , ABS <$> arbitrary - , NEG <$> arbitrary - , LSL <$> arbitrary - , LSR <$> arbitrary - , OR <$> arbitrary - , AND <$> arbitrary - , XOR <$> arbitrary - , NOT <$> arbitrary - , COMPARE <$> arbitrary - , EQ <$> arbitrary - , NEQ <$> arbitrary - , LT <$> arbitrary - , GT <$> arbitrary - , LE <$> arbitrary - , GE <$> arbitrary - , INT <$> arbitrary - , SELF <$> arbitrary <*> arbitrary - , CONTRACT <$> arbitrary <*> arbitrary <*> arbitrary - , TRANSFER_TOKENS <$> arbitrary - , SET_DELEGATE <$> arbitrary - , CREATE_CONTRACT <$> arbitrary <*> arbitrary <*> arbitrary - , IMPLICIT_ACCOUNT <$> arbitrary - , NOW <$> arbitrary - , AMOUNT <$> arbitrary - , BALANCE <$> arbitrary - , CHECK_SIGNATURE <$> arbitrary - , SHA256 <$> arbitrary - , SHA512 <$> arbitrary - , BLAKE2B <$> arbitrary - , HASH_KEY <$> arbitrary - , SOURCE <$> arbitrary - , SENDER <$> arbitrary - , ADDRESS <$> arbitrary - ] - -instance (Arbitrary op, ToADTArbitrary op) => ToADTArbitrary (Value' op) -instance (Arbitrary op) => Arbitrary (Value' op) where - arbitrary = - oneof - [ ValueInt <$> arbitrary - , ValueString <$> arbitrary - , ValueBytes <$> arbitrary - , pure ValueUnit - , pure ValueTrue - , pure ValueFalse - , ValuePair <$> arbitrary <*> arbitrary - , ValueLeft <$> arbitrary - , ValueRight <$> arbitrary - , ValueSome <$> arbitrary - , pure ValueNone - , pure ValueNil - , ValueSeq <$> smallList1 - , ValueMap <$> smallList1 - , ValueLambda <$> smallList1 - ] - -instance (Arbitrary op, ToADTArbitrary op) => ToADTArbitrary (Elt op) -instance (Arbitrary op) => Arbitrary (Elt op) where - arbitrary = Elt <$> arbitrary <*> arbitrary - -instance ToADTArbitrary Type -instance Arbitrary Type where - arbitrary = Type <$> arbitrary <*> arbitrary - -instance ToADTArbitrary ParameterType -instance Arbitrary ParameterType where - arbitrary = ParameterType <$> arbitrary <*> arbitrary - --- | @getRareT k@ generates 'T' producing anything big once per @1 / (k + 1)@ --- invocation. -genRareType :: Word -> Gen Type -genRareType k = Type <$> genRareT k <*> arbitrary - -instance ToADTArbitrary T -instance Arbitrary T where - arbitrary = - oneof - [ pure TKey - , pure TUnit - , pure TSignature - , TOption <$> arbitrary - , TList <$> arbitrary - , TSet <$> arbitrary - , pure TOperation - , TContract <$> arbitrary - , TPair <$> arbitrary <*> arbitrary <*> genRareType 5 <*> genRareType 5 - , TOr <$> arbitrary <*> arbitrary <*> genRareType 5 <*> genRareType 5 - , TLambda <$> genRareType 5 <*> genRareType 5 - , TMap <$> arbitrary <*> arbitrary - , TBigMap <$> arbitrary <*> arbitrary - ] - --- | @getRareT k@ generates 'Type' producing anything big once per @1 / (k + 1)@ --- invocation. --- --- Useful to avoid exponensial growth. -genRareT :: Word -> Gen T -genRareT k = frequency [(1, arbitrary), (fromIntegral k, pure TUnit)] - --- | Run given generator deterministically. -runGen :: Int -> Gen a -> a -runGen seed gen = unGen gen (mkQCGen seed) 10 diff --git a/src/Util/Type.hs b/src/Util/Type.hs --- a/src/Util/Type.hs +++ b/src/Util/Type.hs @@ -37,13 +37,13 @@ ) where import Data.Constraint ((:-)(..), Dict(..)) -import Data.Vinyl.Core (Rec (..)) -import qualified Data.Vinyl.Functor as Vinyl -import Data.Vinyl.Recursive (recordToList, rmap) -import Data.Vinyl.TypeLevel (type (++)) import qualified Data.Kind as Kind import Data.Type.Bool (type (&&), If, Not) import Data.Type.Equality (type (==)) +import Data.Vinyl.Core (Rec(..)) +import qualified Data.Vinyl.Functor as Vinyl +import Data.Vinyl.Recursive (recordToList, rmap) +import Data.Vinyl.TypeLevel (type (++)) import GHC.TypeLits (ErrorMessage(..), Symbol, TypeError) import Unsafe.Coerce (unsafeCoerce)