diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,5 +1,24 @@ +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 ====== diff --git a/app/Main.hs b/app/Main.hs --- a/app/Main.hs +++ b/app/Main.hs @@ -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 diff --git a/morley.cabal b/morley.cabal --- a/morley.cabal +++ b/morley.cabal @@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack name: morley -version: 1.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 diff --git a/src/Morley/CLI.hs b/src/Morley/CLI.hs --- a/src/Morley/CLI.hs +++ b/src/Morley/CLI.hs @@ -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) diff --git a/src/Morley/Micheline/Binary.hs b/src/Morley/Micheline/Binary.hs --- a/src/Morley/Micheline/Binary.hs +++ b/src/Morley/Micheline/Binary.hs @@ -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 diff --git a/src/Morley/Micheline/Binary/Internal.hs b/src/Morley/Micheline/Binary/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Morley/Micheline/Binary/Internal.hs @@ -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 diff --git a/src/Morley/Micheline/Class.hs b/src/Morley/Micheline/Class.hs --- a/src/Morley/Micheline/Class.hs +++ b/src/Morley/Micheline/Class.hs @@ -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 diff --git a/src/Morley/Micheline/Expression.hs b/src/Morley/Micheline/Expression.hs --- a/src/Morley/Micheline/Expression.hs +++ b/src/Morley/Micheline/Expression.hs @@ -77,6 +77,9 @@ -- -- > ./scripts/get-micheline-exprs.sh -- + -- or find the full primitives list in the , + -- 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 diff --git a/src/Morley/Michelson/Interpret.hs b/src/Morley/Michelson/Interpret.hs --- a/src/Morley/Michelson/Interpret.hs +++ b/src/Morley/Michelson/Interpret.hs @@ -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. diff --git a/src/Morley/Michelson/Macro.hs b/src/Morley/Michelson/Macro.hs --- a/src/Morley/Michelson/Macro.hs +++ b/src/Morley/Michelson/Macro.hs @@ -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 -> " " "" - VIEW code -> "" + VIEW_ code -> "" VOID code -> "" CMP parsedInstr carAnn -> "" 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) ++ diff --git a/src/Morley/Michelson/Optimizer.hs b/src/Morley/Michelson/Optimizer.hs --- a/src/Morley/Michelson/Optimizer.hs +++ b/src/Morley/Michelson/Optimizer.hs @@ -20,7 +20,7 @@ , defaultRulesAndPushPack , orRule , orSimpleRule - , Rule + , Rule (..) , OptimizerConf (..) , ocGotoValuesL ) where diff --git a/src/Morley/Michelson/Parser.hs b/src/Morley/Michelson/Parser.hs --- a/src/Morley/Michelson/Parser.hs +++ b/src/Morley/Michelson/Parser.hs @@ -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 ------------------ diff --git a/src/Morley/Michelson/Parser/Common.hs b/src/Morley/Michelson/Parser/Common.hs new file mode 100644 --- /dev/null +++ b/src/Morley/Michelson/Parser/Common.hs @@ -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 diff --git a/src/Morley/Michelson/Parser/Error.hs b/src/Morley/Michelson/Parser/Error.hs --- a/src/Morley/Michelson/Parser/Error.hs +++ b/src/Morley/Michelson/Parser/Error.hs @@ -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" diff --git a/src/Morley/Michelson/Parser/Instr.hs b/src/Morley/Michelson/Parser/Instr.hs --- a/src/Morley/Michelson/Parser/Instr.hs +++ b/src/Morley/Michelson/Parser/Instr.hs @@ -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 diff --git a/src/Morley/Michelson/Parser/Macro.hs b/src/Morley/Michelson/Parser/Macro.hs --- a/src/Morley/Michelson/Parser/Macro.hs +++ b/src/Morley/Michelson/Parser/Macro.hs @@ -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 diff --git a/src/Morley/Michelson/Parser/Type.hs b/src/Morley/Michelson/Parser/Type.hs --- a/src/Morley/Michelson/Parser/Type.hs +++ b/src/Morley/Michelson/Parser/Type.hs @@ -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 diff --git a/src/Morley/Michelson/Runtime.hs b/src/Morley/Michelson/Runtime.hs --- a/src/Morley/Michelson/Runtime.hs +++ b/src/Morley/Michelson/Runtime.hs @@ -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 diff --git a/src/Morley/Michelson/Runtime/Import.hs b/src/Morley/Michelson/Runtime/Import.hs --- a/src/Morley/Michelson/Runtime/Import.hs +++ b/src/Morley/Michelson/Runtime/Import.hs @@ -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 ---------------------------------------------------------------------------- diff --git a/src/Morley/Michelson/TypeCheck/Error.hs b/src/Morley/Michelson/TypeCheck/Error.hs --- a/src/Morley/Michelson/TypeCheck/Error.hs +++ b/src/Morley/Michelson/TypeCheck/Error.hs @@ -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) <> "." diff --git a/src/Morley/Michelson/TypeCheck/Helpers.hs b/src/Morley/Michelson/TypeCheck/Helpers.hs --- a/src/Morley/Michelson/TypeCheck/Helpers.hs +++ b/src/Morley/Michelson/TypeCheck/Helpers.hs @@ -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 diff --git a/src/Morley/Michelson/TypeCheck/Instr.hs b/src/Morley/Michelson/TypeCheck/Instr.hs --- a/src/Morley/Michelson/TypeCheck/Instr.hs +++ b/src/Morley/Michelson/TypeCheck/Instr.hs @@ -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 diff --git a/src/Morley/Michelson/TypeCheck/TypeCheckedOp.hs b/src/Morley/Michelson/TypeCheck/TypeCheckedOp.hs --- a/src/Morley/Michelson/TypeCheck/TypeCheckedOp.hs +++ b/src/Morley/Michelson/TypeCheck/TypeCheckedOp.hs @@ -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) diff --git a/src/Morley/Michelson/TypeCheck/TypeCheckedSeq.hs b/src/Morley/Michelson/TypeCheck/TypeCheckedSeq.hs --- a/src/Morley/Michelson/TypeCheck/TypeCheckedSeq.hs +++ b/src/Morley/Michelson/TypeCheck/TypeCheckedSeq.hs @@ -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. diff --git a/src/Morley/Michelson/TypeCheck/Types.hs b/src/Morley/Michelson/TypeCheck/Types.hs --- a/src/Morley/Michelson/TypeCheck/Types.hs +++ b/src/Morley/Michelson/TypeCheck/Types.hs @@ -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 diff --git a/src/Morley/Michelson/TypeCheck/Value.hs b/src/Morley/Michelson/TypeCheck/Value.hs --- a/src/Morley/Michelson/TypeCheck/Value.hs +++ b/src/Morley/Michelson/TypeCheck/Value.hs @@ -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 diff --git a/src/Morley/Michelson/Typed.hs b/src/Morley/Michelson/Typed.hs --- a/src/Morley/Michelson/Typed.hs +++ b/src/Morley/Michelson/Typed.hs @@ -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 diff --git a/src/Morley/Michelson/Typed/Aliases.hs b/src/Morley/Michelson/Typed/Aliases.hs --- a/src/Morley/Michelson/Typed/Aliases.hs +++ b/src/Morley/Michelson/Typed/Aliases.hs @@ -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 diff --git a/src/Morley/Michelson/Typed/Annotation.hs b/src/Morley/Michelson/Typed/Annotation.hs --- a/src/Morley/Michelson/Typed/Annotation.hs +++ b/src/Morley/Michelson/Typed/Annotation.hs @@ -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 diff --git a/src/Morley/Michelson/Typed/Contract.hs b/src/Morley/Michelson/Typed/Contract.hs new file mode 100644 --- /dev/null +++ b/src/Morley/Michelson/Typed/Contract.hs @@ -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 diff --git a/src/Morley/Michelson/Typed/Convert.hs b/src/Morley/Michelson/Typed/Convert.hs --- a/src/Morley/Michelson/Typed/Convert.hs +++ b/src/Morley/Michelson/Typed/Convert.hs @@ -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 diff --git a/src/Morley/Michelson/Typed/Doc.hs b/src/Morley/Michelson/Typed/Doc.hs --- a/src/Morley/Michelson/Typed/Doc.hs +++ b/src/Morley/Michelson/Typed/Doc.hs @@ -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 diff --git a/src/Morley/Michelson/Typed/Existential.hs b/src/Morley/Michelson/Typed/Existential.hs --- a/src/Morley/Michelson/Typed/Existential.hs +++ b/src/Morley/Michelson/Typed/Existential.hs @@ -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) diff --git a/src/Morley/Michelson/Typed/Extract.hs b/src/Morley/Michelson/Typed/Extract.hs --- a/src/Morley/Michelson/Typed/Extract.hs +++ b/src/Morley/Michelson/Typed/Extract.hs @@ -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) diff --git a/src/Morley/Michelson/Typed/Haskell/Doc.hs b/src/Morley/Michelson/Typed/Haskell/Doc.hs --- a/src/Morley/Michelson/Typed/Haskell/Doc.hs +++ b/src/Morley/Michelson/Typed/Haskell/Doc.hs @@ -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" diff --git a/src/Morley/Michelson/Typed/Haskell/Value.hs b/src/Morley/Michelson/Typed/Haskell/Value.hs --- a/src/Morley/Michelson/Typed/Haskell/Value.hs +++ b/src/Morley/Michelson/Typed/Haskell/Value.hs @@ -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 diff --git a/src/Morley/Michelson/Typed/Instr.hs b/src/Morley/Michelson/Typed/Instr.hs --- a/src/Morley/Michelson/Typed/Instr.hs +++ b/src/Morley/Michelson/Typed/Instr.hs @@ -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) diff --git a/src/Morley/Michelson/Typed/OpSize.hs b/src/Morley/Michelson/Typed/OpSize.hs --- a/src/Morley/Michelson/Typed/OpSize.hs +++ b/src/Morley/Michelson/Typed/OpSize.hs @@ -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 diff --git a/src/Morley/Michelson/Typed/Operation.hs b/src/Morley/Michelson/Typed/Operation.hs --- a/src/Morley/Michelson/Typed/Operation.hs +++ b/src/Morley/Michelson/Typed/Operation.hs @@ -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(..)) diff --git a/src/Morley/Michelson/Typed/Polymorphic.hs b/src/Morley/Michelson/Typed/Polymorphic.hs --- a/src/Morley/Michelson/Typed/Polymorphic.hs +++ b/src/Morley/Michelson/Typed/Polymorphic.hs @@ -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 diff --git a/src/Morley/Michelson/Typed/Scope.hs b/src/Morley/Michelson/Typed/Scope.hs --- a/src/Morley/Michelson/Typed/Scope.hs +++ b/src/Morley/Michelson/Typed/Scope.hs @@ -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 $ diff --git a/src/Morley/Michelson/Typed/T.hs b/src/Morley/Michelson/Typed/T.hs --- a/src/Morley/Michelson/Typed/T.hs +++ b/src/Morley/Michelson/Typed/T.hs @@ -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) diff --git a/src/Morley/Michelson/Typed/Util.hs b/src/Morley/Michelson/Typed/Util.hs --- a/src/Morley/Michelson/Typed/Util.hs +++ b/src/Morley/Michelson/Typed/Util.hs @@ -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 diff --git a/src/Morley/Michelson/Typed/Value.hs b/src/Morley/Michelson/Typed/Value.hs --- a/src/Morley/Michelson/Typed/Value.hs +++ b/src/Morley/Michelson/Typed/Value.hs @@ -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 "" 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 diff --git a/src/Morley/Michelson/Typed/View.hs b/src/Morley/Michelson/Typed/View.hs new file mode 100644 --- /dev/null +++ b/src/Morley/Michelson/Typed/View.hs @@ -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 diff --git a/src/Morley/Michelson/Untyped.hs b/src/Morley/Michelson/Untyped.hs --- a/src/Morley/Michelson/Untyped.hs +++ b/src/Morley/Michelson/Untyped.hs @@ -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 diff --git a/src/Morley/Michelson/Untyped/Aliases.hs b/src/Morley/Michelson/Untyped/Aliases.hs --- a/src/Morley/Michelson/Untyped/Aliases.hs +++ b/src/Morley/Michelson/Untyped/Aliases.hs @@ -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 diff --git a/src/Morley/Michelson/Untyped/Contract.hs b/src/Morley/Michelson/Untyped/Contract.hs --- a/src/Morley/Michelson/Untyped/Contract.hs +++ b/src/Morley/Michelson/Untyped/Contract.hs @@ -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' diff --git a/src/Morley/Michelson/Untyped/Instr.hs b/src/Morley/Michelson/Untyped/Instr.hs --- a/src/Morley/Michelson/Untyped/Instr.hs +++ b/src/Morley/Michelson/Untyped/Instr.hs @@ -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 diff --git a/src/Morley/Michelson/Untyped/OpSize.hs b/src/Morley/Michelson/Untyped/OpSize.hs --- a/src/Morley/Michelson/Untyped/OpSize.hs +++ b/src/Morley/Michelson/Untyped/OpSize.hs @@ -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 diff --git a/src/Morley/Michelson/Untyped/Type.hs b/src/Morley/Michelson/Untyped/Type.hs --- a/src/Morley/Michelson/Untyped/Type.hs +++ b/src/Morley/Michelson/Untyped/Type.hs @@ -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) diff --git a/src/Morley/Michelson/Untyped/View.hs b/src/Morley/Michelson/Untyped/View.hs new file mode 100644 --- /dev/null +++ b/src/Morley/Michelson/Untyped/View.hs @@ -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' diff --git a/src/Morley/Tezos/Crypto.hs b/src/Morley/Tezos/Crypto.hs --- a/src/Morley/Tezos/Crypto.hs +++ b/src/Morley/Tezos/Crypto.hs @@ -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 diff --git a/src/Morley/Tezos/Crypto/BLS12381.hs b/src/Morley/Tezos/Crypto/BLS12381.hs --- a/src/Morley/Tezos/Crypto/BLS12381.hs +++ b/src/Morley/Tezos/Crypto/BLS12381.hs @@ -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 diff --git a/src/Morley/Tezos/Crypto/Timelock.hs b/src/Morley/Tezos/Crypto/Timelock.hs new file mode 100644 --- /dev/null +++ b/src/Morley/Tezos/Crypto/Timelock.hs @@ -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) diff --git a/src/Morley/Util/Sing.hs b/src/Morley/Util/Sing.hs --- a/src/Morley/Util/Sing.hs +++ b/src/Morley/Util/Sing.hs @@ -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 diff --git a/src/Morley/Util/Type.hs b/src/Morley/Util/Type.hs --- a/src/Morley/Util/Type.hs +++ b/src/Morley/Util/Type.hs @@ -3,7 +3,6 @@ -- SPDX-License-Identifier: LicenseRef-MIT-TQ {-# OPTIONS_GHC -Wno-redundant-constraints #-} -{-# LANGUAGE QuantifiedConstraints #-} -- | General type utilities. module Morley.Util.Type diff --git a/src/Morley/Util/Typeable.hs b/src/Morley/Util/Typeable.hs --- a/src/Morley/Util/Typeable.hs +++ b/src/Morley/Util/Typeable.hs @@ -2,8 +2,6 @@ -- -- SPDX-License-Identifier: LicenseRef-MIT-TQ -{-# LANGUAGE QuantifiedConstraints #-} - -- | Utility for 'Typeable'. module Morley.Util.Typeable ( eqParam1