morley 1.16.0 → 1.16.1

raw patch · 58 files changed

+2133/−715 lines, 58 filesdep +crypto-sodiumPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: crypto-sodium

API changes (from Hackage documentation)

Files

• CHANGES.md +19/−0
• app/Main.hs +22/−1
• morley.cabal +10/−1
• src/Morley/CLI.hs +16/−0
• src/Morley/Micheline/Binary.hs +1/−63
• src/Morley/Micheline/Binary/Internal.hs +117/−0
• src/Morley/Micheline/Class.hs +51/−13
• src/Morley/Micheline/Expression.hs +5/−1
• src/Morley/Michelson/Interpret.hs +59/−12
• src/Morley/Michelson/Macro.hs +11/−4
• src/Morley/Michelson/Optimizer.hs +1/−1
• src/Morley/Michelson/Parser.hs +18/−17
• src/Morley/Michelson/Parser/Common.hs +22/−0
• src/Morley/Michelson/Parser/Error.hs +4/−1
• src/Morley/Michelson/Parser/Instr.hs +14/−3
• src/Morley/Michelson/Parser/Macro.hs +1/−1
• src/Morley/Michelson/Parser/Type.hs +9/−0
• src/Morley/Michelson/Runtime.hs +3/−9
• src/Morley/Michelson/Runtime/Import.hs +1/−1
• src/Morley/Michelson/TypeCheck/Error.hs +7/−2
• src/Morley/Michelson/TypeCheck/Helpers.hs +19/−1
• src/Morley/Michelson/TypeCheck/Instr.hs +537/−462
• src/Morley/Michelson/TypeCheck/TypeCheckedOp.hs +11/−0
• src/Morley/Michelson/TypeCheck/TypeCheckedSeq.hs +2/−1
• src/Morley/Michelson/TypeCheck/Types.hs +3/−0
• src/Morley/Michelson/TypeCheck/Value.hs +11/−0
• src/Morley/Michelson/Typed.hs +2/−0
• src/Morley/Michelson/Typed/Aliases.hs +16/−0
• src/Morley/Michelson/Typed/Annotation.hs +10/−0
• src/Morley/Michelson/Typed/Contract.hs +116/−0
• src/Morley/Michelson/Typed/Convert.hs +31/−1
• src/Morley/Michelson/Typed/Doc.hs +2/−0
• src/Morley/Michelson/Typed/Existential.hs +0/−1
• src/Morley/Michelson/Typed/Extract.hs +8/−0
• src/Morley/Michelson/Typed/Haskell/Doc.hs +28/−9
• src/Morley/Michelson/Typed/Haskell/Value.hs +14/−1
• src/Morley/Michelson/Typed/Instr.hs +16/−61
• src/Morley/Michelson/Typed/OpSize.hs +1/−0
• src/Morley/Michelson/Typed/Operation.hs +2/−2
• src/Morley/Michelson/Typed/Polymorphic.hs +4/−0
• src/Morley/Michelson/Typed/Scope.hs +40/−0
• src/Morley/Michelson/Typed/T.hs +4/−0
• src/Morley/Michelson/Typed/Util.hs +20/−2
• src/Morley/Michelson/Typed/Value.hs +19/−21
• src/Morley/Michelson/Typed/View.hs +168/−0
• src/Morley/Michelson/Untyped.hs +1/−0
• src/Morley/Michelson/Untyped/Aliases.hs +2/−0
• src/Morley/Michelson/Untyped/Contract.hs +50/−16
• src/Morley/Michelson/Untyped/Instr.hs +5/−0
• src/Morley/Michelson/Untyped/OpSize.hs +19/−1
• src/Morley/Michelson/Untyped/Type.hs +4/−0
• src/Morley/Michelson/Untyped/View.hs +109/−0
• src/Morley/Tezos/Crypto.hs +11/−0
• src/Morley/Tezos/Crypto/BLS12381.hs +2/−2
• src/Morley/Tezos/Crypto/Timelock.hs +430/−0
• src/Morley/Util/Sing.hs +25/−1
• src/Morley/Util/Type.hs +0/−1
• src/Morley/Util/Typeable.hs +0/−2

@@ -1,5 +1,24 @@ <!-- Unreleased: append new entries here --> +1.16.1+======+* [!1016](https://gitlab.com/morley-framework/morley/-/merge_requests/1016)+  + Add support for on-chain views.+  + The old `VIEW` macro for A1 (aka TZIP-4) views support was renamed to `VIEW_` (A1/TZIP-4).+* [!1010](https://gitlab.com/morley-framework/morley/-/merge_requests/1010)+  Add timelock puzzle support.+  + Binary encoding primitives moved to `Morley.Micheline.Binary.Internal`+  and exposed from there.+  + Added binary encoding primitives for nonnegative integers `buildNatural`+  and `getNatural`.+  + Added timelock puzzle algorithms to `Morley.Tezos.Crypto.Timelock`+  + Added support for `chest` and `chest_key` types. Those are represented+  by `TChest` and `TChestKey` in Haskell.+  + Added support for `OPEN_CHEST` instruction+  + Added `create_chest` command to Morley CLI to create a timelocked chest+  from user-supplied parameters. This isn't necessarily cryptographically safe+  (it was neither written nor audited by security experts), and is primarily+  intended for testing purposes.  1.16.0 ======

@@ -15,6 +15,7 @@ import qualified Options.Applicative as Opt import Options.Applicative.Help.Pretty (Doc, linebreak) import Paths_morley (version)+import Text.Hex (encodeHex)  import Morley.CLI import Morley.Michelson.Analyzer (analyze)@@ -26,11 +27,12 @@ import Morley.Michelson.TypeCheck (tcVerbose, typeCheckContract, typeCheckingWith) import qualified Morley.Michelson.TypeCheck as TypeCheck import Morley.Michelson.TypeCheck.Types (mapSomeContract)-import Morley.Michelson.Typed (Contract(..), SomeContract(..))+import Morley.Michelson.Typed (Contract'(..), SomeContract(..)) import qualified Morley.Michelson.Untyped as U import Morley.Tezos.Address (Address) import Morley.Tezos.Core (Mutez, Timestamp(..), toMutez) import Morley.Tezos.Crypto+import Morley.Tezos.Crypto.Timelock (chestBytes, chestKeyBytes, createChestAndChestKey) import Morley.Util.CLI (mkCommandParser, outputOption) import Morley.Util.Main (wrapMain) import Morley.Util.Named@@ -48,6 +50,7 @@   | Run RunOptions   | Originate OriginateOptions   | Transfer TransferOptions+  | CreateChest CreateChestOptions   | REPL  data OptimizeOptions = OptimizeOptions@@ -60,6 +63,11 @@   { aoContractFile :: Maybe FilePath   } +data CreateChestOptions = CreateChestOptions+  { ccPayload :: ByteString+  , ccTime :: TLTime+  }+ data TypeCheckOptions = TypeCheckOptions   { tcoContractFile :: Maybe FilePath   , tcoTcOptions    :: TypeCheck.TypeCheckOptions@@ -111,6 +119,7 @@   transferSubCmd <>   optimizeSubCmd <>   analyzeSubCmd <>+  createChestSubCmd <>   replSubCmd   where     typecheckSubCmd =@@ -157,6 +166,11 @@       (Analyze <$> analyzeOptions)       "Analyze the contract." +    createChestSubCmd =+      mkCommandParser "create_chest"+      (CreateChest <$> createChestOptions)+      "Create a timelocked chest and key."+     verboseFlag :: Opt.Parser Bool     verboseFlag = switch $       short 'v' <>@@ -199,6 +213,9 @@     analyzeOptions :: Opt.Parser AnalyzeOptions     analyzeOptions = AnalyzeOptions <$> optional contractFileOption +    createChestOptions :: Opt.Parser CreateChestOptions+    createChestOptions = CreateChestOptions <$> payloadOption <*> timeOption+     runOptions :: Opt.Parser RunOptions     runOptions =       RunOptions@@ -330,6 +347,10 @@           ! #verbose toVerbose           ! #dryRun toDryRun       REPL -> runRepl+      CreateChest CreateChestOptions {..} -> do+        (chest, key) <- createChestAndChestKey ccPayload ccTime+        putStrLn $ "Chest: 0x" <> encodeHex (chestBytes chest)+        putStrLn $ "Key: 0x" <> encodeHex (chestKeyBytes key)   usageDoc :: Maybe Doc

@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           morley-version:        1.16.0+version:        1.16.1 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@@ -40,6 +40,7 @@       Morley.CLI       Morley.Micheline       Morley.Micheline.Binary+      Morley.Micheline.Binary.Internal       Morley.Micheline.Class       Morley.Micheline.Expression       Morley.Micheline.Json@@ -56,6 +57,7 @@       Morley.Michelson.Optimizer       Morley.Michelson.Parser       Morley.Michelson.Parser.Annotations+      Morley.Michelson.Parser.Common       Morley.Michelson.Parser.Error       Morley.Michelson.Parser.Ext       Morley.Michelson.Parser.Helpers@@ -89,6 +91,7 @@       Morley.Michelson.Typed.Aliases       Morley.Michelson.Typed.Annotation       Morley.Michelson.Typed.Arith+      Morley.Michelson.Typed.Contract       Morley.Michelson.Typed.Convert       Morley.Michelson.Typed.Doc       Morley.Michelson.Typed.Entrypoints@@ -114,6 +117,7 @@       Morley.Michelson.Typed.TypeLevel       Morley.Michelson.Typed.Util       Morley.Michelson.Typed.Value+      Morley.Michelson.Typed.View       Morley.Michelson.Untyped       Morley.Michelson.Untyped.Aliases       Morley.Michelson.Untyped.Annotation@@ -124,6 +128,7 @@       Morley.Michelson.Untyped.OpSize       Morley.Michelson.Untyped.Type       Morley.Michelson.Untyped.Value+      Morley.Michelson.Untyped.View       Morley.Tezos.Address       Morley.Tezos.Core       Morley.Tezos.Crypto@@ -132,6 +137,7 @@       Morley.Tezos.Crypto.Hash       Morley.Tezos.Crypto.P256       Morley.Tezos.Crypto.Secp256k1+      Morley.Tezos.Crypto.Timelock       Morley.Tezos.Crypto.Util       Morley.Util.Aeson       Morley.Util.Binary@@ -199,6 +205,7 @@       PatternSynonyms       PolyKinds       QuasiQuotes+      QuantifiedConstraints       RankNTypes       RecordWildCards       RecursiveDo@@ -225,6 +232,7 @@     , bytestring     , constraints >=0.11     , containers+    , crypto-sodium >=0.0.5.0     , cryptonite     , data-default     , elliptic-curve@@ -305,6 +313,7 @@       PatternSynonyms       PolyKinds       QuasiQuotes+      QuantifiedConstraints       RankNTypes       RecordWildCards       RecursiveDo

@@ -24,6 +24,8 @@   , onelineOption   , entrypointOption   , mTextOption+  , payloadOption+  , timeOption   ) where  import Options.Applicative@@ -77,6 +79,20 @@   long "contract" <>   metavar "FILEPATH" <>   help "Path to contract file"++-- | Parser for timelocked chest payload.+payloadOption :: Opt.Parser ByteString+payloadOption = strOption $+  long "payload" <>+  metavar "PAYLOAD" <>+  help "Chest payload"++-- | Parser for timelocked chest time.+timeOption :: Opt.Parser TLTime+timeOption = mkCLOptionParser+  Nothing+  (#name :! "time")+  (#help :! "Time constant for timelocked chest")  -- | Parser for the time returned by @NOW@ instruction. nowOption :: Opt.Parser (Maybe Timestamp)

@@ -15,18 +15,15 @@  import qualified Data.Binary.Builder as Bi import qualified Data.Binary.Get as Bi-import Data.Bits (Bits, bit, setBit, shift, testBit, zeroBits, (.&.), (.|.)) import qualified Data.ByteString as BS import qualified Data.ByteString.Lazy as LBS import qualified Data.Sequence as Seq-import qualified Data.Text.Encoding as TE import qualified Unsafe (fromIntegral) +import Morley.Micheline.Binary.Internal import Morley.Micheline.Expression import Morley.Util.Binary (UnpackError(..), ensureEnd, launchGet) -newtype DynamicSize a = DynamicSize { unDynamicSize :: a }- ------------------------------------------------- -- Encode -------------------------------------------------@@ -54,36 +51,6 @@   ExpressionInt x -> buildWord8 0 <> buildInteger x   ExpressionBytes x -> buildWord8 10 <> buildDynamic buildByteString (DynamicSize x) -buildWord8 :: Word8 -> Bi.Builder-buildWord8 = Bi.singleton--buildByteString :: ByteString -> Bi.Builder-buildByteString = Bi.fromByteString--buildInteger :: Integer -> Bi.Builder-buildInteger n =-  let signBit = if n < 0 then bit 6 else zeroBits-      ab = abs n-  in-    -- Refer to: https://gitlab.com/obsidian.systems/tezos-bake-monitor-lib/-/blob/2cf12e53072bcd966d471430ead25f597db5e23f/tezos-bake-monitor-lib/src/Tezos/Common/Binary.hs#L122-    if ab < 0x40 then Bi.singleton (Unsafe.fromIntegral @Integer @Word8 ab .|. signBit)-    else Bi.singleton (Unsafe.fromIntegral @Integer @Word8 (ab .&. 0x3f) .|. signBit .|. bit 7) <> writeZ (-6) ab--writeZ :: forall a. (Integral a, Bits a) => Int -> a -> Bi.Builder-writeZ offset n =-  if n < bit (7 - offset) then Bi.singleton $ Unsafe.fromIntegral @a @Word8 $ n `shift` offset-    else Bi.singleton (Unsafe.fromIntegral @a @Word8 (((n `shift` offset) .&. 0x7f) `setBit` 7)) <> writeZ (offset - 7) n--buildDynamic :: (a -> Bi.Builder) -> (DynamicSize a) -> Bi.Builder-buildDynamic build (DynamicSize x) =-  let b = build x-  in Bi.putWord32be (Unsafe.fromIntegral @Int64 @Word32 $ LBS.length $ Bi.toLazyByteString b) <> b---buildText :: Text -> Bi.Builder-buildText n =-  buildByteString $ TE.encodeUtf8 n- buildList :: [Expression] -> Bi.Builder buildList = foldMap buildExpr @@ -121,35 +88,6 @@   9 -> ExpressionPrim <$> (MichelinePrimAp <$> getPrim <*> (unDynamicSize <$> (getDynamic getList)) <*> getAnnotationList)   10 -> ExpressionBytes . unDynamicSize <$> (getDynamic getByteString)   _ -> fail "invalid Micheline expression tag"--getInteger :: Bi.Get Integer-getInteger = do-  b <- Bi.getWord8-  n <- if b `testBit` 7 then readZ 6 (fromIntegral $ b .&. 0x3f) else pure (fromIntegral $ b .&. 0x3f)-  pure $ if b `testBit` 6 then negate n else n--readZ :: forall a. (Integral a, Bits a) => Int -> a -> Bi.Get a-readZ offset n = do-  b <- Bi.getWord8-  if (b == 0) && (offset > 0) then fail "trailing zero" else pure ()-  let n' = (Unsafe.fromIntegral @Word8 @a (b .&. 0x7f) `shift` offset) .|. n-  if b `testBit` 7 then readZ (offset + 7) n' else pure n'--getDynamic :: (Bi.Get a) -> (Bi.Get (DynamicSize a))-getDynamic getter = do-  len <- Unsafe.fromIntegral @Word32 @Int <$> Bi.getWord32be-  DynamicSize <$> Bi.isolate len getter--{-# ANN getText ("HLint: ignore Redundant fmap" :: Text) #-}-getText :: Bi.Get Text-getText =-  fmap decodeUtf8' getByteString >>= \case-    Left err -> fail $ show err-    Right answer -> pure answer--getByteString :: Bi.Get ByteString-getByteString =-  LBS.toStrict <$> Bi.getRemainingLazyByteString  getList :: Bi.Get [Expression] getList = many getExpr

@@ -0,0 +1,117 @@+-- SPDX-FileCopyrightText: 2021 Tocqueville Group+-- SPDX-FileCopyrightText: 2018 obsidian.systems+--+-- SPDX-License-Identifier: LicenseRef-MIT-TQ+-- SPDX-License-Identifier: LicenseRef-MIT-obsidian-systems++-- | Defines binary encoding primitives which mimic Tezos' binary encoding.+module Morley.Micheline.Binary.Internal+  ( DynamicSize(..)++  -- * Encode+  , buildWord8+  , buildText+  , buildInteger+  , buildNatural+  , buildDynamic+  , buildByteString++  -- * Decode+  , getText+  , getNatural+  , getInteger+  , getDynamic+  , getByteString+  ) where++import Control.Exception (assert)+import qualified Data.Binary.Builder as Bi+import qualified Data.Binary.Get as Bi+import Data.Bits (Bits, bit, setBit, shift, testBit, zeroBits, (.&.), (.|.))+import qualified Data.ByteString.Lazy as LBS+import qualified Data.Text.Encoding as TE+import qualified Unsafe (fromIntegral)++newtype DynamicSize a = DynamicSize { unDynamicSize :: a }++-------------------------------------------------+-- Encode+-------------------------------------------------++buildWord8 :: Word8 -> Bi.Builder+buildWord8 = Bi.singleton++buildByteString :: ByteString -> Bi.Builder+buildByteString = Bi.fromByteString++buildInteger :: Integer -> Bi.Builder+buildInteger n =+  let signBit = if n < 0 then bit 6 else zeroBits+      ab = abs n+  in+    -- Refer to: https://gitlab.com/obsidian.systems/tezos-bake-monitor-lib/-/blob/2cf12e53072bcd966d471430ead25f597db5e23f/tezos-bake-monitor-lib/src/Tezos/Common/Binary.hs#L122+    if ab < 0x40 then Bi.singleton (Unsafe.fromIntegral @Integer @Word8 ab .|. signBit)+    else Bi.singleton (Unsafe.fromIntegral @Integer @Word8 (ab .&. 0x3f) .|. signBit .|. bit 7) <> writeZ (-6) ab++writeZ :: forall a. (Integral a, Bits a) => Int -> a -> Bi.Builder+writeZ offset n =+  if n < bit (7 - offset) then Bi.singleton $ Unsafe.fromIntegral @a @Word8 $ n `shift` offset+    else Bi.singleton (Unsafe.fromIntegral @a @Word8 (((n `shift` offset) .&. 0x7f) `setBit` 7)) <> writeZ (offset - 7) n++-- | Build a binary representation of a Zarith natural. This function is+-- partial, only defined for nonnegative 'Integer's.+--+-- The reason it's not defined to accept a 'Natural' is mostly to avoid+-- 'fromIntegral'/'toInteger' conversions at the use sites, since+-- not all libraries, notably @cryptonite@, support 'Natural'.+buildNatural :: Integer -> Bi.Builder+buildNatural n = assert (n >= 0) $+  if n < 0x80 then Bi.singleton (Unsafe.fromIntegral @Integer @Word8 n)+  else Bi.singleton (Unsafe.fromIntegral @Integer @Word8 (n .&. 0xff) .|. bit 7) <> writeZ (-7) n++buildDynamic :: (a -> Bi.Builder) -> (DynamicSize a) -> Bi.Builder+buildDynamic build (DynamicSize x) =+  let b = build x+  in Bi.putWord32be (Unsafe.fromIntegral @Int64 @Word32 $ LBS.length $ Bi.toLazyByteString b) <> b++buildText :: Text -> Bi.Builder+buildText n =+  buildByteString $ TE.encodeUtf8 n++-------------------------------------------------+-- Decode+-------------------------------------------------++getInteger :: Bi.Get Integer+getInteger = do+  b <- Bi.getWord8+  n <- if b `testBit` 7 then readZ 6 (fromIntegral $ b .&. 0x3f) else pure (fromIntegral $ b .&. 0x3f)+  pure $ if b `testBit` 6 then negate n else n++getNatural :: Bi.Get Integer+getNatural = do+  b <- Bi.getWord8+  if b `testBit` 7 then readZ 7 (fromIntegral $ b .&. 0x7f) else pure (fromIntegral $ b .&. 0x7f)++readZ :: forall a. (Integral a, Bits a) => Int -> a -> Bi.Get a+readZ offset n = do+  b <- Bi.getWord8+  if (b == 0) && (offset > 0) then fail "trailing zero" else pure ()+  let n' = (Unsafe.fromIntegral @Word8 @a (b .&. 0x7f) `shift` offset) .|. n+  if b `testBit` 7 then readZ (offset + 7) n' else pure n'++getDynamic :: (Bi.Get a) -> (Bi.Get (DynamicSize a))+getDynamic getter = do+  len <- Unsafe.fromIntegral @Word32 @Int <$> Bi.getWord32be+  DynamicSize <$> Bi.isolate len getter++{-# ANN getText ("HLint: ignore Redundant fmap" :: Text) #-}+getText :: Bi.Get Text+getText =+  fmap decodeUtf8' getByteString >>= \case+    Left err -> fail $ show err+    Right answer -> pure answer++getByteString :: Bi.Get ByteString+getByteString =+  LBS.toStrict <$> Bi.getRemainingLazyByteString

@@ -24,8 +24,8 @@   (TypeCheckMode(..), TypeCheckOptions(..), runTypeCheck, typeCheckingWith) import Morley.Michelson.TypeCheck.Instr (typeCheckValue) import Morley.Michelson.Typed-  (Contract(..), HasNoOp, Instr, Notes(..), T(..), Value, Value'(..), fromUType, mkUType,-  rfAnyInstr, toUType)+  (Contract, HasNoOp, Instr, Notes(..), T(..), Value, Value'(..), fromUType, mkUType, rfAnyInstr,+  toUType) import Morley.Michelson.Typed.Convert (convertContract, instrToOpsOptimized, untypeValueOptimized) import qualified Morley.Michelson.Untyped as Untyped import Morley.Michelson.Untyped.Annotation@@ -34,6 +34,7 @@ import Morley.Michelson.Untyped.Contract (ContractBlock(..), orderContractBlock) import Morley.Michelson.Untyped.Instr (ExpandedInstr, ExpandedOp(..), InstrAbstract(..)) import Morley.Michelson.Untyped.Type (Ty(..))+import Morley.Michelson.Untyped.View  -- | Type class that provides an ability to convert -- something to Micheline Expression.@@ -112,6 +113,8 @@     Untyped.TBls12381G2 -> PrimExpr "bls12_381_g2" [] []     Untyped.TTimestamp -> PrimExpr "timestamp" [] []     Untyped.TAddress -> PrimExpr "address" [] []+    Untyped.TChest -> PrimExpr "chest" [] []+    Untyped.TChestKey -> PrimExpr "chest_key" [] []     Untyped.TNever -> PrimExpr "never" [] []      where@@ -147,6 +150,9 @@     SeqEx s        -> ExpressionSeq $ toExpression <$> s     WithSrcEx _ op -> toExpression op +instance ToExpression ViewName where+  toExpression (ViewName s) = ExpressionString s+ instance ToExpression ExpandedInstr where   toExpression = \case     PUSH va ty v -> PrimExpr "PUSH" [toExpression ty, toExpression v] $@@ -241,6 +247,8 @@     LE va -> PrimExpr "LE" [] $ mkAnns [] [] [va]     GE va -> PrimExpr "GE" [] $ mkAnns [] [] [va]     INT va -> PrimExpr "INT" [] $ mkAnns [] [] [va]+    VIEW va n t -> PrimExpr "VIEW" [toExpression n, toExpression t] $+      mkAnns [] [] [va]     SELF va fa -> PrimExpr "SELF" [] $ mkAnns [] [fa] [va]     CONTRACT va fa ty -> PrimExpr "CONTRACT" [toExpression ty] $       mkAnns [] [fa] [va]@@ -275,6 +283,7 @@     READ_TICKET va -> PrimExpr "READ_TICKET" [] $ mkAnns [] [] [va]     SPLIT_TICKET va -> PrimExpr "SPLIT_TICKET" [] $ mkAnns [] [] [va]     JOIN_TICKETS va -> PrimExpr "JOIN_TICKETS" [] $ mkAnns [] [] [va]+    OPEN_CHEST va -> PrimExpr "OPEN_CHEST" [] $ mkAnns [] [] [va]     NEVER -> PrimExpr "NEVER" [] []     EXT _ -> ExpressionSeq []     where@@ -288,6 +297,9 @@             [insertRootAnn (toExpression ty) rootAnn] [])           (\storage -> PrimExpr "storage" [toExpression storage] [])           (\code -> PrimExpr "code" [toExpression code] [])+          (\Untyped.View{..} -> PrimExpr "view"+            [toExpression viewName, toExpression viewArgument, toExpression viewReturn, toExpression viewCode] []+          )  instance ToExpression (Contract cp st) where   toExpression = toExpression . convertContract@@ -614,6 +626,11 @@     PrimExpr "LE" [] anns -> mkInstrWithVarAnn LE anns     PrimExpr "GE" [] anns -> mkInstrWithVarAnn GE anns     PrimExpr "INT" [] anns -> mkInstrWithVarAnn INT anns+    PrimExpr "VIEW" [name, t] _ -> do+      let va = firstAnn @VarTag annSet+      name' <- fromExpression @ViewName name+      t' <- fromExpression @Ty t+      checkAnnsCount e annSet (0, 0, 1) $> VIEW va name' t'     PrimExpr "SELF" [] _ ->       let fa = firstAnn @FieldTag annSet           va = firstAnn @VarTag annSet@@ -694,13 +711,11 @@  instance FromExpression Untyped.Contract where   fromExpression blocks = case blocks of-    ExpressionSeq [b1, b2, b3] -> do-      b1' <- exprToCB b1-      b2' <- exprToCB b2-      b3' <- exprToCB b3-      maybeToRight (FromExpressionError blocks fullErrorMsg)-        (orderContractBlock (b1', b2', b3'))-    expr -> Left $ FromExpressionError expr fullErrorMsg+    ExpressionSeq bs -> do+      bs' <- mapM exprToCB bs+      maybeToRight (FromExpressionError blocks "Something's wrong with top-level contract blocks")+        (orderContractBlock bs')+    expr -> Left $ FromExpressionError expr "Failed to parse contract, expected sequence"     where       exprToCB         :: Expression@@ -709,7 +724,9 @@         PrimExpr "parameter" args anns -> mkCbParam e args anns         PrimExpr "storage"   args anns -> mkCBStorage e args anns         PrimExpr "code"      args anns -> mkCBCode e args anns-        _                              -> Left $ FromExpressionError e fullErrorMsg+        PrimExpr "view"      args anns -> mkCBView e args anns+        _                              ->+          Left $ FromExpressionError e "Unexpected primitive at contract top-level"        mkCbParam         :: Expression@@ -753,9 +770,24 @@         _ -> Left $ FromExpressionError e                "Expected 'code' block without annotations" -      fullErrorMsg = "Expected contract expression to have exactly 3 " <>-        "sub-expressions ('parameter', 'storage' and 'code')"-+      mkCBView+        :: Expression+        -> [Expression]+        -> [Annotation]+        -> Either FromExpressionError (ContractBlock ExpandedOp)+      mkCBView e args anns = case (args, anns) of+        ([name, arg, ret, ops], []) -> do+          name' <- fromExpression name+          arg' <- fromExpression arg+          ret' <- fromExpression ret+          ops' <- fromExpression @[ExpandedOp] ops+          pure $ CBView $ Untyped.View name' arg' ret' ops'+        (_, _ : _) ->+          Left $ FromExpressionError e+               "Expected 'view' block without annotations"+        (_, []) ->+          Left $ FromExpressionError e+               "Invalid 'view' block, expected 4 expressions in it"  instance FromExpression Untyped.T where   fromExpression e = case e of@@ -870,6 +902,12 @@   fromExpression expr =     fromExpression @(Value ('TLambda inp out)) expr <&> \case       VLam instr -> rfAnyInstr instr++instance FromExpression ViewName where+  fromExpression e = case e of+    ExpressionString s ->+      first (FromExpressionError e . pretty) $ mkViewName s+    _ -> Left $ FromExpressionError e "Expected view name"  ---------------------------------------------------------------------------- -- Helpers

