morley 1.14.0 → 1.15.0

raw patch · 84 files changed

+4611/−3468 lines, 84 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGES.md +85/−0
• app/Main.hs +44/−21
• app/REPL.hs +23/−14
• morley.cabal +5/−2
• src/Michelson/Doc.hs +7/−7
• src/Michelson/ErrorPos.hs +11/−0
• src/Michelson/FailPattern.hs +8/−14
• src/Michelson/Interpret.hs +178/−111
• src/Michelson/Interpret/Pack.hs +21/−570
• src/Michelson/Interpret/Unpack.hs +24/−914
• src/Michelson/Macro.hs +42/−51
• src/Michelson/Optimizer.hs +106/−97
• src/Michelson/Parser.hs +43/−3
• src/Michelson/Parser/Annotations.hs +19/−10
• src/Michelson/Parser/Error.hs +1/−3
• src/Michelson/Parser/Ext.hs +2/−2
• src/Michelson/Parser/Instr.hs +36/−6
• src/Michelson/Parser/Let.hs +4/−2
• src/Michelson/Parser/Macro.hs +11/−16
• src/Michelson/Parser/Type.hs +10/−4
• src/Michelson/Parser/Value.hs +4/−4
• src/Michelson/Preprocess.hs +2/−2
• src/Michelson/Printer.hs +4/−4
• src/Michelson/Printer/Util.hs +18/−1
• src/Michelson/Runtime.hs +84/−46
• src/Michelson/Runtime/Dummy.hs +5/−1
• src/Michelson/Runtime/GState.hs +29/−6
• src/Michelson/Runtime/Import.hs +205/−0
• src/Michelson/Text.hs +17/−17
• src/Michelson/TypeCheck.hs +3/−0
• src/Michelson/TypeCheck/Error.hs +105/−60
• src/Michelson/TypeCheck/Ext.hs +17/−15
• src/Michelson/TypeCheck/Helpers.hs +72/−60
• src/Michelson/TypeCheck/Instr.hs +222/−140
• src/Michelson/TypeCheck/TypeCheck.hs +44/−19
• src/Michelson/TypeCheck/TypeCheckedOp.hs +5/−5
• src/Michelson/TypeCheck/Types.hs +77/−57
• src/Michelson/TypeCheck/Value.hs +149/−45
• src/Michelson/Typed.hs +1/−0
• src/Michelson/Typed/Aliases.hs +0/−4
• src/Michelson/Typed/Annotation.hs +25/−13
• src/Michelson/Typed/Convert.hs +267/−117
• src/Michelson/Typed/Doc.hs +7/−0
• src/Michelson/Typed/Entrypoints.hs +43/−30
• src/Michelson/Typed/Existential.hs +79/−0
• src/Michelson/Typed/Extract.hs +48/−22
• src/Michelson/Typed/Haskell/Doc.hs +22/−14
• src/Michelson/Typed/Haskell/Instr/Product.hs +16/−16
• src/Michelson/Typed/Haskell/Instr/Sum.hs +15/−15
• src/Michelson/Typed/Haskell/LooseSum.hs +8/−7
• src/Michelson/Typed/Haskell/Value.hs +84/−30
• src/Michelson/Typed/Instr.hs +243/−97
• src/Michelson/Typed/Origination.hs +56/−7
• src/Michelson/Typed/Polymorphic.hs +7/−7
• src/Michelson/Typed/Scope.hs +206/−57
• src/Michelson/Typed/Sing.hs +63/−205
• src/Michelson/Typed/T.hs +6/−0
• src/Michelson/Typed/Util.hs +95/−82
• src/Michelson/Typed/Value.hs +31/−44
• src/Michelson/Untyped/Annotation.hs +51/−19
• src/Michelson/Untyped/Entrypoints.hs +19/−14
• src/Michelson/Untyped/Instr.hs +10/−4
• src/Michelson/Untyped/OpSize.hs +6/−0
• src/Michelson/Untyped/Type.hs +41/−14
• src/Michelson/Untyped/Value.hs +11/−1
• src/Morley/Micheline/Binary.hs +31/−28
• src/Morley/Micheline/Class.hs +874/−73
• src/Morley/Micheline/Expression.hs +77/−16
• src/Tezos/Address.hs +65/−62
• src/Tezos/Core.hs +18/−18
• src/Tezos/Crypto.hs +12/−8
• src/Tezos/Crypto/BLS12381.hs +19/−13
• src/Tezos/Crypto/Ed25519.hs +2/−2
• src/Tezos/Crypto/P256.hs +2/−2
• src/Tezos/Crypto/Secp256k1.hs +2/−2
• src/Tezos/Crypto/Util.hs +24/−17
• src/Util/CLI.hs +53/−7
• src/Util/Peano.hs +5/−25
• src/Util/PeanoNatural.hs +84/−0
• src/Util/Positive.hs +4/−4
• src/Util/Sing.hs +93/−0
• src/Util/Type.hs +25/−25
• src/Util/TypeLits.hs +17/−0
• src/Util/Typeable.hs +2/−18

@@ -2,6 +2,91 @@ ========== <!-- Append new entries here --> +1.15.0+======+* [!878](https://gitlab.com/morley-framework/morley/-/merge_requests/878)+  + Fixed behavior of `packValue` to match the `tezos-client hash data`+    behavior.+  + Pair conversion in `instance ToExpression Untyped.Value` always produces+    `ExpressionPrim` instead `ExpressionSeq`. Optimization of right-combed pairs+    moved to `Michelson.Typed.Convert` and depends on `UntypingOptions`.+* [!880](https://gitlab.com/morley-framework/morley/-/merge_requests/880)+  + Fixed loss of type annotations in serialization of right-combed pairs.+* [!795](https://gitlab.com/morley-framework/morley/-/merge_requests/795)+  + Changed typecheck exception messages.+  +  Changed Buildable instances for several datatypes to be based on+     RenderDoc instances.+  + Changed the regexp in scripts/regenerate-gold-files-for-verbose-typechecking.sh+    so it does not ommit extra space in .gold files on MacOS.+* [!863](https://gitlab.com/morley-framework/morley/-/merge_requests/863)+  + Removed conversion from variable anotations to field anontations in+    `PAIRN` instruction.+* [!856](https://gitlab.com/morley-framework/morley/-/merge_requests/856)+  + Removed `Typeable` constrains from singletons generated by `T`.+  + Added the `Util.Sing` module with functions that allow equality comparison+    using `SDecide`.+* [!858](https://gitlab.com/morley-framework/morley/-/merge_requests/858)+  + Added `SomeStorage` type.+  + Modified `runContract` to return `SomeStorage`.+* [!833](https://gitlab.com/morley-framework/morley/-/merge_requests/833)+  + Fixed `ContainsBigMap` and `ContainsNestedBigMaps` instances for `TContract`.+  + Added `Data` instance to `BigMap` and `BigMapId`.+  + Added `requireEqT`, `castM` and `gcastM` to `Util.Typeable`.+* [!859](https://gitlab.com/morley-framework/morley/-/merge_requests/859)+  + Added `BigMapId` type.+  + Added ID to `VBigMap` and `BigMap`.+  + Updated interpreter to assign a unique big_map ID to each big_map, and+    keep track of how many big_maps have been created with a `BigMapCounter`.+  + Deleted `dfsValue`.+  + Renamed `dfsModifyValue` and `dfsFoldValue` to `dfsMapValue` and `dfsFoldMapValue`.+  + Added `dfsTraverseValue` and `dfsFoldMapValueM`.+* [!840](https://gitlab.com/morley-framework/morley/-/merge_requests/840)+  + Changed behaviour of deserializer: it fails if the expression contains+    more annotations than expected instead of ignoring them.+  + Changed behaviour of serializer: it uses list notation for all pair+    values, not just for right-combed ones.+* [!816](https://gitlab.com/morley-framework/morley/-/merge_requests/816)+  + Removed the `SingI` and `KnownPeano` constraints by introducting the+    `PeanoNatural` data type.+  + The similar updates for `SingT`. Removed the `SingI` constraints in the+    constructors of `SingT`+* [!855](https://gitlab.com/morley-framework/morley/-/merge_requests/855)+  + Fix custom error arguments comparison in nettest by converting them+    to `Value t` before checking for equality.+* [!830](https://gitlab.com/morley-framework/morley/-/merge_requests/830)+  + Added the contract's address to some of the `ExecutorError'`+    constructors: `EEIllTypedParameter` and `EEUnexpectedParameterType`.+* [!820](https://gitlab.com/morley-framework/morley/-/merge_requests/820)+  + Moved functions for contract importing (like `importContract`) from cleveland.+  + Added functions for values importing (`readValue`, `importValue` and others).+* [!832](https://gitlab.com/morley-framework/morley/-/merge_requests/832)+  + Add tickets feature.+  + Add dupable restriction to `DUP`-like instructions.+* [!838](https://gitlab.com/morley-framework/morley/-/merge_requests/838)+  + All unsafe functions and data constructors now contain "unsafe" word+    at prefix position. E.g `UnsafeUParam`, `unsafeParseKeyHash`.+* [!828](https://gitlab.com/morley-framework/morley/-/merge_requests/828)+  + Fix bug in serialization of instructions with variable annotations:+    `EMPTY_SET`, `EMPTY_MAP`, `PUSH`, `LAMBDA`, `CAST`, `CONTRACT`.+* [!770](https://gitlab.com/morley-framework/morley/-/merge_requests/770)+  + Added `Fn` meta-instruction to support Morley's typed stack function in+    typed form.+  + Added `STACKTYPE` as a typed `ExtInstr`.+* [!822](https://gitlab.com/morley-framework/morley/-/merge_requests/822)+  + Add new `edo` instruction: `UNPAIR`.+  + Rename `UNPAIR` macro to `UNPAPAIR`.+  + Expand `UNPAPAIR` macros to `UNPAIR` instructions.+  + The `Seq` constructor can now be used as a right-associative operator.+  + Optimize `DUP; CAR; DIP { CDR }` to `UNPAIR`+  + Optimize `DUP; CDR; DIP { CAR }` to `UNPAIR; SWAP`+* [!825](https://gitlab.com/morley-framework/morley/-/merge_requests/825)+  + Fix bug in morley executable's `repl` command: consume the entire input+    when parsing an instruction.+  + Fix bug in the handling of special annotations for `CAR`/`CDR`.+  + Fix bug in parsing of `PAIR` instructions with exactly 1 field ann.+  + Preserve `CAR`/`CDR`'s original annotations when converting them back to+    michelson/binary/json.+ 1.14.0 ====== * [!799](https://gitlab.com/morley-framework/morley/-/merge_requests/799)

@@ -6,14 +6,13 @@   ( main   ) where -import Data.Default (def) import qualified Data.Text.Lazy.IO.Utf8 as Utf8 (writeFile) import Data.Version (showVersion) import Fmt (pretty) import Named (arg, argF, (!)) import Options.Applicative-  (command, execParser, footerDoc, fullDesc, header, help, helper, info, infoOption, long,-  progDesc, short, subparser, switch)+  (execParser, footerDoc, fullDesc, header, help, helper, info, infoOption, long, progDesc, short,+  subparser, switch) import qualified Options.Applicative as Opt import Options.Applicative.Help.Pretty (Doc, linebreak) import Paths_morley (version)@@ -23,16 +22,17 @@ import Michelson.Printer (printSomeContract, printUntypedContract) import Michelson.Runtime (TxData(..), originateContract, prepareContract, runContract, transfer) import Michelson.Runtime.GState (genesisAddress)-import Michelson.TypeCheck (tcVerbose, typeCheckContract)-import Michelson.TypeCheck.Types (SomeContract(..), mapSomeContract)-import Michelson.Typed (Contract(..))+import Michelson.TypeCheck (tcVerbose, typeCheckContract, typeCheckingWith)+import qualified Michelson.TypeCheck as TypeCheck+import Michelson.TypeCheck.Types (mapSomeContract)+import Michelson.Typed (Contract(..), SomeContract(..)) import qualified Michelson.Untyped as U import Morley.CLI import REPL import Tezos.Address (Address) import Tezos.Core (Mutez, Timestamp(..), unsafeMkMutez) import Tezos.Crypto-import Util.CLI (outputOption)+import Util.CLI (mkCommandParser, outputOption) import Util.Main (wrapMain) import Util.Named @@ -62,12 +62,13 @@  data TypeCheckOptions = TypeCheckOptions   { tcoContractFile :: Maybe FilePath-  , tcoVerbose      :: Bool+  , tcoTcOptions    :: TypeCheck.TypeCheckOptions   }  data RunOptions = RunOptions   { roContractFile :: Maybe FilePath   , roDBPath :: FilePath+  , roTcOptions :: TypeCheck.TypeCheckOptions   , roStorageValue :: U.Value   , roTxData :: TxData   , roVerbose :: Bool@@ -81,6 +82,7 @@ data OriginateOptions = OriginateOptions   { ooContractFile :: Maybe FilePath   , ooDBPath :: FilePath+  , ooTcOptions :: TypeCheck.TypeCheckOptions   , ooOriginator :: Address   , ooDelegate :: Maybe KeyHash   , ooStorageValue :: U.Value@@ -90,6 +92,7 @@  data TransferOptions = TransferOptions   { toDBPath :: FilePath+  , toTcOptions :: TypeCheck.TypeCheckOptions   , toDestination :: Address   , toTxData :: TxData   , toNow :: Maybe Timestamp@@ -110,11 +113,6 @@   analyzeSubCmd <>   replSubCmd   where-    mkCommandParser commandName parser desc =-      command commandName $-      info (helper <*> parser) $-      progDesc desc-     typecheckSubCmd =       mkCommandParser "typecheck"         (TypeCheck <$> typeCheckOptions) $@@ -175,10 +173,19 @@       long "dry-run" <>       help "Do not write updated DB to DB file" +    typeCheckOptionsOption :: Opt.Parser TypeCheck.TypeCheckOptions+    typeCheckOptionsOption = do+      tcVerbose <- verboseFlag+      tcStrict <- fmap not . switch $+        long "typecheck-lax" <>+        help "Whether actions permitted in `tezos-client run` but forbidden in \+             \e.g. `tezos-client originate` should be allowed here"+      return TypeCheck.TypeCheckOptions{..}+     typeCheckOptions :: Opt.Parser TypeCheckOptions     typeCheckOptions = TypeCheckOptions       <$> optional contractFileOption-      <*> verboseFlag+      <*> typeCheckOptionsOption      defaultBalance :: Mutez     defaultBalance = unsafeMkMutez 4000000@@ -197,6 +204,7 @@       RunOptions         <$> optional contractFileOption         <*> dbPathOption+        <*> typeCheckOptionsOption         <*> valueOption Nothing (#name .! "storage")             (#help .! "Initial storage of a running contract")         <*> txDataOption@@ -213,6 +221,7 @@       OriginateOptions         <$> optional contractFileOption         <*> dbPathOption+        <*> typeCheckOptionsOption         <*> addressOption (Just genesisAddress)             (#name .! "originator") (#help .! "Contract's originator")         <*> optional@@ -228,6 +237,7 @@     transferOptions :: Opt.Parser TransferOptions     transferOptions = do       toDBPath <- dbPathOption+      toTcOptions <- typeCheckOptionsOption       toDestination <-         addressOption Nothing         (#name .! "to") (#help .! "Destination address")@@ -239,6 +249,13 @@       toDryRun <- dryRunFlag       pure TransferOptions {..} +-- | Most permitting options, when we don't care much about typechecking.+laxTcOptions :: TypeCheck.TypeCheckOptions+laxTcOptions = TypeCheck.TypeCheckOptions+  { TypeCheck.tcVerbose = False+  , TypeCheck.tcStrict = False+  }+ ---------------------------------------------------------------------------- -- Actual main ----------------------------------------------------------------------------@@ -270,24 +287,29 @@       Optimize OptimizeOptions{..} -> do         untypedContract <- prepareContract optoContractFile         checkedContract <--          either throwM pure $ typeCheckContract untypedContract def+          either throwM pure . typeCheckingWith laxTcOptions $+            typeCheckContract untypedContract         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 def+          either throwM pure . typeCheckingWith laxTcOptions $+            typeCheckContract untypedContract         putTextLn $ pretty $ analyze (cCode contract)       TypeCheck TypeCheckOptions{..} -> do         morleyContract <- prepareContract tcoContractFile-        contract <- either throwM pure-          $ typeCheckContract morleyContract def{ tcVerbose = tcoVerbose }-        when tcoVerbose (putStrLn $ printSomeContract False contract)+        -- At the moment of writing, 'tcStrict' option does not change anything+        -- because it affects only values parsing; but this may change+        contract <- either throwM pure . typeCheckingWith tcoTcOptions+          $ typeCheckContract morleyContract+        when (TypeCheck.tcVerbose tcoTcOptions) $+          putStrLn $ printSomeContract False contract         putTextLn "Contract is well-typed"       Run RunOptions {..} -> do         michelsonContract <- prepareContract roContractFile-        void $ runContract roNow roLevel roMaxSteps roInitBalance roDBPath roStorageValue michelsonContract roTxData+        void $ runContract roNow roLevel roMaxSteps roInitBalance roDBPath roTcOptions roStorageValue michelsonContract roTxData           ! #verbose roVerbose           ! #dryRun (not roWrite)       Originate OriginateOptions {..} -> do@@ -295,6 +317,7 @@         addr <-           originateContract             ooDBPath+            ooTcOptions             ooOriginator             ooDelegate             ooBalance@@ -303,7 +326,7 @@             ! #verbose ooVerbose         putTextLn $ "Originated contract " <> pretty addr       Transfer TransferOptions {..} -> do-        transfer toNow toLevel toMaxSteps toDBPath toDestination toTxData+        transfer toNow toLevel toMaxSteps toDBPath toTcOptions toDestination toTxData           ! #verbose toVerbose           ! #dryRun toDryRun       REPL -> runRepl

@@ -21,7 +21,6 @@ import qualified Data.ByteString.Lazy as BSL import Data.List (stripPrefix) import Data.Text (strip)-import Data.Typeable (cast) import Data.Vinyl (Rec(..)) import Fmt (pretty) import System.Console.Haskeline@@ -29,18 +28,21 @@  import Michelson.Interpret (interpretInstr) import Michelson.Macro (ParsedOp, expandList)-import Michelson.Parser (errorBundlePretty, ops, parseExpandValue, type_)+import Michelson.Parser (errorBundlePretty, ops, parseExpandValue, parseNoEnv, type_) import Michelson.Parser.Types (noLetEnv) import Michelson.Printer (printDoc, printTypedValue) import Michelson.Printer.Util (doesntNeedParens) import Michelson.Runtime.Dummy-import Michelson.TypeCheck (SomeInstr(..), SomeInstrOut(..), getWTP, runTypeCheckIsolated)+import Michelson.TypeCheck+  (SomeInstr(..), SomeInstrOut(..), TypeCheckOptions(..), getWTP, runTypeCheckIsolated,+  typeCheckingWith) import Michelson.TypeCheck.Instr (typeCheckList, typeCheckParameter) import Michelson.TypeCheck.Types (HST(..), NotWellTyped(..)) import qualified Michelson.Typed as T import qualified Michelson.Untyped as U+import Util.Sing (castSing) -data SomeStack = forall t. Typeable t => SomeStack+data SomeStack = forall t. T.SingI t => SomeStack   { stValues :: (Rec T.Value t)   , stTypes :: HST t   }@@ -95,8 +97,9 @@     Right parsedOps -> do       let expandedOps = expandList parsedOps       lift get >>= \case-        SomeStack {..} -> case cast stTypes of-          Just hstInp -> case runTypeCheckIsolated $ typeCheckList expandedOps hstInp of+        SomeStack {..} -> case castSing stTypes of+          Just hstInp -> case typeCheckingWith tcOptions . runTypeCheckIsolated $+                                typeCheckList expandedOps hstInp of             Right someInstr -> do               case someInstr of                 _ :/ (instr ::: hstOut)-> case interpretInstr dummyContractEnv instr stValues of@@ -127,26 +130,32 @@ emptyStack = SomeStack RNil SNil  parseInstructions :: Text -> Either Text [ParsedOp]-parseInstructions src = let-  codeParser = runReaderT ops noLetEnv-  in case parse codeParser "" src of+parseInstructions src =+  case parseNoEnv ops "" src of     Right p -> Right p     Left err -> Left (toText $ errorBundlePretty err) +tcOptions :: TypeCheckOptions+tcOptions = TypeCheckOptions+  { tcVerbose = False+  , tcStrict = False+  }+ -- helpers  addValueToHST-  :: forall t xs. Typeable xs+  :: forall t xs. T.SingI xs   => T.Value t   -> HST xs-  -> Either Text (T.Dict (Typeable (t ': xs)), HST (t ': xs))+  -> Either Text (T.Dict (T.SingI (t ': xs)), HST (t ': xs)) addValueToHST v hstIn = case T.valueTypeSanity v of   T.Dict -> case getWTP @t of     Right wtpDict -> Right (T.Dict, (T.starNotes @t, wtpDict, U.noAnn) ::&  hstIn)-    Left (NotWellTyped t) -> let+    Left (NotWellTyped t cause) -> let       U.Ty t' tann = T.toUType t       in Left $ "Value of type '" <> (renderT t' (U.fullAnnSet [tann] [] []))-                <> "' is not well typed in the provided Value."+                <> "' is not well typed in the provided Value because it "+                <> pretty cause <> "."  renderType :: T.SingI t => T.Notes t -> U.VarAnn -> Text renderType notes vann = let@@ -200,7 +209,7 @@     buildStack (Right (SomeStack stk hst)) (txVal, txTyp) = case       (parseExpandValue txVal, parse (runReaderT type_ noLetEnv) "" txTyp) of         (Right val, Right typ) ->-          case typeCheckParameter mempty typ val of+          case typeCheckingWith tcOptions $ typeCheckParameter mempty typ val of             Right (T.SomeValue tVal) ->               case addValueToHST tVal hst of                 Right (T.Dict, newHst) -> Right $ SomeStack (tVal :& stk) newHst

@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           morley-version:        1.14.0+version:        1.15.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@@ -66,6 +66,7 @@       Michelson.Runtime       Michelson.Runtime.Dummy       Michelson.Runtime.GState+      Michelson.Runtime.Import       Michelson.Runtime.TxData       Michelson.Text       Michelson.TypeCheck@@ -85,6 +86,7 @@       Michelson.Typed.Convert       Michelson.Typed.Doc       Michelson.Typed.Entrypoints+      Michelson.Typed.Existential       Michelson.Typed.Extract       Michelson.Typed.Haskell       Michelson.Typed.Haskell.Compatibility@@ -149,7 +151,9 @@       Util.Named       Util.Num       Util.Peano+      Util.PeanoNatural       Util.Positive+      Util.Sing       Util.Text       Util.TH       Util.Type@@ -230,7 +234,6 @@       aeson     , base-noprelude >=4.7 && <5     , bytestring-    , data-default     , fmt     , haskeline     , megaparsec >=7.0.0

@@ -321,17 +321,17 @@     "Doc items section: " <> show (typeRep $ Proxy @d) <>     " / " <> show (length ds) <> " item(s)" -appendDocSectionUnsafe+unsafeAppendDocSection   :: HasCallStack   => DocSection -> DocSection -> DocSection-appendDocSectionUnsafe (DocSection ls) (DocSection rs) =-  DocSection $ appendDocSectionUnsafeImpl ls (toList rs)+unsafeAppendDocSection (DocSection ls) (DocSection rs) =+  DocSection $ unsafeAppendDocSectionImpl ls (toList rs) -appendDocSectionUnsafeImpl+unsafeAppendDocSectionImpl   :: forall d1 d2.      (Typeable d1, Typeable d2, HasCallStack)   => NonEmpty d1 -> [d2] -> NonEmpty d1-appendDocSectionUnsafeImpl (l :| ls) rs =+unsafeAppendDocSectionImpl (l :| ls) rs =   let rs' = rs <&> \r -> cast r ?: onTypeMismatch   in l :| ls <> rs'   where@@ -496,14 +496,14 @@     { cdContents =         M.merge           M.preserveMissing M.preserveMissing-          (M.zipWithMatched $ \_k l r -> appendDocSectionUnsafe l r)+          (M.zipWithMatched $ \_k l r -> unsafeAppendDocSection l r)           (cdContents cd1) (cdContents cd2)     , cdDefinitions =         M.merge           M.preserveMissing M.preserveMissing           (M.zipWithMatched $ \_k (DocSection ls) (DocSection rs) ->              let removeDups = filter $ not . (`isDefinedIn` cdDefinitionIds cd1) . deItem-             in DocSection $ appendDocSectionUnsafeImpl ls (removeDups $ toList rs)+             in DocSection $ unsafeAppendDocSectionImpl ls (removeDups $ toList rs)           )           (cdDefinitions cd1) (cdDefinitions cd2)     , cdDefinitionsSet =

@@ -18,9 +18,13 @@ import Data.Default (Default(..)) import qualified Data.Text as T import Fmt (Buildable (..))+import Michelson.Printer.Util (RenderDoc (..), renderAnyBuildable)+import Text.PrettyPrint.Leijen.Text + import Util.Aeson + newtype Pos = Pos {unPos :: Word}   deriving stock (Eq, Ord, Show, Generic, Data) @@ -61,6 +65,13 @@   { icsCallStack :: LetCallStack   , icsSrcPos    :: SrcPos   } deriving stock (Eq, Ord, Show, Generic, Data)++instance RenderDoc InstrCallStack where+  renderDoc _ InstrCallStack{icsCallStack, icsSrcPos = SrcPos (Pos row) (Pos col)} =+    "Error occurred on line" <+> (renderAnyBuildable (row + 1)) <+> "char" <+> (renderAnyBuildable (col + 1))+    <> case icsCallStack of+         [] -> "."+         _ -> " inside these let defenitions:" <+> (list $ fmap (text . show) icsCallStack) <> "."  instance NFData InstrCallStack 

@@ -15,25 +15,19 @@   , typicalFailWithTag   , isTypicalFailWith   , modifyTypicalFailWith--  , ConstantScope'   ) where +import Data.Singletons (withSingI)+ import Michelson.Text (MText) import Michelson.Typed --- | We need this class to pass it to 'SomeConstrainedValue'.--- 'ConstantScope' is needed because we push a value and 'Typeable' is--- needed for 'FAILWITH'.-class (Typeable a, ConstantScope a) => ConstantScope' a-instance (Typeable a, ConstantScope a) => ConstantScope' a- -- | This data type captures typical ways to use `FAILWITH` instruction. -- Each constructor corresponds to a usage pattern. data TypicalFailWith   = FailWithString MText   -- ^ Push a constant string and fail with it.-  | FailWithConstantPair MText (SomeConstrainedValue ConstantScope')+  | FailWithConstantPair MText (SomeConstrainedValue ConstantScope)   -- ^ Push a constant pair where the first item is a string and the   -- second one is an arbitrary constant. Fail afterwards.   | FailWithStackValue MText@@ -75,7 +69,7 @@   | VPair (VString str, secondItem) <- v =       -- We need to pattern match to deduce `singI` for second item of the pair.       case sing @t of-        STPair {} -> Just (FailWithConstantPair str (SomeConstrainedValue secondItem))+        STPair l r -> withSingI l $ withSingI r $ Just (FailWithConstantPair str (SomeConstrainedValue secondItem))   | otherwise = Nothing  -- | If given instruction ends with a typical 'FAILWITH' usage, modify@@ -83,7 +77,7 @@ -- return any value, not necessarily a string. modifyTypicalFailWith   :: HasCallStack-  => (MText -> SomeConstrainedValue ConstantScope')+  => (MText -> SomeConstrainedValue ConstantScope)   -> Instr inp out   -> Instr inp out modifyTypicalFailWith f = modifyTypicalFailWith' . linearizeLeft@@ -103,7 +97,7 @@               | _ :: Value a <- v               , _ :: Instr (b ': s) ('TPair a b ': s) <- i1 ->                 case sing @('TPair a b) of-                  STPair {} -> case isStringValue v of+                  STPair l r -> withSingI l $ withSingI r $ case isStringValue v of                     Just (f -> SomeConstrainedValue v') ->                       PUSH v' `Seq` PAIR `Seq` FAILWITH                     Nothing ->@@ -112,7 +106,7 @@               | _ :: Value a <- v               , _ :: Instr s0 ('TPair a b ': s) <- i1 ->                 case sing @('TPair a b) of-                  STPair {} -> Seq i0 $ case isStringValue v of+                  STPair l r -> withSingI l $ withSingI r $ Seq i0 $ case isStringValue v of                     Just (f -> SomeConstrainedValue v') ->                       PUSH v' `Seq` PAIR `Seq` FAILWITH                     Nothing ->@@ -123,7 +117,7 @@         i -> i      onPush ::-      (HasCallStack, Typeable v, ConstantScope v) => Value v -> Instr inp out+      (HasCallStack, ConstantScope v) => Value v -> Instr inp out     onPush v = case isTypicalErrorConstant v of       Just (FailWithString (f -> SomeConstrainedValue v')) -> PUSH v' `Seq` FAILWITH       Just (FailWithConstantPair (f -> SomeConstrainedValue v') (SomeConstrainedValue arg)) ->

@@ -37,16 +37,16 @@   , initInterpreterState   , handleContractReturn   , runInstrImpl+  , assignBigMapIds   ) where  import Prelude hiding (EQ, GT, LT) -import Control.Lens (makeLensesFor)+import Control.Lens (makeLensesFor, traverseOf, (<<+=)) import Control.Monad.Except (MonadError, throwError) import Data.Default (Default(..)) import qualified Data.Map as Map import qualified Data.Set as Set-import Data.Singletons (Sing) import Data.Vinyl (Rec(..), (<+>)) import Data.Vinyl.Recursive (rmap) import Fmt (Buildable(build), Builder, blockListF, prettyLn)@@ -57,18 +57,72 @@ import Michelson.TypeCheck (SomeParamType(..), TcOriginatedContracts, matchTypes) import Michelson.Typed hiding (Branch(..)) import qualified Michelson.Typed as T-import Michelson.Typed.Origination (OriginationOperation(..), mkOriginationOperationHash)-import Michelson.Untyped.Annotation (annQ)+import Michelson.Typed.Origination+  (OperationHash(..), OriginationOperation(..), mkContractAddress, mkOriginationOperationHash) import qualified Michelson.Untyped as U-import Tezos.Address (Address(..), GlobalCounter(..), OriginationIndex(..), mkContractAddress)+import Michelson.Untyped.Annotation (annQ)+import Tezos.Address (Address(..), GlobalCounter(..), OriginationIndex(..)) import Tezos.Core (ChainId, Mutez, Timestamp) import Tezos.Crypto (KeyHash, blake2b, checkSignature, hashKey, keccak, sha256, sha3, sha512) import Tezos.Crypto.BLS12381 (checkPairing)-import Util.Peano (LongerThan, Peano, SingNat(SS, SZ))+import Util.Peano (LongerThan, Peano)+import Util.PeanoNatural (PeanoNatural(..))+import Util.Sing (eqParamSing) import Util.TH import Util.Type import Util.Typeable +-- | Morley logs for interpreter state that are stored in reverse order.+newtype MorleyLogs = MorleyLogs [Text]+  deriving stock (Eq, Show, Generic)+  deriving newtype Default++pickMorleyLogs :: MorleyLogs -> [Text]+pickMorleyLogs (MorleyLogs logs) = reverse logs++instance Buildable MorleyLogs where+  build = blockListF . pickMorleyLogs++instance NFData MorleyLogs++noMorleyLogs :: MorleyLogs+noMorleyLogs = MorleyLogs []++newtype RemainingSteps = RemainingSteps Word64+  deriving stock (Show, Generic)+  deriving newtype (Eq, Ord, Buildable, Num)++instance NFData RemainingSteps++data InterpreterState = InterpreterState+  { isMorleyLogs :: MorleyLogs+  , isRemainingSteps :: RemainingSteps+  , isOriginationNonce :: OriginationIndex+  , isBigMapCounter :: BigMapCounter+  } deriving stock (Show, Generic)++instance NFData InterpreterState+makeLensesFor+  [ ("isMorleyLogs", "isMorleyLogsL")+  , ("isBigMapCounter", "isBigMapCounterL")+  ]+  ''InterpreterState++data StkEl t = StkEl+  { seValue :: Value t+  , seVarAnn :: U.VarAnn+  , seNotes :: Notes t+  } deriving stock (Eq, Show)++makeLensesFor+  [ ("seValue", "seValueL")+  , ("seVarAnn", "seVarAnnL")+  ]+  ''StkEl++starNotesStkEl :: forall t. Value t -> StkEl t+starNotesStkEl v = StkEl v U.noAnn $ withValueTypeSanity v $ starNotes @t+ -- | Environment for contract execution. data ContractEnv = ContractEnv   { ceNow :: Timestamp@@ -92,7 +146,7 @@   -- ^ Distribution of voting power.   , ceChainId :: ChainId   -- ^ Identifier of the current chain.-  , ceOperationHash :: Maybe U.OperationHash+  , ceOperationHash :: Maybe OperationHash   -- ^ Hash of the currently executed operation, required for   -- correct contract address computation in 'CREATE_CONTRACT' instruction.   , ceGlobalCounter :: GlobalCounter@@ -105,7 +159,7 @@ -- | Represents @[FAILED]@ state of a Michelson program. Contains -- value that was on top of the stack when @FAILWITH@ was called. data MichelsonFailed where-  MichelsonFailedWith :: (KnownT t, ConstantScope t) => T.Value t -> MichelsonFailed+  MichelsonFailedWith :: (SingI t, ConstantScope t) => T.Value t -> MichelsonFailed   MichelsonArithError     :: (Typeable n, Typeable m, Typeable instr)     => ArithError (Value' instr n) (Value' instr m) -> MichelsonFailed@@ -115,7 +169,7 @@ deriving stock instance Show MichelsonFailed  instance Eq MichelsonFailed where-  MichelsonFailedWith v1 == MichelsonFailedWith v2 = v1 `eqParam1` v2+  MichelsonFailedWith v1 == MichelsonFailedWith v2 = v1 `eqParamSing` v2   MichelsonFailedWith _ == _ = False   MichelsonArithError ae1 == MichelsonArithError ae2 = ae1 `eqParam2` ae2   MichelsonArithError _ == _ = False@@ -170,22 +224,6 @@   , iurNewState = st   } --- | Morley logs for interpreter state that are stored in reverse order.-newtype MorleyLogs = MorleyLogs [Text]-  deriving stock (Eq, Show, Generic)-  deriving newtype Default--pickMorleyLogs :: MorleyLogs -> [Text]-pickMorleyLogs (MorleyLogs logs) = reverse logs--instance Buildable MorleyLogs where-  build = blockListF . pickMorleyLogs--instance NFData MorleyLogs--noMorleyLogs :: MorleyLogs-noMorleyLogs = MorleyLogs []- type ContractReturn st =   (Either MichelsonFailed ([Operation], T.Value st), InterpreterState) @@ -226,7 +264,7 @@   -> T.Value st   -> T.Notes st   -> Rec StkEl (ContractInp param st)-mkInitStack param T.ParamNotesUnsafe{..} st stNotes = StkEl+mkInitStack param T.UnsafeParamNotes{..} st stNotes = StkEl   (T.VPair (param, st))   U.noAnn   (T.NTPair U.noAnn (U.convAnn pnRootAnn) U.noAnn [annQ|parameter|] [annQ|storage|] pnNotes stNotes)@@ -241,13 +279,14 @@   -> EntrypointCallT cp arg   -> T.Value arg   -> T.Value st+  -> BigMapCounter   -> ContractEnv   -> ContractReturn st-interpret contract epc param initSt env =-  interpret' contract epc param initSt env (initInterpreterState env)+interpret contract epc param initSt bmCounter env =+  interpret' contract epc param initSt env (initInterpreterState bmCounter env) -initInterpreterState :: ContractEnv -> InterpreterState-initInterpreterState env = InterpreterState def (ceMaxSteps env) (OriginationIndex 0)+initInterpreterState :: BigMapCounter -> ContractEnv -> InterpreterState+initInterpreterState bmCounter env = InterpreterState def (ceMaxSteps env) (OriginationIndex 0) bmCounter  -- | Interpret an instruction in vacuum, putting no extra contraints on -- its execution.@@ -278,25 +317,12 @@       { isMorleyLogs = MorleyLogs []       , isRemainingSteps = 9999999999       , isOriginationNonce = OriginationIndex 0+      , isBigMapCounter = 0       }  data SomeItStack where   SomeItStack :: T.ExtInstr inp -> Rec StkEl inp -> SomeItStack -newtype RemainingSteps = RemainingSteps Word64-  deriving stock (Show, Generic)-  deriving newtype (Eq, Ord, Buildable, Num)--instance NFData RemainingSteps--data InterpreterState = InterpreterState-  { isMorleyLogs :: MorleyLogs-  , isRemainingSteps :: RemainingSteps-  , isOriginationNonce :: OriginationIndex-  } deriving stock (Show, Generic)--instance NFData InterpreterState- type EvalOp a =   ExceptT MichelsonFailed     (ReaderT ContractEnv@@ -337,15 +363,6 @@   , MonadError MichelsonFailed m   ) -data StkEl t = StkEl-  { seValue :: Value t-  , seVarAnn :: U.VarAnn-  , seNotes :: Notes t-  } deriving stock (Eq, Show)--starNotesStkEl :: forall t. Value t -> StkEl t-starNotesStkEl v = StkEl v U.noAnn $ withValueTypeSanity v $ starNotes @t- type InstrRunner m =   forall inp out.      Instr inp out@@ -361,6 +378,8 @@ runInstr i@(InstrWithVarAnns _ _i1) r = runInstrImpl runInstr i r runInstr i@Nop r = runInstrImpl runInstr i r runInstr i@(Nested _) r = runInstrImpl runInstr i r+runInstr i@(DocGroup _ _i1) r = runInstrImpl runInstr i r+runInstr i@(Fn _ _ _i1) r = runInstrImpl runInstr i r runInstr i r = do   rs <- isRemainingSteps <$> getInterpreterState   if rs == 0@@ -373,7 +392,7 @@ runInstrNoGas = runInstrImpl runInstrNoGas  -- | Function to interpret Michelson instruction(s) against given stack.-runInstrImpl :: EvalM m => InstrRunner m -> InstrRunner m+runInstrImpl :: forall m. EvalM m => InstrRunner m -> InstrRunner m runInstrImpl runner (Seq i1 i2) r = runner i1 r >>= \r' -> runner i2 r' runInstrImpl runner (WithLoc _ i) r = runner i r runInstrImpl runner (InstrWithNotes (_ :: Proxy rest) notes instr) inp = do@@ -401,11 +420,13 @@ runInstrImpl runner (Ext nop) r = r <$ interpretExt runner (SomeItStack nop r) runInstrImpl runner (Nested sq) r = runner sq r runInstrImpl runner (DocGroup _ sq) r = runInstrImpl runner sq r+runInstrImpl runner (Fn _ _ i) r = runner i r runInstrImpl _ DROP (_ :& r) = pure $ r-runInstrImpl runner (DROPN s) stack =-  case s of-    SZ -> pure stack-    SS s' -> case stack of+runInstrImpl runner (DROPN n) stack =+  case n of+    Zero    -> pure stack+    Succ s' -> case stack of+      (_ :& r) -> runInstrImpl runner (DROPN s') r       -- Note: we intentionally do not use `runner` to recursively       -- interpret `DROPN` here.       -- All these recursive calls together correspond to a single@@ -413,35 +434,38 @@       -- This recursion is implementation detail of `DROPN`.       -- The same reasoning applies to other instructions parameterized       -- by a natural number like 'DIPN'.-      (_ :& r) -> runInstrImpl runner (DROPN s') r-runInstrImpl _ DUP (a :& r) = pure $ a :& a :& r-runInstrImpl _ (DUPN nSing) stack = pure $ go nSing stack+runInstrImpl _ DUP (stkEl :& r) = do+  -- If we're duplicating a big_map, or a value containing big_map(s), we need to generate new big_map ID(s).+  duplicateStkEl <- traverseOf seValueL assignBigMapIds' stkEl+  pure $ duplicateStkEl :& stkEl :& r+runInstrImpl _ (DUPN s) stack = go s stack   where     go :: forall (n :: Peano) inp out a. ConstraintDUPN n inp out a-       => Sing n -> Rec StkEl inp -> Rec StkEl out-    go = curry \case-      -- Discard variable annotations. This is consistent with tezos-client.-      (SS SZ, i@(StkEl a _ n :& _)) -> StkEl a U.noAnn n :& i-      (SS s@(SS _), b :& r) -> case go s r of+       => PeanoNatural n -> Rec StkEl inp -> m (Rec StkEl out)+    go (Succ Zero) stk@(stkEl :& _) = do+        -- If we're duplicating a big_map, or a value containing big_map(s), we need to generate new big_map ID(s).+        duplicateStkEl <- traverseOf seValueL assignBigMapIds' stkEl+        -- Discard variable annotations. This is consistent with tezos-client.+        pure $ (duplicateStkEl & seVarAnnL .~ U.noAnn) :& stk+    go (Succ n@(Succ _)) (b :& r) =+      go n r <&> \case         (a :& resTail) -> a :& b :& resTail runInstrImpl _ SWAP (a :& b :& r) = pure $ b :& a :& r-runInstrImpl _ (DIG nSing0) input0 =-  pure $ go nSing0 input0+runInstrImpl _ (DIG s) input0 =+  pure $ go s input0   where     go :: forall (n :: Peano) inp out a. ConstraintDIG n inp out a-       => Sing n -> Rec StkEl inp -> Rec StkEl out-    go = curry \case-      (SZ, stack) -> stack-      (SS nSing, b :& r) -> case go nSing r of-        (a :& resTail) -> a :& b :& resTail-runInstrImpl _ (DUG nSing0) input0 =-  pure $ go nSing0 input0+       => PeanoNatural n -> Rec StkEl inp -> Rec StkEl out+    go Zero stack = stack+    go (Succ n') (b :& r) = case go n' r of+      (a :& resTail) -> a :& b :& resTail+runInstrImpl _ (DUG s) input0 =+  pure $ go s input0   where     go :: forall (n :: Peano) inp out a. ConstraintDUG n inp out a-       => Sing n -> Rec StkEl inp -> Rec StkEl out-    go = curry \case-      (SZ, stack) -> stack-      (SS s', a :& b :& r) -> b :& go s' (a :& r)+       => PeanoNatural n -> Rec StkEl inp -> Rec StkEl out+    go Zero stack = stack+    go (Succ n') (a :& b :& r) = b :& go n' (a :& r) runInstrImpl _ SOME ((seValue -> a) :& r) =   withValueTypeSanity a $     pure $ starNotesStkEl (VOption (Just a)) :& r@@ -455,28 +479,30 @@ runInstrImpl _ NEVER inp = case inp of {} runInstrImpl _ (AnnPAIR{}) ((StkEl a _ _) :& (StkEl b _ _) :& r) =   pure $ starNotesStkEl (VPair (a, b)) :& r-runInstrImpl _ (PAIRN nSing) stack = pure $ go nSing stack+runInstrImpl _ (AnnUNPAIR{}) ((StkEl (VPair (a, b)) _ _) :& r) =+  pure $ starNotesStkEl a :& starNotesStkEl b :& r+runInstrImpl _ (PAIRN s) stack = pure $ go s stack   where-    go :: forall n inp. ConstraintPairN n inp => Sing n -> Rec StkEl inp -> Rec StkEl (PairN n inp)-    go (SS (SS SZ)) (StkEl a _ _ :& StkEl b _ _ :& r) =+    go :: forall n inp. ConstraintPairN n inp => PeanoNatural n -> Rec StkEl inp -> Rec StkEl (PairN n inp)+    go (Succ (Succ Zero)) (StkEl a _ _ :& StkEl b _ _ :& r) =       -- if n=2       starNotesStkEl (VPair (a, b)) :& r-    go (SS n@(SS (SS _))) (StkEl a _ _ :& r@(_ :& _ :& _)) =+    go (Succ n@(Succ (Succ _))) (StkEl a _ _ :& r@(_ :& _ :& _)) =       -- if n>2       case go n r of         StkEl combed _ _ :& r' ->             starNotesStkEl (VPair (a, combed)) :& r'-runInstrImpl _ (UNPAIRN nSing) (StkEl pair0 _ pairNotes0 :& r) = do-  pure $ go nSing pair0 pairNotes0 <+> r+runInstrImpl _ (UNPAIRN s) (StkEl pair0 _ pairNotes0 :& r) = do+  pure $ go s pair0 pairNotes0 <+> r   where     go       :: forall n pair. ConstraintUnpairN n pair-      => Sing n -> Value pair -> Notes pair+      => PeanoNatural n -> Value pair -> Notes pair       -> Rec StkEl (UnpairN n pair)     go n pair pairNotes =       case (n, pair, pairNotes) of         -- if n=2-        (SS (SS SZ), VPair (a, b), NTPair _ aFieldAnn bFieldAnn _ _ aNotes bNotes) ->+        (Succ (Succ Zero), VPair (a, b), NTPair _ aFieldAnn bFieldAnn _ _ aNotes bNotes) ->           -- @UNPAIR n@ converts field annotations into var annotations.           --           -- > /* [ @pair pair (int %aa) (int %bb) (int %cc) (int %dd) ] */ ;@@ -492,11 +518,11 @@             :& StkEl b (U.convAnn @U.FieldTag @U.VarTag bFieldAnn) bNotes             :& RNil         -- if n>2-        (SS n'@(SS (SS _)), VPair (a, b@(VPair _)), NTPair _ aFieldAnn _ _ _ aNotes bNotes) ->+        (Succ n'@(Succ (Succ _)), VPair (a, b@(VPair _)), NTPair _ aFieldAnn _ _ _ aNotes bNotes) ->           StkEl a (U.convAnn @U.FieldTag @U.VarTag aFieldAnn) aNotes             :& go n' b bNotes-runInstrImpl _ (AnnCAR _) (StkEl (VPair (a, _b)) _ _ :& r) = pure $ starNotesStkEl a :& r-runInstrImpl _ (AnnCDR _) (StkEl (VPair (_a, b)) _ _ :& r) = pure $ starNotesStkEl b :& r+runInstrImpl _ (AnnCAR _ _) (StkEl (VPair (a, _b)) _ _ :& r) = pure $ starNotesStkEl a :& r+runInstrImpl _ (AnnCDR _ _) (StkEl (VPair (_a, b)) _ _ :& r) = pure $ starNotesStkEl b :& r runInstrImpl _ (AnnLEFT nt nf1 nf2) ((StkEl a _ na) :& r) =   withValueTypeSanity a $     pure $ StkEl (VOr $ Left a) U.noAnn (NTOr nt nf1 nf2 na starNotes) :& r@@ -515,7 +541,9 @@ runInstrImpl _ SIZE (a :& r) = pure $ starNotesStkEl (VNat $ (fromInteger . toInteger) $ evalSize $ seValue a) :& r runInstrImpl _ EMPTY_SET r = pure $ starNotesStkEl (VSet Set.empty) :& r runInstrImpl _ EMPTY_MAP r = pure $ starNotesStkEl (VMap Map.empty) :& r-runInstrImpl _ EMPTY_BIG_MAP r = pure $ starNotesStkEl (VBigMap Map.empty) :& r+runInstrImpl _ EMPTY_BIG_MAP r = do+  bigMap <- assignBigMapIds' $ VBigMap Nothing Map.empty+  pure $ starNotesStkEl bigMap :& r runInstrImpl runner (MAP (code :: Instr (MapOpInp c ': s) (b ': s))) (StkEl a vn n :& r) = do   -- Evaluation must preserve all stack modifications that @MAP@'s does.   (newStack, newList) <- foldlM (\(curStack, curList) (val :: StkEl (MapOpInp c)) -> do@@ -532,27 +560,27 @@     (Nothing, _) -> pure r runInstrImpl _ MEM (a :& b :& r) = pure $ starNotesStkEl (VBool (evalMem (seValue a) (seValue b))) :& r runInstrImpl _ GET (a :& b :& r) = pure $ starNotesStkEl (VOption (evalGet (seValue a) (seValue b))) :& r-runInstrImpl _ (GETN index0) (StkEl pair _ _ :& r) = do-  pure $ starNotesStkEl (go index0 pair) :& r+runInstrImpl _ (GETN s) (StkEl pair _ _ :& r) = do+  pure $ starNotesStkEl (go s pair) :& r   where     go       :: forall ix a. ConstraintGetN ix a-      => Sing ix -> Value a+      => PeanoNatural ix -> Value a       -> Value (GetN ix a)-    go SZ           a                  = a-    go (SS SZ)      (VPair (left, _))  = left-    go (SS (SS n')) (VPair (_, right)) = go n' right+    go Zero            a                   = a+    go (Succ Zero)      (VPair (left, _))  = left+    go (Succ (Succ n')) (VPair (_, right)) = go n' right runInstrImpl _ UPDATE (a :& b :& StkEl c _ _ :& r) =   pure $ starNotesStkEl (evalUpd (seValue a) (seValue b) c) :& r-runInstrImpl _ (UPDATEN index0) (StkEl (val :: Value val) _ _  :& StkEl pair _ _ :& r) = do-  pure $ starNotesStkEl (go index0 pair) :& r+runInstrImpl _ (UPDATEN s) (StkEl (val :: Value val) _ _  :& StkEl pair _ _ :& r) = do+  pure $ starNotesStkEl (go s pair) :& r   where     go       :: forall ix pair. ConstraintUpdateN ix pair-      => Sing ix -> Value pair -> Value (UpdateN ix val pair)-    go SZ           _                      = val-    go (SS SZ)      (VPair (_, right))     = VPair (val, right)-    go (SS (SS n')) (VPair (left, right))  = VPair (left, go n' right)+      => PeanoNatural ix -> Value pair -> Value (UpdateN ix val pair)+    go Zero             _                      = val+    go (Succ Zero)      (VPair (_, right))     = VPair (val, right)+    go (Succ (Succ n')) (VPair (left, right))  = VPair (left, go n' right) runInstrImpl _ GET_AND_UPDATE (StkEl key _ _ :& StkEl valMb _ _ :& StkEl collection _ _ :& r) =   pure $     starNotesStkEl (VOption (evalGet key collection))@@ -582,8 +610,8 @@   pure $ a :& res runInstrImpl runner (DIPN s i) stack =   case s of-    SZ -> runner i stack-    SS s' -> case stack of+    Zero -> runner i stack+    Succ s' -> case stack of       (a :& r) -> (a :&) <$> runInstrImpl runner (DIPN s' i) r runInstrImpl _ FAILWITH (a :& _) = throwError $ MichelsonFailedWith (seValue a) runInstrImpl _ CAST (StkEl a _ _ :& r) = pure $ starNotesStkEl a :& r@@ -750,7 +778,28 @@ runInstrImpl _ SELF_ADDRESS r = do   ContractEnv{..} <- ask   pure $ starNotesStkEl (VAddress $ EpAddress ceSelf DefEpName) :& r-+runInstrImpl _ TICKET (StkEl dat _ _ :& StkEl (VNat am) _ _ :& r) = do+  ContractEnv{..} <- ask+  pure $ starNotesStkEl (VTicket ceSelf dat am) :& r+runInstrImpl _ READ_TICKET (te@(StkEl (VTicket addr dat am) _ _) :& r) = do+  pure $+    starNotesStkEl+      (VPair (VAddress (EpAddress addr DefEpName), (VPair (dat, VNat am))))+    :& te :& r+runInstrImpl _ SPLIT_TICKET+    (StkEl tv@(VTicket addr dat am) _ _ :&+     StkEl (VPair (VNat am1, VNat am2)) _ _ :& r) = do+  let result = withValueTypeSanity tv $ VOption do+        guard (am1 + am2 == am)+        return $ VPair (VTicket addr dat am1, VTicket addr dat am2)+  pure $ starNotesStkEl result :& r+runInstrImpl _ JOIN_TICKETS+  (StkEl (VPair (tv1@(VTicket addr1 dat1 am1), VTicket addr2 dat2 am2)) _ _ :& r) = do+  let result = withValueTypeSanity tv1 $ VOption do+        guard (addr1 == addr2)+        guard (dat1 == dat2)+        return $ VTicket addr1 dat1 (am1 + am2)+  pure $ starNotesStkEl result :& r  -- | Evaluates an arithmetic operation and either fails or proceeds. runArithOp@@ -771,7 +820,7 @@ runUnpack bs =   -- TODO [TM-80] Gas consumption here should depend on unpacked data size   -- and size of resulting expression, errors would also spend some (all equally).-  -- Fortunatelly, the inner decoding logic does not need to know anything about gas use.+  -- Fortunately, the inner decoding logic does not need to know anything about gas use.   unpackValue' bs  createOrigOp@@ -810,6 +859,7 @@  interpretExt _ (SomeItStack T.DOC_ITEM{} _) = pass interpretExt _ (SomeItStack T.COMMENT_ITEM{} _) = pass+interpretExt _ (SomeItStack T.STACKTYPE{} _) = pass  -- | Access given stack reference (in CPS style). withStackElem@@ -823,10 +873,27 @@   where     loop       :: forall s (n :: Peano). (LongerThan s n)-      => (Rec StkEl s, Sing n) -> a+      => (Rec StkEl s, PeanoNatural n) -> a     loop = \case-      (e :& _, SZ) -> cont e-      (_ :& es, SS n) -> loop (es, n)+      (e :& _, Zero) -> cont e+      (_ :& es, Succ n) -> loop (es, n) +assignBigMapIds' :: EvalM m => Value t -> m (Value t)+assignBigMapIds' val = do+  bigMapCounter0 <- view isBigMapCounterL <$> getInterpreterState+  let (storageWithIds, bigMapCounter1) = runState (assignBigMapIds val) bigMapCounter0+  modifyInterpreterState (set isBigMapCounterL bigMapCounter1)+  pure storageWithIds++-- | All big_maps stored in a chain have a globally unique ID.+--+-- We use this function to assign a new ID whenever a big_map is created.+assignBigMapIds :: MonadState BigMapCounter m => Value t -> m (Value t)+assignBigMapIds =+  dfsTraverseValue \case+    VBigMap _ vBigMap -> do+      bigMapId <- bigMapCounter <<+= 1+      pure $ VBigMap (Just bigMapId) vBigMap+    v -> pure v+ (deriveGADTNFData ''MichelsonFailed)-makeLensesFor [("isMorleyLogs", "isMorleyLogsL")] ''InterpreterState