@@ -77,6 +77,9 @@   --   -- > ./scripts/get-micheline-exprs.sh   --+  -- or find the full primitives list in the <https://gitlab.com/tezos/tezos/blob/master/src/proto_alpha/lib_protocol/michelson_v1_primitives.ml | sources>,+  -- see "prim_encoding" variable.+  --   "parameter", "storage", "code", "False", "Elt", "Left", "None", "Pair",   "Right", "Some", "True", "Unit", "PACK", "UNPACK", "BLAKE2B", "SHA256",   "SHA512", "ABS", "ADD", "AMOUNT", "AND", "BALANCE", "CAR", "CDR",@@ -94,7 +97,8 @@   "DIG", "DUG", "EMPTY_BIG_MAP", "APPLY", "chain_id", "CHAIN_ID", "LEVEL", "SELF_ADDRESS",   "never", "NEVER", "UNPAIR", "VOTING_POWER", "TOTAL_VOTING_POWER", "KECCAK", "SHA3", "PAIRING_CHECK",   "bls12_381_g1", "bls12_381_g2", "bls12_381_fr", "sapling_state", "sapling_transaction", "SAPLING_EMPTY_STATE", "SAPLING_VERIFY_UPDATE", "ticket",-  "TICKET", "READ_TICKET", "SPLIT_TICKET", "JOIN_TICKETS", "GET_AND_UPDATE"+  "TICKET", "READ_TICKET", "SPLIT_TICKET", "JOIN_TICKETS", "GET_AND_UPDATE", "chest", "chest_key", "OPEN_CHEST",+  "VIEW", "view", "constant"   ]  -- | Type for Micheline Expression

@@ -52,6 +52,7 @@ import Data.Default (Default(..)) import qualified Data.Map as Map import qualified Data.Set as Set+import Data.Singletons.Decide (decideEquality) import Data.Vinyl (Rec(..), (<+>)) import Data.Vinyl.Recursive (rmap) import Fmt (Buildable(build), blockListF, pretty, prettyLn)@@ -61,7 +62,7 @@ import Morley.Michelson.Interpret.Pack (packValue') import Morley.Michelson.Interpret.Unpack (UnpackError, unpackValue') import Morley.Michelson.Runtime.GState-import Morley.Michelson.TypeCheck (SomeParamType(..), TcOriginatedContracts, matchTypes)+import Morley.Michelson.TypeCheck (matchTypes) import Morley.Michelson.Typed hiding (Branch(..)) import qualified Morley.Michelson.Typed as T import Morley.Michelson.Typed.Operation@@ -69,8 +70,10 @@ import qualified Morley.Michelson.Untyped as U import Morley.Michelson.Untyped.Annotation (annQ) import Morley.Tezos.Address (Address(..), GlobalCounter(..))-import Morley.Tezos.Core (ChainId, Mutez, Timestamp)-import Morley.Tezos.Crypto (KeyHash, blake2b, checkSignature, hashKey, keccak, sha256, sha3, sha512)+import Morley.Tezos.Core (ChainId, Mutez, Timestamp, zeroMutez)+import Morley.Tezos.Crypto+  (KeyHash, OpeningResult(..), blake2b, checkSignature, hashKey, keccak, mkTLTime, openChest,+  sha256, sha3, sha512) import Morley.Tezos.Crypto.BLS12381 (checkPairing) import Morley.Util.Peano (LongerThan, Peano) import Morley.Util.PeanoNatural (PeanoNatural(..))@@ -144,9 +147,8 @@   -- ^ Number of steps after which execution unconditionally terminates.   , ceBalance :: Mutez   -- ^ Current amount of mutez of the current contract.-  , ceContracts :: TcOriginatedContracts-  -- ^ Mapping from existing contracts' addresses to their executable-  -- representation.+  , ceContracts :: Map Address AddressState+  -- ^ Information stored about the existing contracts.   , ceSelf :: Address   -- ^ Address of the interpreted contract.   , ceSource :: Address@@ -694,6 +696,41 @@   pure $ starNotesStkEl (evalUnaryArithOp (Proxy @Ge) a) :& rest runInstrImpl _ INT (StkEl a _ _ :& r) =   pure $ starNotesStkEl (evalToIntOp a) :& r+runInstrImpl runner (VIEW name (_ :: Notes ret))+                    (StkEl (arg :: Value arg) _ _ :& StkEl (VAddress epAddr) addrVa _ :& r) = do+  ContractEnv{..} <- ask+  res :: Value ('TOption ret) <- VOption <$> runMaybeT do+    let EpAddress addr _ = epAddr+    Just (ASContract viewedContractState) <- pure $ Map.lookup addr ceContracts+    ContractState+      { csContract = viewedContract+      , csStorage = viewedContractStorage+      } <- pure viewedContractState+    Just view_ <- pure $ lookupView name (cViews viewedContract)+    SomeView (View{ vCode } :: View arg' st ret') <- pure view_+    Just Refl <- pure $ sing @arg `decideEquality` sing @arg'+    Just Refl <- pure $ sing @ret `decideEquality` sing @ret'+    resSt <- lift $+      local (mkViewEnv addr viewedContractState) $+        runInstrImpl runner vCode $+          starNotesStkEl (VPair (arg, viewedContractStorage)) :& RNil+    let StkEl res _ _ :& RNil = resSt+    return res+  let newAnn = addrVa <> [annQ|contract|]  -- TODO [#704]: ¯\_(ツ)_/¯+  pure (StkEl res newAnn starNotes :& r)+  where+    mkViewEnv :: Address -> ContractState -> ContractEnv -> ContractEnv+    mkViewEnv calledAddr viewedContractState ContractEnv{..} = ContractEnv+      { ceBalance = csBalance viewedContractState+      , ceSender = ceSelf+      , ceSelf = calledAddr+      , ceSource+      , ceAmount = zeroMutez+      , ceContracts+      , ceNow, ceMaxSteps, ceVotingPowers, ceChainId, ceOperationHash, ceLevel+      , ceInstrCallStack+      }+ runInstrImpl _ (SELF sepc :: Instr inp out) r = do   ContractEnv{..} <- ask   case Proxy @out of@@ -714,10 +751,12 @@     Nothing -> VOption Nothing     Just epName ->       case addr of-        KeyAddress _ -> castContract addr epName T.tyImplicitAccountParam-        ContractAddress ca ->-          case Map.lookup ca ceContracts of-            Just (SomeParamType _ paramNotes) -> castContract addr epName paramNotes+        KeyAddress{} -> castContract addr epName T.tyImplicitAccountParam+        ContractAddress{} ->+          case Map.lookup addr ceContracts of+            Just (ASSimple _) -> error "Broken addresses map"+            Just (ASContract ContractState{..}) ->+              castContract addr epName (cParamNotes csContract)             Nothing -> VOption Nothing   where   castContract@@ -746,7 +785,6 @@   opHash <- ceOperationHash <$> ask   incrementCounter   globalCounter <- isGlobalCounter <$> getInterpreterState-  let ops = cCode contract   let resAddr =         case opHash of           Just hash -> mkContractAddress hash globalCounter@@ -758,7 +796,7 @@               -- operation.               globalCounter   let resEpAddr = EpAddress resAddr DefEpName-  let resOp = CreateContract originator (unwrapMbKeyHash mbKeyHash) m g ops globalCounter+  let resOp = CreateContract originator (unwrapMbKeyHash mbKeyHash) m g contract globalCounter   pure $ starNotesStkEl (VOp (OpCreateContract resOp))       :& starNotesStkEl (VAddress resEpAddr)       :& r@@ -835,6 +873,15 @@         guard (addr1 == addr2)         guard (dat1 == dat2)         return $ VTicket addr1 dat1 (am1 + am2)+  pure $ starNotesStkEl result :& r+runInstrImpl _ OPEN_CHEST+  (StkEl (VChestKey ck) _ _ :& StkEl (VChest c) _ _ :& StkEl (VNat nat) _ _ :& r) = do+  let result = case mkTLTime nat of+        Right time -> case openChest c ck time of+          Correct bytes -> VOr (Left (VBytes bytes))+          BogusOpening  -> VOr (Right (VBool True))+          BogusCipher   -> VOr (Right (VBool False))+        Left _ -> VOr (Right (VBool True))   pure $ starNotesStkEl result :& r  -- | Evaluates an arithmetic operation and either fails or proceeds.

@@ -122,7 +122,8 @@   | ACCESS Natural Positive   | SET Natural Positive   | CONSTRUCT (NonEmpty [ParsedOp])-  | VIEW [ParsedOp]+    -- A1/TZIP4 VIEW, exists for historical reasons+  | VIEW_ [ParsedOp]   | VOID [ParsedOp]   | CMP ParsedInstr VarAnn   | IFX ParsedInstr [ParsedOp] [ParsedOp]@@ -155,7 +156,7 @@     ACCESS idx size -> "<ACCESS: #"+||idx||+"/"+|size|+""     SET idx size -> "<SET: #"+||idx||+"/"+|size|+""     CONSTRUCT parsedInstrs -> "<CONSTRUCT: "+|toList parsedInstrs|+">"-    VIEW code -> "<VIEW: "+|code|+">"+    VIEW_ code -> "<VIEW_: "+|code|+">"     VOID code -> "<VOID: "+|code|+">"     CMP parsedInstr carAnn -> "<CMP: "+|parsedInstr|+", "+|carAnn|+">"     IFX parsedInstr parsedOps1 parsedOps2 -> "<IFX: "+|parsedInstr|+", "+|parsedOps1|+", "+|parsedOps2|+">"@@ -185,10 +186,16 @@ expandList :: [ParsedOp] -> [ExpandedOp] expandList = fmap (expand []) +expandView :: View' ParsedOp -> View+expandView v = v{ viewCode = expandList (viewCode v) }+ -- | Expand all macros in parsed contract. expandContract :: Contract' ParsedOp -> Contract expandContract contract =-  contract { contractCode = expandList (contractCode contract) }+  contract+  { contractCode = expandList (contractCode contract)+  , contractViews = expandView <$> contractViews contract+  }  -- Probably, some SYB can be used here expandValue :: ParsedValue -> Value@@ -238,7 +245,7 @@  expandMacro :: InstrCallStack -> Macro -> [ExpandedOp] expandMacro p@InstrCallStack{icsCallStack=cs,icsSrcPos=macroPos} = \case-  VIEW a             -> [ PrimEx (UNPAIR 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) ++

@@ -20,7 +20,7 @@   , defaultRulesAndPushPack   , orRule   , orSimpleRule-  , Rule+  , Rule (..)   , OptimizerConf (..)   , ocGotoValuesL   ) where

@@ -50,13 +50,14 @@ import qualified Language.Haskell.TH.Quote as TH import Text.Megaparsec   (Parsec, choice, customFailure, eitherP, eof, errorBundlePretty, getSourcePos, hidden, lookAhead,-  parse, try)+  parse, sepEndBy, try) import Text.Megaparsec.Pos (SourcePos(..), unPos)  import Morley.Michelson.ErrorPos (SrcPos(..), unsafeMkPos) import Morley.Michelson.Macro   (LetMacro, Macro(..), ParsedInstr, ParsedOp(..), ParsedValue, expandValue) import Morley.Michelson.Parser.Annotations (noteF)+import Morley.Michelson.Parser.Common import Morley.Michelson.Parser.Error import Morley.Michelson.Parser.Ext import Morley.Michelson.Parser.Instr@@ -120,11 +121,21 @@ cbCode :: Parser [ParsedOp] cbCode = symbol "code" *> codeEntry +cbView :: Parser (View' ParsedOp)+cbView = do+  symbol "view"+  viewName <- viewName_+  viewArgument <- type_+  viewReturn <- type_+  viewCode <- ops+  return View{..}+ contractBlock :: Parser (ContractBlock ParsedOp) contractBlock = choice   [ (CBParam <$> cbParameter)   , (CBStorage <$> cbStorage)   , (CBCode <$> cbCode)+  , (CBView <$> cbView)   ]  -- | This ensures that the error message will point to the correct line.@@ -137,6 +148,7 @@       (CBParam _, CBParam _ : _) -> failDuplicateField "parameter"       (CBStorage _, CBStorage _: _) -> failDuplicateField "storage"       (CBCode _, CBCode _: _) -> failDuplicateField "code"+      (CBView _, _) -> pure ()       (_, _:xs) -> ensureNotDuplicate xs result       (_, []) -> pure () @@ -153,22 +165,11 @@   where     -- | @ensureNotDuplicate@ provides a better message and point to the correct line     -- when the parser fails.-    contractTuple = do-      result1 <- contractBlock-      semicolon--      result2 <- do-        r <- contractBlock-        ensureNotDuplicate [result1] r-        pure r-      semicolon--      result3 <- do-        r <- contractBlock-        ensureNotDuplicate [result1, result2] r-        pure r-      optional semicolon-      pure (result1, result2, result3)+    contractTuple = fmap reverse . executingStateT [] $ do+      (`sepEndBy` lift semicolon) $ do+        r <- lift contractBlock+        get >>= \prev -> lift $ ensureNotDuplicate prev r+        modify (r :)  -- Value ------------------

@@ -0,0 +1,22 @@+-- SPDX-FileCopyrightText: 2021 Tocqueville Group+--+-- SPDX-License-Identifier: LicenseRef-MIT-TQ++module Morley.Michelson.Parser.Common+  ( viewName_+  ) where++import Text.Megaparsec (anySingle, customFailure, manyTill)+import Text.Megaparsec.Char (string)++import Morley.Michelson.Parser.Error+import Morley.Michelson.Parser.Lexer+import Morley.Michelson.Parser.Types+import Morley.Michelson.Untyped++viewName_ :: Parser ViewName+viewName_ = lexeme do+  string "\""+  str <- manyTill anySingle (string "\"")+  mkViewName (toText str)+    & either (customFailure . ViewNameException) pure

@@ -12,15 +12,17 @@   ) where  import Data.Data (Data(..))-import Fmt (Buildable(build), (+|), (|+))+import Fmt (Buildable(build), pretty, (+|), (|+)) import Text.Megaparsec (ParseErrorBundle, ShowErrorComponent(..), errorBundlePretty) import qualified Text.Show (show) +import Morley.Michelson.Untyped.View import Morley.Util.Instances () import Morley.Util.Positive  data CustomParserException   = StringLiteralException StringLiteralParserException+  | ViewNameException BadViewNameError   | OddNumberBytesException   | WrongTagArgs Natural Positive   | WrongAccessArgs Natural Positive@@ -33,6 +35,7 @@  instance ShowErrorComponent CustomParserException where   showErrorComponent (StringLiteralException e) = showErrorComponent e+  showErrorComponent (ViewNameException e) = pretty e   showErrorComponent OddNumberBytesException = "odd number bytes"   showErrorComponent ExcessFieldAnnotation = "excess field annotation"   showErrorComponent MultiRootAnnotationException = "unexpected multiple root annotations"

@@ -20,12 +20,13 @@  import Prelude hiding (EQ, GT, LT, many, note, some, try) -import Text.Megaparsec (choice, label, notFollowedBy, sepEndBy, try)+import Text.Megaparsec (choice, label, lookAhead, notFollowedBy, satisfy, sepEndBy, try) import qualified Text.Megaparsec.Char.Lexer as L  import Morley.Michelson.Let (LetValue(..)) import Morley.Michelson.Macro (ParsedInstr, ParsedOp(..)) import Morley.Michelson.Parser.Annotations+import Morley.Michelson.Parser.Common import Morley.Michelson.Parser.Lexer import Morley.Michelson.Parser.Type import Morley.Michelson.Parser.Types (Parser, letValues)@@ -42,7 +43,7 @@   , lambdaOp opParser, execOp, applyOp, dipOp opParser, failWithOp, castOp, renameOp, levelOp   , concatOp, packOp, unpackOp, sliceOp, isNatOp, addressOp, selfAddressOp, addOp, subOp   , mulOp, edivOp, absOp, negOp, lslOp, lsrOp, orOp, andOp, xorOp, notOp-  , compareOp, eqOp, neqOp, ltOp, leOp, gtOp, geOp, intOp, selfOp, contractOp+  , compareOp, eqOp, neqOp, ltOp, leOp, gtOp, geOp, intOp, viewOp, selfOp, contractOp   , transferTokensOp, setDelegateOp   , createContractOp contractParser, implicitAccountOp, nowOp, amountOp   , balanceOp, checkSigOp, sha256Op, sha512Op, blake2BOp, hashKeyOp, pairingCheckOp@@ -50,6 +51,7 @@   , votingPowerOp, totalVotingPowerOp, try unpairNOp   , unpairOp   , ticketOp, readTicketOp, splitTicketOp, joinTicketsOp+  , openChestOp   ]  -- | Parse a sequence of instructions.@@ -179,7 +181,7 @@ mulOp = word' "MUL" MUL <*> noteDef  edivOp :: Parser ParsedInstr-edivOp = word' "EDIV"EDIV <*> noteDef+edivOp = word' "EDIV" EDIV <*> noteDef  absOp :: Parser ParsedInstr absOp = word' "ABS" ABS <*> noteDef@@ -360,6 +362,12 @@ implicitAccountOp :: Parser ParsedInstr implicitAccountOp = word' "IMPLICIT_ACCOUNT" IMPLICIT_ACCOUNT <*> noteDef +viewOp :: Parser ParsedInstr+viewOp =+  -- @VIEW_@ A1 macro should not be parsed by this+  -- TODO [#557] this 'lookAhead' and 'try' should become unnecessary+  try (word' "VIEW" VIEW <* lookAhead (satisfy (/= '_'))) <*> noteDef <*> viewName_ <*> type_+ selfOp :: Parser ParsedInstr selfOp = word' "SELF" SELF <*> noteDef <*> noteDef @@ -441,3 +449,6 @@  joinTicketsOp :: Parser ParsedInstr joinTicketsOp = word' "JOIN_TICKETS" JOIN_TICKETS <*> noteDef++openChestOp :: Parser ParsedInstr+openChestOp = word' "OPEN_CHEST" OPEN_CHEST <*> noteDef

@@ -42,7 +42,7 @@   <|> symbol' "ACCESS" *> accessMac   <|> symbol' "SET " *> setMac   <|> word' "CONSTRUCT" CONSTRUCT <*> someNE ops-  <|> word' "VIEW" VIEW <*> ops+  <|> word' "VIEW_" VIEW_ <*> ops   <|> word' "VOID" VOID <*> ops   <|> word' "CMP" CMP <*> cmpOp <*> noteDef   <|> word' "IF_SOME" IF_SOME <*> ops <*> ops

@@ -82,6 +82,7 @@   , t_operation, t_contract, t_ticket, t_pair, t_or   , t_lambda, t_map, t_big_map, t_view   , t_void, t_letType+  , t_chestKey, t_chest   ]  ----------------------------------------------------------------------------@@ -139,6 +140,14 @@ t_bls12381g2 fp = do   symbol' "bls12_381_g2" <|> symbol' "Bls12381G2"   mkType TBls12381G2 <$> fieldType fp++t_chestKey :: (Default a) => Parser a -> Parser (a, Ty)+t_chestKey fp = do+  symbol' "ChestKey" <|> symbol' "chest_key"+  mkType TChestKey <$> fieldType fp++t_chest :: (Default a) => Parser a -> Parser (a, Ty)+t_chest fp = word' "Chest" (mkType TChest) <*> fieldType fp  t_chain_id :: (Default a) => Parser a -> Parser (a, Ty) t_chain_id fp = do

@@ -68,7 +68,7 @@ import Morley.Michelson.TypeCheck import Morley.Michelson.Typed   (CreateContract(..), EntrypointCallT, EpName, Operation'(..), SomeContractAndStorage(..),-  SomeStorage(..), SomeValue(..), TransferTokens(..), starNotes, starParamNotes, untypeValue)+  SomeStorage(..), SomeValue(..), TransferTokens(..), untypeValue) import qualified Morley.Michelson.Typed as T import Morley.Michelson.Typed.Operation import Morley.Michelson.Untyped (Contract)@@ -666,7 +666,7 @@             { ceNow = now             , ceMaxSteps = remainingSteps             , ceBalance = newBalance-            , ceContracts = existingContracts+            , ceContracts = gsAddresses gs             , ceSelf = addr             , ceSource = sourceAddr             , ceSender = senderAddr@@ -777,13 +777,7 @@             , ooDelegate = ccDelegate cc             , ooBalance = ccBalance cc             , ooStorage = ccStorageVal cc-            , ooContract =-                T.Contract-                  { cCode = ccContractCode cc-                  , cParamNotes = starParamNotes-                  , cStoreNotes = starNotes-                  , cEntriesOrder = U.canonicalEntriesOrder-                  }+            , ooContract = ccContract cc             , ooCounter = ccCounter cc             }        in OriginateOp origination

@@ -36,7 +36,7 @@ import Morley.Michelson.TypeCheck   (TCError, typeCheckContract, typeCheckTopLevelType, typeCheckingWith, typeVerifyContract,   typeVerifyTopLevelType)-import Morley.Michelson.Typed (Contract(..), SingI, SomeContract(..), SomeValue, Value)+import Morley.Michelson.Typed (Contract, SingI, SomeContract(..), SomeValue, Value) import qualified Morley.Michelson.Untyped as U  ----------------------------------------------------------------------------

@@ -56,6 +56,7 @@   | ContainerValueType   | FailwithArgument   | TicketsJoin+  | ViewBlock   deriving stock (Show, Eq, Generic)   deriving anyclass (NFData) @@ -80,6 +81,7 @@     ContainerValueType -> "container value type"     FailwithArgument -> "argument to FAILWITH"     TicketsJoin -> "join of two tickets"+    ViewBlock -> "top-level view block"  data TopLevelType   = TltParameterType@@ -211,8 +213,7 @@     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"+      "Cannot use a terminate instruction (like FAILWITH) in this block"     EmptyCode -> "Code block is empty"     AnyError -> "Some of the arguments have invalid types"     where@@ -224,6 +225,7 @@   = TCFailedOnInstr U.ExpandedInstr SomeHST InstrCallStack (Maybe TypeContext) (Maybe TCTypeError)   | TCFailedOnValue U.Value T.T Text InstrCallStack (Maybe TCTypeError)   | TCContractError Text (Maybe TCTypeError)+  | TCViewError Text U.ViewName (Maybe TCTypeError)   | TCUnreachableCode InstrCallStack (NonEmpty U.ExpandedOp)   | TCExtError SomeHST InstrCallStack ExtError   | TCIncompletelyTyped TCError (U.Contract' TypeCheckedOp)@@ -252,6 +254,9 @@       <+> (renderDoc context ics)     TCContractError msg typeError ->       "Error occurred during contract typecheck:"+      <$$> (renderAnyBuildable msg) <> (maybe "" (\e -> " " <> (renderDoc context e)) typeError)+    TCViewError msg viewName typeError ->+      "Error occurred during typecheck of view " <> renderDoc context viewName <> ":"       <$$> (renderAnyBuildable msg) <> (maybe "" (\e -> " " <> (renderDoc context e)) typeError)     TCUnreachableCode ics instrs ->       "Unreachable code:" <$$> buildTruncated 3 (toList instrs) <> "."

@@ -13,9 +13,11 @@     , hstToTs     , eqHST     , eqHST1+    , matchHST1     , lengthHST      , ensureDistinctAsc+    , handleError     , eqType     , onTypeCheckInstrAnnErr     , onTypeCheckInstrErr@@ -47,7 +49,7 @@ import Prelude hiding (EQ, GT, LT)  import Control.Lens (unsnoc)-import Control.Monad.Except (MonadError, throwError)+import Control.Monad.Except (MonadError, catchError, throwError) import Data.Constraint (Dict(..), withDict) import Data.Default (def) import Data.Singletons (Sing, SingI(sing), demote)@@ -187,6 +189,16 @@     Nothing -> Left $ StackEqError (hstToTs hst') (hstToTs hst)     Just Refl -> Right Refl +-- | Version of 'eqHST1' that also checks whether annotations converge+-- like 'matchTypes'.+matchHST1+  :: forall t st. (SingI st, WellTyped t)+  => HST st -> Notes t -> Either TCTypeError (st :~: '[t], HST st)+matchHST1 hst nt = do+  refl@Refl <- eqHST1 @t hst+  hstRes <- convergeHST ((nt, Dict, noAnn) ::& SNil) hst `onFirst` AnnError+  return (refl, hstRes)+ lengthHST :: HST xs -> Natural lengthHST (_ ::& xs) = 1 + lengthHST xs lengthHST SNil = 0@@ -205,6 +217,10 @@     else Left $ "Entries are unordered (" +|| e1 ||+ " >= " +|| e2 ||+ ")"   l -> Right l +-- | Flipped version of 'catchError'.+handleError :: MonadError e m => (e -> m a) -> m a -> m a+handleError = flip catchError+ -- | Function @eqType@ is a simple wrapper around @Data.Singletons.decideEquality@ suited -- for use within @Either TCTypeError a@ applicative. eqType@@ -435,6 +451,7 @@       BLAKE2B -> instr''       SOURCE -> instr''       SENDER -> instr''+      VIEW{} -> instr''       SELF _ -> instr''       SELF_ADDRESS -> instr''       CAST -> instr''@@ -457,6 +474,7 @@       READ_TICKET -> instr''       SPLIT_TICKET -> instr''       JOIN_TICKETS -> instr''+      OPEN_CHEST -> instr''       where         instr' = addNotesNoVarAnn outputStack instr         instr'' = addNotesOneVarAnn outputStack instr

@@ -46,9 +46,11 @@  import Prelude hiding (EQ, GT, LT) -import Control.Monad.Except (MonadError, catchError, liftEither, throwError)+import Control.Monad.Except (MonadError, liftEither, throwError) import Data.Default (def) import Data.Generics (everything, mkQ)+import Data.Sequence ((|>))+import qualified Data.Sequence as Seq import Data.Singletons (Sing, demote, withSingI, withSomeSing) import Data.Typeable ((:~:)(..)) import Fmt (pretty)@@ -60,12 +62,11 @@ import Morley.Michelson.TypeCheck.TypeCheck import Morley.Michelson.TypeCheck.TypeCheckedSeq   (IllTypedInstr(..), TypeCheckedInstr, TypeCheckedOp(..), TypeCheckedSeq(..), someInstrToOp,-  tcsEither)+  someViewToOp, tcsEither) import Morley.Michelson.TypeCheck.Types import Morley.Michelson.TypeCheck.Value-import Morley.Michelson.Typed.Value- import Morley.Michelson.Typed hiding (Branch(..))+ import Morley.Util.Named ((!)) import Morley.Util.Peano import Morley.Util.PeanoNatural@@ -139,7 +140,7 @@ typeCheckContractImpl   :: U.Contract   -> TypeCheck SomeContract-typeCheckContractImpl (U.Contract wholeParam@(U.ParameterType mParam rootAnn) mStorage pCode entriesOrder) = do+typeCheckContractImpl uContract@(U.Contract wholeParam@(U.ParameterType mParam rootAnn) mStorage pCode entriesOrder uViews) = do   _ <- maybe (throwError $ TCContractError "no instructions in contract code" $ Just EmptyCode)                 pure (nonEmpty pCode)   withUType mParam $ \(paramNote :: Notes param) ->@@ -155,20 +156,50 @@           let inpNote = NTPair def def def param store paramNote storageNote           let inp = (inpNote, Dict, def) ::& SNil -          codeRes <- usingReaderT def $-                     liftNoExcept $-                     typeCheckImpl typeCheckInstr pCode inp-          codeRes & tcsEither-            (onFailedTypeCheck)-            (onSuccessfulTypeCheck (NTPair def def def def def starNotes storageNote))+          -- typecheck contract code+          codeRes <-+            usingReaderT def $+            liftNoExcept $+            typeCheckImpl typeCheckInstr pCode inp+          instr@(inp' :/ instrOut) <-+            tcsEither onFailedCodeTypeCheck pure codeRes++          -- typecheck views+          views <- typeCheckViewsImpl+            uContract{ U.contractCode = [someInstrToOp instr], U.contractViews = [] }+            storageNote uViews++          handleError (onFailedFullTypeCheck [someInstrToOp instr] (zipWith someViewToOp uViews views)) $ do+            -- match contract code with contract signature, construct contract+            let (paramNotesRaw, cStoreNotes) = case inp' of+                  (NTPair _ _ _ _ _ cpNotes stNotes, _, _) ::& SNil -> (cpNotes, stNotes)+            cParamNotes <-+              liftEither $+              mkParamNotes paramNotesRaw rootAnn `onFirst`+                  (TCContractError "invalid parameter declaration: " . Just . IllegalParamDecl)+            let cEntriesOrder = entriesOrder+            cViews <- liftEither $+              mkViewsSet views `onFirst` \e -> TCContractError (pretty e) Nothing+            case instrOut of+              instr' ::: out -> liftEither $ do+                let ret = NTPair def def def def def+                          (starNotes :: Notes ('TList 'TOperation)) storageNote+                case matchHST1 out ret of+                  Right (Refl, _) ->+                    pure $ SomeContract Contract{ cCode = instr', .. }+                  Left err ->+                    Left $ TCContractError "contract output type violates convention:" $ Just err+              AnyOutInstr instr' ->+                pure $ SomeContract Contract{ cCode = instr', .. }+   where     hasTypeError :: forall (t :: T) a. SingI t => Text -> BadTypeForScope -> TypeCheck a     hasTypeError name reason = throwError $       TCContractError ("contract " <> name <> " type error") $       Just $ UnsupportedTypeForScope (demote @t) reason -    onFailedTypeCheck :: [TypeCheckedOp] -> TCError -> TypeCheck SomeContract-    onFailedTypeCheck ops err = do+    onFailedCodeTypeCheck :: [TypeCheckedOp] -> TCError -> TypeCheck a+    onFailedCodeTypeCheck ops err = do       verbose <- asks tcVerbose       throwError if verbose         then TCIncompletelyTyped err U.Contract@@ -176,49 +207,79 @@              , contractStorage = mStorage              , contractCode = ops              , entriesOrder = entriesOrder+             , contractViews = []              }         else err -    onSuccessfulTypeCheck-      :: forall st param-      . (ParameterScope param, StorageScope st, WellTyped st)-      => Notes (ContractOut1 st)-      -> SomeInstr (ContractInp param st)-      -> TypeCheck SomeContract-    onSuccessfulTypeCheck outNote i@(inp' :/ instrOut) = wrapErrorsIfVerbose i $ do-      let (paramNotesRaw, cStoreNotes) = case inp' of-            (NTPair _ _ _ _ _ cpNotes stNotes, _, _) ::& SNil -> (cpNotes, stNotes)-      cParamNotes <--        liftEither $-        mkParamNotes paramNotesRaw rootAnn `onFirst`-            (TCContractError "invalid parameter declaration: " . Just . IllegalParamDecl)-      case instrOut of-        instr ::: out -> liftEither $ do-          case eqHST1 @(ContractOut1 st) out of-            Right Refl -> do-              let (outN, _, _) ::& SNil = out-              _ <- converge outN outNote-                      `onFirst`-                  ((TCContractError "contract output type violates convention:") . Just . AnnError)-              pure $ SomeContract Contract-                { cCode = instr-                , cParamNotes-                , cStoreNotes-                , cEntriesOrder = entriesOrder-                }-            Left err -> Left $ TCContractError "contract output type violates convention:" $ Just err+    onFailedFullTypeCheck :: [TypeCheckedOp] -> [U.View' TypeCheckedOp] -> TCError -> TypeCheck a+    onFailedFullTypeCheck ops views err = do+      verbose <- asks tcVerbose+      throwError if verbose+        then TCIncompletelyTyped err U.Contract+             { contractParameter = wholeParam+             , contractStorage = mStorage+             , contractCode = ops+             , entriesOrder = entriesOrder+             , contractViews = views+             }+        else err++typeCheckViewsImpl+  :: (WellTyped st)+  => U.Contract' TypeCheckedOp -> Notes st -> [U.View] -> TypeCheck [SomeView st]+typeCheckViewsImpl tcCotract storageNote cViews =+  let myfoldM l acc f = foldM f acc l in+  fmap (map snd . toList) $ myfoldM cViews (Seq.Empty :: Seq (U.View, SomeView st))+    \processedViews uView@U.View+    { U.viewArgument = AsUType (argNote :: Notes param)+    , U.viewReturn = AsUType (returnNote :: Notes ret)+    , U.viewCode = uInstr+    , U.viewName = viewName+    } -> withWTP @param $ withWTP @ret $ do+      let inp = (NTPair def def def def def argNote storageNote, Dict, def) ::& SNil+      Dict <-+        checkScope @(ViewableScope param)+        & either (hasTypeError @param "parameter" viewName) pure+      Dict <-+        checkScope @(ViewableScope ret)+        & either (hasTypeError @ret "return" viewName) pure+      codeRes <-+        usingReaderT def $+        liftNoExcept $+        typeCheckImpl typeCheckInstr uInstr inp+      let tcViews = map (uncurry someViewToOp) processedViews+      _ :/ instrOut <-+        tcsEither (onFailedViewsTypeCheck tcViews uView) pure codeRes++      let vName = viewName+          vArgument = argNote+          vReturn = returnNote+      resView <- case instrOut of+        instr ::: out -> liftEither do+          (Refl, _) <- matchHST1 out returnNote+            `onFirst` (TCViewError "view return type mismatch:" viewName . Just)+          return $ SomeView View{ vCode = instr, .. }         AnyOutInstr instr ->-          pure $ SomeContract Contract-            { cCode = instr-            , cParamNotes-            , cStoreNotes-            , cEntriesOrder = entriesOrder-            }+          return $ SomeView View{ vCode = instr, .. } -    wrapErrorsIfVerbose :: SomeInstr inp -> TypeCheck SomeContract -> TypeCheck SomeContract-    wrapErrorsIfVerbose instr action =-      action `catchError` (onFailedTypeCheck [someInstrToOp instr])+      return $ processedViews |> (uView, resView)+  where+    onFailedViewsTypeCheck+      :: Seq (U.View' TypeCheckedOp) -> U.View+      -> [TypeCheckedOp] -> TCError -> TypeCheck a+    onFailedViewsTypeCheck processedViews v viewOps err = do+      verbose <- asks tcVerbose+      throwError if verbose+        then TCIncompletelyTyped err tcCotract+             { U.contractViews = toList (processedViews |> v{ U.viewCode = viewOps })+             }+        else err +    hasTypeError :: forall (t :: T) a. SingI t => Text -> ViewName -> BadTypeForScope -> TypeCheck a+    hasTypeError desc viewName reason = throwError $+      TCViewError (desc <> " type error in view") viewName $+      Just $ UnsupportedTypeForScope (demote @t) reason+ -- | Function @typeCheckList@ converts list of Michelson instructions -- given in representation from @Morley.Michelson.Type@ module to representation -- in strictly typed GADT.@@ -1027,503 +1088,517 @@           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-    (U.FAILWITH, ((_ :: Notes a, _, _) ::& _)) -> workOnInstr uInstr $ do-      Dict <- onScopeCheckInstrErr @a uInstr (SomeHST inp) (Just FailwithArgument)-        $ checkScope @(ConstantScope a)-      pure $ inp :/ AnyOutInstr FAILWITH+  (U.FAILWITH, ((_ :: Notes a, _, _) ::& _)) -> workOnInstr uInstr $ do+    Dict <- onScopeCheckInstrErr @a uInstr (SomeHST inp) (Just FailwithArgument)+      $ checkScope @(ConstantScope a)+    pure $ inp :/ AnyOutInstr FAILWITH -    (U.FAILWITH, _) -> notEnoughItemsOnStack+  (U.FAILWITH, _) -> notEnoughItemsOnStack -    (U.CAST vn (AsUType (castToNotes :: Notes t)), (en, _, evn) ::& rs) ->-      workOnInstr uInstr $ do-        (Refl, _) <- errM $ matchTypes en castToNotes-        withWTPInstr @t $-          pure $ inp :/ CAST ::: ((castToNotes, Dict, vn `orAnn` evn) ::& rs)-      where-        errM :: (MonadReader InstrCallStack m, MonadError TCError m) => Either TCTypeError a -> m a-        errM = onTypeCheckInstrErr uInstr (SomeHST inp) (Just Cast)+  (U.CAST vn (AsUType (castToNotes :: Notes t)), (en, _, evn) ::& rs) ->+    workOnInstr uInstr $ do+      (Refl, _) <- errM $ matchTypes en castToNotes+      withWTPInstr @t $+        pure $ inp :/ CAST ::: ((castToNotes, Dict, vn `orAnn` evn) ::& rs)+    where+      errM :: (MonadReader InstrCallStack m, MonadError TCError m) => Either TCTypeError a -> m a+      errM = onTypeCheckInstrErr uInstr (SomeHST inp) (Just Cast) -    (U.CAST _ _, _) -> notEnoughItemsOnStack+  (U.CAST _ _, _) -> notEnoughItemsOnStack -    (U.RENAME vn, (an, Dict, _) ::& rs) -> workOnInstr uInstr $-      pure $ inp :/ RENAME ::: ((an, Dict, vn) ::& rs)+  (U.RENAME vn, (an, Dict, _) ::& rs) -> workOnInstr uInstr $+    pure $ inp :/ RENAME ::: ((an, Dict, vn) ::& rs) -    (U.RENAME _, SNil) -> notEnoughItemsOnStack+  (U.RENAME _, SNil) -> notEnoughItemsOnStack -    (U.UNPACK tn vn mt, (NTBytes{}, _, _) ::& rs) -> workOnInstr uInstr $-      withUType mt $ \(tns :: Notes tn) -> do-        case NTOption tn tns of-          (ns :: Notes ('TOption t1)) -> withWTPInstr @('TOption t1) $ do-            Dict <- onScopeCheckInstrErr @tn uInstr (SomeHST inp) Nothing-              $ checkScope @(UnpackedValScope tn)-            pure $ inp :/ UNPACK ::: ((ns, Dict, vn) ::& rs)+  (U.UNPACK tn vn mt, (NTBytes{}, _, _) ::& rs) -> workOnInstr uInstr $+    withUType mt $ \(tns :: Notes tn) -> do+      case NTOption tn tns of+        (ns :: Notes ('TOption t1)) -> withWTPInstr @('TOption t1) $ do+          Dict <- onScopeCheckInstrErr @tn uInstr (SomeHST inp) Nothing+            $ checkScope @(UnpackedValScope tn)+          pure $ inp :/ UNPACK ::: ((ns, Dict, vn) ::& rs) -    (U.UNPACK {}, _ ::& _) ->-      failWithErr $ UnexpectedType $ ("bytes" :| []) :| []+  (U.UNPACK {}, _ ::& _) ->+    failWithErr $ UnexpectedType $ ("bytes" :| []) :| [] -    (U.UNPACK {}, SNil) -> notEnoughItemsOnStack+  (U.UNPACK {}, SNil) -> notEnoughItemsOnStack -    (U.PACK vn, (_ :: Notes a, _, _) ::& rs) -> workOnInstr uInstr $ do-      Dict <- onScopeCheckInstrErr @a uInstr (SomeHST inp) Nothing-        $ checkScope @(PackedValScope a)-      pure $ inp :/ PACK ::: ((starNotes, Dict, vn) ::& rs)+  (U.PACK vn, (_ :: Notes a, _, _) ::& rs) -> workOnInstr uInstr $ do+    Dict <- onScopeCheckInstrErr @a uInstr (SomeHST inp) Nothing+      $ checkScope @(PackedValScope a)+    pure $ inp :/ PACK ::: ((starNotes, Dict, vn) ::& rs) -    (U.PACK _, SNil) -> notEnoughItemsOnStack+  (U.PACK _, SNil) -> notEnoughItemsOnStack -    (U.CONCAT vn, (NTBytes{}, _, _) ::& (NTBytes{}, _, _) ::& _) ->-      workOnInstr uInstr $ concatImpl inp vn-    (U.CONCAT vn, (NTString{}, _, _) ::& (NTString{}, _, _) ::& _) ->-      workOnInstr uInstr $ concatImpl inp vn-    (U.CONCAT vn, (STList STBytes, _, _, _) ::&+ _) ->-      workOnInstr uInstr $ concatImpl' inp vn-    (U.CONCAT vn, (STList STString, _, _, _) ::&+ _) ->-      workOnInstr uInstr $ concatImpl' inp vn-    (U.CONCAT _, _ ::& _) ->-      failWithErr $ UnexpectedType-        $ ("string" :| ["string"]) :|-        [ ("bytes" :| ["bytes"])-        , ("list string" :| ["list string"])-        , ("list bytes" :| ["list bytes"])-        ]-    (U.CONCAT _, SNil) -> notEnoughItemsOnStack+  (U.CONCAT vn, (NTBytes{}, _, _) ::& (NTBytes{}, _, _) ::& _) ->+    workOnInstr uInstr $ concatImpl inp vn+  (U.CONCAT vn, (NTString{}, _, _) ::& (NTString{}, _, _) ::& _) ->+    workOnInstr uInstr $ concatImpl inp vn+  (U.CONCAT vn, (STList STBytes, _, _, _) ::&+ _) ->+    workOnInstr uInstr $ concatImpl' inp vn+  (U.CONCAT vn, (STList STString, _, _, _) ::&+ _) ->+    workOnInstr uInstr $ concatImpl' inp vn+  (U.CONCAT _, _ ::& _) ->+    failWithErr $ UnexpectedType+      $ ("string" :| ["string"]) :|+      [ ("bytes" :| ["bytes"])+      , ("list string" :| ["list string"])+      , ("list bytes" :| ["list bytes"])+      ]+  (U.CONCAT _, SNil) -> notEnoughItemsOnStack -    (U.SLICE vn, (NTNat{}, _, _) ::&-                 (NTNat{}, _, _) ::&-                 (NTString{}, _, _) ::& _) -> workOnInstr uInstr $ sliceImpl inp vn-    (U.SLICE vn, (NTNat{}, _, _) ::&-                 (NTNat{}, _, _) ::&-                 (NTBytes{}, _, _) ::& _) -> workOnInstr uInstr $ sliceImpl inp vn+  (U.SLICE vn, (NTNat{}, _, _) ::&+               (NTNat{}, _, _) ::&+               (NTString{}, _, _) ::& _) -> workOnInstr uInstr $ sliceImpl inp vn+  (U.SLICE vn, (NTNat{}, _, _) ::&+               (NTNat{}, _, _) ::&+               (NTBytes{}, _, _) ::& _) -> workOnInstr uInstr $ sliceImpl inp vn -    (U.SLICE _, _ ::& _ ::& _ ::& _) ->-      failWithErr $ UnexpectedType-        $ ("nat" :| ["nat", "string"]) :|-        [ ("nat" :| ["nat", "bytes"])-        ]-    (U.SLICE _, _) -> notEnoughItemsOnStack+  (U.SLICE _, _ ::& _ ::& _ ::& _) ->+    failWithErr $ UnexpectedType+      $ ("nat" :| ["nat", "string"]) :|+      [ ("nat" :| ["nat", "bytes"])+      ]+  (U.SLICE _, _) -> notEnoughItemsOnStack -    (U.ISNAT vn', (NTInt{}, _, oldVn) ::& rs) -> workOnInstr uInstr $ do-      let vn = vn' `orAnn` oldVn-      pure $ inp :/ ISNAT ::: ((starNotes, Dict, vn) ::& rs)+  (U.ISNAT vn', (NTInt{}, _, oldVn) ::& rs) -> workOnInstr uInstr $ do+    let vn = vn' `orAnn` oldVn+    pure $ inp :/ ISNAT ::: ((starNotes, Dict, vn) ::& rs) -    (U.ISNAT _, _ ::& _) ->-      failWithErr $ UnexpectedType $ ("int" :| []) :| []+  (U.ISNAT _, _ ::& _) ->+    failWithErr $ UnexpectedType $ ("int" :| []) :| [] -    (U.ISNAT _, SNil)-> notEnoughItemsOnStack+  (U.ISNAT _, SNil)-> notEnoughItemsOnStack -    -- Type checking is already done inside `addImpl`.-    (U.ADD vn, (a, _, _, _) ::&+ (b, _, _, _) ::&+ _) -> workOnInstr uInstr $-      addImpl a b inp vn uInstr+  -- Type checking is already done inside `addImpl`.+  (U.ADD vn, (a, _, _, _) ::&+ (b, _, _, _) ::&+ _) -> workOnInstr uInstr $+    addImpl a b inp vn uInstr -    (U.ADD _, _) -> notEnoughItemsOnStack+  (U.ADD _, _) -> notEnoughItemsOnStack -    (U.SUB vn, (a, _, _, _) ::&+ (b, _, _, _) ::&+ _) -> workOnInstr uInstr $-      subImpl a b inp vn uInstr+  (U.SUB vn, (a, _, _, _) ::&+ (b, _, _, _) ::&+ _) -> workOnInstr uInstr $+    subImpl a b inp vn uInstr -    (U.SUB _, _) -> notEnoughItemsOnStack+  (U.SUB _, _) -> notEnoughItemsOnStack -    (U.MUL vn, (a, _, _, _) ::&+ (b, _, _, _) ::&+ _) -> workOnInstr uInstr $-      mulImpl a b inp vn uInstr+  (U.MUL vn, (a, _, _, _) ::&+ (b, _, _, _) ::&+ _) -> workOnInstr uInstr $+    mulImpl a b inp vn uInstr -    (U.MUL _, _) -> notEnoughItemsOnStack+  (U.MUL _, _) -> notEnoughItemsOnStack -    (U.EDIV vn, (a, _, _, _) ::&+ (b, _, _, _) ::&+ _) -> workOnInstr uInstr $-      edivImpl a b inp vn uInstr+  (U.EDIV vn, (a, _, _, _) ::&+ (b, _, _, _) ::&+ _) -> workOnInstr uInstr $+    edivImpl a b inp vn uInstr -    (U.EDIV _, _) -> notEnoughItemsOnStack+  (U.EDIV _, _) -> notEnoughItemsOnStack -    (U.ABS vn, (STInt, _, _, _) ::&+ _) -> workOnInstr uInstr $-      unaryArithImpl @Abs ABS inp vn-    (U.ABS _, _ ::& _) ->-      failWithErr $ UnexpectedType $ ("int" :| []) :| []+  (U.ABS vn, (STInt, _, _, _) ::&+ _) -> workOnInstr uInstr $+    unaryArithImpl @Abs ABS inp vn+  (U.ABS _, _ ::& _) ->+    failWithErr $ UnexpectedType $ ("int" :| []) :| [] -    (U.ABS _, SNil) -> notEnoughItemsOnStack+  (U.ABS _, SNil) -> notEnoughItemsOnStack -    (U.NEG vn, (STInt, _, _, _) ::&+ _) -> workOnInstr uInstr $-      unaryArithImplAnnotated @Neg NEG inp vn-    (U.NEG vn, (STNat, _, _, _) ::&+ _) -> workOnInstr uInstr $-      unaryArithImpl @Neg NEG inp vn-    (U.NEG vn, (STBls12381Fr, _, _, _) ::&+ _) -> workOnInstr uInstr $-      unaryArithImplAnnotated @Neg NEG inp vn-    (U.NEG vn, (STBls12381G1, _, _, _) ::&+ _) -> workOnInstr uInstr $-      unaryArithImplAnnotated @Neg NEG inp vn-    (U.NEG vn, (STBls12381G2, _, _, _) ::&+ _) -> workOnInstr uInstr $-      unaryArithImplAnnotated @Neg NEG inp vn-    (U.NEG _, _ ::& _) ->-      failWithErr $ UnexpectedType-        $ ("int" :| []) :|-        [ ("nat" :| [])-        , ("bls12_381_fr" :| [])-        , ("bls12_381_g1" :| [])-        , ("bls12_381_g2" :| [])-        ]-    (U.NEG _, SNil) -> notEnoughItemsOnStack+  (U.NEG vn, (STInt, _, _, _) ::&+ _) -> workOnInstr uInstr $+    unaryArithImplAnnotated @Neg NEG inp vn+  (U.NEG vn, (STNat, _, _, _) ::&+ _) -> workOnInstr uInstr $+    unaryArithImpl @Neg NEG inp vn+  (U.NEG vn, (STBls12381Fr, _, _, _) ::&+ _) -> workOnInstr uInstr $+    unaryArithImplAnnotated @Neg NEG inp vn+  (U.NEG vn, (STBls12381G1, _, _, _) ::&+ _) -> workOnInstr uInstr $+    unaryArithImplAnnotated @Neg NEG inp vn+  (U.NEG vn, (STBls12381G2, _, _, _) ::&+ _) -> workOnInstr uInstr $+    unaryArithImplAnnotated @Neg NEG inp vn+  (U.NEG _, _ ::& _) ->+    failWithErr $ UnexpectedType+      $ ("int" :| []) :|+      [ ("nat" :| [])+      , ("bls12_381_fr" :| [])+      , ("bls12_381_g1" :| [])+      , ("bls12_381_g2" :| [])+      ]+  (U.NEG _, SNil) -> notEnoughItemsOnStack -    (U.LSL vn, (STNat, _, _, _) ::&+-               (STNat, _, _, _) ::&+ _) -> workOnInstr uInstr $-      arithImpl @Lsl LSL inp vn uInstr-    (U.LSL _, _ ::& _ ::& _) ->-      failWithErr $ UnexpectedType $ ("nat" :| ["nat"]) :| []-    (U.LSL _, _) -> notEnoughItemsOnStack+  (U.LSL vn, (STNat, _, _, _) ::&++             (STNat, _, _, _) ::&+ _) -> workOnInstr uInstr $+    arithImpl @Lsl LSL inp vn uInstr+  (U.LSL _, _ ::& _ ::& _) ->+    failWithErr $ UnexpectedType $ ("nat" :| ["nat"]) :| []+  (U.LSL _, _) -> notEnoughItemsOnStack -    (U.LSR vn, (STNat, _, _, _) ::&+-               (STNat, _, _, _) ::&+ _) -> workOnInstr uInstr $-      arithImpl @Lsr LSR inp vn uInstr-    (U.LSR _, _ ::& _ ::& _) ->-      failWithErr $ UnexpectedType $ ("nat" :| ["nat"]) :| []-    (U.LSR _, _) -> notEnoughItemsOnStack+  (U.LSR vn, (STNat, _, _, _) ::&++             (STNat, _, _, _) ::&+ _) -> workOnInstr uInstr $+    arithImpl @Lsr LSR inp vn uInstr+  (U.LSR _, _ ::& _ ::& _) ->+    failWithErr $ UnexpectedType $ ("nat" :| ["nat"]) :| []+  (U.LSR _, _) -> notEnoughItemsOnStack -    (U.OR vn, (STBool, _, _, _) ::&+-              (STBool, _, _, _) ::&+ _) -> workOnInstr uInstr $-      arithImpl @Or OR inp vn uInstr-    (U.OR vn, (STNat, _, _, _) ::&+-              (STNat, _, _, _) ::&+ _) -> workOnInstr uInstr $-      arithImpl @Or OR inp vn uInstr-    (U.OR _, _ ::& _ ::& _) ->-      failWithErr $ UnexpectedType-        $ ("bool" :| ["bool"]) :|-        [ ("nat" :| ["nat"])-        ]-    (U.OR _, _) -> notEnoughItemsOnStack+  (U.OR vn, (STBool, _, _, _) ::&++            (STBool, _, _, _) ::&+ _) -> workOnInstr uInstr $+    arithImpl @Or OR inp vn uInstr+  (U.OR vn, (STNat, _, _, _) ::&++            (STNat, _, _, _) ::&+ _) -> workOnInstr uInstr $+    arithImpl @Or OR inp vn uInstr+  (U.OR _, _ ::& _ ::& _) ->+    failWithErr $ UnexpectedType+      $ ("bool" :| ["bool"]) :|+      [ ("nat" :| ["nat"])+      ]+  (U.OR _, _) -> notEnoughItemsOnStack -    (U.AND vn, (STInt, _, _, _) ::&+-               (STNat, _, _, _) ::&+ _) -> workOnInstr uInstr $-      arithImpl @And AND inp vn uInstr-    (U.AND vn, (STNat, _, _, _) ::&+-               (STNat, _, _, _) ::&+ _) -> workOnInstr uInstr $-      arithImpl @And AND inp vn uInstr-    (U.AND vn, (STBool, _, _, _) ::&+-               (STBool, _, _, _) ::&+ _) -> workOnInstr uInstr $-      arithImpl @And AND inp vn uInstr-    (U.AND _, _ ::& _ ::& _) ->-      failWithErr $ UnexpectedType-        $ ("int" :| ["nat"]) :|-        [ ("nat" :| ["nat"])-        , ("bool" :| ["bool"])-        ]-    (U.AND _, _) -> notEnoughItemsOnStack+  (U.AND vn, (STInt, _, _, _) ::&++             (STNat, _, _, _) ::&+ _) -> workOnInstr uInstr $+    arithImpl @And AND inp vn uInstr+  (U.AND vn, (STNat, _, _, _) ::&++             (STNat, _, _, _) ::&+ _) -> workOnInstr uInstr $+    arithImpl @And AND inp vn uInstr+  (U.AND vn, (STBool, _, _, _) ::&++             (STBool, _, _, _) ::&+ _) -> workOnInstr uInstr $+    arithImpl @And AND inp vn uInstr+  (U.AND _, _ ::& _ ::& _) ->+    failWithErr $ UnexpectedType+      $ ("int" :| ["nat"]) :|+      [ ("nat" :| ["nat"])+      , ("bool" :| ["bool"])+      ]+  (U.AND _, _) -> notEnoughItemsOnStack -    (U.XOR vn, (STBool, _, _, _) ::&+-               (STBool, _, _, _) ::&+ _) -> workOnInstr uInstr $-      arithImpl @Xor XOR inp vn uInstr-    (U.XOR vn, (STNat, _, _, _) ::&+-               (STNat, _, _, _) ::&+ _) -> workOnInstr uInstr $-      arithImpl @Xor XOR inp vn uInstr-    (U.XOR _, _ ::& _ ::& _) ->-      failWithErr $ UnexpectedType-        $ ("bool" :| ["bool"]) :|-        [ ("nat" :| ["nat"])-        ]-    (U.XOR _, _) -> notEnoughItemsOnStack+  (U.XOR vn, (STBool, _, _, _) ::&++             (STBool, _, _, _) ::&+ _) -> workOnInstr uInstr $+    arithImpl @Xor XOR inp vn uInstr+  (U.XOR vn, (STNat, _, _, _) ::&++             (STNat, _, _, _) ::&+ _) -> workOnInstr uInstr $+    arithImpl @Xor XOR inp vn uInstr+  (U.XOR _, _ ::& _ ::& _) ->+    failWithErr $ UnexpectedType+      $ ("bool" :| ["bool"]) :|+      [ ("nat" :| ["nat"])+      ]+  (U.XOR _, _) -> notEnoughItemsOnStack -    (U.NOT vn, (STNat, _, _, _) ::&+ _) -> workOnInstr uInstr $-      unaryArithImpl @Not NOT inp vn-    (U.NOT vn, (STBool, _, _, _) ::&+ _) -> workOnInstr uInstr $-      unaryArithImplAnnotated @Not NOT inp vn-    (U.NOT vn, (STInt, _, _, _) ::&+ _) -> workOnInstr uInstr $-      unaryArithImplAnnotated @Not NOT inp vn-    (U.NOT _, _ ::& _) ->-      failWithErr $ UnexpectedType-        $ ("nat" :| []) :|-        [ ("bool" :| [])-        , ("int" :| [])-        ]-    (U.NOT _, SNil) -> notEnoughItemsOnStack+  (U.NOT vn, (STNat, _, _, _) ::&+ _) -> workOnInstr uInstr $+    unaryArithImpl @Not NOT inp vn+  (U.NOT vn, (STBool, _, _, _) ::&+ _) -> workOnInstr uInstr $+    unaryArithImplAnnotated @Not NOT inp vn+  (U.NOT vn, (STInt, _, _, _) ::&+ _) -> workOnInstr uInstr $+    unaryArithImplAnnotated @Not NOT inp vn+  (U.NOT _, _ ::& _) ->+    failWithErr $ UnexpectedType+      $ ("nat" :| []) :|+      [ ("bool" :| [])+      , ("int" :| [])+      ]+  (U.NOT _, SNil) -> notEnoughItemsOnStack -    (U.COMPARE vn,-          (an :: Notes aT, _, _)-      ::& (bn :: Notes bT, _, _)-      ::& rs-      )-      -> workOnInstr uInstr $ do-      case eqType @aT @bT of-        Right Refl -> do-          void . errConv $ converge an bn-          proofScope <- onScopeCheckInstrErr @aT (U.COMPARE vn) (SomeHST inp) (Just ComparisonArguments)-            $ checkScope @(ComparabilityScope aT)-          case proofScope of-            Dict ->-              pure $ inp :/ COMPARE ::: ((starNotes, Dict, vn) ::& rs)+  (U.COMPARE vn,+        (an :: Notes aT, _, _)+    ::& (bn :: Notes bT, _, _)+    ::& rs+    )+    -> workOnInstr uInstr $ do+    case eqType @aT @bT of+      Right Refl -> do+        void . errConv $ converge an bn+        proofScope <- onScopeCheckInstrErr @aT (U.COMPARE vn) (SomeHST inp) (Just ComparisonArguments)+          $ checkScope @(ComparabilityScope aT)+        case proofScope of+          Dict ->+            pure $ inp :/ COMPARE ::: ((starNotes, Dict, vn) ::& rs) -        Left err -> do-          typeCheckInstrErr' uInstr (SomeHST inp) (Just ComparisonArguments) err-      where-        errConv :: (MonadReader InstrCallStack m, MonadError TCError m) => Either AnnConvergeError a -> m a-        errConv = onTypeCheckInstrAnnErr uInstr inp (Just ComparisonArguments)+      Left err -> do+        typeCheckInstrErr' uInstr (SomeHST inp) (Just ComparisonArguments) err+    where+      errConv :: (MonadReader InstrCallStack m, MonadError TCError m) => Either AnnConvergeError a -> m a+      errConv = onTypeCheckInstrAnnErr uInstr inp (Just ComparisonArguments) -    (U.COMPARE _, _) -> notEnoughItemsOnStack+  (U.COMPARE _, _) -> notEnoughItemsOnStack -    (U.EQ vn, (NTInt{}, _, _) ::& _) -> workOnInstr uInstr $-      unaryArithImpl @Eq' EQ inp vn-    (U.EQ _, _ ::& _) ->-      failWithErr $ UnexpectedType $ ("int" :| []) :| []-    (U.EQ _, SNil) -> notEnoughItemsOnStack+  (U.EQ vn, (NTInt{}, _, _) ::& _) -> workOnInstr uInstr $+    unaryArithImpl @Eq' EQ inp vn+  (U.EQ _, _ ::& _) ->+    failWithErr $ UnexpectedType $ ("int" :| []) :| []+  (U.EQ _, SNil) -> notEnoughItemsOnStack -    (U.NEQ vn, (NTInt{}, _, _) ::& _) -> workOnInstr uInstr $-      unaryArithImpl @Neq NEQ inp vn-    (U.NEQ _, _ ::& _) ->-      failWithErr $ UnexpectedType $ ("int" :| []) :| []-    (U.NEQ _, SNil) -> notEnoughItemsOnStack+  (U.NEQ vn, (NTInt{}, _, _) ::& _) -> workOnInstr uInstr $+    unaryArithImpl @Neq NEQ inp vn+  (U.NEQ _, _ ::& _) ->+    failWithErr $ UnexpectedType $ ("int" :| []) :| []+  (U.NEQ _, SNil) -> notEnoughItemsOnStack -    (U.LT vn, (NTInt{}, _, _) ::& _) -> workOnInstr uInstr $-      unaryArithImpl @Lt LT inp vn-    (U.LT _, _ ::& _) ->-      failWithErr $ UnexpectedType $ ("int" :| []) :| []-    (U.LT _, SNil) -> notEnoughItemsOnStack+  (U.LT vn, (NTInt{}, _, _) ::& _) -> workOnInstr uInstr $+    unaryArithImpl @Lt LT inp vn+  (U.LT _, _ ::& _) ->+    failWithErr $ UnexpectedType $ ("int" :| []) :| []+  (U.LT _, SNil) -> notEnoughItemsOnStack -    (U.GT vn, (NTInt{}, _, _) ::& _) -> workOnInstr uInstr $-      unaryArithImpl @Gt GT inp vn-    (U.GT _, _ ::& _) ->-      failWithErr $ UnexpectedType $ ("int" :| []) :| []-    (U.GT _, SNil) -> notEnoughItemsOnStack+  (U.GT vn, (NTInt{}, _, _) ::& _) -> workOnInstr uInstr $+    unaryArithImpl @Gt GT inp vn+  (U.GT _, _ ::& _) ->+    failWithErr $ UnexpectedType $ ("int" :| []) :| []+  (U.GT _, SNil) -> notEnoughItemsOnStack -    (U.LE vn, (NTInt{}, _, _) ::& _) -> workOnInstr uInstr $-      unaryArithImpl @Le LE inp vn-    (U.LE _, _ ::& _) ->-      failWithErr $ UnexpectedType $ ("int" :| []) :| []-    (U.LE _, SNil) -> notEnoughItemsOnStack+  (U.LE vn, (NTInt{}, _, _) ::& _) -> workOnInstr uInstr $+    unaryArithImpl @Le LE inp vn+  (U.LE _, _ ::& _) ->+    failWithErr $ UnexpectedType $ ("int" :| []) :| []+  (U.LE _, SNil) -> notEnoughItemsOnStack -    (U.GE vn, (NTInt{}, _, _) ::& _) -> workOnInstr uInstr $-      unaryArithImpl @Ge GE inp vn-    (U.GE _, _ ::& _) ->-      failWithErr $ UnexpectedType $ ("int" :| []) :| []-    (U.GE _, SNil) -> notEnoughItemsOnStack+  (U.GE vn, (NTInt{}, _, _) ::& _) -> workOnInstr uInstr $+    unaryArithImpl @Ge GE inp vn+  (U.GE _, _ ::& _) ->+    failWithErr $ UnexpectedType $ ("int" :| []) :| []+  (U.GE _, SNil) -> notEnoughItemsOnStack -    (U.INT vn, (NTNat{}, _, _) ::& rs) -> workOnInstr uInstr $-      pure $ inp :/ INT ::: ((starNotes, Dict, vn) ::& rs)-    (U.INT vn, (NTBls12381Fr{}, _, _) ::& rs) -> workOnInstr uInstr $-      pure $ inp :/ INT ::: ((starNotes, Dict, vn) ::& rs)-    (U.INT _, _ ::& _) ->-      failWithErr $ UnexpectedType $ ("nat" :| []) :| ["bls12_381_fr" :| []]-    (U.INT _, SNil) -> notEnoughItemsOnStack+  (U.INT vn, (NTNat{}, _, _) ::& rs) -> workOnInstr uInstr $+    pure $ inp :/ INT ::: ((starNotes, Dict, vn) ::& rs)+  (U.INT vn, (NTBls12381Fr{}, _, _) ::& rs) -> workOnInstr uInstr $+    pure $ inp :/ INT ::: ((starNotes, Dict, vn) ::& rs)+  (U.INT _, _ ::& _) ->+    failWithErr $ UnexpectedType $ ("nat" :| []) :| ["bls12_381_fr" :| []]+  (U.INT _, SNil) -> notEnoughItemsOnStack -    (U.SELF vn fn, _) -> workOnInstr uInstr $ do-      mode <- gets tcMode-      case mode of-        TypeCheckValue (value, ty) ->-          tcFailedOnValue value ty "The SELF instruction cannot appear in a lambda." Nothing-        TypeCheckContract (SomeParamType _ notescp) -> do-          let epName = U.epNameFromSelfAnn fn-          MkEntrypointCallRes (argNotes :: Notes arg) epc <--            mkEntrypointCall epName notescp-              & maybeToRight (EntrypointNotFound epName)-              & onTypeCheckInstrErr uInstr (SomeHST inp) Nothing+  (U.VIEW vn name (AsUType (retNotes :: Notes ret)), _ ::& (NTAddress{}, _, _) ::& rs) ->+    workOnInstr uInstr $+      withWTPInstr @ret $ do+        Dict <- onScopeCheckInstrErr @ret uInstr (SomeHST inp) Nothing+              $ checkScope @(ViewableScope ret)+        pure $ inp :/ VIEW name retNotes ::: ((NTOption U.noAnn retNotes, Dict, vn) ::& rs)+  (U.VIEW{}, _ ::& _ ::& _) ->+    failWithErr $ UnexpectedType $ ("'arg" :| ["address"]) :| []+  (U.VIEW{}, _) -> notEnoughItemsOnStack -          case NTContract U.noAnn argNotes of-                  (ntRes :: Notes ('TContract t1)) ->-                    withWTPInstr @('TContract t1) $-                      pure $ inp :/ SELF @arg (SomeEpc epc) ::: ((ntRes, Dict, vn) ::& inp)-        TypeCheckTest ->-          error "'SELF' appears in test typechecking."-        TypeCheckPack ->-          error "'SELF' appears in packed data."-    (U.CONTRACT vn fn mt, (NTAddress{}, _, _) ::& rs) -> workOnInstr uInstr $-      withUType mt $ \(tns :: Notes t) -> do-        proofScope <- onScopeCheckInstrErr @t uInstr (SomeHST inp) (Just ContractParameter)-          $ checkScope @(ParameterScope t)-        let ns = NTOption def $ NTContract def tns-        epName <- onTypeCheckInstrErr uInstr (SomeHST inp) Nothing-          $ epNameFromRefAnn fn `onFirst` IllegalEntrypoint-        case proofScope of-          Dict ->-            withWTPInstr @t $ pure $ inp :/ CONTRACT tns epName ::: ((ns, Dict, vn) ::& rs)+  (U.SELF vn fn, _) -> workOnInstr uInstr $ do+    mode <- gets tcMode+    case mode of+      TypeCheckValue (value, ty) ->+        tcFailedOnValue value ty "The SELF instruction cannot appear in a lambda." Nothing+      TypeCheckContract (SomeParamType _ notescp) -> do+        let epName = U.epNameFromSelfAnn fn+        MkEntrypointCallRes (argNotes :: Notes arg) epc <-+          mkEntrypointCall epName notescp+            & maybeToRight (EntrypointNotFound epName)+            & onTypeCheckInstrErr uInstr (SomeHST inp) Nothing -    (U.CONTRACT {}, _ ::& _) ->-      failWithErr $ UnexpectedType $ ("address" :| []) :| []-    (U.CONTRACT {}, SNil) -> notEnoughItemsOnStack+        case NTContract U.noAnn argNotes of+                (ntRes :: Notes ('TContract t1)) ->+                  withWTPInstr @('TContract t1) $+                    pure $ inp :/ SELF @arg (SomeEpc epc) ::: ((ntRes, Dict, vn) ::& inp)+      TypeCheckTest ->+        error "'SELF' appears in test typechecking."+      TypeCheckPack ->+        error "'SELF' appears in packed data."+  (U.CONTRACT vn fn mt, (NTAddress{}, _, _) ::& rs) -> workOnInstr uInstr $+    withUType mt $ \(tns :: Notes t) -> do+      proofScope <- onScopeCheckInstrErr @t uInstr (SomeHST inp) (Just ContractParameter)+        $ checkScope @(ParameterScope t)+      let ns = NTOption def $ NTContract def tns+      epName <- onTypeCheckInstrErr uInstr (SomeHST inp) Nothing+        $ epNameFromRefAnn fn `onFirst` IllegalEntrypoint+      case proofScope of+        Dict ->+          withWTPInstr @t $ pure $ inp :/ CONTRACT tns epName ::: ((ns, Dict, vn) ::& rs) -    (U.TRANSFER_TOKENS vn, ((_ :: Notes p'), _, _)-      ::& (NTMutez{}, _, _)-      ::& (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-        (Right Refl, Dict) ->-          pure $ inp :/ TRANSFER_TOKENS ::: ((starNotes, Dict, vn) ::& rs)-        (Left m, _) ->-          typeCheckInstrErr' uInstr (SomeHST inp) (Just ContractParameter) m+  (U.CONTRACT {}, _ ::& _) ->+    failWithErr $ UnexpectedType $ ("address" :| []) :| []+  (U.CONTRACT {}, SNil) -> notEnoughItemsOnStack -    (U.TRANSFER_TOKENS _, _ ::& _ ::& _ ::& _) ->-      failWithErr $ UnexpectedType $ ("'p" :| ["mutez", "contract 'p"]) :| []+  (U.TRANSFER_TOKENS vn, ((_ :: Notes p'), _, _)+    ::& (NTMutez{}, _, _)+    ::& (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+      (Right Refl, Dict) ->+        pure $ inp :/ TRANSFER_TOKENS ::: ((starNotes, Dict, vn) ::& rs)+      (Left m, _) ->+        typeCheckInstrErr' uInstr (SomeHST inp) (Just ContractParameter) m -    (U.TRANSFER_TOKENS _, _) -> notEnoughItemsOnStack+  (U.TRANSFER_TOKENS _, _ ::& _ ::& _ ::& _) ->+    failWithErr $ UnexpectedType $ ("'p" :| ["mutez", "contract 'p"]) :| [] -    (U.SET_DELEGATE vn,-      (STOption STKeyHash, NTOption _ NTKeyHash{}, _, _)-      ::&+ rs) -> workOnInstr uInstr $ do-        pure $ inp :/ SET_DELEGATE ::: ((starNotes, Dict, vn) ::& rs)+  (U.TRANSFER_TOKENS _, _) -> notEnoughItemsOnStack -    (U.SET_DELEGATE _,  _ ::& _) ->-      failWithErr $ UnexpectedType $ ("option key_hash" :| []) :| []+  (U.SET_DELEGATE vn,+    (STOption STKeyHash, NTOption _ NTKeyHash{}, _, _)+    ::&+ rs) -> workOnInstr uInstr $ do+      pure $ inp :/ SET_DELEGATE ::: ((starNotes, Dict, vn) ::& rs) -    (U.SET_DELEGATE _, _) -> notEnoughItemsOnStack+  (U.SET_DELEGATE _,  _ ::& _) ->+    failWithErr $ UnexpectedType $ ("option key_hash" :| []) :| [] -    (U.CREATE_CONTRACT ovn avn contract,-      (STOption STKeyHash, NTOption _ (_ :: Notes ('TKeyHash)), _, _)-      ::&+ (NTMutez{}, _, _)-      ::& (gn :: Notes g, Dict, _) ::& rs) -> workOnInstr uInstr $ do-        (SomeContract-          (Contract-            (contr :: ContractCode p' g')-            paramNotes-            storeNotes-            entriesOrder))-          <- lift $ typeCheckContractImpl contract-        Refl <- onTypeCheckInstrErr uInstr (SomeHST inp) (Just ContractStorage)-          $ eqType @g @g'-        void $ onTypeCheckInstrAnnErr uInstr inp (Just ContractStorage) (converge gn storeNotes)-        pure-          $ inp :/ CREATE_CONTRACT (Contract contr paramNotes storeNotes entriesOrder)-          ::: ((starNotes, Dict, ovn) ::& (starNotes, Dict, avn) ::& rs)+  (U.SET_DELEGATE _, _) -> notEnoughItemsOnStack -    (U.CREATE_CONTRACT {}, _ ::& _ ::& _ ::& _) ->-      failWithErr $ UnexpectedType $ ("option key_hash" :| ["mutez", "'a"]) :| []+  (U.CREATE_CONTRACT ovn avn contract,+    (STOption STKeyHash, NTOption _ (_ :: Notes ('TKeyHash)), _, _)+    ::&+ (NTMutez{}, _, _)+    ::& (gn :: Notes g, Dict, _) ::& rs) -> workOnInstr uInstr $ do+      (SomeContract contr@(Contract _ _ storeNotes _ _))+        <- lift $ typeCheckContractImpl contract+      (Refl, _) <- onTypeCheckInstrErr uInstr (SomeHST inp) (Just ContractStorage) $+        matchTypes gn storeNotes+      pure+        $ inp :/ CREATE_CONTRACT contr+        ::: ((starNotes, Dict, ovn) ::& (starNotes, Dict, avn) ::& rs) -    (U.CREATE_CONTRACT {},  _) -> notEnoughItemsOnStack+  (U.CREATE_CONTRACT {}, _ ::& _ ::& _ ::& _) ->+    failWithErr $ UnexpectedType $ ("option key_hash" :| ["mutez", "'a"]) :| [] -    (U.IMPLICIT_ACCOUNT vn, (NTKeyHash{}, _, _) ::& rs) -> workOnInstr uInstr $-      pure $ inp :/ IMPLICIT_ACCOUNT ::: ((starNotes, Dict, vn) ::& rs)+  (U.CREATE_CONTRACT {},  _) -> notEnoughItemsOnStack -    (U.IMPLICIT_ACCOUNT _, _ ::& _) ->-      failWithErr $ UnexpectedType $ ("key_hash" :| []) :| []-    (U.IMPLICIT_ACCOUNT _, SNil) -> notEnoughItemsOnStack+  (U.IMPLICIT_ACCOUNT vn, (NTKeyHash{}, _, _) ::& rs) -> workOnInstr uInstr $+    pure $ inp :/ IMPLICIT_ACCOUNT ::: ((starNotes, Dict, vn) ::& rs) -    (U.NOW vn, _) -> workOnInstr uInstr $-      pure $ inp :/ NOW ::: ((starNotes, Dict, vn) ::& inp)+  (U.IMPLICIT_ACCOUNT _, _ ::& _) ->+    failWithErr $ UnexpectedType $ ("key_hash" :| []) :| []+  (U.IMPLICIT_ACCOUNT _, SNil) -> notEnoughItemsOnStack -    (U.AMOUNT vn, _) -> workOnInstr uInstr $-      pure $ inp :/ AMOUNT ::: ((starNotes, Dict, vn) ::& inp)+  (U.NOW vn, _) -> workOnInstr uInstr $+    pure $ inp :/ NOW ::: ((starNotes, Dict, vn) ::& inp) -    (U.BALANCE vn, _) -> workOnInstr uInstr $-      pure $ inp :/ BALANCE ::: ((starNotes, Dict, vn) ::& inp)+  (U.AMOUNT vn, _) -> workOnInstr uInstr $+    pure $ inp :/ AMOUNT ::: ((starNotes, Dict, vn) ::& inp) -    (U.VOTING_POWER vn, (NTKeyHash{}, _, _) ::& rs) -> workOnInstr uInstr $-      pure $ inp :/ VOTING_POWER ::: ((starNotes, Dict, vn) ::& rs)+  (U.BALANCE vn, _) -> workOnInstr uInstr $+    pure $ inp :/ BALANCE ::: ((starNotes, Dict, vn) ::& inp) -    (U.TOTAL_VOTING_POWER vn, _) -> workOnInstr uInstr $-      pure $ inp :/ TOTAL_VOTING_POWER ::: ((starNotes, Dict, vn) ::& inp)+  (U.VOTING_POWER vn, (NTKeyHash{}, _, _) ::& rs) -> workOnInstr uInstr $+    pure $ inp :/ VOTING_POWER ::: ((starNotes, Dict, vn) ::& rs)+  (U.VOTING_POWER _, _ ::& _) ->+    failWithErr $ UnexpectedType $ ("key_hash" :| []) :| []+  (U.VOTING_POWER _, SNil) -> notEnoughItemsOnStack -    (U.CHECK_SIGNATURE vn,-               (NTKey _, _, _)-               ::& (NTSignature _, _, _) ::& (NTBytes{}, _, _) ::& rs) ->-      workOnInstr uInstr $-        pure $ inp :/ CHECK_SIGNATURE ::: ((starNotes, Dict, vn) ::& rs)+  (U.TOTAL_VOTING_POWER vn, _) -> workOnInstr uInstr $+    pure $ inp :/ TOTAL_VOTING_POWER ::: ((starNotes, Dict, vn) ::& inp) -    (U.CHECK_SIGNATURE _, _ ::& _ ::& _) ->-      failWithErr $ UnexpectedType $ ("key" :| ["signature", "bytes"]) :| []-    (U.CHECK_SIGNATURE _, _) -> notEnoughItemsOnStack+  (U.CHECK_SIGNATURE vn,+             (NTKey _, _, _)+             ::& (NTSignature _, _, _) ::& (NTBytes{}, _, _) ::& rs) ->+    workOnInstr uInstr $+      pure $ inp :/ CHECK_SIGNATURE ::: ((starNotes, Dict, vn) ::& rs) -    (U.SHA256 vn, (NTBytes{}, _, _) ::& rs) -> workOnInstr uInstr $-      pure $ inp :/ SHA256 ::: ((starNotes, Dict, vn) ::& rs)-    (U.SHA256 _, _ ::& _) ->-      failWithErr $ UnexpectedType $ ("bytes" :| []) :| []-    (U.SHA256 _, SNil) -> notEnoughItemsOnStack+  (U.CHECK_SIGNATURE _, _ ::& _ ::& _) ->+    failWithErr $ UnexpectedType $ ("key" :| ["signature", "bytes"]) :| []+  (U.CHECK_SIGNATURE _, _) -> notEnoughItemsOnStack -    (U.SHA512 vn, (NTBytes{}, _, _) ::& rs) -> workOnInstr uInstr $-      pure $ inp :/ SHA512 ::: ((starNotes, Dict, vn) ::& rs)-    (U.SHA512 _, _ ::& _) ->-      failWithErr $ UnexpectedType $ ("bytes" :| []) :| []-    (U.SHA512 _, SNil) -> notEnoughItemsOnStack+  (U.SHA256 vn, (NTBytes{}, _, _) ::& rs) -> workOnInstr uInstr $+    pure $ inp :/ SHA256 ::: ((starNotes, Dict, vn) ::& rs)+  (U.SHA256 _, _ ::& _) ->+    failWithErr $ UnexpectedType $ ("bytes" :| []) :| []+  (U.SHA256 _, SNil) -> notEnoughItemsOnStack -    (U.BLAKE2B vn, (NTBytes{}, _, _) ::& rs) -> workOnInstr uInstr $-      pure $ inp :/ BLAKE2B ::: ((starNotes, Dict, vn) ::& rs)-    (U.BLAKE2B _, _ ::& _) ->-      failWithErr $ UnexpectedType $ ("bytes" :| []) :| []-    (U.BLAKE2B _, SNil) -> notEnoughItemsOnStack+  (U.SHA512 vn, (NTBytes{}, _, _) ::& rs) -> workOnInstr uInstr $+    pure $ inp :/ SHA512 ::: ((starNotes, Dict, vn) ::& rs)+  (U.SHA512 _, _ ::& _) ->+    failWithErr $ UnexpectedType $ ("bytes" :| []) :| []+  (U.SHA512 _, SNil) -> notEnoughItemsOnStack -    (U.SHA3 vn, (NTBytes{}, _, _) ::& rs) -> workOnInstr uInstr $-      pure $ inp :/ SHA3 ::: ((starNotes, Dict, vn) ::& rs)-    (U.SHA3 _, _ ::& _) ->-      failWithErr $ UnexpectedType $ ("bytes" :| []) :| []-    (U.SHA3 _, SNil) -> notEnoughItemsOnStack+  (U.BLAKE2B vn, (NTBytes{}, _, _) ::& rs) -> workOnInstr uInstr $+    pure $ inp :/ BLAKE2B ::: ((starNotes, Dict, vn) ::& rs)+  (U.BLAKE2B _, _ ::& _) ->+    failWithErr $ UnexpectedType $ ("bytes" :| []) :| []+  (U.BLAKE2B _, SNil) -> notEnoughItemsOnStack -    (U.KECCAK vn, (NTBytes{}, _, _) ::& rs) -> workOnInstr uInstr $-      pure $ inp :/ KECCAK ::: ((starNotes, Dict, vn) ::& rs)-    (U.KECCAK _, _ ::& _) ->-      failWithErr $ UnexpectedType $ ("bytes" :| []) :| []-    (U.KECCAK _, SNil) -> notEnoughItemsOnStack+  (U.SHA3 vn, (NTBytes{}, _, _) ::& rs) -> workOnInstr uInstr $+    pure $ inp :/ SHA3 ::: ((starNotes, Dict, vn) ::& rs)+  (U.SHA3 _, _ ::& _) ->+    failWithErr $ UnexpectedType $ ("bytes" :| []) :| []+  (U.SHA3 _, SNil) -> notEnoughItemsOnStack -    (U.HASH_KEY vn, (NTKey{}, _, _) ::& rs) -> workOnInstr uInstr $-      pure $ inp :/ HASH_KEY ::: ((starNotes, Dict, vn) ::& rs)-    (U.HASH_KEY _, _ ::& _) ->-      failWithErr $ UnexpectedType $ ("key" :| []) :| []-    (U.HASH_KEY _, SNil) -> notEnoughItemsOnStack+  (U.KECCAK vn, (NTBytes{}, _, _) ::& rs) -> workOnInstr uInstr $+    pure $ inp :/ KECCAK ::: ((starNotes, Dict, vn) ::& rs)+  (U.KECCAK _, _ ::& _) ->+    failWithErr $ UnexpectedType $ ("bytes" :| []) :| []+  (U.KECCAK _, SNil) -> notEnoughItemsOnStack -    (U.PAIRING_CHECK vn, (NTList _ (NTPair _ _ _ _ _ (NTBls12381G1 _)-                                                     (NTBls12381G2 _)), _, _) ::& rs) ->-      workOnInstr uInstr $-        pure $ inp :/ PAIRING_CHECK ::: ((starNotes, Dict, vn) ::& rs)-    (U.PAIRING_CHECK _, _ ::& _) ->-      failWithErr $ UnexpectedType $ ("list (pair bls12_381_g1 bls12_381_g2)" :| []) :| []-    (U.PAIRING_CHECK _, SNil) -> notEnoughItemsOnStack+  (U.HASH_KEY vn, (NTKey{}, _, _) ::& rs) -> workOnInstr uInstr $+    pure $ inp :/ HASH_KEY ::: ((starNotes, Dict, vn) ::& rs)+  (U.HASH_KEY _, _ ::& _) ->+    failWithErr $ UnexpectedType $ ("key" :| []) :| []+  (U.HASH_KEY _, SNil) -> notEnoughItemsOnStack -    (U.SOURCE vn, _) -> workOnInstr uInstr $-      pure $ inp :/ SOURCE ::: ((starNotes, Dict, vn) ::& inp)+  (U.PAIRING_CHECK vn, (NTList _ (NTPair _ _ _ _ _ (NTBls12381G1 _)+                                                   (NTBls12381G2 _)), _, _) ::& rs) ->+    workOnInstr uInstr $+      pure $ inp :/ PAIRING_CHECK ::: ((starNotes, Dict, vn) ::& rs)+  (U.PAIRING_CHECK _, _ ::& _) ->+    failWithErr $ UnexpectedType $ ("list (pair bls12_381_g1 bls12_381_g2)" :| []) :| []+  (U.PAIRING_CHECK _, SNil) -> notEnoughItemsOnStack -    (U.SENDER vn, _) -> workOnInstr uInstr $-      pure $ inp :/ SENDER ::: ((starNotes, Dict, vn) ::& inp)+  (U.SOURCE vn, _) -> workOnInstr uInstr $+    pure $ inp :/ SOURCE ::: ((starNotes, Dict, vn) ::& inp) -    (U.ADDRESS vn, (NTContract{}, _, _) ::& rs) -> workOnInstr uInstr $-      pure $ inp :/ ADDRESS ::: ((starNotes, Dict, vn) ::& rs)+  (U.SENDER vn, _) -> workOnInstr uInstr $+    pure $ inp :/ SENDER ::: ((starNotes, Dict, vn) ::& inp) -    (U.ADDRESS _, _ ::& _) ->-      failWithErr $ UnexpectedType $ ("contract 'p" :| []) :| []-    (U.ADDRESS _, SNil) -> notEnoughItemsOnStack+  (U.ADDRESS vn, (NTContract{}, _, _) ::& rs) -> workOnInstr uInstr $+    pure $ inp :/ ADDRESS ::: ((starNotes, Dict, vn) ::& rs) -    (U.CHAIN_ID vn, _) -> workOnInstr uInstr $-      pure $ inp :/ CHAIN_ID ::: ((starNotes, Dict, vn) ::& inp)+  (U.ADDRESS _, _ ::& _) ->+    failWithErr $ UnexpectedType $ ("contract 'p" :| []) :| []+  (U.ADDRESS _, SNil) -> notEnoughItemsOnStack -    (U.LEVEL vn, _) -> workOnInstr uInstr $-      pure $ inp :/ LEVEL ::: ((starNotes, Dict, vn) ::& inp)+  (U.CHAIN_ID vn, _) -> workOnInstr uInstr $+    pure $ inp :/ CHAIN_ID ::: ((starNotes, Dict, vn) ::& inp) -    (U.SELF_ADDRESS vn, _) -> workOnInstr uInstr $-      pure $ inp :/ SELF_ADDRESS ::: ((starNotes, Dict, vn) ::& inp)+  (U.LEVEL vn, _) -> workOnInstr uInstr $+    pure $ inp :/ LEVEL ::: ((starNotes, Dict, vn) ::& inp) -    (U.NEVER, (NTNever{}, _, _) ::& _) -> workOnInstr uInstr $-      pure $ inp :/ AnyOutInstr NEVER+  (U.SELF_ADDRESS vn, _) -> workOnInstr uInstr $+    pure $ inp :/ SELF_ADDRESS ::: ((starNotes, Dict, vn) ::& inp) -    (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.NEVER, (NTNever{}, _, _) ::& _) -> workOnInstr uInstr $+    pure $ inp :/ AnyOutInstr NEVER+  (U.NEVER, _ ::& _) ->+    failWithErr $ UnexpectedType $ ("never" :| []) :| []+  (U.NEVER, SNil) -> 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.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.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.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.JOIN_TICKETS vn,-       (STPair{}, NTPair _ _ _ _ _ nt1@NTTicket{} nt2@NTTicket{}, Dict, _) ::&+ rs) ->+  (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++  (U.OPEN_CHEST vn,+      (NTChestKey _, Dict, _)+      ::& (NTChest _, Dict, _)+      ::& (NTNat _, 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+        pure $ inp :/ OPEN_CHEST ::: (+          (NTOr U.noAnn U.noAnn U.noAnn (NTBytes U.noAnn) (NTBool U.noAnn), Dict, vn)+          ::& rs)+  (U.OPEN_CHEST _, _ ::& _ ::& _ ::& _) ->+    failWithErr $ UnexpectedType $ ("chest_key" :| ["chest", "nat"]) :| []+  (U.OPEN_CHEST _, _) -> notEnoughItemsOnStack -    -- Could not get rid of the catch all clause due to this warning:-    -- @-    -- Pattern match checker exceeded (2000000) iterations in-    -- a case alternative. (Use -fmax-pmcheck-iterations=n-    -- to set the maximum number of iterations to n)-    -- @-    i ->-      error $ "Pattern matches should be exhaustive, but instead got: " <> show i   where     withWTPInstr'       :: forall t inp. SingI t

@@ -9,14 +9,18 @@   , TypeCheckedOp(..)   , IllTypedInstr(..)   , someInstrToOp+  , someViewToOp   ) where  import Data.Singletons (SingI)  import Morley.Michelson.Printer.Util (RenderDoc(..), renderOpsListNoBraces) import Morley.Michelson.TypeCheck.Types (HST(..), SomeInstr(..), SomeInstrOut(..))+import Morley.Michelson.Typed.Aliases import Morley.Michelson.Typed.Convert (instrToOps) import Morley.Michelson.Typed.Instr (Instr, castInstr)+import Morley.Michelson.Typed.View (SomeView'(..), View'(..))+import qualified Morley.Michelson.Untyped as U import Morley.Michelson.Untyped.Instr (ExpandedOp, InstrAbstract(..)) import Morley.Util.TH (deriveGADTNFData) @@ -58,5 +62,12 @@     go :: forall inp. SingI inp => SomeInstrOut inp -> TypeCheckedOp     go (i ::: _) = WellTypedOp i     go (AnyOutInstr i) = WellTypedOp (i @'[])++-- | Makes a view with well-typed code, taking the untyped and typechecked view.+someViewToOp :: U.View' op -> SomeView st -> U.View' TypeCheckedOp+someViewToOp U.View{..} (SomeView View{..}) = U.View+  { U.viewCode = [WellTypedOp vCode]+  , ..+  }  $(deriveGADTNFData ''TypeCheckedOp)

@@ -16,11 +16,12 @@   , tcsEither   , seqToOps   , someInstrToOp+  , someViewToOp   ) where  import Morley.Michelson.TypeCheck.Error (TCError) import Morley.Michelson.TypeCheck.TypeCheckedOp-  (IllTypedInstr(..), TypeCheckedInstr, TypeCheckedOp(..), someInstrToOp)+  (IllTypedInstr(..), TypeCheckedInstr, TypeCheckedOp(..), someInstrToOp, someViewToOp) import Morley.Michelson.TypeCheck.Types (SomeInstr(..))  -- | Represents a partiall typed sequence of instructions.

@@ -34,6 +34,7 @@ import Morley.Michelson.Printer.Util import Morley.Michelson.Typed (Notes(..), SingT(..), SomeContract(..), T(..), notesT, starNotes) import qualified Morley.Michelson.Typed as T+import Morley.Michelson.Typed.Contract import Morley.Michelson.Typed.Haskell.Value (WellTyped) import Morley.Michelson.Typed.Instr import Morley.Michelson.Untyped (Ty, Var, noAnn)@@ -278,6 +279,8 @@   STBls12381G2 -> Right Dict   STTimestamp -> Right Dict   STAddress -> Right Dict+  STChest -> Right Dict+  STChestKey -> Right Dict   STNever -> Right Dict   where     eitherWellTyped

@@ -32,6 +32,7 @@ import Morley.Tezos.Core import Morley.Tezos.Crypto import qualified Morley.Tezos.Crypto.BLS12381 as BLS+import Morley.Tezos.Crypto.Timelock (chestFromBytes, chestKeyFromBytes) import Morley.Util.Type (onFirst)  tcFailedOnValue :: U.Value -> T.T -> Text -> Maybe TCTypeError -> TypeCheckInstr a@@ -254,6 +255,16 @@                         "wrong output type of lambda's value:" (Just m)           AnyOutInstr lam ->             pure $ VLam (T.RfAlwaysFails lam)++      (v@(U.ValueBytes (U.InternalByteString bs)), STChest) ->+        case chestFromBytes bs of+          Right res -> pure $ VChest res+          Left err -> tcFailedOnValue v T.TChest err Nothing++      (v@(U.ValueBytes (U.InternalByteString bs)), STChestKey) ->+        case chestKeyFromBytes bs of+          Right res -> pure $ VChestKey res+          Left err -> tcFailedOnValue v T.TChestKey err Nothing        (v, t) -> tcFailedOnValue v (fromSing t) "unknown value" Nothing 

@@ -9,6 +9,7 @@ import Morley.Michelson.Typed.Aliases as Exports import Morley.Michelson.Typed.Annotation as Exports import Morley.Michelson.Typed.Arith as Exports+import Morley.Michelson.Typed.Contract as Exports import Morley.Michelson.Typed.Convert as Exports import Morley.Michelson.Typed.Doc as Exports import Morley.Michelson.Typed.Entrypoints as Exports@@ -23,3 +24,4 @@ import Morley.Michelson.Typed.T as Exports import Morley.Michelson.Typed.Util as Exports import Morley.Michelson.Typed.Value as Exports+import Morley.Michelson.Typed.View as Exports

@@ -5,10 +5,26 @@ module Morley.Michelson.Typed.Aliases   ( Value   , Operation+  , ContractCode+  , Contract+  , ViewCode+  , View+  , SomeView+  , ViewsSet+  , SomeViewsSet   ) where +import Morley.Michelson.Typed.Contract import Morley.Michelson.Typed.Instr import Morley.Michelson.Typed.Value+import Morley.Michelson.Typed.View  type Value = Value' Instr type Operation = Operation' Instr+type ContractCode cp st = ContractCode' Instr cp st+type Contract = Contract' Instr+type ViewCode arg st ret = ViewCode' Instr arg st ret+type View = View' Instr+type SomeView = SomeView' Instr+type ViewsSet = ViewsSet' Instr+type SomeViewsSet = SomeViewsSet' Instr

@@ -80,6 +80,8 @@   NTBls12381G2 :: TypeAnn -> Notes 'TBls12381G2   NTTimestamp :: TypeAnn -> Notes 'TTimestamp   NTAddress   :: TypeAnn -> Notes 'TAddress+  NTChest     :: TypeAnn -> Notes 'TChest+  NTChestKey  :: TypeAnn -> Notes 'TChestKey   NTNever     :: TypeAnn -> Notes 'TNever  deriving stock instance Eq (Notes t)@@ -110,6 +112,8 @@     NTUnit ta               -> "NTUnit" <+> rendT ta     NTSignature ta          -> "NTSignature" <+> rendT ta     NTChainId ta            -> "NTChainId" <+> rendT ta+    NTChest ta              -> "NTChest" <+> rendT ta+    NTChestKey ta           -> "NTChestKey" <+> rendT ta     NTNever ta              -> "NTNever" <+> rendT ta     NTOption ta nt          -> "NTOption" <+> rendT ta <+> rendN nt     NTList ta nt            -> "NTList" <+> rendT ta <+> rendN nt@@ -182,6 +186,8 @@     NTPair noAnn noAnn noAnn noAnn noAnn (starNotes' t) (starNotes' t')   STOr t t' -> NTOr noAnn noAnn noAnn (starNotes' t) (starNotes' t')   STLambda t t' -> NTLambda noAnn (starNotes' t) (starNotes' t')+  STChest -> NTChest noAnn+  STChestKey -> NTChestKey noAnn  -- | Checks if no annotations are present. isStar :: SingI t => Notes t -> Bool@@ -206,6 +212,8 @@   (NTAddress a, NTAddress b) -> NTAddress <$> convergeAnns a b   (NTKey a, NTKey b) -> NTKey <$> convergeAnns a b   (NTUnit a, NTUnit b) -> NTUnit <$> convergeAnns a b+  (NTChest a, NTChest b) -> NTChest <$> convergeAnns a b+  (NTChestKey a, NTChestKey b) -> NTChestKey <$> convergeAnns a b   (NTNever a, NTNever b) -> NTNever <$> convergeAnns a b   (NTSignature a, NTSignature b) ->     NTSignature <$> convergeAnns a b@@ -268,6 +276,8 @@   NTMap _ n1 n2 -> NTMap nt n1 n2   NTBigMap _ n1 n2 -> NTBigMap nt n1 n2   NTChainId _ -> NTChainId nt+  NTChest _ -> NTChest nt+  NTChestKey _ -> NTChestKey nt   NTNever _ -> NTNever nt  data AnnConvergeError where

@@ -0,0 +1,116 @@+-- SPDX-FileCopyrightText: 2021 Tocqueville Group+--+-- SPDX-License-Identifier: LicenseRef-MIT-TQ++-- 'newtype Container' deriving produced some fake warnings+{-# OPTIONS_GHC -Wno-redundant-constraints #-}++-- | Module, containing top-level entries of a Michelson contract.+module Morley.Michelson.Typed.Contract+  ( -- * Contract+    ContractInp1+  , ContractInp+  , ContractOut1+  , ContractOut+  , ContractCode'+  , Contract' (..)+  , defaultContract+  , mapContractCode+  , mapContractCodeBlock+  , mapContractViewBlocks+  , mapEntriesOrdered+  ) where++import Data.Default (Default(..))++import Morley.Michelson.Typed.Annotation+import Morley.Michelson.Typed.Entrypoints+import Morley.Michelson.Typed.Scope+import Morley.Michelson.Typed.T (T(..))+import Morley.Michelson.Typed.View+import Morley.Michelson.Untyped.Contract (EntriesOrder, entriesOrderToInt)++type ContractInp1 param st = 'TPair param st+type ContractInp param st = '[ ContractInp1 param st ]++type ContractOut1 st = 'TPair ('TList 'TOperation) st+type ContractOut st = '[ ContractOut1 st ]++type ContractCode' instr cp st = instr (ContractInp cp st) (ContractOut st)++-- | Typed contract and information about annotations+-- which is not present in the contract code.+data Contract' instr cp st = (ParameterScope cp, StorageScope st) => Contract+  { cCode         :: ContractCode' instr cp st+  , cParamNotes   :: ParamNotes cp+  , cStoreNotes   :: Notes st+  , cViews        :: ViewsSet' instr st+  , cEntriesOrder :: EntriesOrder+  }++deriving stock instance+  (forall i o. Show (instr i o)) =>+  Show (Contract' instr cp st)++deriving stock instance+  (forall i o. Eq (instr i o)) =>+  Eq (Contract' instr cp st)++instance+  (forall i o. NFData (instr i o)) =>+  NFData (Contract' instr cp st) where+  rnf (Contract a b c d e) = rnf (a, b, c, d, e)++defaultContract :: (ParameterScope cp, StorageScope st) => ContractCode' instr cp st -> Contract' instr cp st+defaultContract code = Contract+  { cCode = code+  , cParamNotes = starParamNotes+  , cStoreNotes = starNotes+  , cEntriesOrder = def+  , cViews = def+  }++-- | Transform contract @code@ block.+--+-- To map e.g. views too, see 'mapContractCode'.+mapContractCodeBlock+  :: (ContractCode' instr cp st -> ContractCode' instr cp st)+  -> Contract' instr cp st+  -> Contract' instr cp st+mapContractCodeBlock f contract = contract { cCode = f $ cCode contract }++mapContractViewBlocks+  :: (forall arg ret. ViewCode' instr arg st ret -> ViewCode' instr arg st ret)+  -> Contract' instr cp st+  -> Contract' instr cp st+mapContractViewBlocks f contract = contract+  { cViews = UnsafeViewsSet $+      unViewsSet (cViews contract) <&> \(SomeView v) -> SomeView v{ vCode = f $ vCode v }+  }++-- | Map all the blocks with some code in the contract.+mapContractCode+  :: (forall i o. instr i o -> instr i o)+  -> Contract' instr cp st+  -> Contract' instr cp st+mapContractCode f =+  mapContractCodeBlock f .+  mapContractViewBlocks f++-- | Map each typed contract fields by the given function and sort the output+-- based on the 'EntriesOrder'.+mapEntriesOrdered+  :: Contract' instr cp st+  -> (ParamNotes cp -> a)+  -> (Notes st -> a)+  -> (ContractCode' instr cp st -> a)+  -> [a]+mapEntriesOrdered Contract{..} fParam fStorage fCode =+  fmap snd+    $ sortWith fst+        [ (paramPos, fParam cParamNotes)+        , (storagePos, fStorage cStoreNotes)+        , (codePos, fCode cCode)+        ]+  where+    (paramPos, storagePos, codePos) = entriesOrderToInt cEntriesOrder

@@ -6,6 +6,8 @@  module Morley.Michelson.Typed.Convert   ( convertParamNotes+  , convertView+  , convertSomeView   , convertContractCode   , convertContract   , instrToOps@@ -36,6 +38,7 @@ import Morley.Michelson.Text import Morley.Michelson.Typed.Aliases import Morley.Michelson.Typed.Annotation (Notes(..))+import Morley.Michelson.Typed.Contract import Morley.Michelson.Typed.Entrypoints import Morley.Michelson.Typed.Extract (mkUType, mkUType', toUType) import Morley.Michelson.Typed.Instr as Instr@@ -43,6 +46,7 @@ import Morley.Michelson.Typed.Sing (SingT(..)) import Morley.Michelson.Typed.T (T(..)) import Morley.Michelson.Typed.Value+import Morley.Michelson.Typed.View import qualified Morley.Michelson.Untyped as U import Morley.Michelson.Untyped.Annotation (Annotation(unAnnotation)) import Morley.Tezos.Address (Address(..), ContractHash(..))@@ -54,6 +58,7 @@ import qualified Morley.Tezos.Crypto.Ed25519 as Ed25519 import qualified Morley.Tezos.Crypto.P256 as P256 import qualified Morley.Tezos.Crypto.Secp256k1 as Secp256k1+import Morley.Tezos.Crypto.Timelock (chestBytes, chestKeyBytes) import Morley.Util.PeanoNatural (fromPeanoNatural) import Morley.Util.Sing (eqParamSing) @@ -72,15 +77,29 @@     , contractStorage = untypeDemoteT @store     , contractCode = instrToOps contract     , entriesOrder = U.canonicalEntriesOrder+    , contractViews = []     } --- | Convert typed 'Contract' to an untyped t'U.Contract'.+convertView :: forall arg store ret. View arg store ret -> U.View+convertView View{..} =+  U.View+    { viewName = vName+    , viewArgument = untypeDemoteT @arg+    , viewReturn = untypeDemoteT @ret+    , viewCode = instrToOps vCode+    }++convertSomeView :: SomeView st -> U.View+convertSomeView (SomeView v) = convertView v++-- | Convert typed t'Contract' to an untyped t'U.Contract'. convertContract :: Contract param store -> U.Contract convertContract fc@Contract{} =   let c = convertContractCode (cCode fc)   in c { U.contractParameter = convertParamNotes (cParamNotes fc)        , U.contractStorage = mkUType (cStoreNotes fc)        , U.entriesOrder = cEntriesOrder fc+       , U.contractViews = convertSomeView <$> toList (cViews fc)        }  -- Note: if you change this type, check 'untypeValueImpl' wildcard patterns.@@ -185,6 +204,8 @@         U.ValueString . mformatEpAddress $ EpAddress addr (sepcName sepc)       _         -> U.ValueBytes . U.InternalByteString . encodeEpAddress $         EpAddress addr (sepcName sepc)+  (VChest c, _) -> U.ValueBytes . U.InternalByteString $ chestBytes c+  (VChestKey c, _) -> U.ValueBytes . U.InternalByteString $ chestKeyBytes c   (VTicket s v a, STTicket vt) ->     case valueTypeSanity v of       Dict ->@@ -447,6 +468,7 @@         (U.LE _, _) -> instr         (U.GE _, _) -> instr         (U.INT _, _) -> instr+        (U.VIEW{}, _) -> instr         (U.SELF _ _, _) -> instr         (U.TRANSFER_TOKENS _, _) -> instr         (U.SET_DELEGATE _, _) -> instr@@ -554,6 +576,7 @@         U.LE _ -> U.LE va         U.GE _ -> U.GE va         U.INT _ -> U.INT va+        U.VIEW _ n t -> U.VIEW va n t         U.SELF _ fa -> U.SELF va fa         U.CONTRACT _ fa t -> U.CONTRACT va fa t         U.TRANSFER_TOKENS _ -> U.TRANSFER_TOKENS va@@ -700,6 +723,7 @@       LE -> U.LE U.noAnn       GE -> U.GE U.noAnn       INT -> U.INT U.noAnn+      VIEW viewName nt -> U.VIEW U.noAnn viewName (mkUType nt)       SELF sepc ->         U.SELF U.noAnn (epNameToRefAnn $ sepcName sepc)       i@(CONTRACT nt epName)@@ -741,6 +765,7 @@       READ_TICKET -> U.READ_TICKET U.noAnn       SPLIT_TICKET -> U.SPLIT_TICKET U.noAnn       JOIN_TICKETS -> U.JOIN_TICKETS U.noAnn+      OPEN_CHEST -> U.OPEN_CHEST U.noAnn  untypeStackRef :: StackRef s -> U.StackRef untypeStackRef (StackRef n) = U.StackRef (fromPeanoNatural n)@@ -823,6 +848,11 @@     STSignature        -> Just $ VSignature $ sampleSignature     STChainId          -> Just $ VChainId sampleChainId     STOperation        -> Nothing+    -- It's not hard to generate a chest with a matching key, but+    -- representing those in source is extremely unwieldy due to large+    -- primes involved.+    STChest            -> Nothing+    STChestKey         -> Nothing     STNever            -> Nothing     STOption t ->       withSingI t $ VOption . Just <$> sampleTypedValue t

@@ -20,6 +20,8 @@ import Prelude hiding (Ordering(..))  import Morley.Michelson.Doc+import Morley.Michelson.Typed.Aliases+import Morley.Michelson.Typed.Contract import Morley.Michelson.Typed.Instr import Morley.Michelson.Typed.Util 

@@ -18,7 +18,6 @@ import Morley.Michelson.Typed.Aliases import Morley.Michelson.Typed.Convert () import Morley.Michelson.Typed.Haskell.Value (KnownIsoT)-import Morley.Michelson.Typed.Instr (Contract(..)) import Morley.Michelson.Typed.Scope import Morley.Michelson.Typed.T (T(..)) import Morley.Util.Sing (eqParamSing)

@@ -57,6 +57,8 @@   (STList t, NTList tn n)         -> Un.Ty (Un.TList $ mkUType' (t, n)) tn   (STSet t, NTSet tn n)           -> Un.Ty (Un.TSet $ mkUType' (t, n)) tn   (STOperation, NTOperation tn)   -> Un.Ty Un.TOperation tn+  (STChest, NTChest tn)           -> Un.Ty Un.TChest tn+  (STChestKey, NTChestKey tn)     -> Un.Ty Un.TChestKey tn   (STNever, NTNever tn)           -> Un.Ty Un.TNever tn   (STContract t, NTContract tn n) ->     Un.Ty (Un.TContract $ mkUType' (t, n)) tn@@ -147,6 +149,12 @@    Un.TChainId ->     cont (NTChainId tn)++  Un.TChest ->+    cont (NTChest tn)++  Un.TChestKey ->+    cont (NTChestKey tn)    Un.TNever ->     cont (NTNever tn)

@@ -19,6 +19,7 @@   , FieldDescriptions   , PolyTypeHasDocC   , SomeTypeWithDoc (..)+  , typeDocBuiltMichelsonRep    , HaveCommonTypeCtor   , IsHomomorphic@@ -56,7 +57,7 @@ import Data.Singletons (SingI, demote) import qualified Data.Text as T import Data.Typeable (typeRep, typeRepArgs)-import Fmt (Buildable, build, (+|), (|+))+import Fmt (Buildable, Builder, build, (+|), (|+)) import GHC.Generics ((:*:)(..), (:+:)(..)) import qualified GHC.Generics as G import GHC.TypeLits (ErrorMessage(..), KnownSymbol, TypeError, symbolVal)@@ -362,19 +363,25 @@                 mdTicked (build lhs) <> " = " <> renderedRep         in rendered <> "\n\n"     , Just $-        let (mlhs, rep) = typeDocMichelsonRep ap'-            renderedRep = mdTicked (build rep)-            rendered = case mlhs of-              Nothing -> mdSubsection "Final Michelson representation"-                         renderedRep-              Just lhs -> mdSubsection "Final Michelson representation (example)" $-                          mdTicked (build lhs) <> " = " <> renderedRep-        in rendered <> "\n\n"+        typeDocBuiltMichelsonRep (Proxy @a) <> "\n\n"     ]    docItemToToc lvl d@(DType ap') =     mdTocFromRef lvl (build $ typeDocName ap') d +-- | Fully render Michelson representation of a type.+typeDocBuiltMichelsonRep :: TypeHasDoc a => Proxy a -> Builder+typeDocBuiltMichelsonRep ap' =+  let (mlhs, rep) = typeDocMichelsonRep ap'+      renderedRep = mdTicked (build rep)+  in case mlhs of+        Nothing ->+          mdSubsection "Final Michelson representation"+          renderedRep+        Just lhs ->+          mdSubsection "Final Michelson representation (example)" $+          mdTicked (build lhs) <> " = " <> renderedRep+ -- | Create a 'DType' in form suitable for putting to 'typeDocDependencies'. dTypeDep :: forall (t :: Type). TypeHasDoc t => SomeDocDefinitionItem dTypeDep = SomeDocDefinitionItem (DType (Proxy @t))@@ -781,6 +788,18 @@   typeDocName _ = "()"   typeDocMdDescription = "Unit primitive."   typeDocDependencies _ = []++instance TypeHasDoc Chest where+  typeDocName _ = "Chest"+  typeDocMdDescription = "Timelock puzzle chest."+  typeDocDependencies _ = []+  typeDocHaskellRep _ _ = Nothing++instance TypeHasDoc ChestKey where+  typeDocName _ = "ChestKey"+  typeDocMdDescription = "Timelock puzzle chest key."+  typeDocDependencies _ = []+  typeDocHaskellRep _ _ = Nothing  instance PolyTypeHasDocC '[a] => TypeHasDoc [a] where   typeDocName _ = "List"

@@ -59,7 +59,8 @@ import Morley.Michelson.Typed.Value import Morley.Tezos.Address (Address) import Morley.Tezos.Core (ChainId, Mutez, Timestamp)-import Morley.Tezos.Crypto (Bls12381Fr, Bls12381G1, Bls12381G2, KeyHash, PublicKey, Signature)+import Morley.Tezos.Crypto+  (Bls12381Fr, Bls12381G1, Bls12381G2, Chest, ChestKey, KeyHash, PublicKey, Signature) import Morley.Util.Named import Morley.Util.Type @@ -228,6 +229,16 @@   toVal = VOp   fromVal (VOp x) = x +instance IsoValue Chest where+  type ToT Chest = 'TChest+  toVal = VChest+  fromVal (VChest x) = x++instance IsoValue ChestKey where+  type ToT ChestKey = 'TChestKey+  toVal = VChestKey+  fromVal (VChestKey x) = x+ deriving newtype instance IsoValue a => IsoValue (Identity a) deriving newtype instance IsoValue a => IsoValue (NamedF Identity a name) deriving newtype instance IsoValue a => IsoValue (NamedF Maybe a name)@@ -484,6 +495,8 @@ instance WellTyped 'TNever where instance WellTyped 'TSignature where instance WellTyped 'TChainId where+instance WellTyped 'TChest where+instance WellTyped 'TChestKey where instance WellTyped t => WellTyped ('TOption t) where   type WellTypedSuperC ('TOption t) = WellTyped t instance WellTyped t => WellTyped ('TList t) where

@@ -15,12 +15,7 @@   , mkStackRef   , PrintComment (..)   , TestAssert (..)-  , ContractCode-  , Contract (..)   , SomeMeta (..)-  , defaultContract-  , mapContractCode-  , mapEntriesOrdered   , pattern CAR   , pattern CDR   , pattern LEFT@@ -46,7 +41,6 @@   , UpdateN   ) where -import Data.Default import Data.Type.Equality ((:~:)(..)) import Data.Vinyl (RMap, Rec(..), RecordToList, ReifyConstraint(..)) import Fmt ((+||), (||+))@@ -56,8 +50,9 @@  import Morley.Michelson.Doc import Morley.Michelson.ErrorPos-import Morley.Michelson.Typed.Annotation (Notes(..), starNotes)+import Morley.Michelson.Typed.Annotation (Notes(..)) import Morley.Michelson.Typed.Arith+import Morley.Michelson.Typed.Contract import Morley.Michelson.Typed.Entrypoints import Morley.Michelson.Typed.Polymorphic import Morley.Michelson.Typed.Scope@@ -65,10 +60,10 @@ import Morley.Michelson.Typed.TypeLevel   (CombedPairLeafCount, CombedPairLeafCountIsAtLeast, CombedPairNodeCount,   CombedPairNodeIndexIsValid, IsPair)-import Morley.Michelson.Typed.Value (Comparable, ContractInp, ContractOut, Value'(..))+import Morley.Michelson.Typed.Value (Comparable, Value'(..))+import Morley.Michelson.Typed.View import Morley.Michelson.Untyped-  (Annotation(..), EntriesOrder(..), FieldAnn, StackFn, StackTypePattern, TypeAnn, VarAnn, VarAnns,-  entriesOrderToInt)+  (Annotation(..), FieldAnn, StackFn, StackTypePattern, TypeAnn, VarAnn, VarAnns) import Morley.Util.Peano import Morley.Util.PeanoNatural import Morley.Util.Sing (eqI)@@ -721,6 +716,13 @@   INT     :: ToIntArithOp n     => Instr (n ': s) ('TInt ': s)+  VIEW+       -- Here really only the return type is constrainted+       -- because it is given explicitly+    :: (SingI arg, ViewableScope ret)+    => ViewName+    -> Notes ret+    -> Instr (arg ': 'TAddress ': s) ('TOption ret ': s)   SELF     :: forall (arg :: T) s .        (ParameterScope arg)@@ -740,7 +742,7 @@    CREATE_CONTRACT     :: (ParameterScope p, StorageScope g)-    => Contract p g+    => Contract' Instr p g     -> Instr ('TOption 'TKeyHash ':               'TMutez ':                g ': s)@@ -782,6 +784,9 @@   JOIN_TICKETS     :: Instr ('TPair ('TTicket a) ('TTicket a) ': s)              ('TOption ('TTicket a) ': s)+  OPEN_CHEST+    :: Instr ('TChestKey ': 'TChest ': 'TNat ': s)+             ('TOr 'TBytes 'TBool ': s)  castInstr   :: forall inp1 out1 inp2 out2.@@ -918,55 +923,5 @@   rnf (SomeMeta meta) = rnf meta  deriving stock instance Show SomeMeta-------------------------------------------------------type ContractCode cp st = Instr (ContractInp cp st) (ContractOut st)---- | Typed contract and information about annotations--- which is not present in the contract code.-data Contract cp st = (ParameterScope cp, StorageScope st) => Contract-  { cCode       :: ContractCode cp st-  , cParamNotes :: ParamNotes cp-  , cStoreNotes :: Notes st-  , cEntriesOrder :: EntriesOrder-  }--deriving stock instance Show (Contract cp st)-deriving stock instance Eq (ContractCode cp st) => Eq (Contract cp st)-instance NFData (Contract cp st) where-  rnf (Contract a b c d) = rnf (a, b, c, d)--defaultContract :: (ParameterScope cp, StorageScope st) => ContractCode cp st -> Contract cp st-defaultContract code = Contract-  { cCode = code-  , cParamNotes = starParamNotes-  , cStoreNotes = starNotes-  , cEntriesOrder = def-  }--mapContractCode-  :: (ContractCode cp st -> ContractCode cp st)-  -> Contract cp st-  -> Contract cp st-mapContractCode f contract = contract { cCode = f $ cCode contract }---- | Map each typed contract fields by the given function and sort the output--- based on the 'EntriesOrder'.-mapEntriesOrdered-  :: Contract cp st-  -> (ParamNotes cp -> a)-  -> (Notes st -> a)-  -> (ContractCode cp st -> a)-  -> [a]-mapEntriesOrdered Contract{..} fParam fStorage fCode =-  fmap snd-    $ sortWith fst-        [ (paramPos, fParam cParamNotes)-        , (storagePos, fStorage cStoreNotes)-        , (codePos, fCode cCode)-        ]-  where-    (paramPos, storagePos, codePos) = entriesOrderToInt cEntriesOrder  $(deriveGADTNFData ''Instr)

@@ -14,6 +14,7 @@   ) where  import Morley.Michelson.Typed.Aliases+import Morley.Michelson.Typed.Contract import Morley.Michelson.Typed.Convert import Morley.Michelson.Typed.Instr import Morley.Michelson.Typed.Scope

@@ -19,10 +19,10 @@ import Morley.Michelson.Interpret.Pack (toBinary, toBinary') import Morley.Michelson.Runtime.TxData (TxData(..)) import Morley.Michelson.Typed (EpName)-import Morley.Michelson.Typed.Aliases (Value)+import Morley.Michelson.Typed.Aliases (Contract, Value)+import Morley.Michelson.Typed.Contract (cCode) import Morley.Michelson.Typed.Entrypoints (EpAddress(..)) import Morley.Michelson.Typed.Haskell.Value (IsoValue(..))-import Morley.Michelson.Typed.Instr (Contract(..), cCode) import Morley.Michelson.Typed.Scope (ParameterScope, StorageScope) import Morley.Tezos.Address (Address(ContractAddress), ContractHash(..), GlobalCounter(..)) import Morley.Tezos.Core (Mutez(..))

@@ -212,6 +212,7 @@       then VOption $ Nothing       else VOption $ Just $         VPair (VInt (divMich i j), VNat $ fromInteger $ modMich i j)+ instance EDivOp 'TInt 'TNat where   type EDivOpRes 'TInt 'TNat = 'TInt   type EModOpRes 'TInt 'TNat = 'TNat@@ -222,6 +223,7 @@       then VOption $ Nothing       else VOption $ Just $         VPair (VInt (divMich i (toInteger j)), VNat $ fromInteger $ modMich i (toInteger j))+ instance EDivOp 'TNat 'TInt where   type EDivOpRes 'TNat 'TInt = 'TInt   type EModOpRes 'TNat 'TInt = 'TNat@@ -232,6 +234,7 @@       then VOption $ Nothing       else VOption $ Just $         VPair (VInt (divMich (toInteger i) j), VNat $ fromInteger $ modMich (toInteger i) j)+ instance EDivOp 'TNat 'TNat where   type EDivOpRes 'TNat 'TNat = 'TNat   type EModOpRes 'TNat 'TNat = 'TNat@@ -242,6 +245,7 @@       then VOption $ Nothing       else VOption $ Just $         VPair (VNat (divMich i j), VNat $ (modMich i j))+ instance EDivOp 'TMutez 'TMutez where   type EDivOpRes 'TMutez 'TMutez = 'TNat   type EModOpRes 'TMutez 'TMutez = 'TMutez

@@ -44,6 +44,7 @@   , ParameterScope   , UntypedValScope   , UnpackedValScope+  , ViewableScope    , ProperParameterBetterErrors   , ProperStorageBetterErrors@@ -52,6 +53,7 @@   , ProperPackedValBetterErrors   , ProperUnpackedValBetterErrors   , ProperUntypedValBetterErrors+  , ProperViewableBetterErrors   , ProperNonComparableValBetterErrors    , properParameterEvi@@ -60,6 +62,7 @@   , properDupableEvi   , properPackedValEvi   , properUnpackedValEvi+  , properViewableEvi   , properUntypedValEvi   , (:-)(..) @@ -244,6 +247,8 @@   IsComparable ('TLambda _ _) = 'False   IsComparable ('TMap _ _) = 'False   IsComparable ('TBigMap _ _) = 'False+  IsComparable 'TChest = 'False+  IsComparable 'TChestKey = 'False   IsComparable _            = 'True  -- | Constraint which ensures that a value of type @t@ does not contain operations.@@ -491,6 +496,8 @@   STBls12381G2 -> OpAbsent   STTimestamp -> OpAbsent   STAddress -> OpAbsent+  STChest -> OpAbsent+  STChestKey -> OpAbsent   STNever -> OpAbsent  -- | Check at runtime whether a value of the given type _may_ contain a @contract@ value.@@ -537,6 +544,8 @@   STBls12381G2 -> ContractAbsent   STTimestamp -> ContractAbsent   STAddress -> ContractAbsent+  STChest -> ContractAbsent+  STChestKey -> ContractAbsent   STNever -> ContractAbsent  -- | Check at runtime whether a value of the given type _may_ contain a @ticket@ value.@@ -583,6 +592,8 @@   STBls12381G2 -> TicketAbsent   STTimestamp -> TicketAbsent   STAddress -> TicketAbsent+  STChest -> TicketAbsent+  STChestKey -> TicketAbsent   STNever -> TicketAbsent  -- | Check at runtime whether a value of the given type _may_ contain a @big_map@ value.@@ -629,6 +640,8 @@   STBls12381G2 -> BigMapAbsent   STTimestamp -> BigMapAbsent   STAddress -> BigMapAbsent+  STChest -> BigMapAbsent+  STChestKey -> BigMapAbsent   STNever -> BigMapAbsent  -- | Check at runtime whether a value of the given type _may_ contain nested @big_map@s.@@ -676,6 +689,8 @@   STBls12381G2 -> NestedBigMapsAbsent   STTimestamp -> NestedBigMapsAbsent   STAddress -> NestedBigMapsAbsent+  STChest -> NestedBigMapsAbsent+  STChestKey -> NestedBigMapsAbsent   STNever -> NestedBigMapsAbsent  -- | Check at runtime that a value of the given type cannot contain operations.@@ -771,6 +786,15 @@ class (PackedValScope t, ConstantScope t) => UnpackedValScope t instance (PackedValScope t, ConstantScope t) => UnpackedValScope t +-- | Set of constraints that Michelson applies to argument type and+-- return type of views.+-- All info related to views can be found in+-- [TZIP](https://gitlab.com/tezos/tzip/-/blob/master/drafts/current/draft_views.md).+--+-- Not just a type alias in order to be able to partially apply it+class (SingI t, HasNoOp t, HasNoBigMap t, HasNoTicket t) => ViewableScope t+instance (SingI t, HasNoOp t, HasNoBigMap t, HasNoTicket t) => ViewableScope t+ -- | Alias for constraints which are required for untyped representation. type UntypedValScope t = (SingI t, HasNoOp t) @@ -833,6 +857,13 @@       <$> checkScope @(PackedValScope t)       <*> checkScope @(ConstantScope t) +instance SingI t => CheckScope (ViewableScope t) where+  checkScope =+    (\Dict Dict Dict -> Dict)+      <$> checkScope @(HasNoOp t)+      <*> checkScope @(HasNoBigMap t)+      <*> checkScope @(HasNoTicket t)+ -- | Allows using a scope that can be proven true with a De Morgan law. -- -- Many scopes are defined as @not a@ (or rather @a ~ 'False@) where @a@ is a@@ -977,6 +1008,9 @@ type ProperUnpackedValBetterErrors t =   (ProperPackedValBetterErrors t, ProperConstantBetterErrors t) +type ProperViewableBetterErrors t =+  (SingI t, ForbidOp t, ForbidBigMap t, ForbidTicket t)+ type ProperUntypedValBetterErrors t =   (SingI t, ForbidOp t) @@ -1015,6 +1049,12 @@ properUnpackedValEvi = Sub $   Dict \\ properPackedValEvi @t        \\ properConstantEvi @t++properViewableEvi :: forall t. ProperViewableBetterErrors t :- ViewableScope t+properViewableEvi = Sub $+  Dict \\ forbiddenOpEvi @t+       \\ forbiddenBigMapEvi @t+       \\ forbiddenTicketTypeEvi @t  properUntypedValEvi :: forall t. ProperUntypedValBetterErrors t :- UntypedValScope t properUntypedValEvi = Sub $

@@ -44,6 +44,8 @@   | TBls12381G2   | TTimestamp   | TAddress+  | TChest+  | TChestKey   | TNever   deriving stock (Eq, Show, Generic) @@ -70,6 +72,8 @@     convert TUnit = Un.TUnit     convert TSignature = Un.TSignature     convert TChainId = Un.TChainId+    convert TChest = Un.TChest+    convert TChestKey = Un.TChestKey     convert TNever = Un.TNever     convert (TOption a) = Un.TOption (toUType a)     convert (TList a) = Un.TList (toUType a)

@@ -37,14 +37,17 @@ import Data.Default (Default(..)) import qualified Data.Map as M import qualified Data.Set as S+import GHC.Exts (fromList) import qualified Text.Show  import Morley.Michelson.Text (MText) import Morley.Michelson.Typed.Aliases+import Morley.Michelson.Typed.Contract import Morley.Michelson.Typed.Instr import Morley.Michelson.Typed.Scope import qualified Morley.Michelson.Typed.T as T import Morley.Michelson.Typed.Value+import Morley.Michelson.Typed.View  -- | Options for 'dfsInstr'. data DfsSettings x = DfsSettings@@ -150,8 +153,15 @@       | otherwise -> step i     CREATE_CONTRACT contract       | dsGoToValues ->-        let updateContractCode code = CREATE_CONTRACT $ contract{ cCode = code }-        in recursion1 updateContractCode $ cCode contract+        let+          (codeI, codeX) = dfsInstr settings step (cCode contract)+          (viewsI, viewsX) = unzip $ toList (cViews contract) <&> \(SomeView v) ->+            first (\c -> SomeView v{ vCode = c }) $ dfsInstr settings step $ vCode v+          (i', x) = step $ CREATE_CONTRACT $ contract+            { cCode = codeI+            , cViews = UnsafeViewsSet $ fromList viewsI+            }+        in ceaApplyEffects dsCtorEffectsApp (sconcat $ codeX :| viewsX) x i'       | otherwise -> step i      Nop{} -> step i@@ -219,6 +229,7 @@     LE{} -> step i     GE{} -> step i     INT{} -> step i+    VIEW{} -> step i     SELF{} -> step i     CONTRACT{} -> step i     TRANSFER_TOKENS{} -> step i@@ -248,6 +259,7 @@     READ_TICKET{} -> step i     SPLIT_TICKET{} -> step i     JOIN_TICKETS{} -> step i+    OPEN_CHEST{} -> step i   where     recursion1 ::       forall a b c d. (Instr a b -> Instr c d) -> Instr a b -> (Instr c d, x)@@ -417,6 +429,7 @@     i@LE -> RfNormal i     i@GE -> RfNormal i     i@INT -> RfNormal i+    i@VIEW{} -> RfNormal i     i@SELF{} -> RfNormal i     i@CONTRACT{} -> RfNormal i     i@TRANSFER_TOKENS -> RfNormal i@@ -447,6 +460,7 @@     i@READ_TICKET -> RfNormal i     i@SPLIT_TICKET -> RfNormal i     i@JOIN_TICKETS -> RfNormal i+    i@OPEN_CHEST -> RfNormal i  -- | There are many ways to represent a sequence of more than 2 instructions. -- E. g. for @i1; i2; i3@ it can be @Seq i1 $ Seq i2 i3@ or @Seq (Seq i1 i2) i3@.@@ -524,6 +538,8 @@   VBls12381G2{} -> step i   VTimestamp{} -> step i   VAddress{} -> step i+  VChestKey{} -> step i+  VChest{} -> step i    -- Non-atomic   VOption mVal -> case mVal of@@ -687,6 +703,8 @@   VBls12381G2{} -> ConstantStorage v   VTimestamp{}  -> ConstantStorage v   VAddress{}    -> ConstantStorage v+  VChest{}      -> ConstantStorage v+  VChestKey{}   -> ConstantStorage v   VTicket{}     -> PartlyPushableStorage v Nop    -- Non-atomic

@@ -2,18 +2,12 @@ -- -- SPDX-License-Identifier: LicenseRef-MIT-TQ -{-# LANGUAGE QuantifiedConstraints #-}- -- | Module, containing data types for Michelson value.  module Morley.Michelson.Typed.Value   ( Comparability (..)   , Comparable   , ComparabilityScope-  , ContractInp1-  , ContractInp-  , ContractOut1-  , ContractOut   , CreateContract (..)   , Operation' (..)   , SetDelegate (..)@@ -41,14 +35,16 @@ import Fmt (Buildable(build), Builder, (+|), (|+))  import Morley.Michelson.Text (MText)+import Morley.Michelson.Typed.Contract import Morley.Michelson.Typed.Entrypoints import Morley.Michelson.Typed.Scope import Morley.Michelson.Typed.Sing import Morley.Michelson.Typed.T (T(..)) import Morley.Tezos.Address (Address, GlobalCounter(..)) import Morley.Tezos.Core (ChainId, Mutez, Timestamp)-import Morley.Tezos.Crypto (Bls12381Fr, Bls12381G1, Bls12381G2, KeyHash, PublicKey, Signature)-import Morley.Util.Sing (eqParamSing, eqParamSing3)+import Morley.Tezos.Crypto+  (Bls12381Fr, Bls12381G1, Bls12381G2, Chest, ChestKey, KeyHash, PublicKey, Signature)+import Morley.Util.Sing (eqParamMixed3, eqParamSing) import Morley.Util.TH  -- | Data type, representing operation, list of which is returned@@ -62,8 +58,8 @@     => TransferTokens instr p -> Operation' instr   OpSetDelegate :: SetDelegate -> Operation' instr   OpCreateContract-    :: ( Show (instr (ContractInp cp st) (ContractOut st))-       , NFData (instr (ContractInp cp st) (ContractOut st))+    :: ( forall i o. Show (instr i o)+       , forall i o. NFData (instr i o)        , Typeable instr, ParameterScope cp, StorageScope st)     => CreateContract instr cp st     -> Operation' instr@@ -83,7 +79,7 @@     (OpTransferTokens _, _) -> False     (OpSetDelegate sd1, OpSetDelegate sd2) -> sd1 == sd2     (OpSetDelegate _, _) -> False-    (OpCreateContract cc1, OpCreateContract cc2) -> cc1 `eqParamSing3` cc2+    (OpCreateContract cc1, OpCreateContract cc2) -> cc1 `eqParamMixed3` cc2     (OpCreateContract _, _) -> False  data TransferTokens instr p = TransferTokens@@ -111,19 +107,21 @@     "Set delegate to " <> maybe "<nobody>" build mbDelegate  data CreateContract instr cp st-  = ( Show (instr (ContractInp cp st) (ContractOut st))-    , Eq (instr (ContractInp cp st) (ContractOut st))+  = ( forall i o. Show (instr i o)+    , forall i o. Eq (instr i o)     )   => CreateContract   { ccOriginator :: Address   , ccDelegate :: Maybe KeyHash   , ccBalance :: Mutez   , ccStorageVal :: Value' instr st-  , ccContractCode :: instr (ContractInp cp st) (ContractOut st)+  , ccContract :: Contract' instr cp st   , ccCounter :: GlobalCounter   } -instance NFData (instr (ContractInp cp st) (ContractOut st)) => NFData (CreateContract instr cp st) where+instance+  ( forall i o. NFData (instr i o)+  ) => NFData (CreateContract instr cp st) where   rnf (CreateContract a b c d e f) = rnf (a, b, c, d, e, f)  instance Buildable (CreateContract instr cp st) where@@ -135,12 +133,6 @@ deriving stock instance Show (CreateContract instr cp st) deriving stock instance Eq (CreateContract instr cp st) -type ContractInp1 param st = 'TPair param st-type ContractInp param st = '[ ContractInp1 param st ]--type ContractOut1 st = 'TPair ('TList 'TOperation) st-type ContractOut st = '[ ContractOut1 st ]- -- | Wrapper over instruction which remembers whether this instruction -- always fails or not. data RemFail (instr :: k -> k -> Type) (i :: k) (o :: k) where@@ -261,6 +253,8 @@   STLambda _ _ -> CannotBeCompared   STMap _ _ -> CannotBeCompared   STBigMap _ _ -> CannotBeCompared+  STChest -> CannotBeCompared+  STChestKey -> CannotBeCompared   STNever -> CanBeCompared   STUnit -> CanBeCompared   STInt -> CanBeCompared@@ -360,6 +354,8 @@   VBls12381Fr :: Bls12381Fr -> Value' instr 'TBls12381Fr   VBls12381G1 :: Bls12381G1 -> Value' instr 'TBls12381G1   VBls12381G2 :: Bls12381G2 -> Value' instr 'TBls12381G2+  VChest      :: Chest -> Value' instr 'TChest+  VChestKey   :: ChestKey -> Value' instr 'TChestKey  deriving stock instance Show (Value' instr t) deriving stock instance Eq (Value' instr t)@@ -433,6 +429,8 @@   VBls12381G2{} -> Dict   VTimestamp{} -> Dict   VAddress{} -> Dict+  VChest{} -> Dict+  VChestKey{} -> Dict  -- | Provide a witness of that value's type is known. withValueTypeSanity :: Value' instr t -> (SingI t => a) -> a

@@ -0,0 +1,168 @@+-- SPDX-FileCopyrightText: 2021 Tocqueville Group+--+-- SPDX-License-Identifier: LicenseRef-MIT-TQ++-- 'newtype Container' deriving produced some fake warnings+{-# OPTIONS_GHC -Wno-redundant-constraints #-}++-- | Module, containing on-chain views declarations.+module Morley.Michelson.Typed.View+  ( -- * View+    ViewName (..)+  , mkViewName+  , unsafeMkViewName+  , viewNameToMText+  , ViewCode'+  , View' (..)+  , SomeView' (..)+  , someViewName++    -- * Views set+  , ViewsSet' (.., ViewsSet, ViewsList)+  , ViewsSetError (..)+  , mkViewsSet+  , emptyViewsSet+  , addViewToSet+  , lookupView+  , viewsSetNames+  , SomeViewsSet' (..)+  ) where++import Control.Monad.Except (throwError)+import Data.Default (Default(..))+import qualified Data.Sequence as Seq+import Fmt (Buildable(..), (+|), (|+))+import GHC.Exts (fromList)++import Morley.Michelson.Typed.Annotation+import Morley.Michelson.Typed.Scope+import Morley.Michelson.Typed.T (T(..))+import Morley.Michelson.Untyped.View (ViewName(..), mkViewName, unsafeMkViewName, viewNameToMText)+import Morley.Util.Sing+++type ViewCode' instr arg st ret = instr '[ 'TPair arg st] '[ret]++-- | Contract view.+data View' instr arg st ret = (ViewableScope arg, SingI st, ViewableScope ret) => View+  { vName :: ViewName+    -- ^ Name of the view.+  , vArgument :: Notes arg+    -- ^ Argument type annotations.+  , vReturn :: Notes ret+    -- ^ Return type annotations.+  , vCode :: ViewCode' instr arg st ret+    -- ^ View code.+  }++deriving stock instance Show (ViewCode' instr arg st ret) => Show (View' instr arg st ret)+deriving stock instance Eq (ViewCode' instr arg st ret) => Eq (View' instr arg st ret)+instance NFData (ViewCode' instr arg st ret) => NFData (View' instr arg st ret) where+  rnf (View a b c d) = rnf (a, b, c, d)++data SomeView' instr st where+  SomeView :: View' instr arg st ret -> SomeView' instr st++deriving stock instance+  (forall arg ret. Show (ViewCode' instr arg st ret)) =>+  Show (SomeView' instr st)+instance+  (forall arg ret. Eq (ViewCode' instr arg st ret)) =>+  Eq (SomeView' instr st) where+    SomeView v1@View{} == SomeView v2@View{} = v1 `eqParamSing3` v2+instance+  (forall arg ret. NFData (ViewCode' instr arg st ret)) =>+  NFData (SomeView' instr st) where+    rnf (SomeView v) = rnf v++-- | Obtain the name of the view.+someViewName :: SomeView' instr st -> ViewName+someViewName (SomeView v) = vName v++-- View sets+----------------------------------------------------------------------------++-- | Views that belong to one contract.+--+-- Invariant: all view names are unique.+--+-- Implementation note: lookups still take linear time.+-- We use 'Seq' for simplicity, as in either case we need to preserve the order+-- of views (so that decoding/encoding roundtrip).+newtype ViewsSet' instr st = UnsafeViewsSet { unViewsSet :: Seq $ SomeView' instr st }+  deriving newtype (Default, Container)++deriving stock instance+  (forall i o. Show (instr i o)) =>+  Show (ViewsSet' instr st)+deriving stock instance+  (forall i o. Eq (instr i o)) =>+  Eq (ViewsSet' instr st)+instance+  (forall i o. NFData (instr i o)) =>+  NFData (ViewsSet' instr st) where+    rnf (ViewsSet vs) = rnf vs++pattern ViewsSet :: Seq (SomeView' instr st) -> ViewsSet' instr st+pattern ViewsSet views <- UnsafeViewsSet views+{-# COMPLETE ViewsSet #-}++pattern ViewsList :: [SomeView' instr st] -> ViewsSet' instr st+pattern ViewsList views <- ViewsSet (toList -> views)+{-# COMPLETE ViewsList #-}++-- | Errors possible when constructing 'ViewsSet\''.+data ViewsSetError+  = DuplicatedViewName ViewName+  deriving stock (Show, Eq)++instance Buildable ViewsSetError where+  build = \case+    DuplicatedViewName name -> "Duplicated view name '" +| name |+ "'"++-- | Construct views set.+mkViewsSet :: [SomeView' instr st] -> Either ViewsSetError (ViewsSet' instr st)+mkViewsSet views = do+  forM_ (group . sort $ map someViewName views) $ \case+    name : _ : _ -> throwError $ DuplicatedViewName name+    _ : _ -> pass+    [] -> error "impossible"+  pure (UnsafeViewsSet $ fromList views)++-- | No views.+emptyViewsSet :: ViewsSet' instr st+emptyViewsSet = UnsafeViewsSet mempty++-- | Add a view to set.+addViewToSet+  :: View' instr arg st ret+  -> ViewsSet' instr st+  -> Either ViewsSetError (ViewsSet' instr st)+addViewToSet v views = do+  when (vName v `elem` viewsSetNames views) $+    throwError $ DuplicatedViewName (vName v)+  return (UnsafeViewsSet $ unViewsSet views Seq.|> SomeView v)++-- | Find a view in the set.+lookupView :: ViewName -> ViewsSet' instr st -> Maybe (SomeView' instr st)+lookupView name (ViewsSet views) =+  find (\(SomeView View{..}) -> vName == name) views++-- | Get all taken names in views set.+viewsSetNames :: ViewsSet' instr st -> [ViewName]+viewsSetNames = map someViewName . toList++data SomeViewsSet' instr where+  SomeViewsSet :: SingI st => ViewsSet' instr st -> SomeViewsSet' instr++deriving stock instance+  (forall i o. Show (instr i o)) =>+  Show (SomeViewsSet' instr)+instance+  (forall i o. Eq (instr i o)) =>+  Eq (SomeViewsSet' instr) where+    SomeViewsSet vs1 == SomeViewsSet vs2 = eqParamSing vs1 vs2+instance+  (forall i o. NFData (instr i o)) =>+  NFData (SomeViewsSet' instr) where+    rnf (SomeViewsSet vs) = rnf vs

@@ -15,3 +15,4 @@ import Morley.Michelson.Untyped.OpSize as Exports import Morley.Michelson.Untyped.Type as Exports import Morley.Michelson.Untyped.Value as Exports+import Morley.Michelson.Untyped.View as Exports

@@ -6,6 +6,7 @@  module Morley.Michelson.Untyped.Aliases   ( Contract+  , View   , Value   , ExpandedExtInstr   ) where@@ -16,5 +17,6 @@ import qualified Morley.Michelson.Untyped.Value as Untyped  type Value = Untyped.Value' Untyped.ExpandedOp+type View = Untyped.View' Untyped.ExpandedOp type Contract = Untyped.Contract' Untyped.ExpandedOp type ExpandedExtInstr = Untyped.ExtInstrAbstract Untyped.ExpandedOp

@@ -14,20 +14,25 @@   , orderContractBlock    , Contract' (..)+  , View' (..)   , Storage+  , mapContractCode   ) where  import Data.Aeson.TH (deriveJSON) import Data.Data (Data(..)) import Data.Default (Default(..)) import Fmt (Buildable(build))-import Text.PrettyPrint.Leijen.Text (nest, semi, text, (<$$>), (<+>))+import Text.PrettyPrint.Leijen.Text (indent, nest, semi, text, (<$$>), (<+>))  import Morley.Michelson.Printer.Util   (Prettier(..), RenderDoc(..), assertParensNotNeeded, buildRenderDoc, needsParens, renderOpsList) import Morley.Michelson.Untyped.Type (ParameterType(..), Ty(..))+import Morley.Michelson.Untyped.View import Morley.Util.Aeson +-- TODO [#698]: views are yet handled in a very hacky and not fully working way+ -- | Top-level entries order of the contract. -- This is preserved due to the fact that it affects -- the output of pretty-printing and serializing contract.@@ -71,19 +76,26 @@   = CBParam ParameterType   | CBStorage Ty   | CBCode [op]-  deriving stock (Eq, Show)+  | CBView (View' op)+  deriving stock (Eq, Show, Functor) --- | Construct a contract representation from three different contract blocks (i.e. parameters,--- storage and code blocks) in arbitrary order. This saves the order in the contract so that--- it can print the contract blocks in the same order it was parsed.-orderContractBlock :: (ContractBlock op, ContractBlock op, ContractBlock op) -> Maybe (Contract' op)-orderContractBlock = \case-  (CBParam   p, CBStorage s, CBCode    c) -> Just $ Contract p s c PSC-  (CBParam   p, CBCode    c, CBStorage s) -> Just $ Contract p s c PCS-  (CBStorage s, CBParam   p, CBCode    c) -> Just $ Contract p s c SPC-  (CBStorage s, CBCode    c, CBParam   p) -> Just $ Contract p s c SCP-  (CBCode    c, CBStorage s, CBParam   p) -> Just $ Contract p s c CSP-  (CBCode    c, CBParam   p, CBStorage s) -> Just $ Contract p s c CPS+-- | Construct a contract representation from the contract blocks (i.e. parameters,+-- storage, code blocks, etc.) in arbitrary order.+-- This makes sure that unique blocks like @code@ do not duplicate, and saves the+-- order in the contract so that it can print the contract blocks in the same+-- order it was parsed. TODO [#698]: this is not fully true now.+orderContractBlock :: [ContractBlock op] -> Maybe (Contract' op)+orderContractBlock blocks =+  let+    vs = mapMaybe (\case CBView v -> Just v; _ -> Nothing) blocks+    plain = filter (\case CBView{} -> False; _ -> True) blocks+  in case plain of+  [CBParam   p, CBStorage s, CBCode    c] -> Just $ Contract p s c PSC vs+  [CBParam   p, CBCode    c, CBStorage s] -> Just $ Contract p s c PCS vs+  [CBStorage s, CBParam   p, CBCode    c] -> Just $ Contract p s c SPC vs+  [CBStorage s, CBCode    c, CBParam   p] -> Just $ Contract p s c SCP vs+  [CBCode    c, CBStorage s, CBParam   p] -> Just $ Contract p s c CSP vs+  [CBCode    c, CBParam   p, CBStorage s] -> Just $ Contract p s c CPS vs   _                                       -> Nothing  -- | Map each contract fields by the given function and sort the output@@ -93,14 +105,17 @@   -> (ParameterType -> a)   -> (Storage -> a)   -> ([op] -> a)+  -> (View' op -> a)   -> [a]-mapEntriesOrdered Contract{..} fParam fStorage fCode =-  fmap snd-    $ sortWith fst+mapEntriesOrdered Contract{..} fParam fStorage fCode fView =+  mconcat+    [ fmap snd $ sortWith fst         [ (paramPos, fParam contractParameter)         , (storagePos, fStorage contractStorage)         , (codePos, fCode contractCode)         ]+    , fmap fView contractViews+    ]   where     (paramPos, storagePos, codePos) = entriesOrderToInt entriesOrder @@ -118,6 +133,8 @@   , entriesOrder :: EntriesOrder     -- ^ Original order of contract blocks, so that we can print them     -- in the same order they were read+  , contractViews :: [View' op]+    -- ^ Contract views   } deriving stock (Eq, Show, Functor, Data, Generic)  instance NFData op => NFData (Contract' op)@@ -130,9 +147,26 @@         (\parameter -> "parameter" <+> renderDoc needsParens (Prettier parameter) <> semi)         (\storage -> "storage" <+> renderDoc needsParens (Prettier storage) <> semi)         (\code -> "code" <+> nest (length ("code {" :: Text)) (renderOpsList False code <> semi))+        (\View{..} -> "view" <+> renderViewName viewName+           <+> renderDoc needsParens viewArgument+           <+> renderDoc needsParens viewReturn+           <$$> indent 5  -- 5 is forced by Michelson+                 (renderOpsList False viewCode)+           <> semi+          )  instance RenderDoc op => Buildable (Contract' op) where   build = buildRenderDoc++-- | Map all the instructions appearing in the contract.+mapContractCode :: (op -> op) -> Contract' op -> Contract' op+mapContractCode f (Contract param st code o vs) =+  Contract+    param+    st+    (code <&> f)+    o+    (vs <&> \v -> v{ viewCode = viewCode v <&> f })  deriveJSON morleyAesonOptions ''EntriesOrder deriveJSON morleyAesonOptions ''Contract'

@@ -30,6 +30,7 @@ import Morley.Michelson.Untyped.Ext (ExtInstrAbstract) import Morley.Michelson.Untyped.Type (Ty) import Morley.Michelson.Untyped.Value (Value'(..))+import Morley.Michelson.Untyped.View import Morley.Util.Aeson  -------------------------------------@@ -176,6 +177,7 @@   | LE                VarAnn   | GE                VarAnn   | INT               VarAnn+  | VIEW              VarAnn ViewName Ty   | SELF              VarAnn FieldAnn   | CONTRACT          VarAnn FieldAnn Ty   | TRANSFER_TOKENS   VarAnn@@ -206,6 +208,7 @@   | READ_TICKET       VarAnn   | SPLIT_TICKET      VarAnn   | JOIN_TICKETS      VarAnn+  | OPEN_CHEST        VarAnn   deriving stock (Eq, Functor, Data, Generic)  instance RenderDoc (InstrAbstract op) => Show (InstrAbstract op) where@@ -302,6 +305,7 @@     LE va                   -> "LE" <+> renderAnnot va     GE va                   -> "GE" <+> renderAnnot va     INT va                  -> "INT" <+> renderAnnot va+    VIEW va name ty         -> "VIEW" <+> renderAnnot va <+> renderViewName name <+> renderTy ty     SELF va fa              -> "SELF" <+> renderAnnots [] [fa] [va]     CONTRACT va fa t        -> "CONTRACT" <+> renderAnnots [] [fa] [va] <+> renderTy t     TRANSFER_TOKENS va      -> "TRANSFER_TOKENS" <+> renderAnnot va@@ -334,6 +338,7 @@     READ_TICKET va          -> "READ_TICKET" <+> renderAnnot va     SPLIT_TICKET va         -> "SPLIT_TICKET" <+> renderAnnot va     JOIN_TICKETS va         -> "JOIN_TICKETS" <+> renderAnnot va+    OPEN_CHEST va           -> "OPEN_CHEST" <+> renderAnnot va     where       renderTy = renderDoc @Ty needsParens       renderComp = renderDoc @Ty needsParens

@@ -39,6 +39,7 @@ import Morley.Michelson.Untyped.Instr import Morley.Michelson.Untyped.Type import Morley.Michelson.Untyped.Value+import Morley.Michelson.Untyped.View  -- | Operation size in bytes. --@@ -140,6 +141,7 @@   GT va -> annsOpSize va   GE va -> annsOpSize va   INT va -> annsOpSize va+  VIEW va n t -> annsOpSize va <> viewNameSize n <> typeOpSize t   SELF va fa -> annsOpSize va fa   CONTRACT va fa t -> annsOpSize va fa <> typeOpSize t   TRANSFER_TOKENS va -> annsOpSize va@@ -170,6 +172,7 @@   READ_TICKET va -> annsOpSize va   SPLIT_TICKET va -> annsOpSize va   JOIN_TICKETS va -> annsOpSize va+  OPEN_CHEST va -> annsOpSize va   where     subcodeOpSize is = expandedInstrOpSize (SeqEx is)     ifOpSize l r = expandedInstrOpSize (SeqEx l) <> expandedInstrOpSize (SeqEx r)@@ -184,9 +187,22 @@ expandedInstrsOpSize :: [ExpandedOp] -> OpSize expandedInstrsOpSize = foldMap expandedInstrOpSize +viewNameSize :: ViewName -> OpSize+viewNameSize = OpSize . Unsafe.fromIntegral @Int @Word . length . unViewName++viewOpSize :: View -> OpSize+viewOpSize (View name param ret code) = mconcat+  [ OpSize 2+  , viewNameSize name+  , typeOpSize param+  , typeOpSize ret+  , expandedInstrsOpSize code+  ]+ contractOpSize :: Contract -> OpSize-contractOpSize (Contract (ParameterType cp rootAnn) st is _) =+contractOpSize (Contract (ParameterType cp rootAnn) st is _ view_) =   OpSize 16 <> typeOpSize' [rootAnn] cp <> typeOpSize st <> expandedInstrsOpSize is+  <> foldMap viewOpSize view_  numOpSize :: Integral i => i -> OpSize numOpSize = OpSize . Unsafe.fromIntegral @Int @Word . length . encodeZarithNumber . fromIntegral@@ -251,6 +267,8 @@     TBls12381G2 -> mempty     TTimestamp -> mempty     TAddress -> mempty+    TChest -> mempty+    TChestKey -> mempty     TNever -> mempty  innerOpSize :: Ty -> OpSize

@@ -139,6 +139,8 @@     TSignature        -> wrapInParens pn $ "signature" :| [annDoc]     TChainId          -> wrapInParens pn $ "chain_id" :| [annDoc]     TOperation        -> wrapInParens pn $ "operation" :| [annDoc]+    TChest            -> wrapInParens pn $ "chest" :| [annDoc]+    TChestKey         -> wrapInParens pn $ "chest_key" :| [annDoc]     TNever            -> wrapInParens pn $ "never" :| [annDoc]      TOption (Ty t1 ta1) ->@@ -245,6 +247,8 @@   | TBls12381G2   | TTimestamp   | TAddress+  | TChest+  | TChestKey   | TNever   deriving stock (Eq, Show, Data, Generic) 

@@ -0,0 +1,109 @@+-- SPDX-FileCopyrightText: 2021 Tocqueville Group+--+-- SPDX-License-Identifier: LicenseRef-MIT-TQ++-- | Michelson view.+module Morley.Michelson.Untyped.View+  ( ViewName (.., ViewName)+  , mkViewName+  , unsafeMkViewName+  , BadViewNameError (..)+  , isValidViewNameChar+  , viewNameMaxLength+  , renderViewName+  , viewNameToMText++  , View' (..)+  ) where++import Control.Monad.Except (throwError)+import Data.Aeson.TH (deriveJSON)+import Data.Data (Data)+import qualified Data.Text as Text+import Fmt (Buildable(..), pretty, (+|), (|+))+import Text.PrettyPrint.Leijen.Text (Doc, dquotes, textStrict)++import Morley.Michelson.Printer.Util+import Morley.Michelson.Text+import Morley.Michelson.Untyped.Type+import Morley.Util.Aeson++-- | Name of the view.+--+-- 1. It must not exceed 31 chars length;+-- 2. Must use [a-zA-Z0-9_.%@] charset.+newtype ViewName = UnsafeViewName { unViewName :: Text }+  deriving stock (Show, Eq, Ord, Data, Generic)+  deriving newtype (Buildable, NFData)++pattern ViewName :: Text -> ViewName+pattern ViewName name <- UnsafeViewName name+{-# COMPLETE ViewName #-}++-- | Whether the given character is valid for a view.+isValidViewNameChar :: Char -> Bool+isValidViewNameChar c = or+  [ 'A' <= c && c <= 'Z'+  , 'a' <= c && c <= 'z'+  , '0' <= c && c <= '9'+  , c `elem` ['_', '.', '%', '@']+  ]++-- | Maximum allowed name length for a view.+viewNameMaxLength :: Int+viewNameMaxLength = 31++data BadViewNameError+  = BadViewTooLong Int+  | BadViewIllegalChars Text+  deriving stock (Show, Eq, Ord, Data, Generic)+  deriving anyclass (NFData)++instance Buildable BadViewNameError where+  build = \case+    BadViewTooLong l ->+      "Bad view name length of " +| l |+ " characters, must not exceed \+      \" +| viewNameMaxLength |+ " characters length"+    BadViewIllegalChars txt ->+      "Invalid characters in the view \"" +| txt |+ ", allowed characters set \+      \is [a-zA-Z0-9_.%@]"++-- | Construct t'ViewName' performing all the checks.+mkViewName :: Text -> Either BadViewNameError ViewName+mkViewName txt = do+  unless (length txt <= viewNameMaxLength) $+    throwError (BadViewTooLong $ length txt)+  unless (Text.all isValidViewNameChar txt) $+    throwError (BadViewIllegalChars txt)+  return (UnsafeViewName txt)++-- | Unsafe constructor for t'ViewName'.+unsafeMkViewName :: HasCallStack => Text -> ViewName+unsafeMkViewName = either (error . pretty) id . mkViewName++renderViewName :: ViewName -> Doc+renderViewName = dquotes . textStrict . unViewName++instance RenderDoc ViewName where+  renderDoc _ = renderViewName++-- | Valid view names form a subset of valid Michelson texts.+viewNameToMText :: ViewName -> MText+viewNameToMText = unsafeMkMText . unViewName++-- | Untyped view in a contract.+data View' op = View+  { viewName :: ViewName+    -- ^ View name+  , viewArgument :: Ty+    -- ^ View argument type+  , viewReturn :: Ty+    -- ^ View return type+  , viewCode :: [op]+    -- ^ View code+  } deriving stock (Eq, Show, Functor, Data, Generic)++instance NFData op => NFData (View' op)++deriveJSON morleyAesonOptions ''ViewName+deriveJSON morleyAesonOptions ''View'

@@ -84,6 +84,15 @@   , sha3   , sha512 +  -- * Timelock puzzle+  , Chest+  , ChestKey+  , OpeningResult(..)+  , TLTime(..)+  , openChest+  , mkTLTime+  , unsafeMkTLTime+   -- * Utilities   , encodeBase58Check   , decodeBase58Check@@ -113,6 +122,8 @@ import Morley.Tezos.Crypto.Hash import qualified Morley.Tezos.Crypto.P256 as P256 import qualified Morley.Tezos.Crypto.Secp256k1 as Secp256k1+import Morley.Tezos.Crypto.Timelock+  (Chest, ChestKey, OpeningResult(..), TLTime(..), mkTLTime, openChest, unsafeMkTLTime) import Morley.Tezos.Crypto.Util import Morley.Util.Binary import Morley.Util.CLI

@@ -380,14 +380,14 @@   in assert (remainder == 0) bytes  -- | Turn a prime field element into a natural.-fromPrime :: KnownNat p => GF.Prime p -> Natural+fromPrime :: forall p. KnownNat p => GF.Prime p -> Natural fromPrime p =   -- This should be safe, since 'Prime's exist in modular arithmetics,   -- so its conversion to an integer should produce non-negative elements.   -- In fact, 'GF.Prime' is a newtype wrapper over 'Natural', but   -- its constructor is not exported :/   assert (p >= 0) $-    Unsafe.fromIntegral p+    Unsafe.fromIntegral @(GF.Prime p) @Natural p  -- | The inverse to 'fromPrime'. toPrime :: KnownNat p => Natural -> GF.Prime p

@@ -0,0 +1,430 @@+-- SPDX-FileCopyrightText: 2021 Tocqueville Group+--+-- SPDX-License-Identifier: LicenseRef-MIT-TQ++{- | Timelock puzzle algorithms implementation.++This module follows the reference implementation for the most part,+which you can find in the+[tezos repository](https://gitlab.com/tezos/tezos/-/blob/b1a2ff0334405cafd7465bfa991d23844f0b4e70/src/lib_crypto/timelock.ml).++For a more high-level overview of the concepts, refer to the [timelock+documentation page](http://tezos.gitlab.io/011/timelock.html).++The general idea is built upon [Rivest, Shamir, Wagner "Time-lock puzzles and+timed-release Crypto"](http://www.hashcash.org/papers/time-lock.pdf), there+are however some differences from the paper:++* The paper suggests using RC5 cipher, which Tezos implementation+eschews in favor of NaCl's "secret box".+* The paper suggest generating the symmetric secret key \(K\) directly, then+encrypting it with a randomly chosen value \(a\) as \(C_K = K + a^{2^t} \pmod n\).+Tezos implementation instead randomly generates only \(a\), and then produces+the secret key using BLAKE2b KDF with a fixed key from \(a^{2^t} \pmod n\).+* Since the secret key is determined only by the "unlocked" value, the+time-locked value representation also differs. In the paper it's represented as+\((n,a,t,C_K,C_M)\), i.e. the tuple of modulus, "locked" value, time,+encrypted key and encrypted message. In Tezos implementation it's instead+\((a,n,C_M)\), and \(t\) is treated as a separate argument.+* Likely to guard the protocol from guessing attacks, additional "proof"+verification is added, described in+[Boneh, Bünz, Fisch "A Survey of Two Verifiable Delay Functions"](https://eprint.iacr.org/2018/712.pdf)+-}+module Morley.Tezos.Crypto.Timelock+  ( TLTime(.., TLTime)+  , Chest(..)+  , ChestKey(..)+  , Ciphertext(..)+  , OpeningResult(..)+  , createChestAndChestKey+  , createChestKey+  , chestBytes+  , chestKeyBytes+  , chestFromBytes+  , chestKeyFromBytes+  , openChest+  , mkTLTime+  , unsafeMkTLTime+  -- * Internal, not safe for cryptography+  , createChestAndChestKeyFromSeed+  ) where++import Control.Monad.Random (evalRand, genByteString, getRandomR, liftRand, mkStdGen)+import Crypto.Number.ModArithmetic (expFast)+import Crypto.Number.Prime (findPrimeFrom)+import Crypto.Number.Serialize.LE (i2osp, os2ip)+import qualified Crypto.Sodium.Encrypt.Symmetric as Box (Key, Nonce, decrypt, encrypt)+import Crypto.Sodium.Hash (blake2bWithKey)+import qualified Crypto.Sodium.Nonce as Nonce (generate)+import qualified Crypto.Sodium.Random as Random (generate)+import qualified Data.Binary as Bi (Binary(..), decodeOrFail, encode)+import qualified Data.Binary.Get as Bi (getByteString)+import qualified Data.Binary.Put as Bi (putBuilder)+import Data.Bits (Bits, shiftL)+import Data.ByteArray.Sized (SizedByteArray, sizedByteArray, unSizedByteArray)+import qualified Data.ByteString as BS (intercalate, length, replicate)+import qualified Data.ByteString.Lazy as LBS (fromStrict, toStrict)+import Fmt (Buildable(..))+import GHC.TypeNats (Div, type (+))+import qualified Options.Applicative as Opt++import Morley.Micheline.Binary.Internal+import Morley.Util.CLI++-- | RSA-inspired prime factors, which produce (literally) the 'PublicModulus'.+--+-- This value should be kept secret.+data RSAFactors = RSAFactors { rsaP :: Integer, rsaQ :: Integer }+  deriving stock Show++-- | RSA-inspired semi-prime modulus.+newtype PublicModulus = PublicModulus { unPublicModulus :: Integer }+  deriving stock (Show, Eq)+  deriving newtype NFData++-- | The "locked" value. Essentially a random integer between 0 and+-- 'PublicModulus' (exclusive).+newtype Locked = Locked { unLocked :: Integer }+  deriving stock (Show, Eq)+  deriving newtype NFData++-- | The "unlocked" value, i.e. \(a^{2^t} \pmod n\), where \(a\) is 'Locked'+-- value, \(t\) is t'TLTime' and \(n\) is 'PublicModulus'.+newtype Unlocked = Unlocked { unUnlocked :: Integer }+  deriving stock (Show, Eq)+  deriving newtype NFData++-- | The key for the symmetric encryption, \(K\).+newtype SymmetricKey = SymmetricKey (Box.Key ByteString)+  deriving stock Show++{- | A "proof" that the chest was opened fairly, i.e. the key wasn't just+guessed.++The proof is verified by checking that++\[+  a ^ (2 ^ t) = (p ^ l) (a ^ r) \pmod n+\]++which is equivalent to++\[+  2 ^ t = (((2 ^ t) / l) * l) + (2 ^ t \mod l) \pmod {\phi(n)}+\]++where \(a\) is a 'Locked' value, \(t\) is t'TLTime', \(p\) is 'Proof', \(n\) is+'PublicModulus', \(l\) is a prime, chosen deterministically from the hash+of the puzzle, and \(r = 2^t \pmod l\)++What this essentially boils down to, is that we can compute the "proof" either+as++\[+  p = a^{2^t / l \mod {\phi(n)}} \pmod n+\]++if we know the modulo factorization, or++\[+  p = a^{2^t / l} \pmod n+\]++if we don't.++See https://eprint.iacr.org/2018/712.pdf section 3.2.+-}+newtype Proof = Proof { unProof :: Integer }+  deriving stock (Show, Eq)+  deriving newtype NFData++-- | Number of steps a timelock needs to be opened without knowing a "secret",+-- i.e. modulo factorization.+--+-- The reference implementation uses OCaml @int@, and it can only be positive,+-- so on 64-bit architecture it's actually a 62-bit natural. We use 'Word64'+-- to represent it.+newtype TLTime = UnsafeTLTime { unTLTime :: Word64 }+  deriving stock (Show, Eq)+  deriving newtype Num++pattern TLTime :: Word64 -> TLTime+pattern TLTime x <- UnsafeTLTime x+{-# COMPLETE TLTime #-}++instance Bounded TLTime where+  minBound = UnsafeTLTime 0+  -- 2⁶² - 1+  -- This value was checked against the reference implementation.+  maxBound = UnsafeTLTime 4611686018427387903++instance HasCLReader TLTime where+  getReader = either (readerError . toString) pure . mkTLTime @Word64 =<< Opt.auto+  getMetavar = "TIME"++instance Buildable TLTime where+  build = build . unTLTime++-- | Safely creates t'TLTime' checking for+-- overflow and underflow. Accepts a number of any type.+mkTLTime :: (Integral i, Bits i) => i -> Either Text TLTime+mkTLTime i = case fromIntegralMaybe i of+  Just n | n <= unTLTime maxBound -> Right (UnsafeTLTime n)+  _ | i < 0 -> Left "TLTime underflow"+  _ -> Left "TLTime overflow"++-- | Partial function for t'TLTime' creation, it's pre-condition is that+-- the argument must not exceed bounds of the t'TLTime'.+unsafeMkTLTime :: HasCallStack => Word64 -> TLTime+unsafeMkTLTime n =+  either (error . ("unsafeMkTLTime: " <>)) id $ mkTLTime n+{-# INLINE unsafeMkTLTime #-}++-- | A nonce for symmetric encryption.+newtype Nonce = Nonce { unNonce :: Box.Nonce ByteString }+  deriving stock (Show, Eq)++instance NFData Nonce where+  rnf (Nonce x) = rnf $ unSizedByteArray x++-- | Ciphertext with nonce.+data Ciphertext = Ciphertext+  { ctNonce :: Nonce+  , ctPayload :: ByteString+  } deriving stock (Show, Eq, Generic)+    deriving anyclass NFData++instance Bi.Binary Ciphertext where+  put Ciphertext{..} = Bi.putBuilder $+      buildByteString (unSizedByteArray $ unNonce ctNonce)+   <> buildDynamic buildByteString (DynamicSize ctPayload)+  get = do+    mbNonce <- sizedByteArray <$> Bi.getByteString 24+    ctNonce <- case mbNonce of+      Just sza -> pure $ Nonce sza+      Nothing -> fail "Incorrect nonce size"+        -- NB: this shouldn't happen unless NaCl box changes nonce size+    DynamicSize ctPayload <- getDynamic getByteString+    when (BS.length ctPayload <= secretBoxTagBytes) $+      fail "Ciphertext size <= 0"+    pure $ Ciphertext{..}+    where+      -- This is hard-coded in the reference implementation,+      -- https://gitlab.com/tezos/tezos/-/blob/b1a2ff0334405cafd7465bfa991d23844f0b4e70/src/lib_hacl_glue/unix/hacl.ml#L183+      -- but essentially this is the length of a NaCl box ciphertext with+      -- empty payload+      secretBoxTagBytes = 16++-- | A chest "key" with proof that it was indeed opened fairly.+data ChestKey = ChestKey+  { ckUnlockedVal :: Unlocked+  , ckProof :: Proof+  } deriving stock (Show, Eq, Generic)+    deriving anyclass NFData++instance Bi.Binary ChestKey where+  put ChestKey{..} = Bi.putBuilder $+    buildNatural (unUnlocked ckUnlockedVal) <> buildNatural (unProof ckProof)+  get = ChestKey <$> (Unlocked <$> getNatural) <*> (Proof <$> getNatural)++-- | A locked chest+data Chest = Chest+  { chestLockedVal :: Locked+  , chestPublicModulus :: PublicModulus+  , chestCiphertext :: Ciphertext+  } deriving stock (Show, Eq, Generic)+    deriving anyclass NFData++instance Bi.Binary Chest where+  put Chest{..} = do+    Bi.putBuilder $ buildNatural (unLocked chestLockedVal)+                 <> buildNatural (unPublicModulus chestPublicModulus)+    Bi.put chestCiphertext++  get = do+    chestLockedVal <- Locked <$> getNatural+    chestPublicModulus <- PublicModulus <$> getNatural+    when (unLocked chestLockedVal >= unPublicModulus chestPublicModulus) $+      fail "locked value is not in the rsa group"+    when (unPublicModulus chestPublicModulus <= minPublicModulus) $+      fail "public modulus is too small"+    chestCiphertext <- Bi.get+    pure Chest{..}+    where+      -- hard-coded in the reference implementation+      -- https://gitlab.com/tezos/tezos/-/blob/b1a2ff0334405cafd7465bfa991d23844f0b4e70/src/lib_crypto/timelock.ml#L193+      minPublicModulus = shiftL 2 2000++type SizeModulus = 256 -- bytes, i.e. 2048 bits+type HalfModulus = Div SizeModulus 2 -- bytes, i.e. 1024 bits++randomInt :: forall n. (KnownNat n) => IO Integer+randomInt = os2ip <$> Random.generate @ByteString @n++randomPrime :: forall n. (KnownNat n) => IO Integer+randomPrime = findPrimeFrom <$> randomInt @n++unlockedValueToSymmetricKey :: Unlocked -> SymmetricKey+unlockedValueToSymmetricKey (Unlocked value) =+  -- "Tezoskdftimelockv0" is hard-coded in the reference implementation+  -- see https://gitlab.com/tezos/tezos/-/blob/b1a2ff0334405cafd7465bfa991d23844f0b4e70/src/lib_crypto/timelock.ml#L47+  let key :: ByteString = "Tezoskdftimelockv0"+      str :: ByteString = show value+  in SymmetricKey $ blake2bWithKey @32 @ByteString key str++genRSAFactors :: IO (PublicModulus, RSAFactors)+genRSAFactors = do+  p <- randomPrime @HalfModulus+  q <- randomPrime @HalfModulus+  pure (PublicModulus (p * q), RSAFactors p q)++genLockedValue :: PublicModulus -> IO Locked+genLockedValue (PublicModulus pub) = do+  z <- randomInt @(SizeModulus + 16)+  pure . Locked $ z `mod` pub++hashToPrime :: PublicModulus -> TLTime -> Locked -> Unlocked -> Integer+hashToPrime (PublicModulus pub) (TLTime time) (Locked locked) (Unlocked unlocked) =+  -- "\32" and "\xff\x00\xff\x00\xff\x00\xff\x00" are hard-coded in the reference implementation+  -- see https://gitlab.com/tezos/tezos/-/blob/b1a2ff0334405cafd7465bfa991d23844f0b4e70/src/lib_crypto/timelock.ml#L78+  -- and https://gitlab.com/tezos/tezos/-/blob/b1a2ff0334405cafd7465bfa991d23844f0b4e70/src/lib_crypto/timelock.ml#L81+  let personalization :: ByteString = "\32"+      s = BS.intercalate "\xff\x00\xff\x00\xff\x00\xff\x00" $+        show time : map (pad . i2osp) [pub, locked, unlocked]+      hash_result :: SizedByteArray 32 ByteString = blake2bWithKey personalization s+  in findPrimeFrom (os2ip hash_result)+  where+    -- pads right with zero bytes so that length is multiple of 8+    -- this is needed due to a quirk of how @Z.to_bits@ works in OCaml+    pad bs =+      let len = length bs+          newlen = ceiling ((fromIntegralOverflowing len :: Rational) / 8) * 8+          diff = newlen - len+      in bs <> BS.replicate diff 0++proveWithoutSecret :: PublicModulus -> TLTime -> Locked -> Unlocked -> Proof+proveWithoutSecret (PublicModulus pub) time (Locked locked) (Unlocked unlocked) =+  let l = hashToPrime (PublicModulus pub) time (Locked locked) (Unlocked unlocked)+      pow = (2 ^ unTLTime time) `div` l+  in Proof $ expFast locked pow pub++verifyTimeLock :: PublicModulus -> TLTime -> Locked -> Unlocked -> Proof -> Bool+verifyTimeLock (PublicModulus pub) time (Locked locked) (Unlocked unlocked) (Proof proof) =+  let l = hashToPrime (PublicModulus pub) time (Locked locked) (Unlocked unlocked)+      r = expFast 2 (toInteger $ unTLTime time) l+  in unlocked == (expFast proof l pub * expFast locked r pub) `mod` pub++unlockAndProveWithSecret :: RSAFactors -> TLTime -> Locked -> (Unlocked, Proof)+unlockAndProveWithSecret RSAFactors{..} time (Locked locked) =+  (Unlocked unlocked, Proof proof)+  where+    phi = (rsaP - 1) * (rsaQ - 1)+    pub = rsaP * rsaQ+    e = expFast 2 (toInteger $ unTLTime time) phi+    unlocked = expFast locked e pub+    l = hashToPrime (PublicModulus pub) time (Locked locked) (Unlocked unlocked)+    pow = ((2 ^ unTLTime time) `div` l) `mod` phi+    proof = expFast locked pow pub++unlockWithoutSecret :: PublicModulus -> TLTime -> Locked -> Unlocked+unlockWithoutSecret (PublicModulus pub) (TLTime time) (Locked locked) =+  Unlocked $ go time locked+  where+    go 0 v = v+    go t v = go (pred t) (v * v `mod` pub)++encrypt :: SymmetricKey -> ByteString -> IO Ciphertext+encrypt (SymmetricKey key) plaintext = do+  nonce <- Nonce.generate+  let payload = Box.encrypt key nonce plaintext+  pure $ Ciphertext (Nonce nonce) payload++decrypt :: SymmetricKey -> Ciphertext -> Maybe ByteString+decrypt (SymmetricKey key) Ciphertext{ctNonce = Nonce nonce, ..}+  = Box.decrypt key nonce ctPayload++-- | Create a timelock puzzle and a key.+createChestAndChestKey+  :: ByteString -- ^ Chest content+  -> TLTime -- ^ Time (in elementary actions) to open without key.+  -> IO (Chest, ChestKey)+createChestAndChestKey payload time = do+  (pub, secret) <- genRSAFactors+  locked <- genLockedValue pub+  let (unlocked, proof) = unlockAndProveWithSecret secret time locked+      key = unlockedValueToSymmetricKey unlocked+  ciphertext <- encrypt key payload+  pure $ (Chest locked pub ciphertext, ChestKey unlocked proof)++-- | Forge a chest key the hard way.+createChestKey :: Chest -> TLTime -> ChestKey+createChestKey Chest{..} time =+  let unlocked = unlockWithoutSecret chestPublicModulus time chestLockedVal+      proof = proveWithoutSecret chestPublicModulus time chestLockedVal unlocked+  in ChestKey unlocked proof++-- | The result of opening the chest.+data OpeningResult+  = Correct ByteString -- ^ The chest was opened correctly.+  | BogusCipher -- ^ The chest was opened correctly, but the contents do not decode with+  -- the given symmetric key.+  | BogusOpening -- ^ The chest was not opened correctly, i.e. proof verification failed.+  deriving stock (Show, Eq)++-- | Try to (quickly) open a chest with the given key, verifying the proof.+openChest :: Chest -> ChestKey -> TLTime -> OpeningResult+openChest Chest{..} ChestKey{..} time+  | verifyTimeLock chestPublicModulus time chestLockedVal ckUnlockedVal ckProof+  = maybe BogusCipher Correct $+      decrypt (unlockedValueToSymmetricKey ckUnlockedVal) chestCiphertext+  | otherwise = BogusOpening++-- | Convert a 'ChestKey' to binary representation, used by Tezos+chestKeyBytes :: ChestKey -> ByteString+chestKeyBytes = LBS.toStrict . Bi.encode++-- | Convert a 'Chest' to binary representation, used by Tezos+chestBytes :: Chest -> ByteString+chestBytes = LBS.toStrict . Bi.encode++-- | Read a 'Chest' from binary representation, used by Tezos+chestFromBytes :: ByteString -> Either Text Chest+chestFromBytes bs = case Bi.decodeOrFail $ LBS.fromStrict bs of+  Right (trail, _, res)+    | null trail -> Right res+    | otherwise -> Left "trailing unconsumed bytes"+  Left (_, _, err) -> Left (fromString err)++-- | Read a 'ChestKey' from binary representation, used by Tezos+chestKeyFromBytes :: ByteString -> Either Text ChestKey+chestKeyFromBytes bs = case Bi.decodeOrFail $ LBS.fromStrict bs of+  Right (trail, _, res)+    | null trail -> Right res+    | otherwise -> Left "trailing unconsumed bytes"+  Left (_, _, err) -> Left (fromString err)++-- | Construct a chest purely based on a seed for pseudorandom generator.+-- This is not suitable for cryptography, used in tests.+createChestAndChestKeyFromSeed+  :: Int -- ^ Pseudo-random seed+  -> ByteString -- ^ Chest content+  -> TLTime -- ^ TLTime (in elementary actions) to open without key.+  -> (Chest, ChestKey)+createChestAndChestKeyFromSeed seed payload time = flip evalRand (mkStdGen seed) do+  let rangeLow = 2 ^ (natVal @HalfModulus Proxy * 8)+      rangeHigh = rangeLow * 2 - 1+      range = (rangeLow, rangeHigh)+  p' <- getRandomR range+  q' <- getRandomR range+  let pub = PublicModulus pub'+      pub' = p * q+      p = findPrimeFrom p'+      q = findPrimeFrom q'+      secret = RSAFactors p q+      lockedMax = 2 ^ (natVal @SizeModulus Proxy + 16) * 8 - 1+  locked <- Locked . (`mod` pub') <$> getRandomR (0, lockedMax)+  let (unlocked, proof) = unlockAndProveWithSecret secret time locked+      SymmetricKey key = unlockedValueToSymmetricKey unlocked+  nonce <- fromMaybe (error "impossible") . sizedByteArray <$> liftRand (genByteString 24)+  let ciphertext = Ciphertext (Nonce nonce) $ Box.encrypt key nonce payload+  pure $ (Chest locked pub ciphertext, ChestKey unlocked proof)

@@ -7,6 +7,7 @@   , eqParamSing   , eqParamSing2   , eqParamSing3+  , eqParamMixed3   , castSing   , SingI1(..)   ) where@@ -60,6 +61,29 @@  -- | Version of 'eqParamSing' for types with 3 parameters. eqParamSing3 ::+  forall a1 a2 b1 b2 c1 c2 t.+  ( SingI a1+  , SingI a2+  , SingI b1+  , SingI b2+  , SingI c1+  , SingI c2+  , SDecide (KindOf a1)+  , SDecide (KindOf b1)+  , SDecide (KindOf c1)+  , Eq (t a1 b1 c1)+  )+  => t a1 b1 c1+  -> t a2 b2 c2+  -> Bool+eqParamSing3 t1 t2 = isJust @() $ do+  Refl <- sing @a1 `decideEquality` sing @a2+  Refl <- sing @b1 `decideEquality` sing @b2+  Refl <- sing @c1 `decideEquality` sing @c2+  guard (t1 == t2)++-- | Version of 'eqParamSing' for types with 3 parameters.+eqParamMixed3 ::   forall instr1 instr2 a1 a2 b1 b2 t.   ( Typeable instr1   , Typeable instr2@@ -74,7 +98,7 @@   => t instr1 a1 b1   -> t instr2 a2 b2   -> Bool-eqParamSing3 t1 t2 = isJust @() $ do+eqParamMixed3 t1 t2 = isJust @() $ do   Refl <- eqT @instr1 @instr2   Refl <- sing @a1 `decideEquality` sing @a2   Refl <- sing @b1 `decideEquality` sing @b2

@@ -3,7 +3,6 @@ -- SPDX-License-Identifier: LicenseRef-MIT-TQ  {-# OPTIONS_GHC -Wno-redundant-constraints #-}-{-# LANGUAGE QuantifiedConstraints #-}  -- | General type utilities. module Morley.Util.Type

@@ -2,8 +2,6 @@ -- -- SPDX-License-Identifier: LicenseRef-MIT-TQ -{-# LANGUAGE QuantifiedConstraints #-}- -- | Utility for 'Typeable'. module Morley.Util.Typeable   ( eqParam1