@@ -6,588 +6,39 @@ -- -- This is nearly symmetric to adjacent Unpack.hs module. module Michelson.Interpret.Pack-  ( packCode'-  , packT'-  , packValue+  ( packValue   , packValue'   , packValuePrefix-    -- * Serializers used in morley-client-  , encodeValue'-  , encodeValue-  , packNotedT'-    -- * Internals-  , encodeIntPayload-  , encodeKeyHashRaw-  , encodeEpAddress+  , toBinary+  , toBinary'   ) where  import Prelude hiding (EQ, GT, LT) -import qualified Data.Binary.Put as Bi-import qualified Data.ByteArray as ByteArray-import qualified Data.ByteString.Lazy as LBS-import qualified Data.Map as Map-import Data.Singletons (Sing, demote)-import Data.Vinyl (Rec(..))-import Util.Type (type (++))--import Michelson.Interpret.Utils-import Michelson.Text import Michelson.Typed-import Michelson.Untyped.Annotation-  (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)-import qualified Tezos.Crypto.BLS12381 as BLS-import qualified Tezos.Crypto.Ed25519 as Ed25519-import qualified Tezos.Crypto.P256 as P256-import qualified Tezos.Crypto.Secp256k1 as Secp256k1-import Util.Peano (peanoValSing)+import Morley.Micheline.Binary (encodeExpression, encodeExpression')+import Morley.Micheline.Class (ToExpression(..)) --- | Prefix prepended to the binary representation of a value.-packValuePrefix :: IsString s => s-packValuePrefix = "\x05"+-- | Generic serializer.+toBinary :: ToExpression a => a -> LByteString+toBinary = encodeExpression . toExpression +-- | Same as 'toBinary', for strict bytestring.+toBinary' :: ToExpression a => a -> ByteString+toBinary' = encodeExpression' . toExpression+ -- | Serialize a value given to @PACK@ instruction. packValue :: PackedValScope t => Value t -> LByteString-packValue x = packValuePrefix <> encodeValue x+packValue x =+  let uval = untypeValueHashable x+  in packValuePrefix <> (encodeExpression $ toExpression uval)  -- | Same as 'packValue', for strict bytestring. packValue' :: PackedValScope t => Value t -> ByteString-packValue' = LBS.toStrict . packValue--encodeValue' :: (SingI t, HasNoOp t) => Value t -> ByteString-encodeValue' = LBS.toStrict . encodeValue--packT' :: forall (t :: T). SingI t => ByteString-packT' = LBS.toStrict $ encodeT' @t--packCode' :: Instr inp out -> ByteString-packCode' = LBS.toStrict . encodeInstrs---- | Generic serializer.------ We don't require @HasNoBigMap@ constraint here since the big_map serialization--- is only prohibited in @PACK@ instructions, however, we still want to be able to--- serialize big_map e.g. in order to transform typed value to low-level Micheline--- representation.--- TODO: Serialize chain operations properly as well since they actually also have--- byte representation.-encodeValue :: forall t. (SingI t, HasNoOp t) => Value t -> LByteString-encodeValue val = case (val, sing @t) of-  (VKey s, _) -> encodeBytes' $ case s of-    PublicKeyEd25519 pk -> "\x00" <> Ed25519.publicKeyToBytes pk-    PublicKeySecp256k1 pk -> "\x01" <> Secp256k1.publicKeyToBytes pk-    PublicKeyP256 pk -> "\x02" <> P256.publicKeyToBytes pk-  (VUnit, _) -> "\x03\x0b"-  (VSignature x, _) -> encodeBytes' $ signatureToBytes x-  (VChainId x, _) ->-    encodeBytes' $ ByteArray.convert (unChainId x)-  (VOption (Just x), STOption _) -> "\x05\x09" <> encodeValue x-  (VOption Nothing, _) -> "\x03\x06"-  (VList xs, STList _) -> encodeList encodeValue xs-  (VSet xs, (STSet (st :: Sing st))) -> case checkOpPresence st of-    OpAbsent -> encodeList encodeValue (toList xs)-  (VContract addr sepc, _) -> encodeEpAddress $ EpAddress addr (sepcName sepc)-  (VPair (v1, v2), STPair l _) ->-    case checkOpPresence l of-      OpAbsent -> "\x07\x07" <> encodeValue v1 <> encodeValue v2-  (VOr (Left v), STOr l _) ->-    case checkOpPresence l of-      OpAbsent -> "\x05\x05" <> encodeValue v-  (VOr (Right v), STOr l _) ->-    case checkOpPresence l of-      OpAbsent-> "\x05\x08" <> encodeValue v-  (VLam lam, _) -> encodeInstrs $ rfAnyInstr lam-  (VMap m, STMap sk _) -> case checkOpPresence sk of-    OpAbsent -> encodeMap m-  (VBigMap m, STBigMap sk _) -> case checkOpPresence sk of-    OpAbsent -> encodeMap m-  (VInt x, STInt) -> encodeNumeric x-  (VNat x, STNat) -> encodeNumeric x-  (VString text, STString) -> encodeString text-  (VBytes bytes, STBytes) -> encodeBytes' bytes-  (VMutez x, STMutez) -> encodeNumeric (unMutez x)-  (VBool True, STBool) -> "\x03\x0a"-  (VBool False, STBool) -> "\x03\x03"-  (VKeyHash kh, STKeyHash) -> encodeBytes $ encodeKeyHashRaw kh-  (VBls12381Fr v, STBls12381Fr) -> encodeBytes' $ BLS.toMichelsonBytes v-  (VBls12381G1 v, STBls12381G1) -> encodeBytes' $ BLS.toMichelsonBytes v-  (VBls12381G2 v, STBls12381G2) -> encodeBytes' $ BLS.toMichelsonBytes v-  (VTimestamp x, STTimestamp) -> encodeNumeric (timestampToSeconds @Integer x)-  (VAddress addr, STAddress) -> encodeEpAddress addr--encodeLength :: Int -> LByteString-encodeLength = Bi.runPut . Bi.putWord32be . fromIntegral---- | Lift encoded list content to an entire encoded list.-encodeAsList :: LByteString -> LByteString-encodeAsList bs = encodeLength (length bs) <> bs---- | Encode a list-like structure.-encodeList :: (a -> LByteString) -> [a] -> LByteString-encodeList encodeElem l = "\x02" <> encodeAsList (LBS.concat $ map encodeElem l)---- | Encode a text.-encodeString :: MText -> LByteString-encodeString text = "\x01" <> encodeAsList (encodeUtf8 $ unMText text)---- | Encode some raw data.-encodeBytes :: LByteString -> LByteString-encodeBytes bs =-  "\x0a" <> encodeAsList bs---- | Version of 'encodeBytes' that accepts a strict bytestring.-encodeBytes' :: ByteString -> LByteString-encodeBytes' = encodeBytes . LBS.fromStrict--encodeEpName :: EpName -> LByteString-encodeEpName = encodeUtf8 . unAnnotation . epNameToRefAnn . canonicalize-  where-    canonicalize :: EpName -> EpName-    canonicalize (EpNameUnsafe "default") = DefEpName-    canonicalize epName                   = epName---- | Encode some map.-encodeMap :: (SingI v, HasNoOp v, SingI k, HasNoOp k) => Map (Value k) (Value v) -> LByteString-encodeMap m =-  encodeList (\(k, v) -> "\x07\x04" <> encodeValue k <> encodeValue v) (Map.toList m)--encodeKeyHashRaw :: KeyHash -> LByteString-encodeKeyHashRaw kh = (<> LBS.fromStrict (khBytes kh)) $-  case khTag kh of-    KeyHashEd25519 -> "\x00"-    KeyHashSecp256k1 -> "\x01"-    KeyHashP256 -> "\x02"--encodeAddress :: Address -> LByteString-encodeAddress = \case-  KeyAddress keyHash ->-    "\x00" <> (encodeKeyHashRaw keyHash)-  ContractAddress (ContractHash address) ->-    "\x01" <> LBS.fromStrict address <> "\x00"--encodeEpAddress :: EpAddress -> LByteString-encodeEpAddress (EpAddress addr epName) =-  encodeBytes $ encodeAddress addr <> encodeEpName epName---- | Encode contents of a given number.-encodeIntPayload :: Integer -> LByteString-encodeIntPayload = LBS.pack . toList . encodeZarithNumber---- | Encode an int-like value.-encodeNumeric :: Integral i => i -> LByteString-encodeNumeric i = "\x00" <> encodeIntPayload (fromIntegral i)---- | Encode a code block.-encodeInstrs :: Instr inp out -> LByteString-encodeInstrs = encodeList id . one . encodeInstr---- | Encode an instruction.-encodeInstr :: forall inp out. Instr inp out -> LByteString-encodeInstr = \case-  WithLoc _ i ->-    encodeInstr i-  InstrWithNotes proxy notes instr ->-    encodeNotedInstr proxy instr notes []-  InstrWithVarNotes varNotes a -> case a of-    AnnLEFT{} | _ :: Proxy ('TOr l r ': s) <- Proxy @out ->-      encodeVarNotedInstr a varNotes (encodeT' @r)-    AnnRIGHT{} | _ :: Proxy ('TOr l r ': s) <- Proxy @out ->-      encodeVarNotedInstr a varNotes (encodeT' @l)-    _ -> encodeVarNotedInstr a varNotes ""-  InstrWithVarAnns _ a ->-    encodeInstr a-  FrameInstr _ i ->-    encodeInstr i-  Seq a b ->-    encodeInstr a <> encodeInstr b-  Nop ->-    mempty-  Nested i ->-    encodeInstrs i-  DocGroup _ i ->-    encodeInstrs i-  Ext _ ->-    ""-  DROP ->-    "\x03\x20"-  DROPN s ->-    "\x05\x20" <> encodeNumeric (peanoValSing s)-  DUP ->-    "\x03\x21"-  DUPN s ->-    "\x05\x21" <> encodeNumeric (peanoValSing s)-  SWAP ->-    "\x03\x4c"-  DIG s ->-    "\x05\x70" <> encodeNumeric (peanoValSing s)-  DUG s ->-    "\x05\x71" <> encodeNumeric (peanoValSing s)-  PUSH (a :: Value t) ->-    "\x07\x43" <> encodeT' @t <> encodeValue a-  SOME ->-    "\x03\x46"-  NONE | _ :: Proxy ('TOption t ': s) <- Proxy @out ->-    "\x05\x3e" <> encodeT' @t-  UNIT ->-    "\x03\x4f"-  IF_NONE a b ->-    "\x07\x2f" <> encodeInstrs a <> encodeInstrs b-  AnnPAIR tn fn1 fn2 ->-    encodeWithAnns [tn] [fn1, fn2] [] "\x03\x42"-  PAIRN n ->-    "\x05\x42" <> encodeNumeric (peanoValSing n)-  UNPAIRN n ->-    "\x05\x7a" <> encodeNumeric (peanoValSing n)-  (AnnCAR fn) ->-    encodeWithAnns [] [fn] [] "\x03\x16"-  (AnnCDR fn) ->-    encodeWithAnns [] [fn] [] "\x03\x17"-  (AnnLEFT tn fn1 fn2) | _ :: Proxy ('TOr l r ': s) <- Proxy @out ->-    encodeWithAnns [tn] [fn1, fn2] [] $ "\x05\x33" <> encodeT' @r-  (AnnRIGHT tn fn1 fn2) | _ :: Proxy ('TOr l r ': s) <- Proxy @out ->-    encodeWithAnns [tn] [fn1, fn2] [] $ "\x05\x44" <> encodeT' @l-  IF_LEFT a b ->-    "\x07\x2e" <> encodeInstrs a <> encodeInstrs b-  NIL | _ :: Proxy ('TList t ': s) <- Proxy @out ->-    "\x05\x3d" <> encodeT' @t-  CONS ->-    "\x03\x1b"-  IF_CONS a b ->-    "\x07\x2d" <> encodeInstrs a <> encodeInstrs b-  SIZE ->-    "\x03\x45"-  EMPTY_SET | _ :: Proxy ('TSet t ': s) <- Proxy @out ->-    "\x05\x24" <> encodeT' @t-  EMPTY_MAP | _ :: Proxy ('TMap k v ': s) <- Proxy @out ->-    "\x07\x23" <> encodeT' @k <> encodeT' @v-  EMPTY_BIG_MAP | _ :: Proxy ('TBigMap k v ': s) <- Proxy @out ->-    "\x07\x72" <> encodeT' @k <> encodeT' @v-  MAP a ->-    "\x05\x38" <> encodeInstrs a-  ITER a ->-    "\x05\x52" <> encodeInstrs a-  MEM ->-    "\x03\x39"-  GET ->-    "\x03\x29"-  GETN n ->-    "\x05\x29" <> encodeNumeric (peanoValSing n)-  UPDATE ->-    "\x03\x50"-  UPDATEN n ->-    "\x05\x50" <> encodeNumeric (peanoValSing n)-  GET_AND_UPDATE ->-    "\x03\x8c"-  IF a b ->-    "\x07\x2c" <> encodeInstrs a <> encodeInstrs b-  LOOP a ->-    "\x05\x34" <> encodeInstrs a-  LOOP_LEFT a ->-    "\x05\x53" <> encodeInstrs a-  LAMBDA (v :: Value ('TLambda i o)) ->-    "\x09\x31" <>-    encodeAsList (encodeT' @i <> encodeT' @o <> encodeValue v) <>-    encodeLength 0  -- encoding of a Variable Annotation (that we don't support)-  EXEC ->-    "\x03\x26"-  APPLY ->-    "\x03\x73"-  DIP a ->-    "\x05\x1f" <> encodeInstrs a-  DIPN s a ->-    "\x07\x1f" <> encodeNumeric (peanoValSing s) <> encodeInstrs a-  FAILWITH ->-    "\x03\x27"-  CAST | _ :: Proxy (t ': s) <- Proxy @out ->-    "\x05\x57" <> encodeT' @t-  RENAME ->-    "\x03\x58"-  PACK ->-    "\x03\x0c"-  UNPACK | _ :: Proxy ('TOption t ': s) <- Proxy @out ->-    "\x05\x0d" <> encodeT' @t-  CONCAT ->-    "\x03\x1a"-  CONCAT' ->-    "\x03\x1a"-  SLICE ->-    "\x03\x6f"-  ISNAT ->-    "\x03\x56"-  ADD ->-    "\x03\x12"-  SUB ->-    "\x03\x4b"-  MUL ->-    "\x03\x3a"-  EDIV ->-    "\x03\x22"-  ABS ->-    "\x03\x11"-  NEG ->-    "\x03\x3b"-  LSL ->-    "\x03\x35"-  LSR ->-    "\x03\x36"-  OR ->-    "\x03\x41"-  AND ->-    "\x03\x14"-  XOR ->-    "\x03\x51"-  NOT ->-    "\x03\x3f"-  COMPARE ->-    "\x03\x19"-  EQ ->-    "\x03\x25"-  NEQ ->-    "\x03\x3c"-  LT ->-    "\x03\x37"-  GT ->-    "\x03\x2a"-  LE ->-    "\x03\x32"-  GE ->-    "\x03\x28"-  INT ->-    "\x03\x30"-  SELF sepc ->-    case sepcName sepc of-      DefEpName ->  "\x03\x49"-      epName -> encodeWithAnns [] [epNameToRefAnn epName] [] "\x03\x49"-  CONTRACT ns ep | _ :: Proxy ('TOption ('TContract t) ': s) <- Proxy @out ->-    encodeWithAnns [] [epNameToRefAnn ep] [] $ "\x05\x55" <> encodeNotedT' @t ns-  TRANSFER_TOKENS ->-    "\x03\x4d"-  SET_DELEGATE ->-    "\x03\x4e"-  CREATE_CONTRACT contract@Contract{..}-    | _ :: Instr '[ 'TPair p g ] '[ 'TPair ('TList 'TOperation) g ] <- cCode ->-    let contents = mapEntriesOrdered contract-            (\np -> "\x05\x00" <> encodeParamNotes' @p np)-            (\ng -> "\x05\x01" <> encodeNotedT' @g ng)-            (\instr -> "\x05\x02" <> encodeInstrs instr)-    in "\x05\x1d" <> encodeList id contents-  IMPLICIT_ACCOUNT ->-   "\x03\x1e"-  NOW ->-   "\x03\x40"-  AMOUNT ->-   "\x03\x13"-  BALANCE ->-   "\x03\x15"-  VOTING_POWER ->-   "\x03\x7b"-  TOTAL_VOTING_POWER ->-   "\x03\x7c"-  CHECK_SIGNATURE ->-   "\x03\x18"-  SHA256 ->-   "\x03\x0f"-  SHA512 ->-   "\x03\x10"-  BLAKE2B ->-   "\x03\x0e"-  SHA3 ->-   "\x03\x7e"-  KECCAK ->-   "\x03\x7d"-  HASH_KEY ->-   "\x03\x2b"-  PAIRING_CHECK ->-   "\x03\x7f"-  SOURCE ->-   "\x03\x47"-  SENDER ->-   "\x03\x48"-  ADDRESS ->-   "\x03\x54"-  CHAIN_ID ->-   "\x03\x75"-  LEVEL ->-   "\x03\x76"-  SELF_ADDRESS ->-   "\x03\x77"-  NEVER ->-   "\x03\x79"----- | Iff there are non-empty annotations it increments the value's tag and--- appends the encoded annotations.-encodeWithAnns :: [TypeAnn] -> [FieldAnn] -> [VarAnn] -> LByteString -> LByteString-encodeWithAnns tns fns vns encodedInput-  | null encodedInput = encodedInput-  | isNoAnnSet annSet = encodedInput-  | otherwise = inputIncrem <> encodedAnns-  where-    annSet = fullAnnSet tns fns vns-    encodedAnns = encodeAsList . encodeUtf8 $ show @Text annSet-    inputIncrem = (1 + LBS.head encodedInput) `LBS.cons` LBS.tail encodedInput---- | Encode an instruction with variable annotations-encodeVarNotedInstr :: Instr inp out -> NonEmpty VarAnn -> LByteString -> LByteString-encodeVarNotedInstr i vns'@(toList -> vns) encodedType = case i of-  InstrWithNotes proxy n a -> encodeNotedInstr proxy a n vns-  InstrWithVarAnns _ a -> encodeInstr $ InstrWithVarNotes vns' a-  -- AnnPAIR, AnnCAR, AnnCDR and AnnLEFT, AnnRIGHT are checked here because-  -- their cases on `encodeInstr` increment them to \x04 and to \x05 respectively-  -- when they have a field annotation, but they would also get increment due to-  -- variable annotations, resulting in incorrect \x05 and \x06 codes respectively.-  AnnPAIR tn fn1 fn2 -> encodeWithAnns [tn] [fn1, fn2] vns "\x03\x42"-  AnnCAR fn -> encodeWithAnns [] [fn] vns "\x03\x16"-  AnnCDR fn -> encodeWithAnns [] [fn] vns "\x03\x17"-  AnnLEFT tn fn1 fn2 -> encodeWithAnns [tn] [fn1, fn2] vns $ "\x05\x33" <> encodedType-  AnnRIGHT tn fn1 fn2 -> encodeWithAnns [tn] [fn1, fn2] vns $ "\x05\x44" <> encodedType-  _ -> encodeWithAnns [] [] vns $ encodeInstr i---- | Encode an instruction with Annotations-encodeNotedInstr-  :: forall inp out topElems rest.-     out ~ (topElems ++ rest)-  => Proxy rest -> Instr inp out -> Rec Notes topElems -> [VarAnn] -> LByteString-encodeNotedInstr proxy instr notes vns = case (instr, Proxy @out, notes) of-  (WithLoc _ instr', _, _) ->-    encodeNotedInstr proxy instr' notes vns-  (SOME, _, NTOption tn _ns :& _) ->-    encodeWithAnns [tn] [] vns $ encodeInstr instr-  (NONE, _ :: Proxy ('TOption t ': s), NTOption tn ns :& _) ->-    encodeWithAnns [tn] [] vns $ "\x05\x3e" <> encodeNotedT' @t ns-  (UNIT, _, NTUnit tn :& _) ->-    encodeWithAnns [tn] [] vns $ encodeInstr instr-  (NIL, _ :: Proxy ('TList t ': s), NTList tn ns :& _) ->-    encodeWithAnns [tn] [] vns $ "\x05\x3d" <> encodeNotedT' @t ns-  (EMPTY_SET, _ :: Proxy ('TSet t ': s), NTSet tn ns :& _) ->-    encodeWithAnns [tn] [] vns $ "\x05\x24" <> encodeNotedT' @t ns-  (EMPTY_MAP, _ :: Proxy ('TMap k v ': s), NTMap tn1 nk ns :& _) ->-    encodeWithAnns [tn1] [] vns $-      "\x07\x23" <> encodeNotedT' @k nk <> encodeNotedT' @v ns-  (EMPTY_BIG_MAP, _ :: Proxy ('TBigMap k v ': s), NTBigMap tn1 nk ns :& _) ->-    encodeWithAnns [tn1] [] vns $-      "\x07\x72" <> encodeNotedT' @k nk <> encodeNotedT' @v ns-  (PUSH (v :: Value t), _, tn :& _) ->-    "\x07\x43" <> encodeNotedT' @t tn <> encodeValue v-  (LAMBDA (v :: Value ('TLambda i o)), _, NTLambda _tn ns1 ns2 :& _) ->-    "\x09\x31" <>-    encodeAsList (encodeNotedT' @i ns1 <> encodeNotedT' @o ns2 <> encodeValue v) <>-    encodeLength 0  -- encoding of a Variable Annotation (that we don't support)-  (CAST, _ :: Proxy (t ': s), tn :& _) ->-    "\x05\x57" <> encodeNotedT' @t tn-  (UNPACK, _ :: Proxy ('TOption t ': s), NTOption tn ns :& _) ->-    encodeWithAnns [tn] [] vns $ "\x05\x0d" <> encodeNotedT' @t ns-  -- NOTE: `CONTRACT` may be part of an `InstrWithNotes` with `NTOption`, but is-  -- taken care of in `encodeInstr` anyway (because it contains the note itself)-  _ -> encodeInstr instr--packNotedT' :: forall (t :: T). SingI t => Notes t -> ByteString-packNotedT' = LBS.toStrict . encodeNotedT'--encodeNotedT' :: forall (t :: T). SingI t => Notes t -> LByteString-encodeNotedT' = encodeNotedST (sing @t) noAnn--encodeParamNotes' ::-  forall (t :: T). SingI t => ParamNotes t -> LByteString-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.-encodeNotedST :: Sing t -> FieldAnn -> Notes t -> LByteString-encodeNotedST st fn n = case (st, n) of-  (STInt, NTInt tn) ->-    encodeWithAnns [tn] [fn] [] $ encodeT (fromSingT st)-  (STNat, NTNat tn) ->-    encodeWithAnns [tn] [fn] [] $ encodeT (fromSingT st)-  (STString, NTString tn) ->-    encodeWithAnns [tn] [fn] [] $ encodeT (fromSingT st)-  (STBytes, NTBytes tn) ->-    encodeWithAnns [tn] [fn] [] $ encodeT (fromSingT st)-  (STMutez, NTMutez tn) ->-    encodeWithAnns [tn] [fn] [] $ encodeT (fromSingT st)-  (STBool, NTBool tn) ->-    encodeWithAnns [tn] [fn] [] $ encodeT (fromSingT st)-  (STKeyHash, NTKeyHash tn) ->-    encodeWithAnns [tn] [fn] [] $ encodeT (fromSingT st)-  (STBls12381Fr, NTBls12381Fr tn) ->-    encodeWithAnns [tn] [fn] [] $ encodeT (fromSingT st)-  (STBls12381G1, NTBls12381G1 tn) ->-    encodeWithAnns [tn] [fn] [] $ encodeT (fromSingT st)-  (STBls12381G2, NTBls12381G2 tn) ->-    encodeWithAnns [tn] [fn] [] $ encodeT (fromSingT st)-  (STTimestamp, NTTimestamp tn) ->-    encodeWithAnns [tn] [fn] [] $ encodeT (fromSingT st)-  (STAddress, NTAddress tn) ->-    encodeWithAnns [tn] [fn] [] $ encodeT (fromSingT st)--  (STKey, NTKey tn) ->-    encodeWithAnns [tn] [fn] [] $ "\x03\x5c"-  (STUnit, NTUnit tn) ->-    encodeWithAnns [tn] [fn] [] $ "\x03\x6c"-  (STNever, NTNever tn) ->-    encodeWithAnns [tn] [fn] [] $ "\x03\x78"-  (STSignature, NTSignature tn) ->-    encodeWithAnns [tn] [fn] [] $ "\x03\x67"-  (STChainId, NTChainId tn) ->-    encodeWithAnns [tn] [fn] [] $ "\x03\x74"-  (STOption a, NTOption tn ns) ->-    encodeWithAnns [tn] [fn] [] $ "\x05\x63" <> encodeNotedST a noAnn ns-  (STList a, NTList tn ns) ->-    encodeWithAnns [tn] [fn] [] $ "\x05\x5f" <> encodeNotedST a noAnn ns-  (STSet a, NTSet tn ns) ->-    encodeWithAnns [tn] [fn] [] $ "\x05\x66" <> encodeNotedST a noAnn ns-  (STOperation, NTOperation tn) ->-    encodeWithAnns [tn] [fn] [] $ "\x03\x6d"-  (STContract a, NTContract tn ns) ->-    encodeWithAnns [tn] [fn] [] $ "\x05\x5a" <> encodeNotedST a noAnn ns-  (STPair a b, NTPair tn fn1 fn2 _vn1 _vn2 ns1 ns2) ->-    encodeWithAnns [tn] [fn] [] $-      "\x07\x65" <> encodeNotedST a fn1 ns1 <> encodeNotedST b fn2 ns2-  (STOr a b, NTOr tn fn1 fn2 ns1 ns2) ->-    encodeWithAnns [tn] [fn] [] $-      "\x07\x64" <> encodeNotedST a fn1 ns1 <> encodeNotedST b fn2 ns2-  (STLambda a r, NTLambda tn ns1 ns2) ->-    encodeWithAnns [tn] [fn] [] $-      "\x07\x5e" <> encodeNotedST a noAnn ns1 <> encodeNotedST r noAnn ns2-  (STMap k v, NTMap tn nk nv) ->-    encodeWithAnns [tn] [fn] [] $-      "\x07\x60" <> encodeNotedST k noAnn nk <> encodeNotedST v noAnn nv-  (STBigMap k v, NTBigMap tn nk nv) ->-    encodeWithAnns [tn] [fn] [] $-      "\x07\x61" <> encodeNotedST k noAnn nk <> encodeNotedST v noAnn nv--encodeT :: T -> LByteString-encodeT = \case-  TKey  -> "\x03\x5c"-  TUnit -> "\x03\x6c"-  TNever -> "\x03\x78"-  TSignature -> "\x03\x67"-  TChainId -> "\x03\x74"-  TOption t -> "\x05\x63" <> encodeT t-  TList t -> "\x05\x5f" <> encodeT t-  TSet t -> "\x05\x66" <> encodeT t-  TOperation -> "\x03\x6d"-  TContract t -> "\x05\x5a" <> encodeT t-  TPair a b -> "\x07\x65" <> encodeT a <> encodeT b-  TOr a b -> "\x07\x64" <> encodeT a <> encodeT b-  TLambda a r -> "\x07\x5e" <> encodeT a <> encodeT r-  TMap k v -> "\x07\x60" <> encodeT k <> encodeT v-  TBigMap k v -> "\x07\x61" <> encodeT k <> encodeT v-  TInt -> "\x03" <> "\x5b"-  TNat -> "\x03" <> "\x62"-  TString -> "\x03" <> "\x68"-  TBytes -> "\x03" <> "\x69"-  TMutez -> "\x03" <> "\x6a"-  TBool -> "\x03" <> "\x59"-  TKeyHash -> "\x03" <> "\x5d"-  TBls12381Fr -> "\x03" <> "\x82"-  TBls12381G1 -> "\x03" <> "\x80"-  TBls12381G2 -> "\x03" <> "\x81"-  TTimestamp -> "\x03" <> "\x6b"-  TAddress -> "\x03" <> "\x6e"+packValue' x =+  let uval = untypeValueHashable x+  in packValuePrefix <> (encodeExpression' $ toExpression uval) -encodeT' :: forall (t :: T). SingI t => LByteString-encodeT' = encodeT (demote @t)+-- | Prefix prepended to the binary representation of a value.+packValuePrefix :: IsString s => s+packValuePrefix = "\x05"

@@ -17,119 +17,25 @@ -} module Michelson.Interpret.Unpack   ( UnpackError (..)-  , unpackValue-  , unpackValue'   , unpackInstr'--  -- * Internals-  , decodeContract-  , decodeType+  , unpackUValue'+  , unpackValue'   ) where  import Prelude hiding (EQ, Ordering(..), get) -import Control.Monad.Except (throwError)-import Data.Binary (Get)-import qualified Data.Binary.Get as Get-import qualified Data.Bits as Bits import qualified Data.ByteString as BS-import qualified Data.ByteString.Lazy as LBS import Data.Constraint (Dict(..))-import Data.Default (def)-import qualified Data.Map as Map-import qualified Data.Set as Set-import Data.Singletons (Sing, SingI(..))-import Data.Typeable ((:~:)(..))-import Fmt (Buildable, Builder, fmt, hexF, padLeftF, pretty, (+|), (|+))+import Fmt (pretty) -import Michelson.Parser (Parser, ParserException(..), parseNoEnv)-import qualified Michelson.Parser.Annotations as PA-import Michelson.Text-import Michelson.TypeCheck-  (HST(..), SomeHST(..), SomeInstr(..), SomeInstrOut(..), TCError(..), TypeCheckEnv(..),-  TypeCheckMode(..), TypeContext(..), withWTPm)-import Michelson.TypeCheck.Helpers (ensureDistinctAsc, eqHST1)-import Michelson.TypeCheck.Instr (typeCheckList)-import Michelson.Typed (KnownT, RemFail(..), SingT(..), starNotes)+import Michelson.Typed (UnpackedValScope) import qualified Michelson.Typed as T-import Michelson.Typed.Entrypoints-import Michelson.Typed.Scope (UnpackedValScope) import Michelson.Untyped-import Tezos.Core-import Tezos.Crypto hiding (sign)-import qualified Tezos.Crypto.BLS12381 as BLS+import qualified Michelson.Untyped as U+import Morley.Micheline.Binary (eitherDecodeExpression)+import Morley.Micheline.Class (FromExpression(..)) import Util.Binary-import Util.Num -------------------------------------------------------------------------------- Helpers--------------------------------------------------------------------------------- | Alias for label attaching.-(?) :: Get a -> String -> Get a-(?) = flip Get.label-infix 0 ?---- | Displays bytes sequence.-bytesF :: [Word8] -> Builder-bytesF bs = "0x" <> foldMap (padLeftF 2 '0' . hexF) bs---- | Read a byte and match it against given value.-expectTag :: String -> Word8 -> Get ()-expectTag desc t =-  Get.label desc $ do-    t' <- Get.getWord8-    unless (t == t') $-      fail . fmt $ "Unexpected tag value (expected " +| bytesF [t] |+-                   ", but got " +| bytesF [t'] |+ ")"----- | Read a byte describing the primitive going further and match it against--- expected tag in the given conditions.------ Aside of context description, you have to specify number of arguments which--- given instruction accepts when written in Michelson. For instance, @PUSH@--- accepts two arguments - type and value.-expectDescTag :: HasCallStack => String -> Word16 -> Get ()-expectDescTag desc argsNum =-  Get.label desc $ do-    tag <- Get.getWord8-    unless (tag == expected) $-      fail . fmt $ "Unexpected preliminary tag: " <> bytesF [tag]-  where-    expected = case argsNum of-      0 -> 0x03-      1 -> 0x05-      2 -> 0x07-      3 -> 0x08-      _ -> error "Bad arguments num"-      -- Intermediate values of tag are also used and designate that annotations-      -- are also attached to the packed data. But they are never produced by-      -- @PACK@, neither @UNPACK@ seem to expect them, so for now we pretend-      -- that annotations do not exist.---- | Read a byte indicating the number of arguments/annotations of--- the primitive that follows it.-decodeDescTag :: String -> Get Word8-decodeDescTag desc =-  Get.label desc-    Get.getWord8---- | Like 'many', but doesn't backtrack if next entry failed to parse--- yet there are some bytes to consume ahead.------ This function exists primarily for better error messages.-manyForced :: Get a -> Get [a]-manyForced decode = do-  emp <- Get.isEmpty-  if emp-    then return []-    else (:) <$> decode <*> manyForced decode--------------------------------------------------------------------------------- Michelson serialisation------------------------------------------------------------------------------ {- Implementation notes:  * We need to know which exact type we unpack to.@@ -152,823 +58,27 @@  -- | Deserialize bytes into the given value. -- Suitable for @UNPACK@ operation only.-unpackValue-  :: (UnpackedValScope t)-  => LByteString -> Either UnpackError (T.Value t)-unpackValue = launchGet (finalizeDecoder decodeValue)---- | Like 'unpackValue', for strict byte array. unpackValue'-  :: (UnpackedValScope t)+  :: forall t. (UnpackedValScope t)   => ByteString -> Either UnpackError (T.Value t)-unpackValue' = unpackValue . LBS.fromStrict+unpackValue' = unpackImpl @(T.Value t)+  where+    _reallyNeedThisConstraint = Dict @(UnpackedValScope t)  -- | Deserialize an instruction into the given value. unpackInstr' :: ByteString -> Either UnpackError [ExpandedOp]-unpackInstr' = launchGet (finalizeDecoder decodeOps) . LBS.fromStrict---- | Turn composable decoder into a final decoder which will be run over data.-finalizeDecoder :: Get a -> Get a-finalizeDecoder decoder =-  expectTag "Packed data start" 0x05 *> decoder <* ensureEnd--decodeValue-  :: forall t.-     (HasCallStack, UnpackedValScope t)-  => Get (T.Value t)-decodeValue = Get.label "Value" $-  case sing @t of-    STKey -> T.VKey <$> decodeAsBytesOrString-      ( decodeWithTag "key" keyDecoders-      , parsePublicKey-      )-    STUnit -> do-      expectDescTag "Unit" 0-      expectTag "Unit" 0x0B-      return T.VUnit-    STSignature -> T.VSignature <$> decodeAsBytesOrString-      ( decodeBytesLikeMaybe "signature wrong size" mkSignature-      , parseSignature-      )-    STChainId -> T.VChainId <$> decodeAsBytesOrString-      ( decodeBytesLikeMaybe "chain_id wrong size" mkChainId-      , parseChainId-      )-    STOption _ -> do-      Get.getByteString 2 >>= \case-        "\x03\x06" -> pure (T.VOption Nothing)-        "\x05\x09" -> T.VOption . Just <$> decodeValue-        other -> fail $ "Unknown option tag: " <> show other-    STList _ -> do-      decodeAsList $ T.VList <$> manyForced decodeValue-    STSet (st :: Sing st) -> withComparable st $ do-      decodeAsList $ do-        vals <- withUnpackedValueScope @st $ manyForced decodeValue-        either (fail . toString) pure $-          T.VSet . Set.fromDistinctAscList <$> ensureDistinctAsc id vals--    STPair (_:: Sing lt) (r :: Sing rt) -> do-      withUnpackedValueScope @rt $ do-        decodeDescTag "Pair" >>= \case-          0x07 -> do-            -- "Normal" pair notation, e.g. `Pair 1 2` or `Pair 1 (Pair 2 3)`-            expectTag "Pair" 0x07-            T.VPair ... (,) <$> decodeValue <*> decodeValue-          0x09 -> do-            -- Right-combed notation, e.g. `Pair 1 2 3`-            expectTag "Pair" 0x07--            -- Find out how many bytes it took to encode the pair's elements, and decode them.-            elemLen <- decodeLength ? "Right-combed pair length"-            val <- Get.isolate elemLen (go @lt @rt r) ? "Right-combed pair elements"--            -- Find out how many bytes it took to encode the pair's annotations - there should be no annotations.-            (decodeLength ? "Right-combed pair annotations' length") >>= \case-              0 -> pass-              _ -> fail "Cannot decode values with annotations"-            pure val-          0x02 -> do-            -- List notation, e.g. `{ 1 ; 2 ; 3 }`-            elemLen <- decodeLength ? "Right-combed pair length"-            Get.isolate elemLen (go @lt @rt r) ? "Right-combed pair elements"-          tag -> fail . fmt $ "Unexpected preliminary tag: 0x" <> hexF tag-      where-        go :: forall l r. (UnpackedValScope l, UnpackedValScope r) => Sing r -> Get (T.Value ('T.TPair l r))-        go singR =-          case singR of-            -- If there are more pairs to the right of the right-combed pair, decode them.-            STPair (_ :: Sing rl) (singRR :: Sing rr) -> do-              withUnpackedValueScope @rr $ do-                T.VPair ... (,) <$> decodeValue @l <*> go @rl @rr singRR-            _ ->-              T.VPair ... (,) <$> decodeValue @l <*> decodeValue @r-    STOr (_ :: Sing lt) _ ->-      withUnpackedValueScope @lt $ do-        expectDescTag "Or" 1-        Get.getWord8 >>= \case-          0x05 -> T.VOr . Left <$> decodeValue-          0x08 -> T.VOr . Right <$> decodeValue-          other -> unknownTag "or constructor" other-    STLambda (_ :: Sing t1) (_ :: Sing t2) -> do-      uinstr <- decodeOps-      withWTPm @t2 $-        withWTPm @t1 (T.VLam <$> decodeTypeCheckLam uinstr)-    STMap (st :: Sing st) (_ :: Sing sv) ->-      withUnpackedValueScope @st $-        withComparable st $ T.VMap <$> decodeMap--    STInt -> T.VInt <$> decodeTaggedInt "Int"-    STNat -> T.VNat <$> decodeTaggedInt "Nat"-    STString -> do-      expectTag "String" 0x01-      T.VString <$> decodeString-    STBytes -> do-      expectTag "Bytes" 0x0a-      T.VBytes <$> decodeBytes-    STMutez -> do-      mmutez <- mkMutez <$> decodeTaggedInt "Mutez"-      maybe (fail "Negative mutez") (pure . T.VMutez) mmutez-    STBool -> do-      expectDescTag "Bool" 0-      Get.getWord8 >>= \case-        0x0A -> pure (T.VBool True)-        0x03 -> pure (T.VBool False)-        other -> unknownTag "bool" other-    STKeyHash -> T.VKeyHash <$> decodeAsBytesOrString-      ( decodeWithTag "key_hash" keyHashDecoders-      , parseKeyHash-      )-    STBls12381Fr -> fmap T.VBls12381Fr $-      Get.label "bls12_381_fr" $ Get.getWord8 >>= \case-        0x0A -> decodeBls12Bytes-        0x00 -> fromInteger <$> decodeInt-        other -> unknownTag "bytes or int" other-    STBls12381G1 -> do-      expectTag "Bls12381G1 bytes" 0x0A-      T.VBls12381G1 <$> decodeBls12Bytes-    STBls12381G2 -> do-      expectTag "Bls12381G2 bytes" 0x0A-      T.VBls12381G2 <$> decodeBls12Bytes-    STTimestamp -> Get.label "Timestamp" $ Get.getWord8 >>= \case-      0x00 -> do-        T.VTimestamp . timestampFromSeconds <$> decodeInt-      0x01 -> do-        str <- decodeString-        maybe (fail $ toString $ "failed to parse timestamp from " <> unMText str)-          (pure . T.VTimestamp) $ parseTimestamp $ unMText str-      other -> unknownTag "int or string" other-    STAddress ->-      T.VAddress <$> decodeAsBytesOrString-      ( decodeBytesLike "EpAddress" parseEpAddressRaw-      , parseEpAddress-      )-    STNever -> fail $ "cannot decode to `never` type"---withUnpackedValueScope-  :: forall a v m. (KnownT a, MonadFail m)-  => (T.UnpackedValScope a => m v)-  -> m v-withUnpackedValueScope act = case T.checkScope @(T.UnpackedValScope a) of-  Right Dict -> act-  _ -> fail "Unpackable value is required here"--withComparable-  :: forall a v m. (MonadFail m)-  => Sing a-  -> (T.Comparable a => m v)-  -> m v-withComparable a act = case T.getComparableProofS a of-  Just Dict -> act-  Nothing -> fail "Comparable type is required here"---- | Read length of something (list, string, ...).-decodeLength :: Get Int-decodeLength = Get.label "Length" $ do-  len <- Get.getWord32be-  -- @martoon: I'm not sure whether returning 'Int' is valid here.-  -- Strictly speaking, it may be 'Word32', but there seems to be no easy way-  -- to check the reference implementation on that.-  -- 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.-  fromIntegralChecked len-    & either (fail . toString) pure-    ? "Length"--decodeAsListRaw :: Get a -> Get a-decodeAsListRaw getElems = do-  l <- decodeLength ? "List length"-  Get.isolate l (getElems ? "List content")---- | Given decoder for list content, get a whole list decoder.-decodeAsList :: Get a -> Get a-decodeAsList getElems = do-  expectTag "List" 0x02-  decodeAsListRaw getElems--decodeString :: Get MText-decodeString = do-  l <- decodeLength ? "String length"-  ss <- replicateM l Get.getWord8 ? "String content"-  ss' <- decodeUtf8' (BS.pack ss)-    & either (fail . show) pure-    ? "String UTF-8 decoding"-  mkMText ss'-    & either (fail . show) pure-    ? "Michelson string validity analysis"--decodeAsBytesRaw :: (Int -> Get a) -> Get a-decodeAsBytesRaw decode = do-  l <- decodeLength ? "Byte array length"-  decode l--decodeAsBytesOrString :: Buildable e => (Get a, Text -> Either e a) -> Get a-decodeAsBytesOrString (bytesDecoder, strParser) =-  Get.getWord8 >>= \case-    0x01 -> do-      str <- decodeString-      either (fail . pretty) pure $ strParser $ unMText str-    0x0A -> do-      decodeAsBytesRaw $ \l ->-        Get.isolate l bytesDecoder ? "Binary content"-    other -> unknownTag "text or string" other---decodeBytesLikeMaybe-  :: String -> (ByteString -> Maybe a) -> Get a-decodeBytesLikeMaybe onErr constructor = do-  bs <- getRemainingByteStringCopy-  case constructor bs of-    Nothing -> fail onErr-    Just res -> pure res--decodeBytes :: Get ByteString-decodeBytes =-  decodeAsBytesRaw $ Get.label "Bytes payload" . getByteStringCopy--decodeBls12Bytes :: BLS.CurveObject a => Get a-decodeBls12Bytes = do-  bs <- decodeBytes-  BLS.fromMichelsonBytes bs-    & either (fail . pretty) pure--decodeMap-  :: forall k v.(UnpackedValScope k, UnpackedValScope v)-  => Get $ Map (T.Value k) (T.Value v)-decodeMap = withComparable (sing @k) $ Get.label "Map" $-  decodeAsList $ do-    es <- manyForced $ do-      expectDescTag "Elt" 2-      expectTag "Elt" 0x04-      (,) <$> decodeValue <*> decodeValue-    either (fail . toString) pure $-      Map.fromDistinctAscList <$> ensureDistinctAsc fst es---- | An integral expression always appears tagged with 0x00.--- This function reads the tag, discards it, and reads the int that follows it.-decodeTaggedInt :: (Integral i, Bits.Bits i) => String -> Get i-decodeTaggedInt label =-  expectTag label 0x00 *> decodeInt---- | Read a numeric value.-decodeInt :: (Integral i, Bits.Bits i) => Get i-decodeInt = (Bits.toIntegralSized @Integer <$> loop 0 0 ? "Number")-            >>= maybe (fail "Value doesn't satisfy type ranges") pure-  where-    loop !offset !acc = do-      byte <- Get.getWord8--      let hasCont = Bits.testBit byte 7-      let doCont shft = if hasCont then loop (shft + offset) else pure-      let addAndCont shft bytePayload =-            doCont shft $ acc + Bits.shiftL (fromIntegral bytePayload) offset--      let payload = Bits.clearBit byte 7-      if offset > 0-        then addAndCont 7 payload-        else do-          let sign = if Bits.testBit byte 6 then -1 else 1-          let upayload = Bits.clearBit payload 6-          (sign *) <$> addAndCont 6 upayload---- | Type check instruction occurred from a lambda.-decodeTypeCheckLam-  :: forall inp out m.-     (T.WellTyped inp, T.WellTyped out, MonadFail m)-  => [ExpandedOp]-  -> m (RemFail T.Instr '[inp] '[out])-decodeTypeCheckLam uinstr =-  either tcErrToFail pure . run $ do-    let inp = (starNotes, Dict, noAnn) ::& SNil-    _ :/ instr' <- typeCheckList uinstr inp-    case instr' of-      instr ::: out' ->-        case eqHST1 @out out' of-          Right Refl ->-            pure $ RfNormal instr-          Left err ->-                -- dummy types, we have no full information to build untyped-                -- 'T' anyway-            let tinp = Ty TUnit noAnn-                tout = Ty TUnit noAnn-            in throwError $-              TCFailedOnInstr (LAMBDA noAnn tinp tout uinstr) (SomeHST inp) def-              (Just LambdaCode) (Just err)-      AnyOutInstr instr ->-        return $ RfAlwaysFails instr-  where-    run = evaluatingState tcInitEnv . runExceptT . usingReaderT def-    tcErrToFail err = fail $ "Type check failed: " +| err |+ ""-    tcInitEnv =-      TypeCheckEnv-      { tcExtFrames = error "runInstrImpl(UNPACK): tcExtFrames touched"-        --- ^ This is safe because @UNPACK@ never produces Ext instructions-      , tcMode = TypeCheckPack-      }--decodeInstr :: Get ExpandedInstr-decodeInstr = Get.label "Instruction" $ do-  pretag <- Get.getWord8 ? "Pre instr tag"-  tag <- Get.getWord8 ? "Instr tag"-  case (pretag, tag) of-    (0x03, 0x20) -> pure $ DROP-    (0x05, 0x20) -> DROPN <$> decodeTaggedInt "'DROP n' parameter"-    (0x03, 0x21) -> DUP <$> decodeNoAnn-    (0x05, 0x21) -> DUPN <$> decodeNoAnn <*> (expectTag "'DUP n' parameter" 0x00 *> decodeInt)-    (0x03, 0x4C) -> pure $ SWAP-    (0x05, 0x70) -> DIG <$> decodeTaggedInt "'DIG n' parameter"-    (0x05, 0x71) -> DUG <$> decodeTaggedInt "'DUG n' parameter"-    (0x07, 0x43) -> do-      (typ, val) <- decodePushVal-      an <- decodeNoAnn-      return $ PUSH an typ val-    (0x03, 0x46) -> SOME <$> decodeNoAnn <*> decodeNoAnn-    (0x05, 0x3E) -> NONE <$> decodeNoAnn <*> decodeNoAnn <*> decodeType-    (0x03, 0x4F) -> UNIT <$> decodeNoAnn <*> decodeNoAnn-    (0x07, 0x2F) -> IF_NONE <$> decodeOps <*> decodeOps-    (0x03, 0x42) -> PAIR <$> decodeNoAnn <*> decodeNoAnn <*> decodeNoAnn <*> decodeNoAnn-    (0x05, 0x42) -> do-      n <- decodeTaggedInt "'PAIR n' parameter"-      varAnn <- decodeNoAnn-      pure $ PAIRN varAnn n-    (0x05, 0x7a) -> UNPAIRN <$> decodeTaggedInt "'UNPAIR n' parameter"-    (0x03, 0x16) -> CAR <$> decodeNoAnn <*> decodeNoAnn-    (0x03, 0x17) -> CDR <$> decodeNoAnn <*> decodeNoAnn-    (0x05, 0x33) -> LEFT <$> decodeNoAnn <*> decodeNoAnn <*> decodeNoAnn <*> decodeNoAnn-                         <*> decodeType-    (0x05, 0x44) -> RIGHT <$> decodeNoAnn <*> decodeNoAnn <*> decodeNoAnn <*> decodeNoAnn-                          <*> decodeType-    (0x07, 0x2E) -> IF_LEFT <$> decodeOps  <*> decodeOps-    (0x05, 0x3D) -> NIL <$> decodeNoAnn <*> decodeNoAnn <*> decodeType-    (0x03, 0x1B) -> CONS <$> decodeNoAnn-    (0x07, 0x2D) -> IF_CONS <$> decodeOps  <*> decodeOps-    (0x03, 0x45) -> SIZE <$> decodeNoAnn-    (0x05, 0x24) -> EMPTY_SET <$> decodeNoAnn <*> decodeNoAnn <*> decodeComparable-    (0x07, 0x23) -> EMPTY_MAP <$> decodeNoAnn <*> decodeNoAnn <*> decodeComparable-                              <*> decodeType-    (0x07, 0x72) -> EMPTY_BIG_MAP <$> decodeNoAnn <*> decodeNoAnn <*> decodeComparable-                                  <*> decodeType-    (0x05, 0x38) -> MAP <$> decodeNoAnn <*> decodeOps-    (0x05, 0x52) -> ITER <$> decodeOps-    (0x03, 0x39) -> MEM <$> decodeNoAnn-    (0x03, 0x29) -> GET <$> decodeNoAnn-    (0x05, 0x29) -> GETN <$> decodeNoAnn <*> decodeTaggedInt "'GET n' parameter"-    (0x03, 0x50) -> UPDATE <$> decodeNoAnn-    (0x05, 0x50) -> UPDATEN <$> decodeNoAnn <*> decodeTaggedInt "'UPDATE n' parameter"-    (0x03, 0x8c) -> GET_AND_UPDATE <$> decodeNoAnn-    (0x07, 0x2C) -> IF <$> decodeOps  <*> decodeOps-    (0x05, 0x34) -> LOOP <$> decodeOps-    (0x05, 0x53) -> LOOP_LEFT <$> decodeOps-    (0x09, 0x31) -> do-      (ti, to, ops) <- decodeAsListRaw $-        (,,) <$> decodeType <*> decodeType <*> decodeOps-      vAnn <- decodeVAnnDef-      return $ LAMBDA vAnn ti to ops-    (0x03, 0x26) -> EXEC <$> decodeNoAnn-    (0x03, 0x73) -> APPLY <$> decodeNoAnn-    (0x05, 0x1F) -> DIP <$> decodeOps-    (0x07, 0x1F) -> DIPN <$> decodeTaggedInt "'DIP n' parameter" <*> decodeOps-    (0x03, 0x27) -> pure FAILWITH-    (0x05, 0x57) -> CAST <$> decodeNoAnn <*> decodeType-    (0x03, 0x58) -> RENAME <$> decodeNoAnn-    (0x03, 0x0C) -> PACK <$> decodeNoAnn-    (0x05, 0x0D) -> UNPACK <$> decodeNoAnn <*> decodeNoAnn <*> decodeType-    (0x03, 0x1A) -> CONCAT <$> decodeNoAnn-    (0x03, 0x6F) -> SLICE <$> decodeNoAnn-    (0x03, 0x56) -> ISNAT <$> decodeNoAnn-    (0x03, 0x12) -> ADD <$> decodeNoAnn-    (0x03, 0x4B) -> SUB <$> decodeNoAnn-    (0x03, 0x3A) -> MUL <$> decodeNoAnn-    (0x03, 0x22) -> EDIV <$> decodeNoAnn-    (0x03, 0x11) -> ABS <$> decodeNoAnn-    (0x03, 0x3B) -> NEG <$> decodeNoAnn-    (0x03, 0x35) -> LSL <$> decodeNoAnn-    (0x03, 0x36) -> LSR <$> decodeNoAnn-    (0x03, 0x41) -> OR <$> decodeNoAnn-    (0x03, 0x14) -> AND <$> decodeNoAnn-    (0x03, 0x51) -> XOR <$> decodeNoAnn-    (0x03, 0x3F) -> NOT <$> decodeNoAnn-    (0x03, 0x19) -> COMPARE <$> decodeNoAnn-    (0x03, 0x25) -> EQ <$> decodeNoAnn-    (0x03, 0x3C) -> NEQ <$> decodeNoAnn-    (0x03, 0x37) -> LT <$> decodeNoAnn-    (0x03, 0x2A) -> GT <$> decodeNoAnn-    (0x03, 0x32) -> LE <$> decodeNoAnn-    (0x03, 0x28) -> GE <$> decodeNoAnn-    (0x03, 0x30) -> INT <$> decodeNoAnn-    (0x05, 0x55) -> CONTRACT <$> decodeNoAnn <*> decodeNoAnn <*> decodeType-    (0x03, 0x4D) -> TRANSFER_TOKENS <$> decodeNoAnn-    (0x03, 0x4E) -> SET_DELEGATE <$> decodeNoAnn-    (0x05, 0x1D) -> do-      contract <- decodeContract-      CREATE_CONTRACT <$> decodeNoAnn <*> decodeNoAnn <*> pure contract-    (0x03, 0x1E) -> IMPLICIT_ACCOUNT <$> decodeNoAnn-    (0x03, 0x40) -> NOW <$> decodeNoAnn-    (0x03, 0x13) -> AMOUNT <$> decodeNoAnn-    (0x03, 0x15) -> BALANCE <$> decodeNoAnn-    (0x03, 0x7b) -> VOTING_POWER <$> decodeNoAnn-    (0x03, 0x7c) -> TOTAL_VOTING_POWER <$> decodeNoAnn-    (0x03, 0x18) -> CHECK_SIGNATURE <$> decodeNoAnn-    (0x03, 0x0F) -> SHA256 <$> decodeNoAnn-    (0x03, 0x10) -> SHA512 <$> decodeNoAnn-    (0x03, 0x0E) -> BLAKE2B <$> decodeNoAnn-    (0x03, 0x7E) -> SHA3 <$> decodeNoAnn-    (0x03, 0x7D) -> KECCAK <$> decodeNoAnn-    (0x03, 0x2B) -> HASH_KEY <$> decodeNoAnn-    (0x03, 0x7F) -> PAIRING_CHECK <$> decodeNoAnn-    (0x03, 0x47) -> SOURCE <$> decodeNoAnn-    (0x03, 0x48) -> SENDER <$> decodeNoAnn-    (0x03, 0x49) -> SELF <$> decodeNoAnn <*> decodeNoAnn-    (0x03, 0x54) -> ADDRESS <$> decodeNoAnn-    (0x03, 0x75) -> CHAIN_ID <$> decodeNoAnn-    (0x03, 0x76) -> LEVEL <$> decodeNoAnn-    (0x03, 0x77) -> SELF_ADDRESS <$> decodeNoAnn-    (0x03, 0x79) -> pure $ NEVER-    -- Instructions with annotations from here on-    (0x04, 0x21) -> DUP <$> decodeVAnn-    (0x06, 0x21) -> flip DUPN <$> (expectTag "'DUP n' parameter" 0x00 *> decodeInt) <*> decodeVAnn-    (0x08, 0x43) -> do-      (typ, val) <- decodePushVal-      an <- decodeVAnn-      return $ PUSH an typ val-    (0x04, 0x46) -> decodeWithTVAnns SOME-    (0x06, 0x3E) -> do-      t <- decodeType-      decodeWithTVAnns NONE <*> pure t-    (0x04, 0x4F) -> decodeWithTVAnns UNIT-    (0x04, 0x42) -> decodeWithTVF2Anns PAIR-    (0x06, 0x42) -> do-      n <- decodeTaggedInt "'PAIR n' parameter"-      varAnn <- decodeVAnn-      pure $ PAIRN varAnn n-    (0x04, 0x16) -> decodeWithVFAnns CAR-    (0x04, 0x17) -> decodeWithVFAnns CDR-    (0x06, 0x33) -> do-      t <- decodeType-      decodeWithTVF2Anns LEFT <*> pure t-    (0x06, 0x44) -> do-      t <- decodeType-      decodeWithTVF2Anns RIGHT <*> pure t-    (0x06, 0x3D) -> do-      t <- decodeType-      decodeWithTVAnns NIL <*> pure t-    (0x04, 0x1B) -> CONS <$> decodeVAnn-    (0x04, 0x45) -> SIZE<$> decodeVAnn-    (0x06, 0x24) -> do-      c <- decodeComparable-      decodeWithTVAnns EMPTY_SET <*> pure c-    (0x08, 0x23) -> do-      c <- decodeComparable-      t <- decodeType-      decodeWithTVAnns EMPTY_MAP <*> pure c <*> pure t-    (0x08, 0x72) -> do-      c <- decodeComparable-      t <- decodeType-      decodeWithTVAnns EMPTY_BIG_MAP <*> pure c <*> pure t-    (0x06, 0x38) -> do-      o <- decodeOps-      MAP <$> decodeVAnn <*> pure o-    (0x04, 0x39) -> MEM <$> decodeVAnn-    (0x04, 0x29) -> GET <$> decodeVAnn-    (0x06, 0x29) -> do-      n <- decodeTaggedInt "'GET n' parameter"-      varAnn <- decodeVAnn-      pure $ GETN varAnn n-    (0x04, 0x50) -> UPDATE <$> decodeVAnn-    (0x06, 0x50) -> do-      n <- decodeTaggedInt "'UPDATE n' parameter"-      varAnn <- decodeVAnn-      pure $ UPDATEN varAnn n-    (0x04, 0x8c) -> GET_AND_UPDATE <$> decodeVAnn-    (0x04, 0x26) -> EXEC <$> decodeVAnn-    (0x04, 0x73) -> APPLY <$> decodeVAnn-    (0x06, 0x57) -> do-      t <- decodeType-      CAST <$> decodeVAnn <*> pure t-    (0x04, 0x58) -> RENAME <$> decodeVAnn-    (0x04, 0x0C) -> PACK <$> decodeVAnn-    (0x06, 0x0D) -> do-      t <- decodeType-      decodeWithTVAnns UNPACK <*> pure t-    (0x04, 0x1A) -> CONCAT <$> decodeVAnn-    (0x04, 0x6F) -> SLICE <$> decodeVAnn-    (0x04, 0x56) -> ISNAT <$> decodeVAnn-    (0x04, 0x12) -> ADD <$> decodeVAnn-    (0x04, 0x4B) -> SUB <$> decodeVAnn-    (0x04, 0x3A) -> MUL <$> decodeVAnn-    (0x04, 0x22) -> EDIV <$> decodeVAnn-    (0x04, 0x11) -> ABS <$> decodeVAnn-    (0x04, 0x3B) -> NEG <$> decodeVAnn-    (0x04, 0x35) -> LSL <$> decodeVAnn-    (0x04, 0x36) -> LSR <$> decodeVAnn-    (0x04, 0x41) -> OR <$> decodeVAnn-    (0x04, 0x14) -> AND <$> decodeVAnn-    (0x04, 0x51) -> XOR <$> decodeVAnn-    (0x04, 0x3F) -> NOT <$> decodeVAnn-    (0x04, 0x19) -> COMPARE <$> decodeVAnn-    (0x04, 0x25) -> EQ <$> decodeVAnn-    (0x04, 0x3C) -> NEQ <$> decodeVAnn-    (0x04, 0x37) -> LT <$> decodeVAnn-    (0x04, 0x2A) -> GT <$> decodeVAnn-    (0x04, 0x32) -> LE <$> decodeVAnn-    (0x04, 0x28) -> GE <$> decodeVAnn-    (0x04, 0x30) -> INT <$> decodeVAnn-    (0x06, 0x55) -> do-      t <- decodeType-      decodeWithVFAnns CONTRACT <*> pure t-    (0x04, 0x4D) -> TRANSFER_TOKENS <$> decodeVAnn-    (0x04, 0x4E) -> SET_DELEGATE <$> decodeVAnn-    (0x06, 0x1D) -> do-      contract <- decodeContract-      decodeWithV2Anns CREATE_CONTRACT <*> pure contract-    (0x04, 0x1E) -> IMPLICIT_ACCOUNT <$> decodeVAnn-    (0x04, 0x40) -> NOW <$> decodeVAnn-    (0x04, 0x13) -> AMOUNT <$> decodeVAnn-    (0x04, 0x15) -> BALANCE <$> decodeVAnn-    (0x04, 0x7b) -> VOTING_POWER <$> decodeVAnn-    (0x04, 0x7c) -> TOTAL_VOTING_POWER <$> decodeVAnn-    (0x04, 0x18) -> CHECK_SIGNATURE <$> decodeVAnn-    (0x04, 0x0F) -> SHA256 <$> decodeVAnn-    (0x04, 0x10) -> SHA512 <$> decodeVAnn-    (0x04, 0x0E) -> BLAKE2B <$> decodeVAnn-    (0x04, 0x7E) -> SHA3 <$> decodeVAnn-    (0x04, 0x7D) -> KECCAK <$> decodeVAnn-    (0x04, 0x2B) -> HASH_KEY <$> decodeVAnn-    (0x04, 0x7F) -> PAIRING_CHECK <$> decodeVAnn-    (0x04, 0x47) -> SOURCE <$> decodeVAnn-    (0x04, 0x48) -> SENDER <$> decodeVAnn-    (0x04, 0x49) -> decodeWithVFAnns SELF-    (0x04, 0x54) -> ADDRESS <$> decodeVAnn-    (0x04, 0x75) -> CHAIN_ID <$> decodeVAnn-    (0x04, 0x76) -> LEVEL <$> decodeVAnn-    (0x04, 0x77) -> SELF_ADDRESS <$> decodeVAnn-    (other1, other2) -> fail $ "Unknown instruction tag: " +|-                        bytesF [other1, other2]--decodePushVal :: Get (Ty, Value)-decodePushVal = do-  typ <- decodeType-  T.withSomeSingT (T.fromUType typ) $ \(_ :: Sing t) ->-    case T.checkScope @(T.ConstantScope t) of-      Left bt -> fail $ "Type can not appear in PUSH because it " <> pretty bt-      Right Dict -> do-        tval <- decodeValue @t-        pure $ (typ, T.untypeValue tval)--decodeContract :: Get Contract-decodeContract = decodeAsList $ do-  result <- contractTuple-  case orderContractBlock result of-    Just contract' -> do-      pure contract'-    Nothing ->-      fail "Duplicate contract field."-  where-    decodeParamsBlock = CBParam <$> do-      expectTag "Pre contract parameter" 0x05-      expectTag "Contract parameter" 0x00-      (t, ta, root) <- decodeTWithAnns-      pure $ ParameterType (Ty t ta) root-    decodeStorageBlock = CBStorage <$> do-      expectTag "Pre contract storage" 0x05-      expectTag "Contract storage" 0x01-      decodeType-    decodeCodeBlock = CBCode <$> do-      expectTag "Pre contract code" 0x05-      expectTag "Contract code" 0x02-      decodeOps--    contractBlock = decodeParamsBlock <|> decodeStorageBlock <|> decodeCodeBlock--    contractTuple = do-      result1 <- contractBlock-      result2 <- contractBlock-      result3 <- contractBlock-      pure (result1, result2, result3)---decodeOp :: Get ExpandedOp-decodeOp = Get.label "Op" $ do-  tag <- Get.lookAhead Get.getWord8-  if tag == 0x02-    then SeqEx <$> decodeOps ? "Ops seq"-    else PrimEx <$> decodeInstr ? "One op"--decodeOps :: Get [ExpandedOp]-decodeOps = decodeAsList $ manyForced decodeOp--decodeComparable :: Get Ty-decodeComparable = do-  (ct, tAnn, fAnn) <- decodeComparableTWithAnns-  if fAnn == noAnn-    then pure $ Ty ct tAnn-    else fail "This Comparable should not have a Field annotation"--decodeType :: Get Ty-decodeType = do-  (t, tAnn, fAnn) <- decodeTWithAnns-  if fAnn == noAnn-    then pure $ Ty t tAnn-    else fail "This Type should not have a Field annotation"--decodeComparableTWithAnns :: Get (T, TypeAnn, FieldAnn)-decodeComparableTWithAnns = Get.label "Comparable primitive type" $ do-  pretag <- Get.getWord8 ? "Pre simple comparable type tag"-  tag <- Get.getWord8 ? "Simple comparable type tag"-  let failMessage = "Unknown primitive tag: " +| bytesF [pretag, tag]-  ct <- case tag of-    0x6C -> pure TUnit-    0x5B -> pure TInt-    0x62 -> pure TNat-    0x68 -> pure TString-    0x69 -> pure TBytes-    0x6A -> pure TMutez-    0x59 -> pure TBool-    0x5C -> pure TKey-    0x5D -> pure TKeyHash-    0x67 -> pure TSignature-    0x6B -> pure TTimestamp-    0x6E -> pure TAddress-    0x74 -> pure TChainId-    0x63 -> TOption <$> decodeType-    0x65 ->-      case pretag of-        0x07 -> decodeTPair-        0x08 -> decodeTPair-        0x09 -> decodeTPairN-        _ -> fail failMessage-    0x64 -> decodeTOr-    _ -> fail failMessage-  case pretag of-    0x03 -> (ct,,) <$> decodeNoAnn <*> decodeNoAnn-    0x04 -> decodeWithTFAnns (ct,,)-    0x05 ->-      case tag of-        0x63 -> (ct,,) <$> decodeNoAnn <*> decodeNoAnn-        _    -> decodeWithTFAnns (ct,,)-    0x06 -> decodeWithTFAnns (ct,,)-    0x07 -> (ct,,) <$> decodeNoAnn <*> decodeNoAnn-    0x08 -> decodeWithTFAnns (ct,,)-    0x09 -> decodeWithTFAnns (ct,,)-    _ -> fail failMessage--{-# ANN decodeTWithAnns ("HLint: ignore Redundant <$>" :: Text) #-}-decodeTWithAnns :: Get (T, TypeAnn, FieldAnn)-decodeTWithAnns = doDecode <|> decodeComparableTWithAnns ? "Type"-  where-    doDecode = do-      pretag <- Get.getWord8 ? "Pre complex type tag"-      tag <- Get.getWord8 ? "Complex type tag"-      case (pretag, tag) of-        (0x03, 0x5C) ->-          (,,) <$> pure TKey <*> decodeNoAnn <*> decodeNoAnn-        (0x03, 0x6C) ->-          (,,) <$> pure TUnit <*> decodeNoAnn <*> decodeNoAnn-        (0x03, 0x78) ->-          (,,) <$> pure TNever <*> decodeNoAnn <*> decodeNoAnn-        (0x03, 0x67) ->-          (,,) <$> pure TSignature <*> decodeNoAnn <*> decodeNoAnn-        (0x03, 0x74) ->-          (,,) <$> pure TChainId <*> decodeNoAnn <*> decodeNoAnn-        (0x03, 0x82) ->-          (,,) <$> pure TBls12381Fr <*> decodeNoAnn <*> decodeNoAnn-        (0x03, 0x80) ->-          (,,) <$> pure TBls12381G1 <*> decodeNoAnn <*> decodeNoAnn-        (0x03, 0x81) ->-          (,,) <$> pure TBls12381G2 <*> decodeNoAnn <*> decodeNoAnn-        (0x05, 0x63) ->-          (,,) <$> (TOption <$> decodeType) <*> decodeNoAnn <*> decodeNoAnn-        (0x05, 0x5F) ->-          (,,) <$> (TList <$> decodeType) <*> decodeNoAnn <*> decodeNoAnn-        (0x05, 0x66) ->-          (,,) <$> (TSet <$> decodeComparable) <*> decodeNoAnn <*> decodeNoAnn-        (0x03, 0x6D) ->-          (,,) <$> pure TOperation <*> decodeNoAnn <*> decodeNoAnn-        (0x05, 0x5A) ->-          (,,) <$> (TContract <$> decodeType) <*> decodeNoAnn <*> decodeNoAnn-        (0x07, 0x5E) ->-          (,,) <$> (TLambda <$> decodeType <*> decodeType) <*> decodeNoAnn <*> decodeNoAnn-        (0x07, 0x60) ->-          (,,) <$> (TMap <$> decodeComparable <*> decodeType) <*> decodeNoAnn <*> decodeNoAnn-        (0x07, 0x61) ->-          (,,) <$> (TBigMap <$> decodeComparable <*> decodeType) <*> decodeNoAnn <*> decodeNoAnn-        -- T with annotations from here on-        (0x04, 0x5C) -> decodeWithTFAnns (TKey,,)-        (0x04, 0x6C) -> decodeWithTFAnns (TUnit,,)-        (0x04, 0x78) -> decodeWithTFAnns (TNever,,)-        (0x04, 0x67) -> decodeWithTFAnns (TSignature,,)-        (0x04, 0x74) -> decodeWithTFAnns (TChainId,,)-        (0x06, 0x63) -> do-          t <- TOption <$> decodeType-          decodeWithTFAnns (t,,)-        (0x06, 0x5F) -> do-          t <- TList <$> decodeType-          decodeWithTFAnns (t,,)-        (0x06, 0x66) -> do-          t <- TSet <$> decodeComparable-          decodeWithTFAnns (t,,)-        (0x04, 0x6D) -> decodeWithTFAnns (TOperation,,)-        (0x06, 0x5A) -> do-          t <- TContract <$> decodeType-          decodeWithTFAnns (t,,)-        (0x08, 0x5E) -> do-          t <- TLambda <$> decodeType <*> decodeType-          decodeWithTFAnns (t,,)-        (0x08, 0x60) -> do-          t <- TMap <$> decodeComparable <*> decodeType-          decodeWithTFAnns (t,,)-        (0x08, 0x61) -> do-          t <- TBigMap <$> decodeComparable <*> decodeType-          decodeWithTFAnns (t,,)-        (other1, other2) -> fail $ "Unknown primitive tag: " +|-                            bytesF [other1, other2]---- | "Normal" pair notation, e.g. `pair int int` or `pair int (pair int int)`------ The pair type doesn't really carry its nested variable annotations, except--- during execution. For this reason, they don't get decoded here and these--- variable annotations fields will be empty. See !763 for more context.-decodeTPair :: Get T-decodeTPair = do-  (t1, tAnn1, fAnn1) <- decodeTWithAnns-  (t2, tAnn2, fAnn2) <- decodeTWithAnns-  pure $ TPair fAnn1 fAnn2 noAnn noAnn (Ty t1 tAnn1) (Ty t2 tAnn2)---- | Right-combed notation, e.g. `pair int int int`------ Just like 'decodeTPair', nested variable annotations are not decoded, as they--- exist only during execution. See !763 for more context.-decodeTPairN :: Get T-decodeTPairN = do-  -- Find out how many bytes it took to encode the pair's fields, and decode them.-  fieldsLen <- decodeLength ? "'pair' number of type arguments"-  fields <- Get.isolate fieldsLen (manyForced decodeTWithAnns) ? "'pair' type arguments"-  go fields-  where-    go :: [(T, TypeAnn, FieldAnn)] -> Get T-    go = \case-      [] -> fail "The 'pair' type expects at least 2 type arguments, but 0 were given."-      [(t, _, _)] -> fail $ "The 'pair' type expects at least 2 type arguments, but only 1 was given: '" <> pretty t <> "'."-      [(t1, tAnn1, fAnn1), (t2, tAnn2, fAnn2)] ->-        pure $ TPair fAnn1 fAnn2 noAnn noAnn (Ty t1 tAnn1) (Ty t2 tAnn2)-      (t1, t1Ann1, fAnn1) : fields -> do-        rightCombedT <- go fields-        pure $ TPair fAnn1 noAnn noAnn noAnn (Ty t1 t1Ann1) (Ty rightCombedT noAnn)--decodeTOr :: Get T-decodeTOr = do-  (t1, tAnn1, fAnn1) <- decodeTWithAnns-  (t2, tAnn2, fAnn2) <- decodeTWithAnns-  pure $ TOr fAnn1 fAnn2 (Ty t1 tAnn1) (Ty t2 tAnn2)--------------------------------------------------------------------------------- Annotations--------------------------------------------------------------------------------- | Utility function to fill a constructor with an empty annotation-decodeNoAnn :: forall (t :: Type). Get (Annotation t)-decodeNoAnn = pure noAnn---- | Decodes an annotations' string and uses the provided `Parser` to parse--- untyped annotations from it. This has to produce at least one annotation--- (Annotations' String parsing will fail otherwise)-decodeAnns :: Parser a -> Get a-decodeAnns annsParser = do-  l <- decodeLength ? "Annotations' String length"-  ss <- replicateM l Get.getWord8 ? "Annotations' String content"-  s <- decodeUtf8' (BS.pack ss)-    & either (fail . show) pure-    ? "Annotations' String UTF-8 decoding"-  either (fail . displayException . ParserException) pure $ parseNoEnv annsParser "" s--decodeVAnn :: Get VarAnn-decodeVAnn = decodeAnns PA.noteV--decodeVAnnDef :: Get VarAnn-decodeVAnnDef = decodeAnns PA.noteDef--decodeWithTVAnns :: (TypeAnn -> VarAnn -> a) -> Get a-decodeWithTVAnns f = do-  (tAnn, vAnn) <- decodeAnns PA.notesTV-  pure $ f tAnn vAnn--decodeWithTVF2Anns :: (TypeAnn -> VarAnn -> FieldAnn -> FieldAnn -> a) -> Get a-decodeWithTVF2Anns f = do-  (tAnn, vAnn, (fAnn1, fAnn2)) <- decodeAnns PA.notesTVF2Def-  pure $ f tAnn vAnn fAnn1 fAnn2--decodeWithTFAnns :: (TypeAnn -> FieldAnn -> a) -> Get a-decodeWithTFAnns f =  do-  (tAnn, fAnn) <- decodeAnns PA.notesTF-  pure $ f tAnn fAnn+unpackInstr' = unpackImpl @([ExpandedOp]) -decodeWithV2Anns :: (VarAnn -> VarAnn -> a) -> Get a-decodeWithV2Anns f = do-  (vAnn1, vAnn2) <- decodeAnns PA.noteV2Def-  pure $ f vAnn1 vAnn2+-- | Deserialize bytes into 'Untyped.Value'.+unpackUValue' :: ByteString -> Either UnpackError U.Value+unpackUValue' = unpackImpl @U.Value -decodeWithVFAnns :: (VarAnn -> FieldAnn -> a) -> Get a-decodeWithVFAnns f = do-  (vAnn, fAnn) <- decodeAnns PA.notesVF-  pure $ f vAnn fAnn+unpackImpl :: forall t. (FromExpression t)+           => ByteString+           -> Either UnpackError t+unpackImpl bs = do+  (tag, bs') <- maybeToRight (UnpackError "Empty bytes") (BS.uncons bs)+  when (tag /= 0x05) . Left . UnpackError $+    "Unexpected tag: '" <> (show tag) <> "'. '0x05' tag expected."+  expr <- eitherDecodeExpression bs'+  either (Left . UnpackError . pretty) Right $ fromExpression @t expr

@@ -25,7 +25,6 @@      -- * For parsing   , mapPairLeaves-  , mapUnpairLeaves      -- * Internals exported for tests   , expand@@ -74,7 +73,7 @@   build = genericF  data UnpairStruct-  = UF (VarAnn, FieldAnn)+  = UF   | UP UnpairStruct UnpairStruct   deriving stock (Eq, Show, Data, Generic) @@ -139,7 +138,7 @@   | IFCMP ParsedInstr VarAnn [ParsedOp] [ParsedOp]   | FAIL   | PAPAIR PairStruct TypeAnn VarAnn-  | UNPAIR UnpairStruct+  | UNPAPAIR UnpairStruct   | CADR [CadrStruct] VarAnn FieldAnn   | CARN VarAnn Word   | CDRN VarAnn Word@@ -172,7 +171,7 @@     IFCMP parsedInstr varAnn parsedOps1 parsedOps2 -> "<IFCMP: "+|parsedInstr|+", "+|varAnn|+", "+|parsedOps1|+", "+|parsedOps2|+">"     FAIL -> "FAIL"     PAPAIR pairStruct typeAnn varAnn -> "<PAPAIR: "+|pairStruct|+", "+|typeAnn|+", "+|varAnn|+">"-    UNPAIR pairStruct -> "<UNPAIR: "+|pairStruct|+">"+    UNPAPAIR pairStruct -> "<UNPAPAIR: "+|pairStruct|+">"     CADR cadrStructs varAnn fieldAnn -> "<CADR: "+|cadrStructs|+", "+|varAnn|+", "+|fieldAnn|+">"     CARN varAnn idx -> "<CAR: #"+||idx||+","+||varAnn||+">"     CDRN varAnn idx -> "<CDR: #"+||idx||+","+||varAnn||+">"@@ -248,9 +247,9 @@  expandMacro :: InstrCallStack -> Macro -> [ExpandedOp] expandMacro p@InstrCallStack{icsCallStack=cs,icsSrcPos=macroPos} = \case-  VIEW a             -> expandMacro p (UNPAIR $ UP (UF (noAnn, noAnn)) (UF (noAnn, noAnn))) ++-                        [ PrimEx (DIP $ oprimEx $ DUPN noAnn 2) ] ++-                        [ PrimEx $ PAIR noAnn noAnn noAnn noAnn ] +++  VIEW a             -> [ PrimEx (UNPAIR noAnn noAnn noAnn noAnn)+                        , PrimEx (DIP $ oprimEx $ DUPN noAnn 2)+                        , PrimEx $ PAIR noAnn noAnn noAnn noAnn ] ++                         (expand cs <$> a) ++                         [ PrimEx (DIP [PrimEx $ AMOUNT noAnn])                         , PrimEx $ TRANSFER_TOKENS noAnn@@ -259,8 +258,8 @@                         , PrimEx $ CONS noAnn                         , PrimEx $ PAIR noAnn noAnn noAnn noAnn                         ]-  VOID a             -> expandMacro p (UNPAIR (UP (UF (noAnn, noAnn)) (UF (noAnn, noAnn)))) ++-                        [ PrimEx SWAP+  VOID a             -> [ PrimEx (UNPAIR noAnn noAnn noAnn noAnn)+                        , PrimEx SWAP                         , PrimEx $ DIP $ expand cs <$> a                         , PrimEx SWAP                         , PrimEx $ EXEC noAnn@@ -285,7 +284,7 @@   ASSERT_LEFT        -> oprimEx $ IF_LEFT [] (expandMacro p FAIL)   ASSERT_RIGHT       -> oprimEx $ IF_LEFT (expandMacro p FAIL) []   PAPAIR ps t v      -> expandPapair p ps t v-  UNPAIR ps          -> expandUnpapair p ps+  UNPAPAIR ps        -> expandUnpapair p ps   CADR c v f         -> expandCadr p c v f   CARN v idx         -> [PrimEx (GETN v (2 * idx + 1))]   CDRN v idx         -> [PrimEx (GETN v (2 * idx))]@@ -301,50 +300,58 @@     xo = PrimEx . fmap (expand cs)     xp = fmap (expand cs) --- the correctness of type-annotation expansion is currently untested, as these--- expansions are not explicitly documented in the Michelson Specification+-- | The macro expansion rules below were taken from: https://tezos.gitlab.io/008/michelson.html#syntactic-conveniences+--+-- The correctness of type-annotation expansion is currently untested, as these+-- expansions are not explicitly documented in the Michelson Specification. expandPapair :: InstrCallStack -> PairStruct -> TypeAnn -> VarAnn -> [ExpandedOp] expandPapair ics ps t v = case ps of   P (F a) (F b) -> [PrimEx $ PAIR t v a b]++  -- > PA(\right)R / S => DIP ((\right)R) ; PAIR / S   P (F a) r     -> PrimEx <$> [ DIP $ expandMacro ics (PAPAIR r noAnn noAnn)                               , PAIR t v a noAnn]++  -- > P(\left)IR / S => (\left)R ; PAIR / S   P l     (F b) -> expandMacro ics (PAPAIR l noAnn noAnn) ++                    [PrimEx $ PAIR t v noAnn b]++  -- > P(\left)(\right)R =>  (\left)R ; DIP ((\right)R) ; PAIR / S   P l     r     -> expandMacro ics (PAPAIR l noAnn noAnn) ++                    [ PrimEx $ DIP $ expandMacro ics (PAPAIR r noAnn noAnn)                    , PrimEx $ PAIR t v noAnn noAnn]-  F _           -> [] -- Do nothing in this case.+   -- It's impossible from the structure of PairStruct and considered cases above,   -- but if it accidentally happened let's just do nothing.+  F _           -> [] +-- | The macro expansion rules below were taken from: https://tezos.gitlab.io/008/michelson.html#syntactic-conveniences expandUnpapair :: InstrCallStack -> UnpairStruct -> [ExpandedOp] expandUnpapair ics = \case-  UP (UF (v,f)) (UF (w,g)) ->-    PrimEx <$> [ DUP noAnn-               , CAR v f-               , DIP [PrimEx $ CDR w g]-               ]-  UP (UF (v, f)) r ->-    PrimEx <$> [ DUP noAnn-               , CAR v f-               , DIP (PrimEx (CDR noAnn noAnn) : expandMacro ics (UNPAIR r))+  UP UF UF ->+    [ PrimEx (UNPAIR noAnn noAnn noAnn noAnn) ]++  -- > UNPA(\right)R / S => UNPAIR ; DIP (UN(\right)R) / S+  UP UF r ->+    PrimEx <$> [ UNPAIR noAnn noAnn noAnn noAnn+               , DIP (expandMacro ics (UNPAPAIR r))                ]-  UP l (UF (v, f)) ->-    map PrimEx [ DUP noAnn-               , DIP [PrimEx $ CDR v f]-               , CAR noAnn noAnn-               ] ++-               expandMacro ics (UNPAIR l)++  -- > UNP(\left)IR / S => UNPAIR ; UN(\left)R / S+  UP l UF ->+    PrimEx (UNPAIR noAnn noAnn noAnn noAnn)+      : expandMacro ics (UNPAPAIR l)++  -- > UNP(\left)(\right)R => UNPAIR ; DIP (UN(\right)R) ; UN(\left)R / S   UP l r ->-    expandMacro ics unpairOne ++-    [PrimEx $ DIP $ expandMacro ics $ UNPAIR r] ++-    expandMacro ics (UNPAIR l)-  UF _  -> [] -- Do nothing in this case.+    [ PrimEx (UNPAIR noAnn noAnn noAnn noAnn)+    , PrimEx $ DIP $ expandMacro ics $ UNPAPAIR r+    ] +++    expandMacro ics (UNPAPAIR l)+   -- It's impossible from the structure of UnpairStruct and considered cases above,   -- but if it accidentally happened let's just do nothing.-  where-    unpairOne = UNPAIR (UP fn fn)-    fn = UF (noAnn, noAnn)+  UF -> []  expandCadr :: InstrCallStack -> [CadrStruct] -> VarAnn -> FieldAnn -> [ExpandedOp] expandCadr ics cs v f = case cs of@@ -455,22 +462,6 @@     where       getLeaf (a:as) = (a, as)       getLeaf _      = (noAnn, [])--mapUnpairLeaves :: [(VarAnn, FieldAnn)] -> UnpairStruct -> UnpairStruct-mapUnpairLeaves fs p = evalState (unpairLeavesST p) fs--unpairLeavesST :: UnpairStruct -> State [(VarAnn, FieldAnn)] UnpairStruct-unpairLeavesST = \case-  (UP l r) -> do-    l' <- unpairLeavesST l-    r' <- unpairLeavesST r-    return $ UP l' r'-  (UF _) -> do-    f <- state getLeaf-    return $ UF f-    where-      getLeaf (a:as) = (a, as)-      getLeaf _      = ((noAnn, noAnn), [])  deriveJSON morleyAesonOptions ''ParsedOp deriveJSON morleyAesonOptions ''LetMacro

@@ -46,7 +46,7 @@ import Michelson.Typed.T import Michelson.Typed.Util (DfsSettings(..), dfsInstr) import Michelson.Typed.Value-import Util.Peano (SingNat(..))+import Util.PeanoNatural  ---------------------------------------------------------------------------- -- High level@@ -98,6 +98,8 @@ defaultRules =   flattenSeqLHS     `orSimpleRule` removeNesting+    `orSimpleRule` removeExtStackType+    `orSimpleRule` flattenFn     `orSimpleRule` dipDrop2swapDrop     `orSimpleRule` ifNopNop2Drop     `orSimpleRule` nopIsNeutralForSeq@@ -134,9 +136,20 @@   Nested i -> Just i   _        -> Nothing +-- | STACKTYPE is currently a Nop and may safely be removed.+removeExtStackType :: Rule+removeExtStackType = \case+  Ext (STACKTYPE{}) -> Just Nop+  _                 -> Nothing++flattenFn :: Rule+flattenFn = \case+  Fn _ _ i -> Just i+  _        -> Nothing+ dipDrop2swapDrop :: Rule dipDrop2swapDrop = \case-  DIP DROP -> Just $ Seq SWAP DROP+  DIP DROP -> Just $ SWAP :# DROP   _        -> Nothing  ifNopNop2Drop :: Rule@@ -146,99 +159,99 @@  nopIsNeutralForSeq :: Rule nopIsNeutralForSeq = \case-  Seq Nop i  -> Just i-  Seq i Nop  -> Just i+  Nop :# i   -> Just i+  i   :# Nop -> Just i   _          -> Nothing  variousNops :: Rule variousNops = \case-  Seq  SWAP    (Seq SWAP c) -> Just c-  Seq (PUSH _) (Seq DROP c) -> Just c-  Seq  DUP     (Seq DROP c) -> Just c-  Seq  UNIT    (Seq DROP c) -> Just c-  Seq  NOW     (Seq DROP c) -> Just c-  Seq  SENDER  (Seq DROP c) -> Just c-  Seq  EMPTY_MAP (Seq DROP c) -> Just c-  Seq  EMPTY_SET (Seq DROP c) -> Just c+  SWAP      :# SWAP :# c -> Just c+  PUSH _    :# DROP :# c -> Just c+  DUP       :# DROP :# c -> Just c+  UNIT      :# DROP :# c -> Just c+  NOW       :# DROP :# c -> Just c+  SENDER    :# DROP :# c -> Just c+  EMPTY_MAP :# DROP :# c -> Just c+  EMPTY_SET :# DROP :# c -> Just c -  Seq  SWAP         SWAP    -> Just Nop-  Seq (PUSH _)      DROP    -> Just Nop-  Seq  DUP          DROP    -> Just Nop-  Seq  UNIT         DROP    -> Just Nop-  Seq  NOW          DROP    -> Just Nop-  Seq  SENDER       DROP    -> Just Nop-  Seq  EMPTY_MAP   DROP    -> Just Nop-  Seq  EMPTY_SET   DROP    -> Just Nop-  _                         -> Nothing+  SWAP      :# SWAP      -> Just Nop+  PUSH _    :# DROP      -> Just Nop+  DUP       :# DROP      -> Just Nop+  UNIT      :# DROP      -> Just Nop+  NOW       :# DROP      -> Just Nop+  SENDER    :# DROP      -> Just Nop+  EMPTY_MAP :# DROP      -> Just Nop+  EMPTY_SET :# DROP      -> Just Nop+  _                      -> Nothing  dupSwap2dup :: Rule dupSwap2dup = \case-  Seq DUP (Seq SWAP c) -> Just (Seq DUP c)-  Seq DUP      SWAP    -> Just      DUP-  _                    -> Nothing+  DUP :# SWAP :# c -> Just (DUP :# c)+  DUP :# SWAP      -> Just DUP+  _                -> Nothing  noDipNeeded :: Rule noDipNeeded = \case   -- If we put a constant value on stack and then do something under it,   -- we can do this "something" on original stack and then put that constant.-  Seq (PUSH x) (Seq (DIP f) c) -> Just (Seq f (Seq (PUSH x) c))-  Seq (PUSH x)      (DIP f)    -> Just (Seq f      (PUSH x))-  Seq UNIT     (Seq (DIP f) c) -> Just (Seq f (Seq UNIT c))-  Seq UNIT          (DIP f)    -> Just (Seq f      UNIT)-  Seq NOW     (Seq (DIP f) c) -> Just (Seq f (Seq NOW c))-  Seq NOW          (DIP f)    -> Just (Seq f      NOW)-  Seq SENDER  (Seq (DIP f) c) -> Just (Seq f (Seq SENDER c))-  Seq SENDER       (DIP f)    -> Just (Seq f      SENDER)-  Seq EMPTY_MAP     (Seq (DIP f) c) -> Just (Seq f (Seq EMPTY_MAP c))-  Seq EMPTY_MAP          (DIP f)    -> Just (Seq f      EMPTY_MAP)-  Seq EMPTY_SET     (Seq (DIP f) c) -> Just (Seq f (Seq EMPTY_SET c))-  Seq EMPTY_SET          (DIP f)    -> Just (Seq f      EMPTY_SET)+  PUSH x    :# DIP f :# c -> Just $ f :# PUSH x :# c+  PUSH x    :# DIP f      -> Just $ f :# PUSH x+  UNIT      :# DIP f :# c -> Just $ f :# UNIT :# c+  UNIT      :# DIP f      -> Just $ f :# UNIT+  NOW       :# DIP f :# c -> Just $ f :# NOW :# c+  NOW       :# DIP f      -> Just $ f :# NOW+  SENDER    :# DIP f :# c -> Just $ f :# SENDER :# c+  SENDER    :# DIP f      -> Just $ f :# SENDER+  EMPTY_MAP :# DIP f :# c -> Just $ f :# EMPTY_MAP :# c+  EMPTY_MAP :# DIP f      -> Just $ f :# EMPTY_MAP+  EMPTY_SET :# DIP f :# c -> Just $ f :# EMPTY_SET :# c+  EMPTY_SET :# DIP f      -> Just $ f :# EMPTY_SET    -- If we do something ignoring top of the stack and then immediately   -- drop top of the stack, we can drop that item in advance and   -- not use 'DIP' at all.-  Seq (DIP f) (Seq DROP c)     -> Just (Seq DROP (Seq f c))-  Seq (DIP f) DROP             -> Just (Seq DROP f)+  DIP f :# DROP :# c -> Just $ DROP :# f :# c+  DIP f :# DROP         -> Just $ DROP :# f -  _                            -> Nothing+  _ -> Nothing  branchShortCut :: Rule branchShortCut = \case-  Seq LEFT  (Seq (IF_LEFT f _) c) -> Just (Seq f c)-  Seq RIGHT (Seq (IF_LEFT _ f) c) -> Just (Seq f c)-  Seq CONS  (Seq (IF_CONS f _) c) -> Just (Seq f c)-  Seq NIL   (Seq (IF_CONS _ f) c) -> Just (Seq f c)-  Seq NONE  (Seq (IF_NONE f _) c) -> Just (Seq f c)-  Seq SOME  (Seq (IF_NONE _ f) c) -> Just (Seq f c)+  LEFT  :# IF_LEFT f _ :# c -> Just (f :# c)+  RIGHT :# IF_LEFT _ f :# c -> Just (f :# c)+  CONS  :# IF_CONS f _ :# c -> Just (f :# c)+  NIL   :# IF_CONS _ f :# c -> Just (f :# c)+  NONE  :# IF_NONE f _ :# c -> Just (f :# c)+  SOME  :# IF_NONE _ f :# c -> Just (f :# c) -  Seq (PUSH (VBool True))  (Seq (IF f _) c) -> Just (Seq f c)-  Seq (PUSH (VBool False)) (Seq (IF _ f) c) -> Just (Seq f c)+  PUSH (VBool True)  :# IF f _ :# c -> Just (f :# c)+  PUSH (VBool False) :# IF _ f :# c -> Just (f :# c) -  Seq LEFT  (IF_LEFT f _) -> Just f-  Seq RIGHT (IF_LEFT _ f) -> Just f-  Seq CONS  (IF_CONS f _) -> Just f-  Seq NIL   (IF_CONS _ f) -> Just f-  Seq NONE  (IF_NONE f _) -> Just f-  Seq SOME  (IF_NONE _ f) -> Just f+  LEFT  :# IF_LEFT f _ -> Just f+  RIGHT :# IF_LEFT _ f -> Just f+  CONS  :# IF_CONS f _ -> Just f+  NIL   :# IF_CONS _ f -> Just f+  NONE  :# IF_NONE f _ -> Just f+  SOME  :# IF_NONE _ f -> Just f -  Seq (PUSH (VBool True))  (IF f _) -> Just f-  Seq (PUSH (VBool False)) (IF _ f) -> Just f+  PUSH (VBool True)  :# IF f _ -> Just f+  PUSH (VBool False) :# IF _ f -> Just f    _ -> Nothing  compareWithZero :: Rule compareWithZero = \case-  Seq (PUSH (VInt 0)) (Seq COMPARE (Seq EQ c)) -> Just          (Seq EQ c)-  Seq (PUSH (VNat 0)) (Seq COMPARE (Seq EQ c)) -> Just (Seq INT (Seq EQ c))-  Seq (PUSH (VInt 0)) (Seq COMPARE      EQ)    -> Just               EQ-  Seq (PUSH (VNat 0)) (Seq COMPARE      EQ)    -> Just (Seq INT      EQ)-  _                                            -> Nothing+  PUSH (VInt 0) :# COMPARE :# EQ :# c -> Just $ EQ :# c+  PUSH (VNat 0) :# COMPARE :# EQ :# c -> Just $ INT :# EQ :# c+  PUSH (VInt 0) :# COMPARE :# EQ      -> Just $ EQ+  PUSH (VNat 0) :# COMPARE :# EQ      -> Just $ INT :# EQ+  _                                   -> Nothing  simpleDrops :: Rule simpleDrops = \case   -- DROP 0 is Nop-  Seq (DROPN SZ) c -> Just c-  DROPN SZ -> Just Nop+  DROPN Zero :# c -> Just c+  DROPN Zero -> Just Nop    -- DROP 1 is DROP.   -- @gromak: DROP seems to be cheaper (in my experiments it consumed 3 less gas).@@ -251,8 +264,8 @@   -- I will leave this note and rule here in hope that someone will manage to   -- deal with this problem one day. -  -- Seq (DROPN (SS SZ)) c -> Just (Seq DROP c)-  -- DROPN (SS SZ) -> Just DROP+  -- DROPN One :# c -> Just (DROP :# c)+  -- DROPN One -> Just DROP    _ -> Nothing @@ -263,27 +276,27 @@ -- 'MAP' as well (which is harder). internalNop :: Rule internalNop = \case-  DIP Nop -> Just Nop-  Seq (DIP Nop) c -> Just c+  DIP Nop      -> Just Nop+  DIP Nop :# c -> Just c    _ -> Nothing  simpleDips :: Rule simpleDips = \case   -- DIP 0 is redundant-  Seq (DIPN SZ i) c -> Just (Seq i c)-  DIPN SZ i -> Just i+  DIPN Zero i :# c -> Just (i :# c)+  DIPN Zero i -> Just i    -- @gromak: same situation as with `DROP 1` (see above).-  -- Seq (DIPN (SS SZ) i) c -> Just (Seq (DIP i) c)-  -- DIPN (SS SZ) i -> Just (DIP i)+  -- DIPN One i :# c -> Just (DIP i :# c)+  -- DIPN One i -> Just (DIP i)    _ -> Nothing  adjacentDips :: Rule adjacentDips = \case-  Seq (DIP f) (DIP g) -> Just (DIP (Seq f g))-  Seq (DIP f) (Seq (DIP g) c) -> Just (DIP (Seq f g) `Seq` c)+  DIP f :# DIP g -> Just (DIP (f :# g))+  DIP f :# DIP g :# c -> Just (DIP (f :# g) :# c)    _ -> Nothing @@ -293,18 +306,18 @@ -- When @n@ is 2 it saves gas only. adjacentDrops :: Rule adjacentDrops = \case-  Seq DROP DROP -> Just (DROPN (SS $ SS SZ))-  Seq DROP (Seq DROP c) -> Just (DROPN (SS $ SS SZ) `Seq` c)+  DROP :# DROP -> Just (DROPN Two)+  DROP :# DROP :# c -> Just (DROPN Two :# c)    -- Does not compile, need to do something smart-  -- Seq (DROPN (SS (SS SZ))) DROP -> Just (DROPN (SS $ SS $ SS SZ))+  -- DROPN Two :# DROP -> Just (DROPN (Succ Two))    _ -> Nothing  specificPush :: Rule specificPush = \case-  push@PUSH{} -> optimizePush push-  Seq (push@PUSH{}) c -> (`Seq` c) <$> optimizePush push+  push@PUSH{}         -> optimizePush push+  push@PUSH{} :# c -> (:# c) <$> optimizePush push    _ -> Nothing   where@@ -323,33 +336,29 @@  isSomeOnIf :: Rule isSomeOnIf = \case-  Seq (IF (PUSH (VOption Just{})) (PUSH (VOption Nothing))) c -> case c of-    Seq (IF_NONE (PUSH (VBool False)) (Seq DROP (PUSH (VBool True)))) s -> Just s-    IF_NONE (PUSH (VBool False)) (Seq DROP (PUSH (VBool True))) -> Just Nop+  IF (PUSH (VOption Just{})) (PUSH (VOption Nothing)) :# c -> case c of+    IF_NONE (PUSH (VBool False)) (DROP :# PUSH (VBool True)) :# s -> Just s+    IF_NONE (PUSH (VBool False)) (DROP :# PUSH (VBool True))      -> Just Nop     _ -> Nothing   _ -> Nothing --- UNPAIR with continuation-pattern UNPAIR_c-  :: ()-  => (i ~ ('TPair a b : s), i' ~ (a : b : s), o' ~ o)-  => Instr i' o' -> Instr i o-pattern UNPAIR_c c = Seq DUP (Seq CAR (Seq (DIP CDR) c))- pairUnpair :: Rule pairUnpair = \case-  Seq PAIR (UNPAIR_c c) -> Just c-  Seq PAIR UNPAIR       -> Just Nop+  PAIR :# UNPAIR :# c -> Just c+  PAIR :# UNPAIR      -> Just Nop -  UNPAIR_c (Seq PAIR c) -> Just c-  UNPAIR_c      PAIR    -> Just Nop+  UNPAIR :# PAIR :# c -> Just c+  UNPAIR :# PAIR      -> Just Nop    _ -> Nothing  unpairMisc :: Rule unpairMisc = \case-  Seq UNPAIR SWAP -> Just (DUP `Seq` CDR `Seq` DIP CAR)-  Seq UNPAIR (Seq SWAP c) -> Just (DUP `Seq` CDR `Seq` DIP CAR `Seq` c)+  DUP :# CAR :# DIP CDR      -> Just $ UNPAIR+  DUP :# CAR :# DIP CDR :# c -> Just $ UNPAIR :# c++  DUP :# CDR :# DIP CAR      -> Just $ UNPAIR :# SWAP+  DUP :# CDR :# DIP CAR :# c -> Just $ UNPAIR :# SWAP :# c   _ -> Nothing  commuteArith ::@@ -364,15 +373,15 @@  swapBeforeCommutative :: Rule swapBeforeCommutative = \case-  Seq SWAP (Seq i c) -> (`Seq` c) <$> commuteArith i-  Seq SWAP i -> commuteArith i+  SWAP :# i :# c -> (:# c) <$> commuteArith i+  SWAP :# i -> commuteArith i    _ -> Nothing  pushPack :: Rule pushPack = \case-  Seq (PUSH x) PACK -> Just (pushPacked x)-  Seq (PUSH x) (Seq PACK c) -> Just (pushPacked x `Seq` c)+  PUSH x :# PACK -> Just (pushPacked x)+  PUSH x :# PACK :# c -> Just (pushPacked x :# c)    _ -> Nothing   where

@@ -20,6 +20,8 @@   , parseNoEnv   , parseValue   , parseExpandValue+  , parseValueFromFile+  , parseExpandValueFromFile    -- * For tests   , codeEntry@@ -46,8 +48,8 @@ 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)+  (Parsec, choice, customFailure, eitherP, eof, errorBundlePretty, getSourcePos, hidden, lookAhead,+  parse, try) import Text.Megaparsec.Pos (SourcePos(..), unPos)  import Michelson.ErrorPos (SrcPos(..), unsafeMkPos)@@ -175,6 +177,15 @@ -- | Parse untyped value from text which comes from something that is -- not a file (which is often the case). So we assume it does not need -- any parsing environment.+--+-- >>> parseValue "{PUSH int aaa}"+-- Left 1:11:+--   |+-- 1 | {PUSH int aaa}+--   |           ^^^^+-- unexpected "aaa}"+-- expecting value+-- <BLANKLINE> parseValue :: Text -> Either ParserException ParsedValue parseValue = first ParserException . parseNoEnv value "" @@ -182,6 +193,15 @@ parseExpandValue :: Text -> Either ParserException U.Value parseExpandValue = fmap expandValue . parseValue +-- | Like 'parseValue', but from text that comes from a file,+-- for which we get the 'FilePath'.+parseValueFromFile :: FilePath -> Text -> Either ParserException ParsedValue+parseValueFromFile filePath = first ParserException . parseNoEnv value filePath -- TODO remove filPath?++-- | Like 'parseValueFromFile', but also expands macros.+parseExpandValueFromFile :: FilePath -> Text -> Either ParserException U.Value+parseExpandValueFromFile filePath = fmap expandValue . parseValueFromFile filePath+ -- Primitive instruction ------------------ @@ -200,6 +220,15 @@ bracewrappedOps :: Parser [ParsedOp] bracewrappedOps = lookAhead (symbol "{") *> ops +-- |+-- >>> first ParserException $ parseNoEnv parsedOp "" "{a}"+-- Left 1:2:+--   |+-- 1 | {a}+--   |  ^+-- unexpected 'a'+-- expecting '{', '}', macro, morley instruction, or primitive instruction+-- <BLANKLINE> parsedOp :: Parser ParsedOp parsedOp = do   lms <- asks letMacros@@ -256,7 +285,8 @@ -- Some of the operations and macros have the same prefixes in their names -- So this case should be handled separately primOrMac :: Parser ParsedOp-primOrMac = (macWithPos (ifCmpMac parsedOp) <|> ifOrIfX)+primOrMac = hidden+   $  (macWithPos (ifCmpMac parsedOp) <|> ifOrIfX)   <|> (macWithPos (mapCadrMac parsedOp) <|> primWithPos (mapOp parsedOp))   <|> (try (primWithPos pairOp) <|> try (primWithPos pairNOp) <|> macWithPos pairMac)   <|> (try (macWithPos duupMac) <|> primWithPos dupOp)@@ -282,6 +312,16 @@ -- -- >>> [utypeQ| (int :a | nat :b) |] -- Ty (TOr % % (Ty TInt :a) (Ty TNat :b)) :+--+-- >>> [utypeQ|a|]+-- <BLANKLINE>+-- ...+--   |+-- 1 | a+--   | ^+-- unexpected 'a'+-- expecting type+-- ... utypeQ :: TH.QuasiQuoter utypeQ = parserToQuasiQuoter type_ 

@@ -9,8 +9,8 @@   , noteDef   , noteV2Def   , notesTVF-  , notesTVF2   , notesTVF2Def+  , notesVVFF   , notesTV   , notesTF   , notesVF@@ -37,14 +37,14 @@ note = lexeme $ string (annPrefix @tag) >> (specialNote <|> note' <|> emptyNote)   where     -- TODO [#48] these are special annotations and should not always be accepted-    specialVNote = mkAnnotationUnsafe <$> asum (map string specialVarAnns)-    specialFNote = mkAnnotationUnsafe <$> string specialFieldAnn+    specialVNote = unsafeMkAnnotation <$> asum (map string specialVarAnns)+    specialFNote = unsafeMkAnnotation <$> string specialFieldAnn     specialNote = specialVNote <|> specialFNote     emptyNote = pure noAnn     note' = do       a <- satisfy isValidAnnStart       b <- takeWhileP Nothing isValidAnnBodyChar-      return . mkAnnotationUnsafe $ T.cons a b+      return . unsafeMkAnnotation $ T.cons a b  noteV :: Parser VarAnn noteV = note@@ -55,20 +55,29 @@ noteF :: Parser FieldAnn noteF = note -noteF2 :: Parser (FieldAnn, FieldAnn)-noteF2 = do a <- note; b <- note; return (a, b)- noteV2Def :: Parser (VarAnn, VarAnn) noteV2Def = permute2Def note note  notesTVF :: Parser (TypeAnn, VarAnn, FieldAnn) notesTVF = permute3Def note note note -notesTVF2 :: Parser (TypeAnn, VarAnn, (FieldAnn, FieldAnn))-notesTVF2 = permute3Def note note noteF2- notesTVF2Def :: Parser (TypeAnn, VarAnn, (FieldAnn, FieldAnn)) notesTVF2Def = permute3Def note note (permute2Def note note)++-- | Parse 0/1/2 var anns and 0/1/2 field anns.+-- It doesn't matter which come first, so long as annotations of the same type appear together.+--+-- E.g.:+--+-- * "" is valid+-- * "%a" is valid+-- * "%a @c" is valid+-- * "%a %b @c @d" is valid+-- * "@c @d %a %b" is valid+-- * "@c %a %b @d" is not valid, because the two var anns are not "grouped" together.+-- * "%a @c @d %b" is not valid, because the two fields anns are not "grouped" together.+notesVVFF :: Parser ((VarAnn, VarAnn), (FieldAnn, FieldAnn))+notesVVFF = permute2Def (liftA2 (,) note noteDef) (liftA2 (,) note noteDef)  notesVF :: Parser (VarAnn, FieldAnn) notesVF = permute2Def note note

@@ -21,8 +21,7 @@ import Util.Positive  data CustomParserException-  = UnknownTypeException-  | StringLiteralException StringLiteralParserException+  = StringLiteralException StringLiteralParserException   | OddNumberBytesException   | WrongTagArgs Natural Positive   | WrongAccessArgs Natural Positive@@ -34,7 +33,6 @@ instance NFData CustomParserException  instance ShowErrorComponent CustomParserException where-  showErrorComponent UnknownTypeException = "unknown type"   showErrorComponent (StringLiteralException e) = showErrorComponent e   showErrorComponent OddNumberBytesException = "odd number bytes"   showErrorComponent ExcessFieldAnnotation = "excess field annotation"

@@ -14,7 +14,7 @@  import Prelude hiding (try) -import Text.Megaparsec (choice, satisfy, try)+import Text.Megaparsec (choice, label, satisfy, try) import Text.Megaparsec.Char (alphaNumChar, string) import qualified Text.Megaparsec.Char.Lexer as L @@ -25,7 +25,7 @@ import qualified Michelson.Untyped as U  extInstr :: Parser [ParsedOp] -> Parser ParsedUExtInstr-extInstr opsParser = choice [stackOp, testAssertOp opsParser, printOp]+extInstr opsParser = label "morley instruction" $ choice [stackOp, testAssertOp opsParser, printOp]  stackOp :: Parser ParsedUExtInstr stackOp = word' "STACKTYPE" U.STACKTYPE <*> stackType

@@ -10,6 +10,7 @@   -- * These are handled separately to have better error messages   , mapOp   , pairOp+  , unpairOp   , pairNOp   , cmpOp   , dupOp@@ -19,7 +20,7 @@  import Prelude hiding (EQ, GT, LT, many, note, some, try) -import Text.Megaparsec (choice, notFollowedBy, sepEndBy, try)+import Text.Megaparsec (choice, label, notFollowedBy, sepEndBy, try) import qualified Text.Megaparsec.Char.Lexer as L  import Michelson.Let (LetValue(..))@@ -33,7 +34,7 @@  -- | Parser for primitive Michelson instruction (no macros and extensions). primInstr :: Parser (Contract' ParsedOp) -> Parser ParsedOp -> Parser ParsedInstr-primInstr contractParser opParser = choice+primInstr contractParser opParser = label "primitive instruction" $ choice   [ dropOp, swapOp, digOp, dugOp, pushOp opParser, someOp, noneOp, unitOp   , ifNoneOp opParser, leftOp, rightOp, ifLeftOp opParser, nilOp   , consOp, ifConsOp opParser, sizeOp, emptySetOp, emptyMapOp, emptyBigMapOp, iterOp opParser@@ -47,6 +48,8 @@   , balanceOp, checkSigOp, sha256Op, sha512Op, blake2BOp, hashKeyOp, pairingCheckOp   , sourceOp, senderOp, chainIdOp, sha3Op, keccakOp, neverOp   , votingPowerOp, totalVotingPowerOp, try unpairNOp+  , unpairOp+  , ticketOp, readTicketOp, splitTicketOp, joinTicketsOp   ]  -- | Parse a sequence of instructions.@@ -203,11 +206,26 @@ -- Operations on pairs pairOp :: Parser ParsedInstr pairOp = do-  symbol' "PAIR";-  (t, v, (p, q)) <- notesTVF2;+  symbol' "PAIR"+  (t, v, (p, q)) <- notesTVF2Def++  -- Make sure this is a `PAIR` instruction,+  -- and not a `PAIR n` instruction.   notFollowedBy (lexeme L.decimal :: Parser Word)+   return $ PAIR t v p q +unpairOp :: Parser ParsedInstr+unpairOp = do+  symbol' "UNPAIR"+  ((vn1, vn2), (fn1, fn2)) <- notesVVFF++  -- Make sure this is an `UNPAIR` instruction,+  -- and not an `UNPAIR n` instruction.+  notFollowedBy (lexeme L.decimal :: Parser Word)++  return $ UNPAIR vn1 vn2 fn1 fn2+ pairNOp :: Parser ParsedInstr pairNOp = do   symbol' "PAIR"@@ -294,8 +312,6 @@  -- Operations on unions --- Using `notesTVF2Def` instead of `notesTVF2` allows for the second annotation--- to be unspecified. leftOp :: Parser ParsedInstr leftOp = do symbol' "LEFT"; (t, v, (f, f')) <- notesTVF2Def;                LEFT t v f f' <$> type_@@ -411,3 +427,17 @@  intOp :: Parser ParsedInstr intOp = word' "INT" INT <*> noteDef++-- Ticket Operations++ticketOp :: Parser ParsedInstr+ticketOp = word' "TICKET" TICKET <*> noteDef++readTicketOp :: Parser ParsedInstr+readTicketOp = word' "READ_TICKET" READ_TICKET <*> noteDef++splitTicketOp :: Parser ParsedInstr+splitTicketOp = word' "SPLIT_TICKET" SPLIT_TICKET <*> noteDef++joinTicketsOp :: Parser ParsedInstr+joinTicketsOp = word' "JOIN_TICKETS" JOIN_TICKETS <*> noteDef

@@ -53,7 +53,7 @@   semicolon   local (addLet l) (letInner opParser) <|> return (addLet l env) --- | add a Let to the environment in the correct place+-- | Add a Let to the environment in the correct place addLet :: Let -> LetEnv -> LetEnv addLet l (LetEnv lms lvs lts) = case l of   LetM lm -> LetEnv (Map.insert (lmName lm) lm lms) lvs lts@@ -67,10 +67,12 @@   , (LetT <$> letType)   ] --- | build a let name parser from a leading character parser+-- | Build a let name parser from a leading character parser letName :: Parser Char -> Parser Text letName p = lexeme $ do   v <- p+  -- FIXME (#557): It is possible to define a let name such as "add3", but then+  -- the parser doesn't recognize when it's used as an instruction.   let validChar x = Char.isAscii x && (Char.isAlphaNum x || x == '\'' || x == '_')   vs <- many (satisfy validChar)   return $ toText (v:vs)

@@ -18,10 +18,10 @@  import Prelude hiding (note, try) -import Text.Megaparsec (customFailure, notFollowedBy, try)+import Text.Megaparsec (customFailure, label, notFollowedBy, skipMany, try) import Text.Megaparsec.Char.Lexer (decimal) -import Michelson.Macro (CadrStruct(..), Macro(..), PairStruct(..), UnpairStruct(..), ParsedOp(..))+import Michelson.Macro (CadrStruct(..), Macro(..), PairStruct(..), ParsedOp(..), UnpairStruct(..)) import qualified Michelson.Macro as Macro import Michelson.Parser.Annotations import Michelson.Parser.Error@@ -35,8 +35,8 @@ import Util.Positive  macro :: Parser ParsedOp -> Parser Macro-macro opParser =-      word' "CASE" CASE <*> someNE ops+macro opParser = label "macro"+   $  word' "CASE" CASE <*> someNE ops   <|> symbol' "TAG" *> tagMac   <|> symbol' "ACCESS" *> accessMac   <|> symbol' "SET " *> setMac@@ -81,25 +81,20 @@   let ps = Macro.mapPairLeaves fns a   return $ PAPAIR ps tn vn -upairMacInner :: Parser UnpairStruct-upairMacInner = do+unpairMacInner :: Parser UnpairStruct+unpairMacInner = do   string' "P"-  l <- (string' "A" $> UF (noAnn, noAnn)) <|> upairMacInner-  r <- (string' "I" $> UF (noAnn, noAnn)) <|> upairMacInner+  l <- (string' "A" $> UF) <|> unpairMacInner+  r <- (string' "I" $> UF) <|> unpairMacInner   return $ UP l r  unpairMac :: Parser Macro unpairMac = do   string' "UN"-  a <- upairMacInner+  a <- unpairMacInner   symbol' "R"-  (vns, fns) <- permute2Def (some note) (some note)-  return $ UNPAIR (Macro.mapUnpairLeaves (padAnnotations vns fns) a)-  where-    padAnnotations []       []       = []-    padAnnotations []       (f : fs) = (noAnn, f) : padAnnotations [] fs-    padAnnotations (v : vs) []       = (v, noAnn) : padAnnotations vs []-    padAnnotations (v : vs) (f : fs) = (v, f    ) : padAnnotations vs fs+  skipMany $ (void noteF) <|> (void noteV)+  return $ UNPAPAIR a  cadrMac :: Parser Macro cadrMac = lexeme $ do

@@ -15,7 +15,7 @@ import Data.Default (Default, def) import qualified Data.Map as Map import Fmt (pretty)-import Text.Megaparsec (choice, customFailure, sepBy)+import Text.Megaparsec (choice, customFailure, label, sepBy)  import Michelson.Let (LetType(..)) import Michelson.Parser.Annotations@@ -65,17 +65,16 @@  typeInner   :: Parser FieldAnn -> Parser (FieldAnn, Ty)-typeInner fp = lexeme $ choice $ (\x -> x fp) <$>+typeInner fp = label "type" $ lexeme $ choice $ (\x -> x fp) <$>   [ t_int, t_nat, t_string, t_bytes, t_mutez, t_bool   , t_keyhash, t_timestamp, t_address   , t_key, t_unit, t_never, t_signature, t_chain_id   , t_bls12381fr, t_bls12381g1, t_bls12381g2   , t_option, t_list, t_set-  , t_operation, t_contract, t_pair, t_or+  , t_operation, t_contract, t_ticket, t_pair, t_or   , t_lambda, t_map, t_big_map, t_view   , t_void, t_letType   , t_operator-  , const (customFailure UnknownTypeException)   ]  ----------------------------------------------------------------------------@@ -155,6 +154,13 @@   (f, t) <- fieldType fp   a <- type_   return (f, Ty (TContract a) t)++t_ticket :: (Default a) => Parser a -> Parser (a, Ty)+t_ticket fp = do+  symbol' "Ticket"+  (f, t) <- fieldType fp+  a <- type_+  return (f, Ty (TTicket a) t)  t_unit :: (Default a) => Parser a -> Parser (a, Ty) t_unit fp = do

@@ -20,7 +20,7 @@ import qualified Data.Map as Map import qualified Text.Hex as Hex -import Text.Megaparsec (anySingle, choice, customFailure, manyTill, satisfy, takeWhileP, try)+import Text.Megaparsec (anySingle, choice, customFailure, label, manyTill, satisfy, takeWhileP, try) import Text.Megaparsec.Char (char, string) import qualified Text.Megaparsec.Char.Lexer as L @@ -30,7 +30,7 @@ import Michelson.Parser.Helpers import Michelson.Parser.Lexer import Michelson.Parser.Types (Parser, letValues)-import Michelson.Text (isMChar, mkMTextUnsafe)+import Michelson.Text (isMChar, unsafeMkMText) import qualified Michelson.Untyped as U  -- | Parse untyped 'ParsedValue'. Take instruction parser as argument@@ -41,7 +41,7 @@     valueInner' = valueInner opParser  valueInner :: Parser ParsedOp -> Parser ParsedValue-valueInner opParser = choice $+valueInner opParser = label "value" $ choice $   [ stringLiteral, bytesLiteral, intLiteral, unitValue   , trueValue, falseValue, pairValue opParser, leftValue opParser   , rightValue opParser, someValue opParser, noneValue, nilValue@@ -52,7 +52,7 @@ seqOrLambda opParser = try (lambdaValue opParser) <|> seqValue opParser  stringLiteral :: Parser ParsedValue-stringLiteral = U.ValueString . mkMTextUnsafe . toText <$> do+stringLiteral = U.ValueString . unsafeMkMText . toText <$> do   _ <- try $ string "\""   manyTill validChar (string "\"")   where

@@ -42,12 +42,12 @@      forall inp out.      Bool   -> (forall t. Value t -> Value t)-  -- ^ Should transform only atomic values, 'dfsValue' will be applied to it.+  -- ^ Should transform only atomic values, 'dfsMapValue' will be applied to it.   -> Instr inp out   -> Instr inp out transformConstants dsGoToValues f = fst . dfsInstr def{ dsGoToValues } step   where     step :: forall i o. Instr i o -> (Instr i o, ())     step = (,()) . \case-      PUSH v -> PUSH (dfsModifyValue f v)+      PUSH v -> PUSH (dfsMapValue f v)       i -> i

@@ -4,6 +4,7 @@  module Michelson.Printer   ( RenderDoc(..)+  , renderAnyBuildable   , printDoc   , printUntypedContract   , printTypedContractCode@@ -17,8 +18,7 @@ import Data.Singletons (SingI) import qualified Data.Text.Lazy as TL -import Michelson.Printer.Util (RenderDoc(..), doesntNeedParens, printDoc)-import Michelson.TypeCheck.Types (SomeContract(..))+import Michelson.Printer.Util (RenderDoc(..), renderAnyBuildable, doesntNeedParens, printDoc) import qualified Michelson.Typed as T import qualified Michelson.Untyped as U @@ -57,6 +57,6 @@  -- | Convert 'SomeContract' into a textual representation which -- will be accepted by the OCaml reference client.-printSomeContract :: Bool -> SomeContract -> TL.Text-printSomeContract forceSingleLine (SomeContract fc) =+printSomeContract :: Bool -> T.SomeContract -> TL.Text+printSomeContract forceSingleLine (T.SomeContract fc) =   printTypedContract forceSingleLine fc

@@ -11,9 +11,12 @@   , renderOps   , renderOpsList   , renderOpsListNoBraces+  , renderAnyBuildable   , spaces   , wrapInParens   , buildRenderDoc+  , buildRenderDocExtended+  , renderDocList      -- * Smart parentheses   , RenderContext@@ -23,12 +26,13 @@   , assertParensNotNeeded   ) where +import Fmt (Buildable, pretty) import Control.Exception (assert) import qualified Data.Text.Lazy as LT import Data.Text.Lazy.Builder (Builder) import Text.PrettyPrint.Leijen.Text   (Doc, SimpleDoc, align, braces, displayB, displayT, enclose, hcat, isEmpty, parens, punctuate,-  renderOneLine, renderPretty, semi, space, vcat, (<+>))+  renderOneLine, renderPretty, semi, space, text, vcat, (<+>), lbracket, rbracket, encloseSep)  -- | Environment carried during recursive rendering. newtype RenderContext = RenderContext@@ -55,6 +59,14 @@   isRenderable :: a -> Bool   isRenderable _ = True +-- | Renders a list of 'RenderDoc' elements surrounded with square brackets,+-- separated by a comma and a space.+renderDocList :: RenderDoc a => RenderContext -> [a] -> Doc+renderDocList context = encloseSep lbracket rbracket ", " . fmap (renderDoc context)++renderAnyBuildable :: Buildable a => a -> Doc+renderAnyBuildable = text . pretty+ -- | A new type that can wrap values so that the RenderDoc -- instances of the combined value can have a different -- behavior for the pretty printer.@@ -106,6 +118,11 @@ -- It's formatted the same way as `printDoc` formats docs. buildRenderDoc :: RenderDoc a => a -> Builder buildRenderDoc = printDocB True . renderDoc doesntNeedParens++-- | Works as 'buildRenderDoc' above, but doesn't force the doc to be printed in one line+buildRenderDocExtended :: RenderDoc a => a -> Builder+buildRenderDocExtended = printDocB False . renderDoc doesntNeedParens+  -- | Here using a page width of 80 and a ribbon width of 1.0 -- https://hackage.haskell.org/package/wl-pprint-1.2.1/docs/Text-PrettyPrint-Leijen.html

@@ -56,29 +56,28 @@ import Data.Text.IO (getContents) import qualified Data.Text.IO.Utf8 as Utf8 (readFile) import Fmt (Buildable(build), blockListF, fmt, fmtLn, nameF, pretty, (+|), (|+))-import Named ((:!), (:?), arg, argDef, defaults, (!))+import Named (arg, argDef, defaults, (!), (:!), (:?)) import Text.Megaparsec (parse) -import Data.Singletons (demote)-import Data.Typeable (gcast) import Michelson.Interpret   (ContractEnv(..), InterpretError(..), InterpretResult(..), InterpreterState(..), MorleyLogs(..),-  RemainingSteps(..), handleContractReturn, interpret)+  RemainingSteps(..), assignBigMapIds, handleContractReturn, interpret) import qualified Michelson.Interpret.Pack as Pack import Michelson.Macro (ParsedOp, expandContract) import qualified Michelson.Parser as P import Michelson.Runtime.GState import Michelson.Runtime.TxData import Michelson.TypeCheck-  (SomeContractAndStorage(..), TCError, typeCheckContractAndStorage, typeVerifyParameter) import Michelson.Typed   (CreateContract(..), EntrypointCallT, EpAddress(..), EpName, Operation'(..), ParameterScope,-  SomeValue'(..), TransferTokens(..), starNotes, starParamNotes, untypeValue)+  SomeContractAndStorage(..), SomeStorage(..), SomeValue(..), TransferTokens(..), starNotes,+  starParamNotes, untypeValue) import qualified Michelson.Typed as T-import Michelson.Typed.Origination (OriginationOperation(..), mkOriginationOperationHash)-import Michelson.Untyped (Contract, OperationHash(..))+import Michelson.Typed.Origination+  (OperationHash(..), OriginationOperation(..), mkContractAddress, mkOriginationOperationHash)+import Michelson.Untyped (Contract) import qualified Michelson.Untyped as U-import Tezos.Address (Address(..), OriginationIndex(..), mkContractAddress)+import Tezos.Address (Address(..), OriginationIndex(..)) import Tezos.Core   (Mutez, Timestamp(..), getCurrentTime, unMutez, unsafeAddMutez, unsafeSubMutez, zeroMutez) import Tezos.Crypto (KeyHash, blake2b, parseKeyHash)@@ -167,15 +166,17 @@   -- ^ Sending 0tz towards an address.   | EEFailedToApplyUpdates GStateUpdateError   -- ^ Failed to apply updates to GState.-  | EEIllTypedParameter TCError+  | EEIllTypedParameter a TCError   -- ^ Contract parameter is ill-typed.-  | EEUnexpectedParameterType T.T T.T+  | EEUnexpectedParameterType a T.T T.T   -- ^ Contract parameter is well-typed, but its type does   -- not match the entrypoint's type.   | EEUnknownEntrypoint EpName   -- ^ Specified entrypoint to run is not found.   | EETransactionFromContract a Mutez   -- ^ A transaction from an originated contract was attempted as a global operation.+  | EEWrongParameterType a+  -- ^ Type of parameter in transfer to an implicit account is not Unit.   deriving stock (Show, Functor)  instance (Buildable a) => Buildable (ExecutorError' a) where@@ -195,14 +196,16 @@       EEZeroTransaction addr ->         "Transaction of 0ꜩ towards a key address " +| addr |+ " which has no code is prohibited"       EEFailedToApplyUpdates err -> "Failed to update GState: " +| err |+ ""-      EEIllTypedParameter err -> "The contract parameter is ill-typed: " +| err |+ ""-      EEUnexpectedParameterType expectedT actualT ->+      EEIllTypedParameter _ err -> "The contract parameter is ill-typed: " +| err |+ ""+      EEUnexpectedParameterType _ actualT expectedT ->         "The contract parameter is well-typed, but did not match the contract's entrypoint's type.\n" <>         "Expected: " +| expectedT |+ "\n" <>         "Got: " +| actualT |+ ""       EEUnknownEntrypoint epName -> "The contract does not contain entrypoint '" +| epName |+ "'"       EETransactionFromContract addr amount ->         "Global transaction of funds (" +| amount |+ ") from an originated contract (" +| addr |+ ") is prohibited."+      EEWrongParameterType addr ->+        "Bad contract parameter for: " +| addr |+ ""  type ExecutorError = ExecutorError' Address @@ -243,6 +246,7 @@ -- contract. originateContract   :: FilePath+  -> TypeCheckOptions   -> Address   -> Maybe KeyHash   -> Mutez@@ -250,8 +254,8 @@   -> U.Contract   -> "verbose" :! Bool   -> IO Address-originateContract dbPath originator delegate balance uStorage uContract verbose = do-  origination <- either throwM pure $+originateContract dbPath tcOpts originator delegate balance uStorage uContract verbose = do+  origination <- either throwM pure . typeCheckingWith tcOpts $     mkOrigination <$> typeCheckContractAndStorage uContract uStorage   -- pass 100500 as maxSteps, because it doesn't matter for origination,   -- as well as 'now'@@ -274,22 +278,23 @@   -> Word64   -> Mutez   -> FilePath+  -> TypeCheckOptions   -> U.Value   -> U.Contract   -> TxData   -> "verbose" :! Bool   -> "dryRun" :! Bool-  -> IO U.Value-runContract maybeNow maybeLevel maxSteps initBalance dbPath uStorage uContract txData+  -> IO SomeStorage+runContract maybeNow maybeLevel maxSteps initBalance dbPath tcOpts uStorage uContract txData   verbose (arg #dryRun -> dryRun) = do-  origination <- either throwM pure $+  origination <- either throwM pure . typeCheckingWith tcOpts $     mkOrigination <$> typeCheckContractAndStorage uContract uStorage   (_, newSt) <- runExecutorMWithDB maybeNow maybeLevel dbPath (RemainingSteps maxSteps) verbose ! #dryRun dryRun $ do     -- Here we are safe to bypass executeGlobalOperations for origination,     -- since origination can't generate more operations.     addr <- executeGlobalOrigination origination     let transferOp = TransferOp addr txData-    executeGlobalOperations [transferOp]+    executeGlobalOperations tcOpts [transferOp]     getContractStorage addr   return newSt   where@@ -309,13 +314,13 @@       , ooContract = contract       } -    getContractStorage :: Address -> ExecutorM U.Value+    getContractStorage :: Address -> ExecutorM SomeStorage     getContractStorage addr = do       addrs <- use (esGState . gsAddressesL)       case addrs ^. at addr of         Nothing -> error $ pretty addr <> " is unknown"         Just (ASSimple {}) -> error $ pretty addr <> " is a simple address"-        Just (ASContract (ContractState{..})) -> return $ untypeValue csStorage+        Just (ASContract (ContractState{..})) -> return $ SomeStorage csStorage  -- | Send a transaction to given address with given parameters. transfer ::@@ -323,14 +328,15 @@   -> Maybe Natural   -> Word64   -> FilePath+  -> TypeCheckOptions   -> Address   -> TxData   -> "verbose" :! Bool   -> "dryRun" :? Bool   -> IO ()-transfer maybeNow maybeLevel maxSteps dbPath destination txData verbose dryRun = do+transfer maybeNow maybeLevel maxSteps dbPath tcOpts destination txData verbose dryRun = do   void $ runExecutorMWithDB maybeNow maybeLevel dbPath (RemainingSteps maxSteps) verbose dryRun $-    executeGlobalOperations [TransferOp destination txData]+    executeGlobalOperations tcOpts [TransferOp destination txData]  ---------------------------------------------------------------------------- -- Executor@@ -432,9 +438,10 @@  -- | Execute a list of global operations, discarding their results. executeGlobalOperations-  :: [ExecutorOp]+  :: TypeCheckOptions+  -> [ExecutorOp]   -> ExecutorM ()-executeGlobalOperations = mapM_ $ \op ->+executeGlobalOperations tcOpts = mapM_ $ \op ->   executeMany (#isGlobalOp .! True) [op]   where     -- | Execute a list of operations and additional operations they return, until there are none.@@ -445,8 +452,8 @@           case op of             OriginateOp origination -> void $ executeOrigination isGlobalOp origination             TransferOp addr txData -> do-              moreOps <- executeTransfer isGlobalOp addr txData-              executeMany (#isGlobalOp .! False) $ opsTail <> moreOps+              moreOps <- executeTransfer isGlobalOp tcOpts addr txData+              executeMany (#isGlobalOp .! False) $ moreOps <> opsTail  -- | Execute a global origination operation. executeGlobalOrigination :: OriginationOperation -> ExecutorM Address@@ -457,7 +464,7 @@   :: "isGlobalOp" :! Bool   -> OriginationOperation   -> ExecutorM Address-executeOrigination (arg #isGlobalOp -> isGlobalOp) origination = do+executeOrigination (arg #isGlobalOp -> isGlobalOp) origination@(OriginationOperation _ _ bal st contract) = do   when isGlobalOp $ do     beginGlobalOperation     assign esOperationHash $ mkOriginationOperationHash origination@@ -466,9 +473,13 @@    gs <- use esGState   originationNonce <- use esOriginationNonce-  let contractState =-        case origination of-          OriginationOperation _ _ bal st contract -> ContractState bal contract st++  -- Add big_map IDS to storage+  let bigMapCounter0 = gs ^. gsBigMapCounterL+  let (storageWithIds, bigMapCounter1) = runState (assignBigMapIds st) bigMapCounter0++  let contractState = ContractState bal contract storageWithIds+   let originatorAddress = ooOriginator origination   originatorBalance <- case gsAddresses gs ^. at originatorAddress of     Nothing -> throwError (EEUnknownManager originatorAddress)@@ -482,10 +493,15 @@   let     address = mkContractAddress opHash (OriginationIndex originationNonce) (gsCounter gs)     updates =-      [ GSAddAddress address (ASContract contractState)-      , GSSetBalance originatorAddress originatorBalance-      , GSIncrementCounter-      ]+      catMaybes+        [ Just $ GSAddAddress address (ASContract contractState)+        , Just $ GSSetBalance originatorAddress originatorBalance+        , Just $ GSIncrementCounter+        , if bigMapCounter0 == bigMapCounter1+            then Nothing+            else Just $ GSSetBigMapCounter bigMapCounter1+        ]+   case applyUpdates updates gs of     Left _ ->       throwError $ EEAlreadyOriginated address contractState@@ -500,10 +516,11 @@ -- | Execute a transfer operation. executeTransfer   :: "isGlobalOp" :! Bool+  -> TypeCheckOptions   -> Address   -> TxData   -> ExecutorM [ExecutorOp]-executeTransfer (arg #isGlobalOp -> isGlobalOp) addr txData = do+executeTransfer (arg #isGlobalOp -> isGlobalOp) tcOpts addr txData = do     when isGlobalOp $       beginGlobalOperation @@ -520,6 +537,9 @@         isKeyAddress _ = False     let isZeroTransfer = tdAmount txData == zeroMutez +    when (badParamToImplicitAccount addr $ tdParameter txData) $+      throwError $ EEWrongParameterType addr+     -- Transferring 0 XTZ to a key address is prohibited.     when (isZeroTransfer && isKeyAddress addr) $       throwError $ EEZeroTransaction addr@@ -571,13 +591,15 @@         -- we need to typecheck the parameter.         typedParameter <-           case tdParameter txData of-            TxTypedParam (typedVal :: T.Value t) ->-              maybe (throwError $ EEUnexpectedParameterType (demote @epArg) (demote @t)) pure $-                gcast @t @epArg typedVal+            TxTypedParam (typedVal :: T.Value t) -> do+              T.castM @t @epArg typedVal (throwError ... EEUnexpectedParameterType addr)             TxUntypedParam untypedVal ->-              liftEither $ first EEIllTypedParameter $+              liftEither $ first (EEIllTypedParameter addr) $ typeCheckingWith tcOpts $                 typeVerifyParameter @epArg existingContracts untypedVal +        let bigMapCounter0 = gs ^. gsBigMapCounterL+        let (typedParameterWithIds, bigMapCounter1) = runState (assignBigMapIds typedParameter) bigMapCounter0+         -- I'm not entirely sure why we need to pattern match on `()` here,         -- but, if we don't, we get a compiler error that I suspect is somehow related         -- to the existential types we're matching on a few lines above.@@ -588,7 +610,7 @@         () <- when isGlobalOp $           esOperationHash .= mkTransferOperationHash             addr-            typedParameter+            typedParameterWithIds             (tdEntrypoint txData)             (tdAmount txData) @@ -613,12 +635,17 @@         iur@InterpretResult           { iurOps = sideEffects           , iurNewStorage = newValue-          , iurNewState = InterpreterState _ newRemainingSteps _+          , iurNewState = InterpreterState _ newRemainingSteps _ bigMapCounter2           }           <- liftEither $ first (EEInterpreterFailed addr) $              handleContractReturn $-                interpret csContract epc-                typedParameter csStorage contractEnv+                interpret+                  csContract+                  epc+                  typedParameterWithIds+                  csStorage+                  bigMapCounter1+                  contractEnv         let           updBalance             | newBalance == csBalance = Nothing@@ -626,9 +653,13 @@           updStorage             | SomeValue newValue == SomeValue csStorage = Nothing             | otherwise = Just $ GSSetStorageValue addr newValue+          updBigMapCounter+            | bigMapCounter0 == bigMapCounter2 = Nothing+            | otherwise = Just $ GSSetBigMapCounter bigMapCounter2           updates = catMaybes             [ updBalance             , updStorage+            , updBigMapCounter             ]         return (updates, sideEffects, Just iur, newRemainingSteps) @@ -661,8 +692,8 @@     packedOperation =       BSL.toStrict $         (runPut $ putWord64be $ unMutez amount)-        <> Pack.encodeEpAddress (EpAddress to epName)-        <> Pack.encodeValue param+        <> (Pack.toBinary $ T.toVal (EpAddress to epName))+        <> Pack.toBinary param  -- The argument is the address of the contract that generated this operation. convertOp :: Address -> T.Operation -> Maybe ExecutorOp@@ -701,3 +732,10 @@ beginGlobalOperation = do   esOriginationNonce .= 0   esSourceAddress .= Nothing++-- | Return True if address is an implicit account yet the param is not Unit.+badParamToImplicitAccount :: Address -> TxParam -> Bool+badParamToImplicitAccount (ContractAddress _) _                       = False+badParamToImplicitAccount (KeyAddress _) (TxTypedParam T.VUnit)       = False+badParamToImplicitAccount (KeyAddress _) (TxUntypedParam U.ValueUnit) = False+badParamToImplicitAccount _ _                                         = True

@@ -9,12 +9,13 @@   , dummyLevel   , dummyMaxSteps   , dummyVotingPowers+  , dummyBigMapCounter   , dummyContractEnv   , dummyOrigination   ) where  import Michelson.Interpret (ContractEnv(..), RemainingSteps)-import Michelson.Runtime.GState (dummyVotingPowers, genesisAddress)+import Michelson.Runtime.GState (BigMapCounter, dummyVotingPowers, genesisAddress) import Michelson.Typed (ParameterScope, StorageScope) import qualified Michelson.Typed as T import Michelson.Typed.Origination (OriginationOperation(..))@@ -35,6 +36,9 @@ -- interpreter from working for eternity. dummyMaxSteps :: RemainingSteps dummyMaxSteps = 100500++dummyBigMapCounter :: BigMapCounter+dummyBigMapCounter = 0  -- | Dummy 'ContractEnv' with some reasonable hardcoded values. You -- can override values you are interested in using record update

@@ -16,6 +16,8 @@   , mkVotingPowers   , mkVotingPowersFromMap   , dummyVotingPowers+  , BigMapCounter(..)+  , bigMapCounter    -- * GState   , GState (..)@@ -23,6 +25,7 @@   , gsAddressesL   , gsVotingPowersL   , gsCounterL+  , gsBigMapCounterL   , genesisAddresses   , genesisKeyHashes   , genesisAddress@@ -50,22 +53,24 @@   , extractAllContracts   ) where -import Control.Lens (at)+import Control.Lens (at, makeLenses) import Data.Aeson (FromJSON(..), ToJSON(..), object, withObject, (.:), (.=)) import qualified Data.Aeson as Aeson import qualified Data.Aeson.Encode.Pretty as Aeson import Data.Aeson.TH (deriveJSON) import qualified Data.ByteString.Lazy as LBS+import Data.Default (def) import Data.List.NonEmpty ((!!)) import qualified Data.Map.Strict as Map-import Data.Typeable ((:~:)(..), eqT)+import Data.Type.Equality ((:~:)(..)) import Fmt (Buildable(build), (+|), (|+), (||+)) import System.IO.Error (IOError, isDoesNotExistError)  import Michelson.TypeCheck-  (SomeContractAndStorage(..), SomeParamType(..), TcOriginatedContracts,-  typeCheckContractAndStorage)+  (SomeParamType(..), TcOriginatedContracts,+  typeCheckContractAndStorage, typeCheckingWith) import qualified Michelson.Typed as T+import Michelson.Typed.Existential (SomeContractAndStorage(..)) import Michelson.Typed.Scope import Michelson.Untyped (Contract, Value) import Tezos.Address (Address(..), ContractHash, GlobalCounter(..))@@ -73,6 +78,7 @@ import Tezos.Crypto import Util.Aeson import Util.Lens+import Util.Sing (eqI)  -- | State of a contract with code. data ContractState =@@ -104,7 +110,7 @@       (balance :: Mutez) <- o .: "balance"       (uStorage :: Value) <- o .: "storage"       (uContract :: Contract) <- o .: "contract"-      case typeCheckContractAndStorage uContract uStorage of+      case typeCheckingWith def $ typeCheckContractAndStorage uContract uStorage of         Right (SomeContractAndStorage contract storage) ->           pure $ ContractState balance contract storage         Left err -> fail $ "Unable to parse `ContractState`: " <> (show err)@@ -170,6 +176,17 @@ mkVotingPowers :: [(KeyHash, Natural)] -> VotingPowers mkVotingPowers = mkVotingPowersFromMap . Map.fromListWith (+) +-- | All big_maps stored in a chain have a globally unique ID.+--+-- We use this counter to keep track of how many big_maps have been created so far,+-- and to generate new IDs whenever a new big_map is created.+newtype BigMapCounter = BigMapCounter { _bigMapCounter :: Natural }+  deriving stock (Show, Eq, Generic)+  deriving anyclass (NFData)+  deriving newtype (ToJSON, FromJSON, Num, Buildable)++makeLenses ''BigMapCounter+ -- | Persistent data passed to Morley contracts which can be updated -- as result of contract execution. data GState = GState@@ -181,6 +198,7 @@   -- ^ Voting power distribution.   , gsCounter :: GlobalCounter   -- ^ Ever increasing operation counter.+  , gsBigMapCounter :: BigMapCounter   } deriving stock (Show)  makeLensesWith postfixLFields ''GState@@ -252,6 +270,7 @@     ]   , gsVotingPowers = dummyVotingPowers   , gsCounter = GlobalCounter 0+  , gsBigMapCounter = BigMapCounter 0   }  data GStateParseError =@@ -290,6 +309,7 @@   GSSetStorageValue :: StorageScope st => Address -> T.Value st -> GStateUpdate   GSSetBalance :: Address -> Mutez -> GStateUpdate   GSIncrementCounter :: GStateUpdate+  GSSetBigMapCounter :: BigMapCounter -> GStateUpdate  deriving stock instance Show GStateUpdate @@ -304,6 +324,8 @@         "Set balance of address " +| addr |+ " to " +| balance |+ ""       GSIncrementCounter ->         "Increment internal counter after operation"+      GSSetBigMapCounter inc ->+        "Increment internal big_map counter by: " +| build inc  data GStateUpdateError   = GStateAddressExists Address@@ -332,6 +354,7 @@       setStorageValue addr newValue     GSSetBalance addr newBalance -> setBalance addr newBalance     GSIncrementCounter -> Right . over gsCounterL (+1)+    GSSetBigMapCounter bmCounter -> Right . set gsBigMapCounterL bmCounter  -- | Apply a list of 'GStateUpdate's to 'GState'. applyUpdates :: [GStateUpdate] -> GState -> Either GStateUpdateError GState@@ -353,7 +376,7 @@     modifier :: AddressState -> Either GStateUpdateError AddressState     modifier (ASSimple _) = Left (GStateNotContract addr)     modifier (ASContract (ContractState b c (_ :: T.Value st') )) = do-      case (eqT @st @st') of+      case eqI @st @st' of         Just Refl -> Right $ ASContract $ ContractState b c newValue         _ -> Left $ GStateStorageNotMatch addr 

@@ -0,0 +1,205 @@+-- SPDX-FileCopyrightText: 2020 Tocqueville Group+--+-- SPDX-License-Identifier: LicenseRef-MIT-TQ++module Michelson.Runtime.Import+  (+    -- * Read, parse, typecheck contract+    readContract+  , readSomeContract+  , readUntypedContract+  , importContract+  , importSomeContract+  , importUntypedContract+  , ImportContractError(..)++    -- * Read, parse, typecheck value+  , readValue+  , importValue+  , importSomeValue+  , importUntypedValue+  , ImportValueError (..)++    -- * Generic helpers+  , importUsing+  ) where++import Data.Default (def)+import qualified Data.Text.IO.Utf8 as Utf8 (readFile)+import Fmt (Buildable(build), pretty, unlinesF, (+|), (|+))++import Michelson.Parser (parseExpandValueFromFile)+import Michelson.Parser.Error (ParserException(..))+import Michelson.Runtime (parseExpandContract)+import Michelson.TypeCheck+  (TCError, typeCheckContract, typeCheckTopLevelType, typeCheckingWith,+  typeVerifyContract, typeVerifyTopLevelType)+import Michelson.Typed (Contract(..), SingI, SomeContract(..), SomeValue, Value)+import qualified Michelson.Untyped as U++----------------------------------------------------------------------------+-- Reading, parsing, typechecking contract+----------------------------------------------------------------------------++-- | Purely read an untyped contract from Michelson textual representation.+--+-- 'FilePath' is accepted solely as a hint for error messages.+readUntypedContract+  :: FilePath+  -> Text+  -> Either ImportContractError U.Contract+readUntypedContract filePath txt = do+  first (ICEParse filePath) $ parseExpandContract (Just filePath) txt++-- | Purely read a typed contract from Michelson textual representation.+readSomeContract+  :: FilePath+  -> Text+  -> Either ImportContractError SomeContract+readSomeContract filePath txt = do+  contract <- readUntypedContract filePath txt+  first (ICETypeCheck filePath) $+    typeCheckingWith def $ typeCheckContract contract++-- | Purely read a typed contract from Michelson textual representation,+-- failing if parameter or storage types mismatch with the expected ones.+readContract+  :: forall cp st .+     Each '[SingI] [cp, st]+  => FilePath+  -> Text+  -> Either ImportContractError (Contract cp st)+readContract filePath txt = do+  contract <- readUntypedContract filePath txt+  first (ICETypeCheck filePath) $+    typeCheckingWith def $ typeVerifyContract contract++-- | Read a thing from a file, using the provided parsing function.+importUsing+  :: (Exception e)+  => (FilePath -> Text -> Either e a)+  -> FilePath -> IO a+importUsing readFn file =+  either throwM pure . readFn file =<< Utf8.readFile file++-- | Import untyped contract from a given file path.+--+-- This function reads file, and parses a contract.+--+-- This function may throw 'IOException' and 'ImportContractError'.+importUntypedContract :: FilePath -> IO U.Contract+importUntypedContract = importUsing readUntypedContract++-- | Import contract from a given file path.+--+-- This function reads file, parses and type checks a contract.+-- Within the typechecking we assume that no contracts are originated,+-- otherwise a type checking error will be caused.+--+-- This function may throw 'IOException' and 'ImportContractError'.+importContract+  :: forall cp st .+     Each '[SingI] [cp, st]+  => FilePath -> IO (Contract cp st)+importContract = importUsing readContract++-- | Version of 'importContract' that doesn't require you to know+-- contract's parameter and storage types.+importSomeContract :: FilePath -> IO SomeContract+importSomeContract = importUsing readSomeContract++-- | Error type for 'importContract' function.+data ImportContractError+  = ICEParse FilePath ParserException+  | ICETypeCheck FilePath TCError+  deriving stock (Show, Eq)++instance Buildable ImportContractError where+  build =+    \case+      ICEParse filePath e -> unlinesF+        [ "Error at " <> build filePath+        , "Failed to parse the contract: " +| e |+ ""+        ]+      ICETypeCheck filePath e -> unlinesF+        [ "Error at " <> build filePath+        , "The contract is ill-typed: " +| e |+ ""+        ]++instance Exception ImportContractError where+  displayException = pretty++----------------------------------------------------------------------------+-- Reading, parsing, typechecking value+----------------------------------------------------------------------------++-- | Purely read an untyped Michelson value from textual representation.+--+-- 'FilePath' is accepted solely as a hint for error messages.+readUntypedValue+  :: FilePath+  -> Text+  -> Either ImportValueError U.Value+readUntypedValue filePath txt = do+  first (IVEParse filePath) $ parseExpandValueFromFile filePath txt++-- | Purely read a typed Michelson value from textual representation.+--+-- Expected type is provided explicitly.+readSomeValue+  :: U.Ty+  -> FilePath+  -> Text+  -> Either ImportValueError SomeValue+readSomeValue ty filePath txt = do+  valueU <- readUntypedValue filePath txt+  first (IVETypeCheck filePath) $+    typeCheckingWith def $ typeCheckTopLevelType Nothing ty valueU++-- | Purely read a typed Michelson value from textual representation.+readValue+  :: forall t. SingI t+  => FilePath+  -> Text+  -> Either ImportValueError (Value t)+readValue filePath txt = do+  valueU <- readUntypedValue filePath txt+  first (IVETypeCheck filePath) $+    typeCheckingWith def $ typeVerifyTopLevelType Nothing valueU++-- | Import an untyped value from a given file path.+importUntypedValue :: FilePath -> IO U.Value+importUntypedValue = importUsing readUntypedValue++-- | Import a typed value from a given file path.+--+-- Expected type is provided explicitly.+importSomeValue :: U.Ty -> FilePath -> IO SomeValue+importSomeValue = importUsing . readSomeValue++-- | Import a typed value from a given file path.+importValue+  :: forall t . SingI t+  => FilePath -> IO (Value t)+importValue = importUsing readValue++-- | Error type for 'importValue' function.+data ImportValueError+  = IVEParse FilePath ParserException+  | IVETypeCheck FilePath TCError+  deriving stock (Show, Eq)++instance Buildable ImportValueError where+  build =+    \case+      IVEParse filePath e -> unlinesF+        [ "Error at " <> build filePath+        , "Failed to parse the value: " +| e |+ ""+        ]+      IVETypeCheck filePath e -> unlinesF+        [ "Error at " <> build filePath+        , "The value is ill-typed: " +| e |+ ""+        ]++instance Exception ImportValueError where+  displayException = pretty

@@ -19,7 +19,7 @@ module Michelson.Text   ( MText (..)   , mkMText-  , mkMTextUnsafe+  , unsafeMkMText   , mkMTextCut   , writeMText   , takeMText@@ -61,16 +61,16 @@ -- * With QuasyQuotes when need to create a string literal. -- -- >>> [mt|Some text|]--- MTextUnsafe {unMText = "Some text"}+-- UnsafeMText {unMText = "Some text"} -- -- * With 'mkMText' when constructing from a runtime text value. ----- * With 'mkMTextUnsafe' or 'MTextUnsafe' when absolutelly sure that+-- * With 'unsafeMkMText' or 'UnsafeMText' when absolutelly sure that -- given string does not violate invariants. -- -- * With 'mkMTextCut' when not sure about text contents and want -- to make it compliant with Michelson constraints.-newtype MText = MTextUnsafe { unMText :: Text }+newtype MText = UnsafeMText { unMText :: Text }   deriving stock (Show, Eq, Ord, Data, Generic)   deriving newtype (Semigroup, Monoid, Container, Buildable, Hashable) @@ -93,7 +93,7 @@ -- You can use e.g. @'\n'@ character directly in supplied argument, -- but attempt to use other bad characters like @'\r'@ will cause failure. mkMText :: Text -> Either Text MText-mkMText txt = mapM checkMChar (toString txt) $> MTextUnsafe txt+mkMText txt = mapM checkMChar (toString txt) $> UnsafeMText txt   where     checkMChar c       | isMChar c || c == '\n' = pass@@ -101,30 +101,30 @@  -- | Contruct 'MText' from a Haskell text, failing if provided Haskell text -- is invalid Michelson string.-mkMTextUnsafe :: HasCallStack => Text -> MText-mkMTextUnsafe = either error id . mkMText+unsafeMkMText :: HasCallStack => Text -> MText+unsafeMkMText = either error id . mkMText  -- | Construct 'MText' from a Haskell text, eliminating all characters which -- should not appear in Michelson strings. -- Characters which can be displayed normally via escaping are preserved. mkMTextCut :: Text -> MText mkMTextCut txt =-  MTextUnsafe . toText . filter isAllowed $ toString txt+  UnsafeMText . toText . filter isAllowed $ toString txt   where     isAllowed c = isMChar c || c == '\n'  -- | Print 'MText' for Michelson code, with all unusual characters escaped. writeMText :: MText -> Text-writeMText (MTextUnsafe t) = t+writeMText (UnsafeMText t) = t   & T.replace "\\" "\\\\"   & T.replace "\n" "\\n"   & T.replace "\"" "\\\""  takeMText :: Int -> MText -> MText-takeMText n (MTextUnsafe txt) = MTextUnsafe $ T.take n txt+takeMText n (UnsafeMText txt) = UnsafeMText $ T.take n txt  dropMText :: Int -> MText -> MText-dropMText n (MTextUnsafe txt) = MTextUnsafe $ T.drop n txt+dropMText n (UnsafeMText txt) = UnsafeMText $ T.drop n txt  instance ToText MText where   toText = unMText@@ -159,11 +159,11 @@   { TH.quoteExp = \s ->       case qqMText s of         Left err -> fail $ toString err-        Right txt -> [e| MTextUnsafe (toText @String txt) |]+        Right txt -> [e| UnsafeMText (toText @String txt) |]   , TH.quotePat = \s ->       case qqMText s of         Left err -> fail $ toString err-        Right txt -> [p| MTextUnsafe $(TH.litP $ TH.StringL txt) |]+        Right txt -> [p| UnsafeMText $(TH.litP $ TH.StringL txt) |]   , TH.quoteType = \_ ->       fail "Cannot use this QuasiQuoter at type position"   , TH.quoteDec = \_ ->@@ -198,19 +198,19 @@ -- We assume that no unicode characters are used in plain Haskell code, -- so unless special tricky manipulations are used this should be safe. symbolToMText :: forall name. KnownSymbol name => MText-symbolToMText = mkMTextUnsafe $ symbolValT' @name+symbolToMText = unsafeMkMText $ symbolValT' @name  -- | Create a 'MText' from label. -- -- We assume that no unicode characters are used in plain Haskell code, -- so unless special tricky manipulations are used this should be safe. labelToMText :: Label name -> MText-labelToMText = mkMTextUnsafe . labelToText+labelToMText = unsafeMkMText . labelToText  -- | Leads first character of text to upper case. -- -- For empty text this will throw an error. mtextHeadToUpper :: HasCallStack => MText -> MText-mtextHeadToUpper (MTextUnsafe txt) = case T.uncons txt of+mtextHeadToUpper (UnsafeMText txt) = case T.uncons txt of   Nothing -> error "Empty text"-  Just (c, cs) -> MTextUnsafe $ T.cons (C.toUpper c) cs+  Just (c, cs) -> UnsafeMText $ T.cons (C.toUpper c) cs

@@ -11,9 +11,12 @@   , typeCheckListNoExcept   , typeCheckParameter   , typeCheckStorage+  , typeCheckTopLevelType   , typeCheckValue+  , typeVerifyContract   , typeVerifyParameter   , typeVerifyStorage+  , typeVerifyTopLevelType   , module E   , module M   , module T

@@ -6,6 +6,7 @@  module Michelson.TypeCheck.Error   ( TypeContext (..)+  , TopLevelType (..)   , TCTypeError (..)   , TCError (..)   , ExtError (..)@@ -14,17 +15,19 @@   , pairWithElems   ) where -import Fmt (Buildable(..), listF, pretty, unlinesF, (+|), (+||), (|+), (||+))+import Fmt (Buildable(..), pretty, (+|), (|+), (||+))+import Named ((:!), arg)+import Prelude hiding ((<$>), empty)+import Text.PrettyPrint.Leijen.Text hiding (pretty, bool) import qualified Text.Show (show) -import Michelson.ErrorPos (InstrCallStack(..), Pos(..), SrcPos(..))-import Michelson.Printer.Util (doesntNeedParens, printDocB, renderDoc)+import Michelson.ErrorPos (InstrCallStack(..))+import Michelson.Printer.Util (RenderDoc (..), renderAnyBuildable,+  buildRenderDoc, buildRenderDocExtended, doesntNeedParens, renderDoc, renderDocList) import Michelson.TypeCheck.TypeCheckedOp (TypeCheckedOp) import Michelson.TypeCheck.Types (SomeHST(..)) import qualified Michelson.Typed as T import Michelson.Typed.Annotation (AnnConvergeError(..))-import Michelson.Typed.Extract (toUType)-import Michelson.Typed.T (buildStack) import Michelson.Untyped (StackFn, Ty, Var) import qualified Michelson.Untyped as U import Tezos.Address (Address)@@ -43,6 +46,7 @@   | ArithmeticOperation   | Iteration   | Cast+  | UnpairArgument   | CarArgument   | CdrArgument   | If@@ -50,11 +54,12 @@   | ContainerKeyType   | ContainerValueType   | FailwithArgument+  | TicketsJoin   deriving stock (Show, Eq, Generic)   deriving anyclass (NFData) -instance Buildable TypeContext where-  build = \case+instance RenderDoc TypeContext where+  renderDoc _ = \case     LambdaArgument -> "argument to some lambda"     LambdaCode -> "code in LAMBDA"     DipCode -> "code in DIP"@@ -65,6 +70,7 @@     ArithmeticOperation -> "arguments to arithmetic operation"     Iteration -> "iteration (ITER / MAP / etc) code"     Cast -> "argument to CAST"+    UnpairArgument -> "argument to UNPAIR"     CarArgument -> "argument to CAR"     CdrArgument -> "argument to CDR"     If -> "conditional expression"@@ -72,7 +78,25 @@     ContainerKeyType -> "container key type"     ContainerValueType -> "container value type"     FailwithArgument -> "argument to FAILWITH"+    TicketsJoin -> "join of two tickets" +data TopLevelType+  = TltParameterType+  | TltStorageType+  deriving stock (Show, Eq, Generic)+  deriving anyclass (NFData)++instance Buildable TopLevelType where+  build = buildRenderDoc++instance RenderDoc TopLevelType where+  renderDoc _ = \case+    TltParameterType -> "parameter"+    TltStorageType -> "storage"++instance Buildable TypeContext where+  build = buildRenderDoc+ -- | Data type that represents various errors -- which are related to type system. -- These errors are used to specify info about type check errors@@ -96,6 +120,9 @@   -- ^ Error that happens when actual types are different from the type that instruction expects.   -- The param is an non-empty list of all expected stack types that the instruction would accept.   -- Each expected stack types is represented as non-empty list as well.+  | UnexpectedTopLevelType TopLevelType ("expected" :! T.T) ("got" :! T.T)+  -- ^ Error that happens when the caller expected one top-level type, but+  -- the contract has another type specified.   | InvalidInstruction U.ExpandedInstr Text   -- ^ Some instruction is invalid or used in an invalid way.   -- For example, @PAIR 0@ or @PAIR 1@, or a @SELF@ instruction was used in a @LAMBDA@.@@ -137,49 +164,59 @@   deriving anyclass (NFData)  instance Buildable TCTypeError where-  build = \case-    AnnError e -> build e+  build = buildRenderDocExtended++instance RenderDoc TCTypeError where+  renderDoc context = \case+    AnnError e -> renderAnyBuildable e     TypeEqError type1 type2 ->-      "Types not equal: " +| type1 |+ " /= " +| type2 |+ ""+      "Types not equal:" <+> (renderDoc context type1) <+> "/=" <+> (renderDoc context type2)     StackEqError st1 st2 ->-      "Stacks not equal: " +| buildStack st1 |+ " /= " +| buildStack st2 |+ ""+      "Stacks not equal:"<+> (renderDocList context st1) <+> "/=" <+> (renderDocList context st2)     UnsupportedTypeForScope typ reason ->-      "Type '" +| typ |+ "' is unsupported here because it "-      +| reason |+ ""+      "Type '" <> (renderDoc context typ) <> "' is unsupported here because it"+      <+> (renderDoc context reason)     NotNumericTypes t1 t2 ->-      "Some of the types in an arithmetic operation are not numeric: "-      +| t1 |+ " and " +| t2 |+ ""+      "Some of the types in an arithmetic operation are not numeric:"+      <+> (renderDoc context t1) <+> "and" <+> (renderDoc context t2)     UnexpectedType (t :| ts) ->-      "Wrong stack type for instruction, expect stack type to begin with " +|-        ( intercalate " or "-          $ fmap (\(x :| xs) -> "" +| listF (x:xs) |+ "")+      "Wrong stack type for instruction, expect stack type to begin with " <+>+        (cat $ punctuate "or"+          $ fmap (\(x :| xs) -> list $ fmap (renderAnyBuildable) (x:xs))           $ (t:ts)-        ) |+ ""-    InvalidInstruction instr reason -> unlinesF-      [ "Invalid instruction " +| instr |+ ""-      , "Reason: " <> reason-      ]+        )+    UnexpectedTopLevelType tyDesc (arg #expected -> expected) (arg #got -> got) ->+      "Unexpected" <+> renderDoc context tyDesc <+> "type:"+      <$$> renderLargeType got+      <$$> "Expected:"+      <$$> renderLargeType expected+    InvalidInstruction instr reason ->+      "Invalid instruction" <+> (renderDoc context instr)+      <$$> "Reason:" <+> textStrict reason     InvalidValueType t ->-      "Value type is never a valid `" +| t |+ "`"+      "Value type is never a valid" <+> enclose "`" "`" (renderDoc context t)     NotEnoughItemsOnStack ->       "Not enough items on stack"     UnknownContract addr ->-      "Contract is not registered: " +| addr |+ ""-    IllegalEntrypoint err -> build err+      "Contract is not registered:" <+> (renderAnyBuildable addr)+    IllegalEntrypoint err -> renderDoc context err     EntrypointNotFound ep ->-      "No such entrypoint '" +| ep |+ "'"-    IllegalParamDecl err -> build err+      "No such entrypoint" <+> enclose "`" "`" (renderAnyBuildable ep)+    IllegalParamDecl err -> renderDoc context err     NegativeNat -> "Natural number cannot be negative"     MutezOverflow -> "Exceeds maximal value for mutez"-    InvalidAddress e -> build e-    InvalidKeyHash e -> build e-    InvalidBls12381Object e -> build e+    InvalidAddress e -> renderDoc context e+    InvalidKeyHash e -> renderDoc context e+    InvalidBls12381Object e -> renderDoc context e     InvalidTimestamp -> "Is not a valid RFC3339 timestamp"     CodeAlwaysFails ->       "Cannot use a terminate instruction (like FAILWITH) as part of another \       \instruction's body"     EmptyCode -> "Code block is empty"     AnyError -> "Some of the arguments have invalid types"+    where+      renderLargeType :: T.T -> Doc+      renderLargeType = indent 2 . renderDoc doesntNeedParens . T.toUType  -- | Type check error data TCError@@ -194,42 +231,50 @@ instance NFData TCError  instance Buildable TCError where-  build = \case-    TCFailedOnInstr instr (SomeHST t) ics mbTCTypeContext mbTCTypeError ->-      "Error checking expression "-      +| instr |+ " against input stack type "-      +| t |+ maybe "" (\c -> ". Error in " +| c |+ "") mbTCTypeContext-      +| maybe ". " (\e -> ": " +| e |+ ". ") mbTCTypeError-      +| buildCallStack ics+  build = buildRenderDocExtended++instance RenderDoc TCError where+  renderDoc context = \case+    TCFailedOnInstr instr (SomeHST t) ics mbTCTypeContext mbTCTypeError -> line+      <> "Error checking expression:"+      <> surroundWithNewLines (renderDoc context instr)+      <> "against input stack type:"+      <> surroundWithNewLines (renderDoc context t)+      <> maybe "" (\c -> "Error in" <+> renderDoc context c) mbTCTypeContext+      <> maybe "" (\e -> ":" <+> (renderDoc context e) <> "." <$$> line) mbTCTypeError+      <> (renderDoc context ics)     TCFailedOnValue v t custom ics mbTCTypeError ->-      "Error checking value "-      +| v |+ " against type "-      +| toUType t |+ bool (": " +| custom |+ " ") "." (null custom)-      +| (maybe "" (\e -> "\n" +| e |+ ".\n") mbTCTypeError)-      +| buildCallStack ics+      "Error checking value"+      <$$> (renderDoc context v) <+> "against type"+      <+> (renderDoc context t) <> (bool (":" <+> (renderAnyBuildable custom)) "." (null custom))+      <+> (maybe "" (\e -> line <> (renderDoc context e) <> line) mbTCTypeError)+      <+> (renderDoc context ics)     TCContractError msg typeError ->-      "Error occurred during contract typecheck: "-      +|| msg ||+ (maybe "" (\e -> " " +| e |+ "") typeError)+      "Error occurred during contract typecheck:"+      <$$> (renderAnyBuildable msg) <> (maybe "" (\e -> " " <> (renderDoc context e)) typeError)     TCUnreachableCode ics instrs ->-      "Unreachable code: " +| buildTruncated 3 (toList instrs) |+ ". "-      +| buildCallStack ics+      "Unreachable code:" <$$> buildTruncated 3 (toList instrs) <> "."+      <+> (renderDoc context ics)     TCExtError (SomeHST t) ics e ->-      "Error occurred during Morley extension typecheck: "-      +| e |+ " on stack " +| t |+ ". "-      +| buildCallStack ics+      "Error occurred during Morley extension typecheck:" <>+      (renderAnyBuildable e) <+> "on stack" <+> (renderDoc context t) <> "."+      <+> (renderDoc context ics)     TCIncompletelyTyped err contract ->-      "\n"-      +| printDocB False (renderDoc doesntNeedParens contract) |+ "\n"-      +| build err+      line+      <> renderDoc doesntNeedParens contract+      <$> renderDoc context err     where     buildTruncated k l-      | null (drop k l) = build l-      | otherwise = build (take k l) <> " ..."-    buildCallStack InstrCallStack{icsCallStack, icsSrcPos = SrcPos (Pos line) (Pos col)} =-      "Error occurred on line " +| line + 1 |+ " char " +| col + 1 |+ ""-      +| case icsCallStack of-           [] -> "."-           _ -> " inside these let defenitions: " +| listF icsCallStack |+ "."+      | null (drop k l) = renderDocList context l+      | otherwise = (renderDocList context (take k l)) <> " ..."++    -- | Helper to format a line using empty lines at the end and at the beginning,+    -- and 4-space indents for the line itself+    surroundWithNewLines :: Doc -> Doc+    surroundWithNewLines l =+      line+      <$$> indent 4 l+      <$$> line  instance Show TCError where   show = pretty

@@ -11,6 +11,7 @@ import Control.Monad.Except (MonadError, liftEither, throwError) import Data.Constraint (Dict(..)) import Data.Map.Lazy (insert, lookup)+import Data.Singletons (SingI) import Data.Typeable ((:~:)(..))  import Michelson.ErrorPos@@ -25,7 +26,7 @@   (ExpandedOp, StackFn, TyVar(..), Ty, Var, VarAnn, sfnInPattern, sfnOutPattern,   sfnQuantifiedVars, varSet) import qualified Michelson.Untyped as U-import Util.Peano (SingNat(SS, SZ))+import Util.PeanoNatural (PeanoNatural(..))  -- | Perform some, possibly throwing, action presumably making use of a supplied -- external instruction. In case of an error, return @IllTypedSeq@ wrapping the@@ -40,7 +41,7 @@   (pure . WellTypedSeq)  typeCheckExt-  :: forall s. Typeable s+  :: forall s. SingI s   => TcInstrHandler   -> U.ExpandedExtInstr   -> HST s@@ -49,8 +50,8 @@   instrPos <- ask   case ext of     U.STACKTYPE s -> workOnInstr ext $-      liftExtError hst $ nopSomeInstr <$ checkStackType noBoundVars s hst-    U.FN t sf op  -> checkFn tcInstr t sf op hst+      liftExtError hst $ stackTypeSomeInstr s <$ checkStackType noBoundVars s hst+    U.FN t sf op  -> checkFn tcInstr t sf op hst instrPos     U.UPRINT pc   -> workOnInstr ext $       verifyPrint pc <&> \tpc -> toSomeInstr (T.PRINT tpc)     U.UTEST_ASSERT U.TestAssert{..} -> do@@ -81,9 +82,9 @@       T.PrintComment <$> traverse checkStRef pc      toSomeInstr ext' = hst :/ T.Ext ext' ::: hst-    nopSomeInstr = hst :/ T.Nop ::: hst+    stackTypeSomeInstr s = hst :/ T.Ext (T.STACKTYPE s) ::: hst -liftExtError :: Typeable s => HST s -> Either ExtError a -> TypeCheckInstr a+liftExtError :: SingI s => HST s -> Either ExtError a -> TypeCheckInstr a liftExtError hst ei = do   instrPos <- ask   liftEither $ first (TCExtError (SomeHST hst) instrPos) ei@@ -98,18 +99,19 @@ -- | Executes function body, pushing @ExtFrame@ onto the state and checks -- the pattern in @FN@. checkFn-  :: Typeable inp+  :: SingI inp   => TcInstrHandler   -> Text   -> StackFn   -> [ExpandedOp]   -> HST inp+  -> InstrCallStack   -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)-checkFn tcInstr t sf body inp = do+checkFn tcInstr t sf body inp loc = do   guarding (con body) (checkStart inp) $ \vars ->     preserving (typeCheckImplStripped tcInstr body inp) con $ \someI@(_ :/ instrAndOut) ->       case instrAndOut of-        _ ::: out -> checkEnd vars out $> someI+        _ ::: out -> checkEnd vars out $> mapSomeInstr (T.WithLoc loc . T.Fn t sf) someI         AnyOutInstr{} -> pure someI   where     checkStart hst = do@@ -118,7 +120,7 @@       tcExtFramesL %= (vars :)       return vars -    checkEnd :: Typeable out => BoundVars -> HST out -> TypeCheckInstr ()+    checkEnd :: SingI out => BoundVars -> HST out -> TypeCheckInstr ()     checkEnd vars out = liftExtError out $       void $ checkStackType vars (sfnOutPattern sf) out @@ -127,14 +129,14 @@  -- | Check that a @StackTypePattern@ matches the type of the current stack checkStackType-  :: Typeable xs+  :: SingI xs   => BoundVars   -> U.StackTypePattern   -> HST xs   -> Either ExtError BoundVars checkStackType (BoundVars vars boundStkRest) s hst = go vars 0 s hst   where-    go :: Typeable xs => Map Var Ty -> Int -> U.StackTypePattern -> HST xs+    go :: SingI xs => Map Var Ty -> Int -> U.StackTypePattern -> HST xs        -> Either ExtError BoundVars     go m _ U.StkRest sr = case boundStkRest of       Nothing -> pure $ BoundVars m (Just $ SomeHST sr)@@ -165,7 +167,7 @@ -- -- Fails when index is too large for the given stack. createStackRef-  :: (MonadError TCError m, MonadReader InstrCallStack m, Typeable s)+  :: (MonadError TCError m, MonadReader InstrCallStack m, SingI s)   => Natural -> HST s -> m (T.StackRef s) createStackRef idx hst =   case doCreate (hst, idx) of@@ -179,7 +181,7 @@     doCreate :: forall s. (HST s, Natural) -> Maybe (T.StackRef s)     doCreate = \case       (SNil, _) -> Nothing-      ((_ ::& _), 0) -> Just (T.StackRef SZ)+      ((_ ::& _), 0) -> Just (T.StackRef Zero)       ((_ ::& st), i) -> do         T.StackRef ns <- doCreate (st, i - 1)-        return $ T.StackRef (SS ns)+        return $ T.StackRef (Succ ns)

@@ -51,8 +51,8 @@ import Data.Constraint (Dict(..), withDict) import Data.Default (def) import Data.Singletons (Sing, SingI(sing), demote)+import Data.Singletons.Decide import qualified Data.Text as T-import Data.Typeable (eqT, (:~:)(..)) import Data.Vinyl (Rec(..)) import Fmt ((+||), (||+)) @@ -63,15 +63,16 @@ import Michelson.TypeCheck.Types import Michelson.Typed   (BadTypeForScope(..), CommentType(StackTypeComment), Comparable, ExtInstr(COMMENT_ITEM),-  Instr(..), KnownT, Notes(..), SingT(..), T(..), WellTyped, converge, getComparableProofS, notesT,-  starNotes)+  Instr(..), Notes(..), SingT(..), T(..), WellTyped, converge, getComparableProofS, notesT,+  requireEq, starNotes) import Michelson.Typed.Annotation (AnnConvergeError, isStar) import Michelson.Typed.Arith (Add, ArithOp(..), Mul, Sub, UnaryArithOp(..)) import Michelson.Typed.Polymorphic   (ConcatOp, EDivOp(..), GetOp(..), MemOp(..), SizeOp, SliceOp, UpdOp(..))- import qualified Michelson.Untyped as Un-import Michelson.Untyped.Annotation (Annotation(..), FieldAnn, VarAnn, orAnn, annQ, mkAnnotationUnsafe, noAnn)+import Michelson.Untyped.Annotation+  (Annotation(..), FieldAnn, VarAnn, annQ, noAnn, orAnn, unsafeMkAnnotation)+import Util.Sing (eqI) import Util.Type (onFirst)  -- | Function which derives special annotations@@ -100,7 +101,7 @@     splitLastDot v = case unsnoc $ T.splitOn "." $ unAnnotation v of       Nothing      -> def       Just (_, "") -> (def, Un.convAnn v)-      Just (vs, l) -> (foldMap mkAnnotationUnsafe vs, bool (mkAnnotationUnsafe l) def (l == "car" || l == "cdr"))+      Just (vs, l) -> (foldMap unsafeMkAnnotation vs, bool (unsafeMkAnnotation l) def (l == "car" || l == "cdr"))      commonPrefix :: VarAnn -> VarAnn -> VarAnn     commonPrefix = curry \case@@ -114,6 +115,9 @@ deriveSpecialVN :: VarAnn -> FieldAnn -> VarAnn -> VarAnn -> VarAnn deriveSpecialVN vn elFn pairVN elVn   | (unAnnotation vn) == "%" = Un.convAnn elFn+  -- TODO [#534]:+  -- In the `%%` branch, if the pair's field annotation (`elFn`) is empty, we should default it to "cdr"/"car".+  -- See: <https://tezos.gitlab.io/008/michelson.html#automatic-variable-and-field-annotations-inferring>   | (unAnnotation vn) == "%%" = pairVN <> Un.convAnn elFn   | otherwise = vn `orAnn` elVn @@ -163,11 +167,10 @@  -- | Check whether the given stack types are equal. eqHST-  :: forall as bs.-      (Typeable as, Typeable bs)+  :: forall as bs. (SingI as, SingI bs)   => HST as -> HST bs -> Either TCTypeError (as :~: bs) eqHST (hst :: HST xs) (hst' :: HST ys) = do-  case eqT @as @bs of+  case eqI @as @bs of     Nothing -> Left $ StackEqError (hstToTs hst) (hstToTs hst')     Just Refl -> do       void $ convergeHST hst hst' `onFirst` AnnError@@ -176,12 +179,11 @@ -- | Check whether the given stack has size 1 and its only element matches the -- given type. This function is a specialized version of `eqHST`. eqHST1-  :: forall t st.-      (Typeable st, WellTyped t)+  :: forall t st. (SingI st, WellTyped t)   => HST st -> Either TCTypeError (st :~: '[t]) eqHST1 hst = do   let hst' = sing @t -:& SNil-  case eqT @'[t] @st of+  case eqI @'[t] @st of     Nothing -> Left $ StackEqError (hstToTs hst') (hstToTs hst)     Just Refl -> Right Refl @@ -203,13 +205,13 @@     else Left $ "Entries are unordered (" +|| e1 ||+ " >= " +|| e2 ||+ ")"   l -> Right l --- | Function @eqType@ is a simple wrapper around @Data.Typeable.eqT@ suited+-- | Function @eqType@ is a simple wrapper around @Data.Singletons.decideEquality@ suited -- for use within @Either TCTypeError a@ applicative. eqType-  :: forall (a :: T) (b :: T).-      (Each '[KnownT] [a, b])+  :: forall (a :: T) (b :: T). (Each '[SingI] [a, b])   => Either TCTypeError (a :~: b)-eqType = maybe (Left $ TypeEqError (demote @a) (demote @b)) pure eqT+eqType =+  requireEq @a @b $ Left ... TypeEqError  onTypeCheckInstrErr   :: (MonadReader InstrCallStack m, MonadError TCError m)@@ -247,14 +249,14 @@   throwError $ TCFailedOnInstr instr hst pos mContext (Just err)  onTypeCheckInstrAnnErr-  :: (MonadReader InstrCallStack m, MonadError TCError m, Typeable ts)+  :: (MonadReader InstrCallStack m, MonadError TCError m, SingI ts)   => Un.ExpandedInstr -> HST ts -> Maybe TypeContext   -> Either AnnConvergeError a -> m a onTypeCheckInstrAnnErr instr i mContext ei =   onTypeCheckInstrErr instr (SomeHST i) mContext (ei `onFirst` AnnError)  withCompareableCheck-  :: forall a m v ts. (Typeable ts, MonadReader InstrCallStack m, MonadError TCError m)+  :: forall a m v ts. (SingI ts, MonadReader InstrCallStack m, MonadError TCError m)   => Sing a   -> Un.ExpandedInstr   -> HST ts@@ -265,7 +267,7 @@   Nothing -> typeCheckInstrErr instr (SomeHST i) $ Just ComparisonArguments  typeCheckOpImpl-  :: forall inp. Typeable inp+  :: forall inp. SingI inp   => TcInstrHandler   -> Un.ExpandedOp   -> HST inp@@ -293,11 +295,11 @@                   <&> mapSeq (addNotes . mapSomeInstr Nested)      addNotes :: SomeInstr inp -> SomeInstr inp-    addNotes (inp :/ i ::: out) = inp :/ wrapWithNotes inp out i ::: out+    addNotes (inp :/ i ::: out) = inp :/ wrapWithNotes out i ::: out     addNotes i = i -    wrapWithNotes :: HST c -> HST d -> Instr c d -> Instr c d-    wrapWithNotes inputStack outputStack instr = case instr of+    wrapWithNotes :: HST d -> Instr c d -> Instr c d+    wrapWithNotes outputStack instr = case instr of       -- Abstractions for instructions:       Nop -> instr'       Seq _ _ -> instr'@@ -306,6 +308,7 @@       Ext _ -> instr'       FrameInstr _ _ -> instr'       WithLoc _ _ -> instr'+      Fn {} -> instr'       -- These three shouldn't happen, since annotations are added here.       InstrWithNotes {} -> instr'       InstrWithVarAnns _ _ -> instr'@@ -329,6 +332,24 @@       FAILWITH -> instr'       NEVER -> instr' +      -- These instructions technically may have one/two explicit var anns, BUT because they support special var anns,+      -- the var anns are stored directly inside the instruction's constructor.+      -- For this reason, they must NOT be wrapped in `InstrWithVarNotes`.+      AnnCAR _ _ -> instr'+      AnnCDR _ _ -> instr'+      AnnUNPAIR{} ->+        case outputStack of+          (notes1, _, varAnn1) ::& (notes2, _, varAnn2) ::& _ ->+            let withNotes+                  | isStar notes1 && isStar notes2 = id+                  | isStar notes2 = InstrWithNotes Proxy (notes1 :& RNil)+                  | otherwise = InstrWithNotes Proxy (notes1 :& notes2 :& RNil)+                withVarAnns+                  | varAnn1 == def && varAnn2 == def = id+                  | varAnn2 == def = InstrWithVarAnns $ Un.OneVarAnn varAnn1+                  | otherwise = InstrWithVarAnns (Un.TwoVarAnns varAnn1 varAnn2)+            in withNotes $ withVarAnns instr+       -- We purposefully don't wrap `UNPAIRN` in meta-instructions       -- like `InstrWithNotes` and `InstrWithVarAnns`.       -- See !769 for a lengthy explanation.@@ -354,20 +375,6 @@               withVarNotes' = if valVarAnn == Un.noAnn && mapVarAnn == Un.noAnn then id else InstrWithVarAnns $ Un.TwoVarAnns valVarAnn mapVarAnn           in  withNotes . withVarNotes . withVarNotes' $ instr -      -- Instructions that produce at most one note:-      -- The cases for Ann{CAR,CDR} basically try to answer the question:-      -- were the var annotations explicitly written or do they come from-      -- unnesting nested annotations?-      AnnCAR _ -> case (inputStack, outputStack) of-        ((NTPair _ _ _ vn1 _vn2 _ _, _, _) ::& _, (_, _, vn) ::& _)-          | vn  /= def && vn /= vn1 -> instr''-          | vn1 == def -> instr''-          | otherwise -> instr'-      AnnCDR _ -> case (inputStack, outputStack) of-        ((NTPair _ _ _ _vn1 vn2 _ _, _, _) ::& _, (_, _, vn) ::& _)-          | vn  /= def && vn /= vn2 -> instr''-          | vn2 == def -> instr''-          | otherwise -> instr'       DUP -> instr''       DUPN _ -> instr''       PUSH _ -> instr''@@ -445,6 +452,10 @@       SHA3 -> instr''       KECCAK -> instr''       PAIRING_CHECK -> instr''+      TICKET -> instr''+      READ_TICKET -> instr''+      SPLIT_TICKET -> instr''+      JOIN_TICKETS -> instr''       where         instr' = addNotesNoVarAnn outputStack instr         instr'' = addNotesOneVarAnn outputStack instr@@ -469,7 +480,7 @@ -- | Like 'typeCheckImpl' but doesn't add a stack type comment after the -- sequence. typeCheckImplNoLastTypeComment-  :: forall inp . Typeable inp+  :: forall inp . SingI inp   => TcInstrHandler   -> [Un.ExpandedOp]   -> HST inp@@ -522,7 +533,7 @@ -- | 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+  :: forall inp . SingI inp   => TcInstrHandler   -> [Un.ExpandedOp]   -> HST inp@@ -534,7 +545,7 @@   continueTypeChecking tcInstr done ops  typeCheckImpl-  :: forall inp . Typeable inp+  :: forall inp . SingI inp   => TcInstrHandler   -> [Un.ExpandedOp]   -> HST inp@@ -605,7 +616,7 @@ -- | Check whether given types are structurally equal and annotations converge. matchTypes   :: forall t1 t2.-      (Each '[KnownT] [t1, t2])+      (Each '[SingI] [t1, t2])   => Notes t1 -> Notes t2 -> Either TCTypeError (t1 :~: t2, Notes t1) matchTypes n1 n2 = do   Refl <- eqType @t1 @t2@@ -620,8 +631,9 @@ memImpl   :: forall c memKey rs inp m .     ( MemOp c-    , KnownT (MemOpKey c)+    , SingI (MemOpKey c)     , inp ~ (memKey : c : rs)+    , SingI rs     , MonadReader InstrCallStack m     , MonadError TCError m     )@@ -630,7 +642,7 @@   -> VarAnn   -> m (SomeInstr inp) memImpl cKeyNotes inputHST@(hst0 ::& _ ::& hstTail) varAnn =-  case eqType @memKey  @(MemOpKey c) of+  case eqType @memKey @(MemOpKey c) of     Right Refl -> do       _ <- onTypeCheckInstrAnnErr uInstr inputHST         (Just ContainerKeyType) (converge memKeyNotes cKeyNotes)@@ -644,9 +656,10 @@  getImpl   :: forall c getKey rs inp m .-    ( GetOp c, KnownT (GetOpKey c)+    ( GetOp c, SingI (GetOpKey c)     , WellTyped (GetOpVal c)     , inp ~ (getKey : c : rs)+    , SingI rs     , MonadReader InstrCallStack m     , MonadError TCError m     )@@ -671,7 +684,8 @@ updImpl   :: forall c updKey updParams rs inp m .     ( UpdOp c-    , KnownT (UpdOpKey c), KnownT (UpdOpParams c)+    , SingI (UpdOpKey c), SingI (UpdOpParams c)+    , SingI rs     , inp ~ (updKey : updParams : c : rs)     , MonadReader InstrCallStack m     , MonadError TCError m@@ -703,9 +717,10 @@ getUpdImpl   :: forall c updKey updParams rs inp m .     ( UpdOp c, GetOp c-    , KnownT (UpdOpKey c)-    , KnownT (GetOpVal c)+    , SingI (UpdOpKey c)+    , SingI (GetOpVal c)     , inp ~ (updKey : updParams : c : rs)+    , SingI rs     , GetOpKey c ~ UpdOpKey c     , UpdOpParams c ~ 'TOption (GetOpVal c)     , MonadReader InstrCallStack m@@ -744,7 +759,7 @@   pure $ i :/ SIZE ::: ((starNotes, Dict, vn) ::& rs)  sliceImpl-  :: (SliceOp c, Typeable c, inp ~ ('TNat ': 'TNat ': c ': rs), Monad m)+  :: (SliceOp c, inp ~ ('TNat ': 'TNat ': c ': rs), Monad m)   => HST inp   -> Un.VarAnn   -> m (SomeInstr inp)@@ -779,7 +794,6 @@ arithImpl   :: forall aop inp m n s t.      ( ArithOp aop n m-     , Typeable (ArithRes aop n m ': s)      , WellTyped (ArithRes aop n m)      , inp ~ (n ': m ': s)      , MonadReader InstrCallStack t@@ -799,9 +813,9 @@  addImpl   :: forall a b inp rs m.-     ( Typeable rs-     , Each '[KnownT] [a, b]+     ( Each '[SingI] [a, b]      , inp ~ (a ': b ': rs)+     , SingI rs      , MonadReader InstrCallStack m      , MonadError TCError m      )@@ -826,8 +840,8 @@  edivImpl   :: forall a b inp rs m.-     ( Typeable rs-     , Each '[KnownT] [a, b]+     ( SingI rs+     , Each '[SingI] [a, b]      , inp ~ (a ': b ': rs)      , MonadReader InstrCallStack m      , MonadError TCError m@@ -868,9 +882,9 @@  subImpl   :: forall a b inp rs m.-     ( Typeable rs-     , Each '[KnownT] [a, b]+     ( Each '[SingI] [a, b]      , inp ~ (a ': b ': rs)+     , SingI rs      , MonadReader InstrCallStack m      , MonadError TCError m      )@@ -892,9 +906,9 @@  mulImpl   :: forall a b inp rs m.-     ( Typeable rs-     , Each '[KnownT] [a, b]+     ( Each '[SingI] [a, b]      , inp ~ (a ': b ': rs)+     , SingI rs      , MonadReader InstrCallStack m      , MonadError TCError m      )@@ -923,8 +937,7 @@ -- | Helper function to construct instructions for unary arithmetic -- operations. unaryArithImpl-  :: ( Typeable (UnaryArithRes aop n ': s)-     , WellTyped (UnaryArithRes aop n)+  :: ( WellTyped (UnaryArithRes aop n)      , inp ~ (n ': s)      , Monad t      )@@ -938,8 +951,7 @@ -- | Helper function to construct instructions for unary arithmetic -- operations that should preserve annotations. unaryArithImplAnnotated-  :: ( Typeable (UnaryArithRes aop n ': s)-     , WellTyped (UnaryArithRes aop n)+  :: ( WellTyped (UnaryArithRes aop n)      , inp ~ (n ': s)      , Monad t      , n ~ UnaryArithRes aop n

@@ -36,9 +36,12 @@     , typeCheckListNoExcept     , typeCheckParameter     , typeCheckStorage+    , typeCheckTopLevelType     , typeCheckValue+    , typeVerifyContract     , typeVerifyParameter     , typeVerifyStorage+    , typeVerifyTopLevelType     ) where  import Prelude hiding (EQ, GT, LT)@@ -46,8 +49,10 @@ import Control.Monad.Except (MonadError, catchError, liftEither, throwError) import Data.Default (def) import Data.Generics (everything, mkQ)-import Data.Singletons (Sing, demote)+import Data.Singletons (Sing, demote, withSingI, withSomeSing) import Data.Typeable ((:~:)(..))+import Fmt (pretty)+import Named ((!))  import Michelson.ErrorPos import Michelson.TypeCheck.Error@@ -63,38 +68,59 @@  import Michelson.Typed hiding (Branch(..)) import Util.Peano+import Util.PeanoNatural+import Util.Sing (SingI1(..)) import Util.Type (onFirst, type (++))  import qualified Michelson.Untyped as U-import Michelson.Untyped.Annotation (FieldTag, VarAnn, VarTag, convAnn, orAnn, annQ)+import Michelson.Untyped.Annotation (FieldTag, VarAnn, VarTag, annQ, convAnn, orAnn)  -- | Type check a contract and verify that the given storage -- is of the type expected by the contract.-typeCheckContractAndStorage :: U.Contract -> U.Value -> Either TCError SomeContractAndStorage+typeCheckContractAndStorage+  :: U.Contract -> U.Value -> TypeCheckResult SomeContractAndStorage typeCheckContractAndStorage uContract uStorage = do-  SomeContract (contract@Contract{} :: Contract cp st) <- typeCheckContract uContract def+  SomeContract (contract@Contract{} :: Contract cp st) <- typeCheckContract uContract   storage <- typeVerifyStorage @st uStorage-  Right $ SomeContractAndStorage contract storage+  pure $ SomeContractAndStorage contract storage  typeCheckContract   :: U.Contract-  -> TypeCheckOptions-  -> Either TCError SomeContract-typeCheckContract c options = do-  paramType <- mkSomeParamType (U.contractParameter c)-  runTypeCheck (TypeCheckContract paramType) options $ typeCheckContractImpl c+  -> TypeCheckResult SomeContract+typeCheckContract c = do+  paramType <- liftEither $ mkSomeParamType (U.contractParameter c)+  runTypeCheck (TypeCheckContract paramType) $ typeCheckContractImpl c +typeVerifyContract+  :: forall cp st.+     (SingI cp, SingI st)+  => U.Contract -> TypeCheckResult (Contract cp st)+typeVerifyContract uContract = do+  SomeContract tContract@(Contract{} :: Contract cp' st') <-+    typeCheckContract uContract+  Refl <- requireEq @cp' @cp (mkErr TltParameterType)+  Refl <- requireEq @st' @st (mkErr TltParameterType)+  return tContract+  where+    mkErr :: TopLevelType -> T -> T -> TypeCheckResult any+    mkErr tyDesc got expected =+      throwError $ TCContractError "error in contract type" $ Just $+          UnexpectedTopLevelType tyDesc+            ! #expected expected+            ! #got got+ withWTP :: forall t a. SingI t => (WellTyped t => TypeCheck a) -> TypeCheck a withWTP fn = case getWTP @t of   Right Dict -> fn-  Left (NotWellTyped t) -> throwError $ TCContractError ("Not a well typed value: " <> show t) Nothing+  Left (NotWellTyped t cause) -> throwError $ TCContractError+    ("Not a well typed value: '" <> show t <> "' because it " <> pretty cause) Nothing  withWTPInstr_ :: forall t a. SingI t => U.ExpandedInstr -> SomeHST -> (WellTyped t => TypeCheckInstr a) -> TypeCheckInstr a withWTPInstr_ v t fn = case getWTP @t of   Right Dict -> fn-  Left (NotWellTyped badType) -> do+  Left (NotWellTyped badType cause) -> do     loc <- ask-    throwError $ TCFailedOnInstr v t loc Nothing (Just $ UnsupportedTypeForScope badType BtNotComparable)+    throwError $ TCFailedOnInstr v t loc Nothing (Just $ UnsupportedTypeForScope badType cause)  withWTPInstr'_   :: forall t inp. SingI t@@ -104,10 +130,10 @@   -> TypeCheckInstrNoExcept (TypeCheckedSeq inp) withWTPInstr'_ v t fn = case getWTP @t of   Right Dict -> fn-  Left (NotWellTyped badType) -> do+  Left (NotWellTyped badType cause) -> do     loc <- ask     let err = TCFailedOnInstr v t loc Nothing-              (Just $ UnsupportedTypeForScope badType BtNotComparable)+              (Just $ UnsupportedTypeForScope badType cause)     pure $ IllTypedSeq err [NonTypedInstr $ U.PrimEx v]  typeCheckContractImpl@@ -202,7 +228,7 @@ -- -- As a second argument, @typeCheckList@ accepts input stack type representation. typeCheckList-  :: (Typeable inp)+  :: (SingI inp)   => [U.ExpandedOp]   -> HST inp   -> TypeCheck (SomeInstr inp)@@ -215,7 +241,7 @@ -- 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)+  :: (SingI inp)   => [U.ExpandedOp] -> HST inp -> TypeCheckNoExcept (TypeCheckedSeq inp) typeCheckListNoExcept = usingReaderT def ... typeCheckImpl typeCheckInstr @@ -239,19 +265,19 @@  typeVerifyParameter   :: SingI t-  => TcOriginatedContracts -> U.Value -> Either TCError (Value t)+  => TcOriginatedContracts -> U.Value -> TypeCheckResult (Value t) typeVerifyParameter originatedContracts = typeVerifyTopLevelType (Just originatedContracts)  typeVerifyStorage   :: SingI t-  => U.Value -> Either TCError (Value t)+  => U.Value -> TypeCheckResult (Value t) typeVerifyStorage = typeVerifyTopLevelType Nothing  typeVerifyTopLevelType   :: forall t. SingI t-  => Maybe TcOriginatedContracts -> U.Value -> Either TCError (Value t)+  => Maybe TcOriginatedContracts -> U.Value -> TypeCheckResult (Value t) typeVerifyTopLevelType mOriginatedContracts valueU =-  runTypeCheck (TypeCheckValue (valueU, demote @t)) def $ usingReaderT def $+  runTypeCheck (TypeCheckValue (valueU, demote @t)) $ usingReaderT def $     typeCheckValImpl mOriginatedContracts typeCheckInstr valueU  -- | Like 'typeCheckValue', but for values to be used as parameter.@@ -259,47 +285,47 @@ -- Also accepts a 'TcOriginatedContracts' in order to be able to type-check -- @contract p@ values (which can only be part of a parameter). typeCheckParameter-  :: TcOriginatedContracts -> U.Ty -> U.Value -> Either TCError SomeValue+  :: TcOriginatedContracts -> U.Ty -> U.Value -> TypeCheckResult SomeValue typeCheckParameter originatedContracts = typeCheckTopLevelType (Just originatedContracts)  -- | Like 'typeCheckValue', but for values to be used as storage. typeCheckStorage-  :: U.Ty -> U.Value -> Either TCError SomeValue+  :: U.Ty -> U.Value -> TypeCheckResult SomeValue typeCheckStorage = typeCheckTopLevelType Nothing  typeCheckTopLevelType-  :: Maybe TcOriginatedContracts -> U.Ty -> U.Value -> Either TCError SomeValue+  :: Maybe TcOriginatedContracts -> U.Ty -> U.Value -> TypeCheckResult SomeValue typeCheckTopLevelType mOriginatedContracts typeU valueU =-  withSomeSingT (fromUType typeU) $ \(_ :: Sing t) ->-    SomeValue <$> typeVerifyTopLevelType @t mOriginatedContracts valueU+  withSomeSing (fromUType typeU) $ \(s :: Sing t) ->+    withSingI s $ SomeValue <$> typeVerifyTopLevelType @t mOriginatedContracts valueU  -- | Helper data type we use to typecheck DUPN. data TCDupNHelper inp where   TCDupNHelper ::     forall (n :: Peano) inp out a.-    (Typeable out, ConstraintDUPN n inp out a) =>-    Sing n -> HST out -> TCDupNHelper inp+    (SingI out, ConstraintDUPN n inp out a, DupableScope a) =>+    PeanoNatural n -> HST out -> TCDupNHelper inp  -- | Helper data type we use to typecheck DROPN. data TCDropHelper inp where   TCDropHelper ::     forall (n :: Peano) inp out.-    (Typeable out, SingI n, KnownPeano n, LongerOrSameLength inp n, Drop n inp ~ out) =>-    Sing n -> HST out -> TCDropHelper inp+    (SingI out, LongerOrSameLength inp n, Drop n inp ~ out) =>+    PeanoNatural n -> HST out -> TCDropHelper inp  -- | Helper data type we use to typecheck DIG. data TCDigHelper inp where   TCDigHelper ::     forall (n :: Peano) inp out a.-    (Typeable out, ConstraintDIG n inp out a) =>-    Sing n -> HST out -> TCDigHelper inp+    (SingI out, ConstraintDIG n inp out a) =>+    PeanoNatural n -> HST out -> TCDigHelper inp  -- | Helper data type we use to typecheck DUG. data TCDugHelper inp where   TCDugHelper ::     forall (n :: Peano) inp out a.-    (Typeable out, ConstraintDUG n inp out a) =>-    Sing n -> HST out -> TCDugHelper inp+    (SingI out, ConstraintDUG n inp out a) =>+    PeanoNatural n -> HST out -> TCDugHelper inp  -- | Helper data type we use to typecheck PAIRN. --@@ -308,8 +334,8 @@ data TCPairNHelper inp where   TCPairNHelper ::     forall (n :: Peano) (inp :: [T]).-    (Typeable (PairN n inp), ConstraintPairN n inp) =>-    Sing n -> HST (PairN n inp) -> TCPairNHelper inp+    (SingI (PairN n inp), ConstraintPairN n inp) =>+    PeanoNatural n -> HST (PairN n inp) -> TCPairNHelper inp  -- | Helper data type we use to typecheck UNPAIRN. --@@ -318,8 +344,8 @@ data TCUnpairNHelper (inp :: [T]) where   TCUnpairNHelper ::     forall (n :: Peano) (a :: T) (b :: T) (rest :: [T]).-    (Typeable (UnpairN n ('TPair a b) ++ rest), ConstraintUnpairN n ('TPair a b)) =>-    Sing n -> HST (UnpairN n ('TPair a b) ++ rest) -> TCUnpairNHelper ('TPair a b : rest)+    (SingI (UnpairN n ('TPair a b) ++ rest), ConstraintUnpairN n ('TPair a b)) =>+    PeanoNatural n -> HST (UnpairN n ('TPair a b) ++ rest) -> TCUnpairNHelper ('TPair a b : rest)  -- | Helper data type we use to typecheck GETN. --@@ -328,8 +354,8 @@ data TCGetNHelper (inp :: [T]) where   TCGetNHelper ::     forall (ix :: Peano) (pair :: T) (rest :: [T]).-    (Typeable (GetN ix pair ': rest), ConstraintGetN ix pair) =>-    Sing ix -> HST (GetN ix pair ': rest) -> TCGetNHelper (pair : rest)+    (SingI (GetN ix pair ': rest), ConstraintGetN ix pair) =>+    PeanoNatural ix -> HST (GetN ix pair ': rest) -> TCGetNHelper (pair : rest)  -- | Helper data type we use to typecheck UPDATEN. --@@ -338,8 +364,8 @@ data TCUpdateNHelper (inp :: [T]) where   TCUpdateNHelper ::     forall (ix :: Peano) (val :: T) (pair :: T) (rest :: [T]).-    (Typeable (UpdateN ix val pair ': rest), ConstraintUpdateN ix pair) =>-    Sing ix -> HST (UpdateN ix val pair ': rest) -> TCUpdateNHelper (val : pair : rest)+    (SingI (UpdateN ix val pair ': rest), ConstraintUpdateN ix pair) =>+    PeanoNatural ix -> HST (UpdateN ix val pair ': rest) -> TCUpdateNHelper (val : pair : rest)  -- | Helper function to convert a simple throwing typechecking action into a -- non-throwing one, embedding possible errors into the type checking tree.@@ -353,7 +379,7 @@  -- | Less verbose version of `lift ... typeCheckListNoExcept`. tcList-  :: (Typeable inp)+  :: (SingI inp)   => [U.ExpandedOp] -> HST inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp) tcList ops stack = lift $ typeCheckListNoExcept ops stack @@ -383,19 +409,22 @@     go nTotal inputHST <&> \case       TCDropHelper s out -> inputHST :/ DROPN s ::: out     where-      go :: forall inp. Typeable inp+      go :: forall inp. SingI inp         => Word         -> HST inp         -> TypeCheckInstr (TCDropHelper inp)       go = curry \case-        (0, i) -> pure (TCDropHelper SZ i)+        (0, i) -> pure (TCDropHelper Zero i)          (_, SNil) -> notEnoughItemsOnStack'          (n, (_ ::& iTail)) -> do-          go (n - 1) iTail <&> \(TCDropHelper s out) -> TCDropHelper (SS s) out+          go (n - 1) iTail <&> \(TCDropHelper s out) -> TCDropHelper (Succ s) out -  (U.DUP vn1, a@(n, d, _vn2) ::& rs) -> workOnInstr uInstr $+  (U.DUP vn1, a@(n :: Notes t, d, _vn2) ::& rs) -> workOnInstr uInstr $ do+    Dict <-+      onScopeCheckInstrErr @t uInstr (SomeHST inp) Nothing $+      checkScope @(DupableScope t)     pure (inp :/ DUP ::: ((n, d, vn1) ::& a ::& rs))    (U.DUP _vn, SNil) -> notEnoughItemsOnStack@@ -403,7 +432,7 @@   (U.DUPN vn nTotal, inputHST) -> workOnInstr uInstr $     go nTotal inputHST <&> \(TCDupNHelper s out) -> inputHST :/ DUPN s ::: out     where-      go :: forall inp. Typeable inp+      go :: forall inp. SingI inp         => Word         -> HST inp         -> TypeCheckInstr (TCDupNHelper inp)@@ -415,11 +444,15 @@          -- Don't bind whatever variable annotation is here because DUP n doesn't         -- duplicate variable annotations. This is consistent with tezos-client.-        (1, i@((an, dict, _) ::& _)) -> pure (TCDupNHelper (SS SZ) ((an, dict, vn) ::& i))+        (1, i@((an :: Notes a, dict, _) ::& _)) -> do+          Dict <-+            onScopeCheckInstrErr @a uInstr (SomeHST inp) Nothing $+            checkScope @(DupableScope a)+          pure (TCDupNHelper One ((an, dict, vn) ::& i))          (n, (b ::& iTail)) ->-          go (n - 1) iTail <&> \(TCDupNHelper s@(SS _) (a ::& resTail)) ->-            TCDupNHelper (SS s) (a ::& b ::& resTail)+          go (n - 1) iTail <&> \(TCDupNHelper s@(Succ _) (a ::& resTail)) ->+            TCDupNHelper (Succ s) (a ::& b ::& resTail)    (U.SWAP, a ::& b ::& rs) -> workOnInstr uInstr $     pure (inp :/ SWAP ::: (b ::& a ::& rs))@@ -429,7 +462,7 @@   (U.DIG nTotal, inputHST) -> workOnInstr uInstr $     go nTotal inputHST <&> \(TCDigHelper s out) -> inputHST :/ DIG s ::: out     where-      go :: forall inp. Typeable inp+      go :: forall inp. SingI inp         => Word         -> HST inp         -> TypeCheckInstr (TCDigHelper inp)@@ -437,25 +470,25 @@         -- Even 'DIG 0' is invalid on empty stack (so it is not strictly `Nop`).         (_, SNil) -> notEnoughItemsOnStack' -        (0, i@(_ ::& _)) -> pure (TCDigHelper SZ i)+        (0, i@(_ ::& _)) -> pure (TCDigHelper Zero i)          (n, (b ::& iTail)) ->           go (n - 1) iTail <&> \(TCDigHelper s (a ::& resTail)) ->-            TCDigHelper (SS s) (a ::& b ::& resTail)+            TCDigHelper (Succ s) (a ::& b ::& resTail)    (U.DUG nTotal, inputHST) -> workOnInstr uInstr $     go nTotal inputHST <&> \(TCDugHelper s out) -> inputHST :/ DUG s ::: out     where-      go :: forall inp. Typeable inp+      go :: forall inp. SingI inp         => Word         -> HST inp         -> TypeCheckInstr (TCDugHelper inp)       go = curry \case-        (0, i@(_ ::& _)) -> pure (TCDugHelper SZ i)+        (0, i@(_ ::& _)) -> pure (TCDugHelper Zero i)          (n, (a ::& b ::& iTail)) ->           go (n - 1) (a ::& iTail) <&> \(TCDugHelper s resTail) ->-            TCDugHelper (SS s) (b ::& resTail)+            TCDugHelper (Succ s) (b ::& resTail)          -- Two cases:         -- 1. Input stack is empty.@@ -499,7 +532,27 @@       pure (inp :/ AnnPAIR tn pfn qfn ::: ((NTPair tn pfn' qfn' avn bvn an bn, Dict, vn') ::& rs))    (U.PAIR {}, _) -> notEnoughItemsOnStack+  (U.UNPAIR instrVn1 instrVn2 instrFn1 instrFn2, (NTPair _ fn1 fn2 vn1 vn2 n1 n2, Dict, vn) ::& rs) ->+    workOnInstr uInstr $ do+      -- We purposefully ignore the result of `convergeDestrAnns` here.+      -- We're only interested in checking that the instruction's field ann matches the pair's field ann,+      -- we don't need to "unify" them.+      _ <- onTypeCheckInstrAnnErr uInstr inp (Just UnpairArgument) (convergeDestrAnns fn1 instrFn1)+      _ <- onTypeCheckInstrAnnErr uInstr inp (Just UnpairArgument) (convergeDestrAnns fn2 instrFn2) +      let vn1' = deriveSpecialVN instrVn1 fn1 vn vn1+      let vn2' = deriveSpecialVN instrVn2 fn2 vn vn2+      pure $+        inp :/ AnnUNPAIR instrVn1 instrVn2 instrFn1 instrFn2 :::+          ( (n1, Dict, vn1') ::&+            (n2, Dict, vn2') ::&+            rs+          )++  (U.UNPAIR {}, _ ::& _) ->+    failWithErr $ UnexpectedType $ ("pair 'a 'b" :| []) :| []++  (U.UNPAIR {}, _) -> notEnoughItemsOnStack   (U.PAIRN varAnn nTotal, _) -> workOnInstr uInstr $ do     go nTotal inp <&> \case       TCPairNHelper s out -> inp :/ PAIRN s ::: addVarAnn out@@ -511,32 +564,26 @@               (InvalidInstruction uInstr "'PAIR n' expects n ≥ 2")         | n == 2 =             case hst of-              (an :: Notes a, _, avn) ::& (bn :: Notes b, _, bvn) ::& hstTail -> do+              (an :: Notes a, _, _) ::& (bn :: Notes b, _, _) ::& hstTail -> do                 withWTPInstr @('TPair a b) $ do-                  pure $ TCPairNHelper (SS (SS SZ)) $-                    (mkNotes an bn avn bvn, Dict, U.noAnn) ::& hstTail+                  pure $ TCPairNHelper Two $+                    (mkNotes an bn, Dict, U.noAnn) ::& hstTail               _ -> notEnoughItemsOnStack'         | otherwise =             case hst of-              (an :: Notes a, _, avn) ::& hstTail@(_ ::& _ ::& _) -> do+              (an :: Notes a, _, _) ::& hstTail@(_ ::& _ ::& _) -> do                 go (n - 1) hstTail >>= \case-                  TCPairNHelper nSing@(SS (SS _)) ((bn :: Notes b, _, bvn) ::& hstTail') -> do+                  TCPairNHelper nSing@(Succ (Succ _)) ((bn :: Notes b, _, _) ::& hstTail') -> do                     withWTPInstr @('TPair a b) $ do-                      pure $ TCPairNHelper (SS nSing) $-                        (mkNotes an bn avn bvn, Dict, U.noAnn) ::& hstTail'+                      pure $ TCPairNHelper (Succ nSing) $+                        (mkNotes an bn, Dict, U.noAnn) ::& hstTail'               _ -> notEnoughItemsOnStack' -      -- | @PAIR n@ instructions take the variable annotations of each-      -- element in the stack and turn them into field annotations. E.g.:-      ---      -- > /* [ @bb nat : @aa nat ] */ ;-      -- > PAIR 2-      -- > /* [ pair (nat %bb) (nat %aa) ] */ ;-      mkNotes :: forall a b. Notes a -> Notes b -> VarAnn -> VarAnn -> Notes ('TPair a b)-      mkNotes an bn avn bvn =+      mkNotes :: forall a b. Notes a -> Notes b -> Notes ('TPair a b)+      mkNotes an bn =         NTPair U.noAnn-          (convAnn @VarTag @FieldTag avn) (convAnn @VarTag @FieldTag bvn)           U.noAnn U.noAnn+          U.noAnn U.noAnn           an bn        -- | If a @PAIR n@ instruction has a variable annotation,@@ -563,7 +610,7 @@         | n == 2 =             case hst of               (NTPair _ aFieldAnn bFieldAnn _ _ aNotes bNotes, Dict, _) ::& rest -> do-                pure $ TCUnpairNHelper (SS (SS SZ)) $+                pure $ TCUnpairNHelper Two $                   (aNotes, Dict, convAnn @FieldTag @VarTag aFieldAnn)                   ::& (bNotes, Dict, convAnn @FieldTag @VarTag bFieldAnn)                   ::& rest@@ -572,35 +619,34 @@             case hst of               (NTPair _ aFieldAnn _ _ _ aNotes bNotes, Dict, _) ::& rest -> do                 go (n - 1) ((bNotes, Dict, U.noAnn) ::& rest) >>= \case-                  TCUnpairNHelper nSing@(SS (SS _)) out -> do-                    pure $ TCUnpairNHelper (SS nSing) $+                  TCUnpairNHelper nSing@(Succ (Succ _)) out -> do+                    pure $ TCUnpairNHelper (Succ nSing) $                       (aNotes, Dict, convAnn @FieldTag @VarTag aFieldAnn) ::& out               _ -> unexpectedType        unexpectedType :: TypeCheckInstr a       unexpectedType = failWithErr' $ UnexpectedType $ (pairWithElems nTotal :| []) :| [] -  (U.CAR vn fn, (STPair{}, NTPair pairTN pfn qfn pvn qvn (pns :: Notes p) (qns :: Notes q), _, pairVN) ::&+ rs) -> workOnInstr uInstr $ do-    pfn' <- onTypeCheckInstrAnnErr uInstr inp (Just CarArgument) (convergeDestrAnns fn pfn)-    withWTPInstr @p $-      withWTPInstr @('TPair p q) $ do-        let vn' = deriveSpecialVN vn pfn' pairVN pvn-            i' = (NTPair pairTN pfn' qfn pvn qvn pns qns, Dict, pairVN) ::& rs-        pure $ i' :/ AnnCAR fn ::: ((pns, Dict, vn') ::& rs)+  (U.CAR vn fn, (STPair{}, NTPair _ pfn _ pvn _ pns _, Dict, pairVN) ::&+ rs) -> workOnInstr uInstr $ do+    -- We purposefully ignore the result of `convergeDestrAnns` here.+    -- We're only interested in checking that the instruction's field ann matches the pair's field ann,+    -- we don't need to "unify" them.+    _ <- onTypeCheckInstrAnnErr uInstr inp (Just CarArgument) (convergeDestrAnns fn pfn)+    let vn' = deriveSpecialVN vn pfn pairVN pvn+    pure $ inp :/ AnnCAR vn fn ::: ((pns, Dict, vn') ::& rs)    (U.CAR _ _, _ ::& _) ->     failWithErr $ UnexpectedType $ ("pair 'a 'b" :| []) :| []    (U.CAR _ _, SNil) -> notEnoughItemsOnStack -  (U.CDR vn fn, (STPair{}, NTPair pairTN pfn qfn pvn qvn (pns :: Notes p) (qns :: Notes q), _, pairVN) ::&+ rs) -> workOnInstr uInstr $ do-    qfn' <- onTypeCheckInstrAnnErr uInstr inp (Just CdrArgument) (convergeDestrAnns fn qfn)--    withWTPInstr @q $-      withWTPInstr @('TPair p q) $ do-        let vn' = deriveSpecialVN vn qfn' pairVN qvn-            i' = (NTPair pairTN pfn qfn' pvn qvn pns qns, Dict, pairVN) ::& rs-        pure $ i' :/ AnnCDR fn ::: ((qns, Dict, vn') ::& rs)+  (U.CDR vn fn, (STPair{}, NTPair _ _ qfn _ qvn _ qns, Dict, pairVN) ::&+ rs) -> workOnInstr uInstr $ do+    -- We purposefully ignore the result of `convergeDestrAnns` here.+    -- We're only interested in checking that the instruction's field ann matches the pair's field ann,+    -- we don't need to "unify" them.+    _ <- onTypeCheckInstrAnnErr uInstr inp (Just CdrArgument) (convergeDestrAnns fn qfn)+    let vn' = deriveSpecialVN vn qfn pairVN qvn+    pure $ inp :/ AnnCDR vn fn ::: ((qns, Dict, vn') ::& rs)    (U.CDR _ _, _ ::& _) ->     failWithErr $ UnexpectedType $ ("pair 'a 'b" :| []) :| []@@ -625,9 +671,9 @@    (U.RIGHT {}, SNil) -> notEnoughItemsOnStack -  (U.IF_LEFT mp mq, (STOr{}, ons, _, ovn) ::&+ rs) -> do+  (U.IF_LEFT mp mq, (STOr lt rt, ons, _, ovn) ::&+ rs) -> do     case deriveNsOr ons ovn of-      (an :: Notes a, bn :: Notes b, avn, bvn) ->+      (an :: Notes a, bn :: Notes b, avn, bvn) -> withSingI lt $ withSingI rt $         withWTPInstr' @a $           withWTPInstr' @b $ do             let@@ -700,12 +746,12 @@         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+  (U.MAP vn mp, (STList l, NTList _ (vns :: Notes t1), Dict, _vn) ::&+ _) -> withSingI l $ do     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+  (U.MAP vn mp, (STMap k v, NTMap _ kns vns, Dict, _vn) ::&+ _) -> withSingI k $ withSingI v $ do     case NTPair def def def def def kns vns of       (pns :: Notes ('TPair k v1)) ->         withWTPInstr' @('TPair k v1) $@@ -720,15 +766,15 @@    (U.MAP _ _, SNil) -> notEnoughItemsOnStack -  (U.ITER is, (STSet (_ :: Sing t1), NTSet _ en, _, _) ::&+ _) -> do+  (U.ITER is, (STSet (s :: Sing t1), NTSet _ en, _, _) ::&+ _) -> withSingI s $ do     withWTPInstr' @t1 $       iterImpl en uInstr is inp -  (U.ITER is, (STList (_ :: Sing t1), NTList _ en, _, _) ::&+ _) -> do+  (U.ITER is, (STList (l :: Sing t1), NTList _ en, _, _) ::&+ _) -> withSingI l $ do     withWTPInstr' @t1 $       iterImpl en uInstr is inp -  (U.ITER is, (STMap _ _, NTMap _ kns vns, _, _) ::&+ _) -> do+  (U.ITER is, (STMap k v, NTMap _ kns vns, _, _) ::&+ _) -> withSingI k $ withSingI v $ do     case NTPair def def def def def kns vns of       (en :: Notes ('TPair a b)) ->         withWTPInstr' @('TPair a b) $ iterImpl en uInstr is inp@@ -743,13 +789,15 @@   (U.ITER _, SNil) -> notEnoughItemsOnStack    (U.MEM varNotes,-   _ ::& (STSet{}, NTSet _ notesK, _, _) ::&+ _) -> workOnInstr uInstr $+   _ ::& (STSet s, NTSet _ notesK, _, _) ::&+ _) -> withSingI s $ workOnInstr uInstr $     memImpl notesK inp varNotes   (U.MEM varNotes,-   _ ::& (STMap{}, NTMap _ notesK _, _, _) ::&+ _) -> workOnInstr uInstr $+   _ ::& (STMap k v, NTMap _ notesK _, _, _) ::&+ _) ->+    withSingI k $ withSingI v $ workOnInstr uInstr $     memImpl notesK inp varNotes   (U.MEM varNotes,-   _ ::& (STBigMap{}, NTBigMap _ notesK _, _, _) ::&+ _) -> workOnInstr uInstr $+   _ ::& (STBigMap k v, NTBigMap _ notesK _, _, _) ::&+ _) ->+    withSingI k $ withSingI v $ workOnInstr uInstr $     memImpl notesK inp varNotes   (U.MEM _, _ ::& _ ::& _) ->     failWithErr $ UnexpectedType@@ -761,12 +809,12 @@   (U.MEM _, _) -> notEnoughItemsOnStack    (U.GET varNotes,-   _ ::& (STMap{}, NTMap _ notesK (notesV :: Notes v), _, _) ::&+ _) ->-    workOnInstr uInstr $ withWTPInstr @v $+   _ ::& (STMap k v, NTMap _ notesK (notesV :: Notes v), _, _) ::&+ _) ->+    withSingI k $ withSingI v $ workOnInstr uInstr $ withWTPInstr @v $       getImpl notesK inp notesV varNotes   (U.GET varNotes,-   _ ::& (STBigMap{}, NTBigMap _ notesK (notesV :: Notes v), _, _) ::&+ _) ->-    workOnInstr uInstr $ withWTPInstr @v $+   _ ::& (STBigMap k v, NTBigMap _ notesK (notesV :: Notes v), _, _) ::&+ _) ->+    withSingI k $ withSingI v $ workOnInstr uInstr $ withWTPInstr @v $       getImpl notesK inp notesV varNotes    (U.GET _, _ ::& _ ::& _) ->@@ -785,23 +833,23 @@     where       go :: forall x xs. Word -> HST (x : xs) -> TypeCheckInstr (TCGetNHelper (x : xs))       go 0 ((a, Dict, _) ::& rest) =-        pure $ TCGetNHelper SZ ((a, Dict, getNVarAnn) ::& rest)+        pure $ TCGetNHelper Zero ((a, Dict, getNVarAnn) ::& rest)       go 1 ((NTPair _ _ _ _ _ leftNotes _, Dict, _) ::& rest) =-        pure $ TCGetNHelper (SS SZ) $ (leftNotes, Dict, getNVarAnn) ::& rest+        pure $ TCGetNHelper One $ (leftNotes, Dict, getNVarAnn) ::& rest       go ix ((NTPair _ _ _ _ _ _ rightNotes, Dict, _) ::& rest) =         go (ix - 2) ((rightNotes, Dict, U.noAnn) ::& rest) <&> \(TCGetNHelper ixSing out) ->-          TCGetNHelper (SS (SS ixSing)) out+          TCGetNHelper (Succ (Succ ixSing)) out       go _ _ = failWithErr' $ UnexpectedType $ (pairWithNodeIndex ix0 :| []) :| []    (U.UPDATE varAnn,-   _ ::& _ ::& (STMap{}, (NTMap _ notesK (notesV :: Notes v)), _, _) ::&+ _) ->-    workOnInstr uInstr $ updImpl notesK inp (NTOption U.noAnn notesV) varAnn+   _ ::& _ ::& (STMap k v, (NTMap _ notesK (notesV :: Notes v)), _, _) ::&+ _) ->+    withSingI k $ withSingI v $ workOnInstr uInstr $ updImpl notesK inp (NTOption U.noAnn notesV) varAnn   (U.UPDATE varAnn,-   _ ::& _ ::& (STBigMap{}, NTBigMap _ notesK (notesV :: Notes v), _, _) ::&+ _) ->-    workOnInstr uInstr $ updImpl notesK inp (NTOption U.noAnn notesV) varAnn+   _ ::& _ ::& (STBigMap k v, NTBigMap _ notesK (notesV :: Notes v), _, _) ::&+ _) ->+    withSingI k $ withSingI v $ workOnInstr uInstr $ updImpl notesK inp (NTOption U.noAnn notesV) varAnn   (U.UPDATE varAnn,-   _ ::& _ ::& (STSet{}, NTSet _ (notesK :: Notes k), _, _) ::&+ _) ->-    workOnInstr uInstr $ updImpl notesK inp (NTBool U.noAnn) varAnn+   _ ::& _ ::& (STSet s, NTSet _ (notesK :: Notes k), _, _) ::&+ _) ->+    withSingI s $ workOnInstr uInstr $ updImpl notesK inp (NTBool U.noAnn) varAnn    (U.UPDATE _, _ ::& _ ::& _ ::& _) ->     failWithErr $ UnexpectedType@@ -819,27 +867,27 @@     where       go :: forall val pair rest. Word -> HST (val : pair : rest) -> TypeCheckInstr (TCUpdateNHelper (val : pair : rest))       go 0 ((valNotes, Dict, _) ::& (_, _, _) ::& rest) =-        pure $ TCUpdateNHelper SZ $+        pure $ TCUpdateNHelper Zero $           (valNotes, Dict, updateNVarAnn) ::& rest       go 1 ((valNotes, Dict, _) ::& (NTPair pairTA leftFA rightFA leftVA rightVA _ rightNotes, Dict, _) ::& rest) =-        pure $ TCUpdateNHelper (SS SZ) $+        pure $ TCUpdateNHelper One $           (NTPair pairTA leftFA rightFA leftVA rightVA valNotes rightNotes, Dict, updateNVarAnn) ::& rest       go ix (val ::& (NTPair pairTA leftFA rightFA leftVA rightVA leftNotes rightNotes, Dict, _) ::& rest) =         go (ix - 2) (val ::& (rightNotes, Dict, U.noAnn) ::& rest) <&>           \(TCUpdateNHelper ixSing ((updatedRightNotes, Dict, _) ::& outRest)) ->-            TCUpdateNHelper (SS (SS ixSing)) $+            TCUpdateNHelper (Succ (Succ ixSing)) $               (NTPair pairTA leftFA rightFA leftVA rightVA leftNotes updatedRightNotes, Dict, updateNVarAnn) ::& outRest       go _ _ = failWithErr' $ UnexpectedType $ ("'val" :| [pairWithNodeIndex ix0]) :| []   (U.UPDATEN _ _, _) -> notEnoughItemsOnStack    (U.GET_AND_UPDATE varAnn,-   _ ::& _ ::& (STMap{}, (NTMap _ notesK (notesV :: Notes v)), _, _) ::&+ _) ->-    workOnInstr uInstr $+   _ ::& _ ::& (STMap k v, (NTMap _ notesK (notesV :: Notes v)), _, _) ::&+ _) ->+    withSingI k $ withSingI v $ workOnInstr uInstr $       withWTPInstr @v $         getUpdImpl notesK inp (NTOption U.noAnn notesV) varAnn   (U.GET_AND_UPDATE varAnn,-   _ ::& _ ::& (STBigMap{}, (NTBigMap _ notesK (notesV :: Notes v)), _, _) ::&+ _) ->-    workOnInstr uInstr $+   _ ::& _ ::& (STBigMap k v, (NTBigMap _ notesK (notesV :: Notes v)), _, _) ::&+ _) ->+    withSingI k $ withSingI v $ workOnInstr uInstr $       withWTPInstr @v $         getUpdImpl notesK inp (NTOption U.noAnn notesV) varAnn   (U.GET_AND_UPDATE _, _ ::& _ ::& _ ::& _) ->@@ -907,12 +955,12 @@         lamImpl (U.LAMBDA vn p1 p2) uInstr is vn ins ons i    (U.EXEC vn, ((tn :: Notes t1), _, _)-                              ::& ( STLambda _ _+                              ::& ( STLambda v b                                   , NTLambda _ (t1n :: Notes t1') (t2n :: Notes t2')                                   , _                                   , _                                   )-                              ::&+ rs) -> workOnInstr uInstr $ do+                              ::&+ rs) -> withSingI v $ withSingI b $ workOnInstr uInstr $ do     Refl <- onTypeCheckInstrErr uInstr (SomeHST inp) (Just LambdaArgument)                   (eqType @t1 @t1')     (Refl, _) <- errM $ matchTypes tn t1n@@ -928,11 +976,11 @@   (U.EXEC _, _) -> notEnoughItemsOnStack    (U.APPLY vn, ((_ :: Notes a'), _, _)-                  ::& ( STLambda (STPair _ _) _+                  ::& ( STLambda (STPair lt rt) b                       , NTLambda vann (NTPair _ _ _ _ _ (_ :: Notes a) (nb :: Notes b)) sc                       , _                       , _)-                  ::&+ rs) -> workOnInstr uInstr $ do+                  ::&+ rs) -> withSingI lt $ withSingI rt $ withSingI b $ workOnInstr uInstr $ do     case NTLambda vann nb sc of       (l2n :: Notes ('TLambda t1 t2)) -> withWTPInstr @('TLambda t1 t2) $ do @@ -962,21 +1010,21 @@       TCDipHelperErr err rest -> IllTypedSeq err rest       TCDipHelperOk s subI out -> WellTypedSeq $ inputHST :/ DIPN s subI ::: out     where-      go :: forall inp. Typeable inp+      go :: forall inp. SingI inp         => Word         -> HST inp         -> TypeCheckInstrNoExcept (TCDipHelper inp)       go n curHST = case (n, curHST) of         (0, _) -> typeCheckDipBody (U.DIPN nTotal) uInstr instructions curHST           (TCDipHelperErr)-          (TCDipHelperOk SZ)+          (TCDipHelperOk Zero)         (_, 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-          TCDipHelperOk s subI out -> TCDipHelperOk (SS s) subI (hstHead ::& out)+          TCDipHelperOk s subI out -> TCDipHelperOk (Succ s) subI (hstHead ::& out)           TCDipHelperErr err rest -> TCDipHelperErr err rest    (u, v) -> case (u, v) of -- Workaround for not exceeding -fmax-pmcheck-iterations limit@@ -1286,7 +1334,7 @@      (U.TRANSFER_TOKENS vn, ((_ :: Notes p'), _, _)       ::& (NTMutez{}, _, _)-      ::& (STContract (_ :: Sing p), _, _, _) ::&+ rs) -> workOnInstr uInstr $ do+      ::& (STContract (s :: Sing p), _, _, _) ::&+ rs) -> withSingI s $ workOnInstr uInstr $ do       proofScope <- onScopeCheckInstrErr @p uInstr (SomeHST inp) (Just ContractParameter)         $ checkScope @(ParameterScope p)       case (eqType @p @p', proofScope) of@@ -1434,6 +1482,40 @@     (U.NEVER, (NTNever{}, _, _) ::& _) -> workOnInstr uInstr $       pure $ inp :/ AnyOutInstr NEVER +    (U.TICKET vn, (stVal :: Sing v, _, _, _) ::&+ (NTNat{}, _, _) ::& rs) -> workOnInstr uInstr $+      withWTPInstr @v $+      withCompareableCheck stVal uInstr inp $+        inp :/ TICKET ::: ((starNotes, Dict, vn) ::& rs)+    (U.TICKET _, _ ::& _ ::& _) ->+      failWithErr $ UnexpectedType $ ("a'" :| ["nat"]) :| []+    (U.TICKET _, _) -> notEnoughItemsOnStack++    (U.READ_TICKET vn, ticket@(ntTicket@NTTicket{}, Dict, _) ::& rs) -> workOnInstr uInstr $+      case notesSing ntTicket of+        STTicket{} ->+          pure $ inp :/ READ_TICKET ::: ((starNotes, Dict, vn) ::& ticket ::& rs)+    (U.READ_TICKET _, _ ::& _) ->+      failWithErr $ UnexpectedType $ ("ticket 'a" :| []) :| []+    (U.READ_TICKET _, _) -> notEnoughItemsOnStack++    (U.SPLIT_TICKET vn, (NTTicket{}, Dict, _) ::& (NTPair _ _ _ _ _ NTNat{} NTNat{}, _, _) ::& rs) ->+      workOnInstr uInstr $+        pure $ inp :/ SPLIT_TICKET ::: ((starNotes, Dict, vn) ::& rs)+    (U.SPLIT_TICKET _, _ ::& _ ::& _) ->+      failWithErr $ UnexpectedType $ ("pair nat nat" :| ["ticket 'a"]) :| []+    (U.SPLIT_TICKET _, _) -> notEnoughItemsOnStack++    (U.JOIN_TICKETS vn,+       (STPair{}, NTPair _ _ _ _ _ nt1@NTTicket{} nt2@NTTicket{}, Dict, _) ::&+ rs) ->+      workOnInstr uInstr $ do+        (Refl, nt) <-+          onTypeCheckInstrErr uInstr (SomeHST inp) (Just TicketsJoin) $+            matchTypes nt1 nt2+        pure $ inp :/ JOIN_TICKETS ::: ((NTOption U.noAnn nt, Dict, vn) ::& rs)+    (U.JOIN_TICKETS _, _ ::& _) ->+      failWithErr $ UnexpectedType $ ("pair (ticket 'a) (ticket 'a)" :| []) :| []+    (U.JOIN_TICKETS _, _) -> notEnoughItemsOnStack+     -- Could not get rid of the catch all clause due to this warning:     -- @     -- Pattern match checker exceeded (2000000) iterations in@@ -1469,7 +1551,7 @@ -- value. genericIf   :: forall bti bfi cond rs .-    (Typeable bti, Typeable bfi)+    (SingI bti, SingI bfi)   => (forall s'.         Instr bti s' ->         Instr bfi s' ->@@ -1502,17 +1584,17 @@           pure $ AnyOutInstr (cons p q)  mapImpl-  :: forall c rs .+  :: forall c rs.     ( MapOp c     , WellTyped (MapOpInp c)-    , Typeable (MapOpRes c)+    , SingI1 (MapOpRes c)     )   => ([TypeCheckedOp] -> TypeCheckedInstr)   -> Notes (MapOpInp c)   -> U.ExpandedInstr   -> [U.ExpandedOp]   -> HST (c ': rs)-  -> (forall v' . (KnownT v') =>+  -> (forall v'. (SingI v') =>         Notes v' -> HST rs -> TypeCheckInstr (HST (MapOpRes c v' ': rs)))   -> TypeCheckInstrNoExcept (TypeCheckedSeq (c ': rs)) mapImpl cons vn instr mp i@(_ ::& rs) mkRes = do@@ -1520,11 +1602,11 @@     case subp of       sub ::: subo ->         case subo of-          (bn, _, _bvn) ::& rs' -> do+          (bn :: Notes v', _, _bvn) ::& rs' -> do             Refl <- onTypeCheckInstrErr instr (SomeHST i) (Just Iteration)               $ eqHST rs rs'             x <- mkRes bn rs'-            pure $ i :/ MAP sub ::: x+            pure $ i :/ withSingI1 @(MapOpRes c) @v' (MAP sub ::: x)           _ -> typeCheckInstrErr instr (SomeHST i) (Just Iteration)       AnyOutInstr _ ->         typeCheckInstrErr' instr (SomeHST i) (Just Iteration) CodeAlwaysFails@@ -1555,7 +1637,7 @@ lamImpl   :: forall it ot ts .     ( WellTyped it, WellTyped ot-    , Typeable ts+    , SingI ts     )   => ([TypeCheckedOp] -> TypeCheckedInstr)   -> U.ExpandedInstr@@ -1601,18 +1683,18 @@ data TCDipHelper inp where   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+    (SingI out, ConstraintDIPN n inp out s s') =>+    PeanoNatural n -> Instr s s' -> HST out -> TCDipHelper inp   TCDipHelperErr :: TCError -> [IllTypedInstr] -> TCDipHelper inp  typeCheckDipBody-  :: Typeable inp+  :: SingI inp   => ([TypeCheckedOp] -> TypeCheckedInstr)   -> U.ExpandedInstr   -> [U.ExpandedOp]   -> HST inp   -> (TCError -> [IllTypedInstr] -> r)-  -> (forall out. Typeable out => Instr inp out -> HST out -> r)+  -> (forall out. SingI out => Instr inp out -> HST out -> r)   -> TypeCheckInstrNoExcept r typeCheckDipBody cons mainInstr instructions inputHST onErr onOk = do   listRes <- lift $ typeCheckListNoExcept instructions inputHST

@@ -5,16 +5,17 @@ module Michelson.TypeCheck.TypeCheck   ( TcInstrHandler   , TcOriginatedContracts-  , TcResult   , TypeCheckEnv(..)   , TypeCheckOptions(..)   , TypeCheck   , TypeCheckNoExcept+  , TypeCheckResult   , runTypeCheck   , TypeCheckInstr   , TypeCheckInstrNoExcept   , runTypeCheckIsolated   , runTypeCheckInstrIsolated+  , typeCheckingWith   , liftNoExcept   , liftNoExcept'   , throwingTCError@@ -30,11 +31,12 @@   , TypeCheckMode(..)   , SomeParamType(..)   , mkSomeParamType-  , mkSomeParamTypeUnsafe+  , unsafeMkSomeParamType   ) where  -import Control.Monad.Except (throwError)+import Control.Monad.Except (Except, mapExceptT, runExcept, throwError)+import Control.Monad.Reader (mapReaderT) import Data.Default (Default(..)) import Data.Singletons (Sing) import Fmt (Buildable, build, pretty)@@ -47,6 +49,7 @@   tcsEither) import Michelson.TypeCheck.Types import qualified Michelson.Typed as T+import Michelson.Typed (SingI) import qualified Michelson.Untyped as U import Tezos.Address (ContractHash) import Util.Lens@@ -62,6 +65,15 @@   (ReaderT TypeCheckOptions     (State TypeCheckEnv)) +-- | Monad for performing some typechecking operations with the same options.+--+-- Unlike 'TypeCheck' monad, this does not carry the context of intra-contract+-- or intra-value typechecking.+-- TODO [this MR]: probably come up with a better name? IntraTypeCheck?+type TypeCheckResult =+  (ReaderT TypeCheckOptions+    (Except TCError))+ data SomeParamType = forall t. (T.ParameterScope t) =>   SomeParamType (Sing t) (T.ParamNotes t) @@ -80,14 +92,14 @@ -- | Helper function means to provide a quick way for creating instance -- of @SomeParamType@ needed in test. someParamToParameterType :: SomeParamType -> U.ParameterType-someParamToParameterType (SomeParamType s T.ParamNotesUnsafe{..}) =+someParamToParameterType (SomeParamType s T.UnsafeParamNotes{..}) =   U.ParameterType (T.AsUTypeExt s pnNotes) pnRootAnn  -- | Construct @SomeParamType@ from @ParameterType@, mainly used in test.-mkSomeParamTypeUnsafe :: HasCallStack => U.ParameterType -> SomeParamType-mkSomeParamTypeUnsafe p =+unsafeMkSomeParamType :: HasCallStack => U.ParameterType -> SomeParamType+unsafeMkSomeParamType p =   case mkSomeParamType p of-    Right sp ->  sp+    Right sp -> sp     Left err -> error $ "Illegal type in parameter of env contract: " <> pretty err  mkSomeParamType :: U.ParameterType -> Either TCError SomeParamType@@ -118,19 +130,31 @@   }  data TypeCheckOptions = TypeCheckOptions-  { tcVerbose :: Bool -- ^ Whether to add stack type comments after every-                      -- instruction a la tezos-client.+  { tcVerbose :: Bool+    -- ^ Whether to add stack type comments after every+    -- instruction a la tezos-client.+  , tcStrict :: Bool+    -- ^ Whether should we behave like in test run or real run+    -- (real run is more strict).+    --+    -- @tezos-client run@'s behaviour can slightly differ from the behaviour+    -- of @tezos-client originate@ and @tezos-client transfer@. For instance,+    -- some values can be "forged" in test run, but not in a real one,+    -- see: Note [Tickets forging].+    --+    -- Set this to @True@ when need to match the behaviour in the network,+    -- and to @False@ if you prefer providing the user with some convenient+    -- features.   }  instance Default TypeCheckOptions where-  def = TypeCheckOptions{ tcVerbose = False }+  def = TypeCheckOptions{ tcVerbose = False, tcStrict = True }  makeLensesWith postfixLFields ''TypeCheckEnv -runTypeCheck :: TypeCheckMode -> TypeCheckOptions -> TypeCheck a -> Either TCError a-runTypeCheck mode options = evaluatingState (TypeCheckEnv [] mode)-                          . runExceptT-                          . usingReaderT options+runTypeCheck :: TypeCheckMode -> TypeCheck a -> TypeCheckResult a+runTypeCheck mode =+  mapReaderT $ mapExceptT $ evaluatingStateT (TypeCheckEnv [] mode)  -- | Run type checker as if it worked isolated from other world - -- no access to environment of the current contract is allowed.@@ -140,10 +164,11 @@ -- whatever we typecheck does not depend on the parameter type of the -- contract which is being typechecked (because there is no contract -- that we are typechecking).-runTypeCheckIsolated :: TypeCheck a -> Either TCError a-runTypeCheckIsolated = runTypeCheck TypeCheckTest def+runTypeCheckIsolated :: TypeCheck a -> TypeCheckResult a+runTypeCheckIsolated = runTypeCheck TypeCheckTest -type TcResult inp = Either TCError (SomeInstr inp)+typeCheckingWith :: TypeCheckOptions -> TypeCheckResult a -> Either TCError a+typeCheckingWith options = runExcept . usingReaderT options  type TypeCheckInstr =   ReaderT InstrCallStack TypeCheck@@ -152,7 +177,7 @@   ReaderT InstrCallStack TypeCheckNoExcept  -- | Similar to 'runTypeCheckIsolated', but for 'TypeCheckInstr.'-runTypeCheckInstrIsolated :: TypeCheckInstr a -> Either TCError a+runTypeCheckInstrIsolated :: TypeCheckInstr a -> TypeCheckResult a runTypeCheckInstrIsolated = runTypeCheckIsolated . flip runReaderT def  liftNoExcept :: TypeCheckInstrNoExcept a -> TypeCheckInstr a@@ -249,7 +274,7 @@ -- have to be refactored too. -- Therefore, I am using ReaderT over TypeCheck. type TcInstrHandler-   = forall inp. (Typeable inp, HasCallStack)+   = forall inp. (SingI inp, HasCallStack)       => U.ExpandedInstr       -> HST inp       -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)

@@ -11,12 +11,12 @@   , someInstrToOp   ) where -import Data.Typeable (cast)+import Data.Singletons (SingI)  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.Typed.Instr (Instr, castInstr) import Michelson.Untyped.Instr (ExpandedOp, InstrAbstract(..)) import Util.TH (deriveGADTNFData) @@ -26,13 +26,13 @@ -- | Represents nodes of a partially typed operation tree. data TypeCheckedOp where   -- | Constructs well-typed node.-  WellTypedOp :: (Typeable inp, Typeable out) => Instr inp out -> TypeCheckedOp+  WellTypedOp :: (SingI inp, SingI 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+  WellTypedOp i1 == WellTypedOp i2 = castInstr i1 == Just i2   IllTypedOp i1 == IllTypedOp i2 = i1 == i2   _ == _ = False @@ -55,7 +55,7 @@   SNil -> go rest   (::&){} -> go rest   where-    go :: forall inp. Typeable inp => SomeInstrOut inp -> TypeCheckedOp+    go :: forall inp. SingI inp => SomeInstrOut inp -> TypeCheckedOp     go (i ::: _) = WellTypedOp i     go (AnyOutInstr i) = WellTypedOp (i @'[]) 

@@ -9,12 +9,11 @@     , SomeHST (..)     , SomeInstrOut (..)     , SomeInstr (..)-    , SomeContract (..)-    , SomeContractAndStorage (..)     , BoundVars (..)     , TcExtFrames     , NotWellTyped (..)     , getWTP+    , getWTP_     , withWTPm     , unsafeWithWTP     , mapSomeContract@@ -25,18 +24,21 @@  import Data.Constraint (Dict(..)) import qualified Data.Map.Lazy as Map-import Data.Singletons (Sing, SingI(..), demote)-import Fmt (Buildable(..), Builder, (+|), (|+), pretty)+import Data.Singletons (Sing, SingI(..), demote, withSingI)+import Fmt (Buildable(..), pretty) import Prelude hiding (EQ, GT, LT) import qualified Text.Show+import Text.PrettyPrint.Leijen.Text hiding (pretty) -import Michelson.Typed (ParameterScope, StorageScope, Notes(..), T(..), SingT(..), notesT, starNotes)-import Michelson.Typed.Haskell.Value (WellTyped)++import Michelson.Typed (Notes(..), SingT(..), SomeContract(..), T(..), notesT, starNotes) import qualified Michelson.Typed as T+import Michelson.Typed.Haskell.Value (WellTyped) import Michelson.Typed.Instr+import Michelson.Printer.Util import Michelson.Untyped (Ty, Var, noAnn) import Michelson.Untyped.Annotation (VarAnn)-import Util.Typeable+import Util.Sing (eqParamSing)  -- | Data type holding type information for stack (Heterogeneous Stack Type). --@@ -63,7 +65,7 @@ -- Additionally constructor keeps 'SingI' constraint for the current type. data HST (ts :: [T])  where   SNil :: HST '[]-  (::&) :: (Typeable xs, T.KnownT x)+  (::&) :: (T.SingI x, T.SingI xs)         => (Notes x, Dict (WellTyped x), VarAnn)         -> HST xs         -> HST (x ': xs)@@ -82,14 +84,16 @@       showDo ((notesT -> t, Dict, _vn) ::& SNil) = show t  instance Buildable (HST ts) where-  build SNil = "[]"-  build (r ::& rs) = "[ " +| showDo (r ::& rs) |+ " ]"-    where-      showDo :: HST (t ': ts_) -> Builder-      showDo ((notesT -> t, Dict, _vn) ::& (b ::& c)) =-          build t |+ ", " +| showDo (b ::& c)-      showDo ((notesT -> t, Dict, _vn) ::& SNil) = build t+  build = buildRenderDocExtended +instance RenderDoc (HST ts) where+  renderDoc _ SNil = "[]"+  renderDoc context (r ::& rs) = "[" <+> doRender (r ::& rs) <+> "]"+    where+      doRender :: HST (t ': ts_) -> Doc+      doRender ((notesT -> t, Dict, _vn) ::& (b ::& c)) =+          renderDoc context t <> "," <+> doRender (b ::& c)+      doRender ((notesT -> t, Dict, _vn) ::& SNil) = renderDoc context t infixr 7 ::&  instance Eq (HST ts) where@@ -100,7 +104,7 @@ -- | Append a type to 'HST', assuming that notes and annotations -- for this type are unknown. (-:&)-  :: (Typeable xs, WellTyped x)+  :: (WellTyped x, SingI xs)   => Sing x   -> HST xs   -> HST (x ': xs)@@ -112,7 +116,7 @@ pattern (::&+)   :: ()   => ( ys ~ (x ': xs)-     , T.KnownT x, Typeable xs+     , SingI x, SingI xs      )   => (Sing x, Notes x, Dict (WellTyped x), VarAnn)   -> HST xs@@ -122,14 +126,14 @@  -- | No-argument type wrapper for @HST@ data type. data SomeHST where-  SomeHST :: Typeable ts => HST ts -> SomeHST+  SomeHST :: SingI ts => HST ts -> SomeHST  deriving stock instance Show SomeHST instance NFData SomeHST where   rnf (SomeHST h) = rnf h  instance Eq SomeHST where-  SomeHST hst1 == SomeHST hst2 = hst1 `eqParam1` hst2+  SomeHST hst1 == SomeHST hst2 = hst1 `eqParamSing` hst2  -- | This data type keeps part of type check result - instruction and -- corresponding output stack.@@ -139,7 +143,7 @@   -- Output stack type is wrapped inside the type and @Typeable@   -- constraint is provided to allow convenient unwrapping.   (:::)-    :: (Typeable out)+    :: SingI out     => Instr inp out     -> HST out     -> SomeInstrOut inp@@ -182,31 +186,12 @@ instance Show (ExtInstr inp) => Show (SomeInstr inp) where   show (inp :/ out) = show inp <> " -> " <> show out -data SomeContract where-  SomeContract :: Contract cp st -> SomeContract--instance NFData SomeContract where-  rnf (SomeContract c) = rnf c- mapSomeContract ::   (forall inp out. Instr inp out -> Instr inp out)   -> SomeContract   -> SomeContract mapSomeContract f (SomeContract fc) = SomeContract $ mapContractCode f fc -deriving stock instance Show SomeContract---- | Represents a typed contract & a storage value of the type expected by the contract.-data SomeContractAndStorage where-  SomeContractAndStorage-    :: forall cp st.-       (StorageScope st, ParameterScope cp)-       => Contract cp st-       -> T.Value st-       -> SomeContractAndStorage--deriving stock instance Show SomeContractAndStorage- -- | Set of variables defined in a let-block. data BoundVars = BoundVars (Map Var Ty) (Maybe SomeHST) @@ -217,12 +202,14 @@ type TcExtFrames = [BoundVars]  -- | Error type for when a value is not well-typed.-data NotWellTyped = NotWellTyped T+data NotWellTyped = NotWellTyped+  { nwtBadType :: T+  , nwtCause :: T.BadTypeForScope+  }  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"+  build (NotWellTyped t c) =+    "Given type is not well typed because '" <> (build t) <> "' " <> (build c)  fromEDict :: Either e (Dict a) -> (a => Either e (Dict b)) -> Either e (Dict b) fromEDict ma b = ma >>= (\Dict -> b)@@ -235,30 +222,62 @@   STUnit -> Right Dict   STSignature -> Right Dict   STChainId -> Right Dict-  STOption s -> fromEDict (getWTP_ s) (Right Dict)-  STList s -> fromEDict (getWTP_ s) (Right Dict)+  STOption s -> withSingI s $ fromEDict (getWTP_ s) (Right Dict)+  STList s -> withSingI s $ fromEDict (getWTP_ s) (Right Dict)   STSet (s :: Sing si) ->+    withSingI s $     fromEDict (getWTP_ s) $     fromEDict-        ( maybeToRight (NotWellTyped $ demote @si) $ T.getComparableProofS s+        ( maybeToRight (NotWellTyped (demote @si) T.BtNotComparable) $ T.getComparableProofS s         ) $ Right Dict   STOperation  -> Right Dict-  STContract s -> fromEDict (getWTP_ s) (Right Dict)-  STPair s1 s2 -> fromEDict (getWTP_ s1) $ fromEDict (getWTP_ s2) $ Right Dict-  STOr s1 s2 -> fromEDict (getWTP_ s1) $ fromEDict (getWTP_ s2) $ Right Dict-  STLambda s1 s2 -> fromEDict (getWTP_ s1) $ fromEDict (getWTP_ s2) $ Right Dict+  STContract (s :: Sing si) ->+    withSingI s $ fromEDict (getWTP_ s) $+    fromEDict+        ( maybeToRight (NotWellTyped (demote @si) T.BtIsOperation) $ T.opAbsense s+        ) $ Right Dict++  STTicket (s :: Sing si) ->+    withSingI s $ fromEDict (getWTP_ s) $+    fromEDict+        ( maybeToRight (NotWellTyped (demote @si) T.BtNotComparable) $ T.getComparableProofS s+        ) $ Right Dict+  STPair s1 s2 ->+    withSingI s1 $+    withSingI s2 $+    fromEDict (getWTP_ s1) $+    fromEDict (getWTP_ s2) $ Right Dict+  STOr s1 s2 ->+    withSingI s1 $+    withSingI s2 $+    fromEDict (getWTP_ s1) $+    fromEDict (getWTP_ s2) $ Right Dict+  STLambda s1 s2 ->+    withSingI s1 $+    withSingI s2 $+    fromEDict (getWTP_ s1) $ fromEDict (getWTP_ s2) $ Right Dict   STMap (s1 :: Sing si) s2 ->+      withSingI s1 $+      withSingI s2 $       fromEDict (getWTP_ s1) $       fromEDict (getWTP_ s2) $       fromEDict-        ( maybeToRight (NotWellTyped $ demote @si) $ T.getComparableProofS s1+        ( maybeToRight (NotWellTyped (demote @si) T.BtNotComparable) $ T.getComparableProofS s1         ) $ Right Dict-  STBigMap (s1 :: Sing si) s2 ->+  STBigMap (s1 :: Sing si) (s2 :: Sing si2) ->+      withSingI s1 $+      withSingI s2 $       fromEDict (getWTP_ s1) $       fromEDict (getWTP_ s2) $       fromEDict-        ( maybeToRight (NotWellTyped $ demote @si) $ T.getComparableProofS s1-        ) $ Right Dict+      ( maybeToRight (NotWellTyped (demote @si) T.BtNotComparable) $ T.getComparableProofS s1+      ) $+      fromEDict+      ( maybeToRight (NotWellTyped (demote @si2) T.BtIsOperation) $ T.opAbsense s2+      ) $+      fromEDict+      ( maybeToRight (NotWellTyped (demote @si2) T.BtHasBigMap) $ T.bigMapAbsense s2+      ) $ Right Dict   STInt -> Right Dict   STNat -> Right Dict   STString -> Right Dict@@ -272,9 +291,10 @@   STTimestamp -> Right Dict   STAddress -> Right Dict   STNever -> Right Dict-  where-    getWTP_ :: forall t1. SingI t1 => Sing t1 -> Either NotWellTyped (Dict (WellTyped t1))-    getWTP_ _ = getWTP @t1++-- | Version of 'getWTP' that accepts 'Sing' at term-level.+getWTP_ :: forall t. Sing t -> Either NotWellTyped (Dict (WellTyped t))+getWTP_ s = withSingI s $ getWTP @t  -- | Given a type and an action that requires evidence that the type is well typed, --  generate the evidence and execute the action, or else fail with an error.