morley 1.17.0 → 1.18.0

raw patch · 49 files changed

+2003/−1162 lines, 49 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGES.md +50/−0
• app/Main.hs +16/−10
• morley.cabal +6/−1
• src/Morley/AsRPC.hs +2/−27
• src/Morley/CLI.hs +13/−11
• src/Morley/Micheline/Class.hs +8/−5
• src/Morley/Micheline/Expression.hs +1/−1
• src/Morley/Michelson/Interpret.hs +49/−40
• src/Morley/Michelson/Interpret/Unpack.hs +1/−1
• src/Morley/Michelson/Parser/Instr.hs +4/−0
• src/Morley/Michelson/Printer/Util.hs +16/−13
• src/Morley/Michelson/Runtime.hs +290/−219
• src/Morley/Michelson/Runtime/Dummy.hs +8/−4
• src/Morley/Michelson/Runtime/GState.hs +120/−111
• src/Morley/Michelson/Runtime/TxData.hs +2/−2
• src/Morley/Michelson/TypeCheck.hs +1/−0
• src/Morley/Michelson/TypeCheck/Error.hs +20/−2
• src/Morley/Michelson/TypeCheck/Helpers.hs +2/−2
• src/Morley/Michelson/TypeCheck/Instr.hs +51/−22
• src/Morley/Michelson/TypeCheck/TypeCheck.hs +64/−66
• src/Morley/Michelson/TypeCheck/Types.hs +0/−4
• src/Morley/Michelson/TypeCheck/Value.hs +213/−198
• src/Morley/Michelson/Typed/Convert.hs +12/−10
• src/Morley/Michelson/Typed/Entrypoints.hs +10/−5
• src/Morley/Michelson/Typed/Existential.hs +4/−0
• src/Morley/Michelson/Typed/Haskell/Doc.hs +6/−0
• src/Morley/Michelson/Typed/Haskell/Instr/Product.hs +0/−1
• src/Morley/Michelson/Typed/Haskell/ValidateDescription.hs +10/−11
• src/Morley/Michelson/Typed/Haskell/Value.hs +7/−10
• src/Morley/Michelson/Typed/Instr.hs +14/−7
• src/Morley/Michelson/Typed/Operation.hs +20/−12
• src/Morley/Michelson/Typed/Scope.hs +97/−45
• src/Morley/Michelson/Typed/Sing.hs +1/−10
• src/Morley/Michelson/Typed/Util.hs +7/−0
• src/Morley/Michelson/Typed/Value.hs +28/−5
• src/Morley/Michelson/Untyped/Instr.hs +36/−43
• src/Morley/Michelson/Untyped/Value.hs +17/−9
• src/Morley/Tezos/Address.hs +239/−79
• src/Morley/Tezos/Address/Alias.hs +92/−17
• src/Morley/Tezos/Address/Kinds.hs +33/−0
• src/Morley/Tezos/Crypto.hs +40/−34
• src/Morley/Util/Bimap.hs +63/−0
• src/Morley/Util/Binary.hs +38/−11
• src/Morley/Util/Interpolate/Internal.hs +1/−0
• src/Morley/Util/MultiReader.hs +98/−0
• src/Morley/Util/Peano.hs +17/−19
• src/Morley/Util/Sing.hs +12/−4
• src/Morley/Util/Type.hs +162/−17
• src/Morley/Util/TypeLits.hs +2/−74

@@ -1,6 +1,56 @@ <!-- Unreleased: append new entries here -->  +1.18.0+======+* [!1212](https://gitlab.com/morley-framework/morley/-/merge_requests/1212)+  Implement `EMIT` and other Kathmandu changes+  + Update michelson primitives for the new protocol+  + Add support for parsing/typechecking/serializing `EMIT` instruction+  + Support `EMIT` on the emulator+* [!1202](https://gitlab.com/morley-framework/morley/-/merge_requests/1202)+  Make error messages less confusing when types are ambiguous.+  + Use `FailUnless` and similar rather than `If` to reduce the prevalence+    of confusing type errors.+  + Remove `TypeErrorUnless` in favor of `FailUnless`.+* [!1207](https://gitlab.com/morley-framework/morley/-/merge_requests/1207)+  Rename our custom `SingI1` to `SingIOne` to avoid confusion with+  `singletons`, remove its method, and reduce it to just one polymorphic+  instance.+* [!1203](https://gitlab.com/morley-framework/morley/-/merge_requests/1203)+  Remove `Morley.Util.Type.reifyTypeEquality`+* [!1185](https://gitlab.com/morley-framework/morley/-/merge_requests/1185)+  Refactor typechecker monad+* [!1192](https://gitlab.com/morley-framework/morley/-/merge_requests/1192)+  Refactor aliases storage in Cleveland+  + Added `Morley.Util.Bimap.Bimap`+  + Changed the type of `GState.gsImplicitAddressAliases` to `Bimap ImplicitAlias Address`+  + Changed the type of `GState.gsContractAddressAliases` to `Bimap ContractAlias Address`+  * Deleted `GSAddImplicitAddressAlias`+* [!1177](https://gitlab.com/morley-framework/morley/-/merge_requests/1177)+  Distinguish implicit/contract aliases and addresses on the type level+* [!1190](https://gitlab.com/morley-framework/morley/-/merge_requests/1190)+  Remove some `SingI` constraints from some `WithDeMorganScope` instances.+* [!1186](https://gitlab.com/morley-framework/morley/-/merge_requests/1186)+  Make `ITER{FAILWITH;}` typecheck+* [!1176](https://gitlab.com/morley-framework/morley/-/merge_requests/1176)+  Render Michelson values on multiple lines+* [!1168](https://gitlab.com/morley-framework/morley/-/merge_requests/1168)+  Support a mix of RPC and non-RPC representations in `runCode`+  + Deleted `WellTypedIsoValue`+  + Added `IsoValue` constraint to `WellTypedToT`, `HasNoOpToT`, `HasNoBigMapToT`, `KnownIsoT`.+  + Added `typeCheckValueRunCodeCompat` to simulate the typechecking behavior of the+    tezos RPC's `run_code` endpoint.+  + Changed the return type of `typeCheckValue` from `TypeCheckInstr` to `TypeCheckResult`.+  + Delete `runTypeCheckInstrIsolated`+  + Restrict the type of `runTypeCheckIsolated`+  + Delete `MaybeRPC`+* [!1137](https://gitlab.com/morley-framework/morley/-/merge_requests/1137)+  Support a delimiting but otherwise empty escape `\&` in+  `Morley.Util.Interpolate`+* [!1175](https://gitlab.com/morley-framework/morley/-/merge_requests/1175)+  Use tagged decoder for Address+ 1.17.0 ====== * [!1173](https://gitlab.com/morley-framework/morley/-/merge_requests/1173)

@@ -28,8 +28,9 @@ import Morley.Michelson.TypeCheck.Types (mapSomeContract) import Morley.Michelson.Typed (Contract'(..), SomeContract(..), unContractCode) import Morley.Michelson.Untyped qualified as U-import Morley.Tezos.Address (Address)-import Morley.Tezos.Address.Alias (AddressOrAlias, Alias)+import Morley.Tezos.Address+import Morley.Tezos.Address.Alias+import Morley.Tezos.Address.Kinds import Morley.Tezos.Core (Mutez, Timestamp(..), tz) import Morley.Tezos.Crypto import Morley.Tezos.Crypto.Timelock (chestBytes, chestKeyBytes, createChestAndChestKey)@@ -92,8 +93,8 @@   { ooContractFile :: Maybe FilePath   , ooDBPath :: FilePath   , ooTcOptions :: TypeCheck.TypeCheckOptions-  , ooOriginator :: Address-  , ooAlias :: Maybe Alias+  , ooOriginator :: ImplicitAddress+  , ooAlias :: Maybe ContractAlias   , ooDelegate :: Maybe KeyHash   , ooStorageValue :: U.Value   , ooBalance :: Mutez@@ -103,7 +104,7 @@ data TransferOptions = TransferOptions   { toDBPath :: FilePath   , toTcOptions :: TypeCheck.TypeCheckOptions-  , toDestination :: AddressOrAlias+  , toDestination :: SomeAddressOrAlias   , toTxData :: TxData   , toNow :: Maybe Timestamp   , toLevel :: Maybe Natural@@ -265,10 +266,15 @@     transferOptions = do       toDBPath <- dbPathOption       toTcOptions <- typeCheckOptionsOption-      toDestination <- addressOrAliasOption-        Nothing-        (#name :! "to")-        (#help :! "Address or alias of the transfer's destination")+      toDestination <-+        SomeAddressOrAlias <$> addressOrAliasOption @'AddressKindImplicit+          Nothing+          (#name :! "to-implicit")+          (#help :! "Address or alias of the transfer's destination implicit address (tz1/tz2/tz3)")+        <|> SomeAddressOrAlias <$> addressOrAliasOption @'AddressKindContract+          Nothing+          (#name :! "to-contract")+          (#help :! "Address or alias of the transfer's destination contract (KT1)")       toTxData <- txDataOption       toNow <- nowOption       toLevel <- levelOption@@ -353,7 +359,7 @@             michelsonContract             ! #verbose ooVerbose         putTextLn $ "Originated contract " <> pretty addr-      Transfer TransferOptions {..} -> do+      Transfer TransferOptions {toDestination=SomeAddressOrAlias toDestination, ..} -> do         transfer toNow toLevel toMinBlockTime toMaxSteps toDBPath toTcOptions toDestination toTxData           ! #verbose toVerbose           ! #dryRun toDryRun

@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           morley-version:        1.17.0+version:        1.18.0 synopsis:       Developer tools for the Michelson Language description:    A library to make writing smart contracts in Michelson — the smart contract language of the Tezos blockchain — pleasant and effective. category:       Language@@ -124,6 +124,7 @@       Morley.Michelson.Untyped.View       Morley.Tezos.Address       Morley.Tezos.Address.Alias+      Morley.Tezos.Address.Kinds       Morley.Tezos.Core       Morley.Tezos.Crypto       Morley.Tezos.Crypto.BLS12381@@ -134,6 +135,7 @@       Morley.Tezos.Crypto.Timelock       Morley.Tezos.Crypto.Util       Morley.Util.Aeson+      Morley.Util.Bimap       Morley.Util.Binary       Morley.Util.ByteString       Morley.Util.CLI@@ -150,6 +152,7 @@       Morley.Util.Main       Morley.Util.Markdown       Morley.Util.MismatchError+      Morley.Util.MultiReader       Morley.Util.Named       Morley.Util.Peano       Morley.Util.PeanoNatural@@ -191,6 +194,7 @@       GADTs       GeneralizedNewtypeDeriving       ImportQualifiedPost+      InstanceSigs       LambdaCase       MultiParamTypeClasses       MultiWayIf@@ -304,6 +308,7 @@       GADTs       GeneralizedNewtypeDeriving       ImportQualifiedPost+      InstanceSigs       LambdaCase       MultiParamTypeClasses       MultiWayIf

@@ -6,7 +6,6 @@ module Morley.AsRPC   ( TAsRPC   , HasRPCRepr(..)-  , MaybeRPC(..)   , deriveRPC   , deriveRPCWithStrategy   , deriveManyRPC@@ -43,13 +42,12 @@ import Language.Haskell.TH.ReifyMany (reifyManyTyCons) import Language.Haskell.TH.ReifyMany.Internal (decConcreteNames) -import Morley.Micheline (ToExpression(..)) import Morley.Michelson.Text (MText) import Morley.Michelson.Typed   (BigMap, BigMapId, ContractPresence(ContractAbsent), ContractRef, EpAddress, HasNoBigMap,   HasNoContract, HasNoNestedBigMaps, HasNoOp, IsoValue, Notes(..), OpPresence(..), Operation,   SingI(sing), SingT(..), StorageScope, T(..), ToT, Value, Value'(..), WellTyped,-  checkContractTypePresence, checkOpPresence, toVal, withDict)+  checkContractTypePresence, checkOpPresence, withDict) import Morley.Tezos.Address (Address, TxRollupL2Address) import Morley.Tezos.Core (ChainId, Mutez, Timestamp) import Morley.Tezos.Crypto@@ -62,8 +60,7 @@ {-# ANN module ("HLint: ignore Avoid lambda using `infix`" :: Text) #-}  -- $setup--- >>> import Morley.Michelson.Typed (T(..), BigMap, mkBigMap)--- >>> import Morley.Michelson.Typed.Haskell.Value (BigMapId(..))+-- >>> import Morley.Michelson.Typed -- >>> import Morley.Michelson.Text (MText)  ----------------------------------------------------------------------------@@ -268,28 +265,6 @@   type AsRPC ChestKey = ChestKey instance HasRPCRepr TxRollupL2Address where   type AsRPC TxRollupL2Address = TxRollupL2Address--------------------------------------------------------------------------------- MaybeRPC--------------------------------------------------------------------------------- | Represents a value that may or may not be in its RPC representation.------ >>> :t NotRPC @(BigMap Integer MText) (mkBigMap @[(Integer, MText)] [])--- ...---   :: MaybeRPC (BigMap Integer MText)------ >>> :t IsRPC @(BigMap Integer MText) (BigMapId 1)--- ...---   :: MaybeRPC (BigMap Integer MText)-data MaybeRPC v where-  NotRPC :: IsoValue  v => v -> MaybeRPC v-  IsRPC :: (SingI (ToT v), IsoValue (AsRPC v), HasRPCRepr v) => AsRPC v -> MaybeRPC v--instance HasNoOp (ToT v) => ToExpression (MaybeRPC v) where-  toExpression = \case-    NotRPC v -> toExpression (toVal v)-    IsRPC v -> withDict (rpcHasNoOpEvi @(ToT v)) $ toExpression (toVal v)  ---------------------------------------------------------------------------- -- Derive RPC repr

@@ -30,6 +30,7 @@   , timeOption   ) where +import Data.Singletons (SingI) import Options.Applicative   (footerDoc, fullDesc, header, help, helper, info, long, metavar, option, progDesc, strOption,   switch)@@ -44,8 +45,8 @@ import Morley.Michelson.Text (MText) import Morley.Michelson.Untyped (EpName) import Morley.Michelson.Untyped qualified as U-import Morley.Tezos.Address (Address)-import Morley.Tezos.Address.Alias (AddressOrAlias(..), Alias(..))+import Morley.Tezos.Address+import Morley.Tezos.Address.Alias import Morley.Tezos.Core (Mutez, Timestamp, parseTimestamp, timestampFromSeconds) import Morley.Tezos.Crypto import Morley.Util.CLI@@ -141,18 +142,19 @@   help "Path to DB with data which is used instead of real blockchain data" <>   Opt.showDefault -aliasOption :: String -> Opt.Parser Alias-aliasOption key = fmap Alias . Opt.strOption $+aliasOption :: (SingI kind, L1AddressKind kind) => String -> Opt.Parser (Alias kind)+aliasOption key = fmap mkAlias . Opt.strOption $   long key <>   metavar "ALIAS" <>   help "An alias to be associated with the originated contract's address, e.g: 'alice', 'bob'"  -- | Generic parser to read an option of 'AddressOrAlias' type. addressOrAliasOption-  :: Maybe AddressOrAlias+  :: (SingI kind, L1AddressKind kind)+  => Maybe (AddressOrAlias kind)   -> "name" :! String   -> "help" :! String-  -> Opt.Parser AddressOrAlias+  -> Opt.Parser (AddressOrAlias kind) addressOrAliasOption = mkCLOptionParser  -- | Parser for transaction parameters.@@ -167,10 +169,10 @@       (#name :! "amount") (#help :! "Amount sent by a transaction")     <*> entrypointOption (#name :! "entrypoint") (#help :! "Entrypoint to call")   where-    mkTxData :: Address -> U.Value -> Mutez -> EpName -> TxData+    mkTxData :: ImplicitAddress -> U.Value -> Mutez -> EpName -> TxData     mkTxData addr param amount epName =       TxData-        { tdSenderAddress = addr+        { tdSenderAddress = MkConstrainedAddress addr         , tdParameter = TxUntypedParam param         , tdEntrypoint = epName         , tdAmount = amount@@ -196,9 +198,9 @@   Maybe Mutez -> "name" :! String -> "help" :! String -> Opt.Parser Mutez mutezOption = mkCLOptionParser --- | Generic parser to read an option of 'Address' type.-addressOption ::-  Maybe Address -> "name" :! String -> "help" :! String -> Opt.Parser Address+-- | Generic parser to read an option of 'KindedAddress' type.+addressOption :: SingI kind =>+  Maybe (KindedAddress kind) -> "name" :! String -> "help" :! String -> Opt.Parser (KindedAddress kind) addressOption = mkCLOptionParser  -- | @--oneline@ flag.

@@ -14,14 +14,12 @@  import Control.Lens ((<>~)) import Data.Bits (Bits)-import Data.Default (def) import Data.Singletons (SingI(..), demote) import Fmt (Buildable(..), indentF, pretty, unlinesF)  import Morley.Micheline.Expression import Morley.Michelson.Text (mkMText, unMText)-import Morley.Michelson.TypeCheck-  (TypeCheckMode(..), TypeCheckOptions(..), runTypeCheck, typeCheckingWith)+import Morley.Michelson.TypeCheck (TypeCheckOptions(..), typeCheckingWith) import Morley.Michelson.TypeCheck.Instr (typeCheckValue) import Morley.Michelson.Typed   (Contract, HasNoOp, Instr, Notes(..), T(..), Value, Value'(..), fromUType, mkUType, rfAnyInstr,@@ -296,6 +294,7 @@     SAPLING_EMPTY_STATE va n -> expressionPrim' "SAPLING_EMPTY_STATE" [integralToExpr n] $ mkAnns [] [] [va]     SAPLING_VERIFY_UPDATE va -> expressionPrim' "SAPLING_VERIFY_UPDATE" [] $ mkAnns [] [] [va]     MIN_BLOCK_TIME va -> expressionPrim' "MIN_BLOCK_TIME" [] $ mkAnnsFromAny va+    EMIT va tag ty -> expressionPrim' "EMIT" (toExpression <$> maybeToList ty) $ mkAnns [] [tag] [va]  instance ToExpression Untyped.Contract where   toExpression contract@@ -366,8 +365,6 @@     Left e -> Left e     where       typeCheck uv = typeCheckingWith (TypeCheckOptions False False) $-        (runTypeCheck $ TypeCheckValue (uv, demote @t)) $-        usingReaderT def $         typeCheckValue uv  instance FromExp x op => FromExp x (Untyped.Value' op) where@@ -718,6 +715,12 @@     ExpPrim' _ "SAPLING_VERIFY_UPDATE" [] anns ->       mkInstrWithVarAnn SAPLING_VERIFY_UPDATE anns     ExpPrim' _ "MIN_BLOCK_TIME" [] anns -> pure $ mkInstrWithAnyAnns MIN_BLOCK_TIME anns+    ExpPrim' _ "EMIT" mty _ -> do+      checkAnnsCount e annSet (0, 1, 1)+      let tag = firstAnn @FieldTag annSet+          va = firstAnn @VarTag annSet+      ty' <- maybe (pure Nothing) (fmap Just . fromExp @x @Ty) $ listToMaybe mty+      pure $ EMIT va tag ty'     _ -> Left $ FromExpError e "Expected an instruction"      where

@@ -132,7 +132,7 @@   "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_deprecated", "SAPLING_EMPTY_STATE", "SAPLING_VERIFY_UPDATE", "ticket",   "TICKET", "READ_TICKET", "SPLIT_TICKET", "JOIN_TICKETS", "GET_AND_UPDATE", "chest", "chest_key", "OPEN_CHEST",-  "VIEW", "view", "constant", "SUB_MUTEZ", "tx_rollup_l2_address", "MIN_BLOCK_TIME", "sapling_transaction"+  "VIEW", "view", "constant", "SUB_MUTEZ", "tx_rollup_l2_address", "MIN_BLOCK_TIME", "sapling_transaction", "EMIT"   ]  -- | Type for Micheline Expression with extension points.

@@ -65,8 +65,9 @@ import Morley.Michelson.Typed qualified as T import Morley.Michelson.Typed.Operation   (OperationHash(..), OriginationOperation(..), mkContractAddress, mkOriginationOperationHash)-import Morley.Tezos.Address (Address(..), GlobalCounter(..))-import Morley.Tezos.Address.Alias (Alias)+import Morley.Michelson.Untyped (unAnnotation)+import Morley.Tezos.Address+import Morley.Tezos.Address.Alias import Morley.Tezos.Core (ChainId, Mutez, Timestamp, zeroMutez) import Morley.Tezos.Crypto   (KeyHash, OpeningResult(..), blake2b, checkSignature, hashKey, keccak, mkTLTime, openChest,@@ -138,14 +139,16 @@   -- ^ Number of steps after which execution unconditionally terminates.   , ceBalance :: Mutez   -- ^ Current amount of mutez of the current contract.-  , ceContracts :: Map Address AddressState+  , ceContracts :: Map ContractAddress ContractState   -- ^ Information stored about the existing contracts.-  , ceSelf :: Address+  , ceSelf :: ContractAddress   -- ^ Address of the interpreted contract.-  , ceSource :: Address-  -- ^ The contract that initiated the current transaction.-  , ceSender :: Address-  -- ^ The contract that initiated the current internal transaction.+  , ceSource :: L1Address+  -- ^ The contract that initiated the current transaction. Note that this+  -- contract should in normal operation be an implicit account.+  , ceSender :: L1Address+  -- ^ The contract that initiated the current internal transaction. This may+  -- either be an implicit account or a smart contract.   , ceAmount :: Mutez   -- ^ Amount of the current transaction.   , ceVotingPowers :: VotingPowers@@ -663,8 +666,8 @@                     (StkEl (arg :: Value arg) :& StkEl (VAddress epAddr) :& r) = do   ContractEnv{..} <- ask   res :: Value ('TOption ret) <- VOption <$> runMaybeT do-    let EpAddress addr _ = epAddr-    Just (ASContract viewedContractState) <- pure $ Map.lookup addr ceContracts+    EpAddress addr@ContractAddress{} _ <- pure epAddr+    Just viewedContractState <- pure $ Map.lookup addr ceContracts     ContractState       { csContract = viewedContract       , csStorage = viewedContractStorage@@ -681,10 +684,10 @@     return res   pure (StkEl res :& r)   where-    mkViewEnv :: Address -> ContractState -> ContractEnv -> ContractEnv+    mkViewEnv :: ContractAddress -> ContractState -> ContractEnv -> ContractEnv     mkViewEnv calledAddr viewedContractState ContractEnv{..} = ContractEnv       { ceBalance = csBalance viewedContractState-      , ceSender = ceSelf+      , ceSender = MkConstrainedAddress ceSelf       , ceSelf = calledAddr       , ceSource       , ceAmount = zeroMutez@@ -697,10 +700,10 @@   ContractEnv{..} <- ask   case Proxy @out of     (_ :: Proxy ('TContract cp ': s)) -> do-      pure $ StkEl (VContract ceSelf sepc) :& r+      pure $ StkEl (VContract (MkAddress ceSelf) sepc) :& r runInstrImpl _ (AnnCONTRACT (Anns2' _ (_ :: T.Notes a)) instrEpName) (StkEl (VAddress epAddr) :& r) = do   ContractEnv{..} <- ask-  let T.EpAddress addr addrEpName = epAddr+  T.EpAddress' (MkConstrainedAddress addr) addrEpName <- pure epAddr   let mepName =         case (instrEpName, addrEpName) of           (DefEpName, DefEpName) -> Just DefEpName@@ -711,27 +714,25 @@   let withNotes v = StkEl v :& r   withNotes <$> case mepName of     Nothing -> pure $ VOption Nothing-    Just epName ->-      case addr of-        KeyAddress{} -> pure $ castContract addr epName T.tyImplicitAccountParam-        ContractAddress{} -> pure $-          case Map.lookup addr ceContracts of-            Just (ASSimple _) -> error "Broken addresses map"-            Just (ASContract ContractState{..}) ->-              castContract addr epName (cParamNotes csContract)-            Nothing -> VOption Nothing-        TransactionRollupAddress{} ->-          -- TODO [#838]: support transaction rollups on the emulator-          throwMichelson $ MichelsonUnsupported "txr1 addresses with CONTRACT"+    Just epName -> case addr of+      ImplicitAddress{} -> pure $ castContract addr epName T.tyImplicitAccountParam+      ContractAddress{} -> pure $+        case Map.lookup addr ceContracts of+          Just ContractState{..} ->+            castContract addr epName (cParamNotes csContract)+          Nothing -> VOption Nothing+      TxRollupAddress{} ->+        -- TODO [#838]: support transaction rollups on the emulator+        throwMichelson $ MichelsonUnsupported "txr1 addresses with CONTRACT"   where   castContract-    :: forall p. T.ParameterScope p-    => Address -> EpName -> T.ParamNotes p -> T.Value ('TOption ('TContract a))+    :: forall p kind. (T.ParameterScope p)+    => KindedAddress kind -> EpName -> T.ParamNotes p -> T.Value ('TOption ('TContract a))   castContract addr epName param = VOption $ do     -- As we are within Maybe monad, pattern-match failure results in Nothing     MkEntrypointCallRes (_ :: Notes a') epc <- T.mkEntrypointCall epName param     Right Refl <- pure $ eqType @a @a'-    return $ VContract addr (T.SomeEpc epc)+    return $ VContract (MkAddress addr) (T.SomeEpc epc)  runInstrImpl _ AnnTRANSFER_TOKENS{}   (StkEl p :& StkEl (VMutez mutez) :& StkEl contract :& r) = do@@ -755,18 +756,21 @@           Just hash -> mkContractAddress hash globalCounter           Nothing ->             mkContractAddress-              (mkOriginationOperationHash (createOrigOp originator Nothing mbKeyHash m contract g globalCounter))+              (mkOriginationOperationHash $+                  createOrigOp originator Nothing mbKeyHash m contract g globalCounter+              )               -- If opHash is Nothing it means that interpreter is running in some kind of test               -- context, therefore we generate dummy contract address with its own origination               -- operation.               globalCounter   let resEpAddr = EpAddress resAddr DefEpName-  let resOp = CreateContract originator (unwrapMbKeyHash mbKeyHash) m g contract globalCounter+  let resOp = CreateContract+        (MkConstrainedAddress originator) (unwrapMbKeyHash mbKeyHash) m g contract globalCounter   pure $ StkEl (VOp (OpCreateContract resOp))       :& StkEl (VAddress resEpAddr)       :& r runInstrImpl _ AnnIMPLICIT_ACCOUNT{} (StkEl (VKeyHash k) :& r) =-  pure $ (StkEl (VContract (KeyAddress k) sepcPrimitive)) :& r+  pure $ (StkEl (VContract (MkAddress $ ImplicitAddress k) sepcPrimitive)) :& r runInstrImpl _ AnnNOW{} r = do   ContractEnv{..} <- ask   pure $ StkEl (VTimestamp ceNow) :& r@@ -801,13 +805,13 @@   let pairs' = [ (g1, g2) | VPair (VBls12381G1 g1, VBls12381G2 g2) <- pairs ]   pure $ StkEl (VBool $ checkPairing pairs') :& r runInstrImpl _ AnnSOURCE{} r = do-  ContractEnv{..} <- ask+  ContractEnv{ceSource=MkConstrainedAddress ceSource} <- ask   pure $ StkEl (VAddress $ EpAddress ceSource DefEpName) :& r runInstrImpl _ AnnSENDER{} r = do-  ContractEnv{..} <- ask+  ContractEnv{ceSender=MkConstrainedAddress ceSender} <- ask   pure $ StkEl (VAddress $ EpAddress ceSender DefEpName) :& r runInstrImpl _ AnnADDRESS{} (StkEl (VContract a sepc) :& r) =-  pure $ StkEl (VAddress $ EpAddress a (sepcName sepc)) :& r+  pure $ StkEl (VAddress $ EpAddress' a (sepcName sepc)) :& r runInstrImpl _ AnnCHAIN_ID{} r = do   ContractEnv{..} <- ask   pure $ StkEl (VChainId ceChainId) :& r@@ -819,11 +823,11 @@   pure $ StkEl (VAddress $ EpAddress ceSelf DefEpName) :& r runInstrImpl _ AnnTICKET{} (StkEl dat :& StkEl (VNat am) :& r) = do   ContractEnv{..} <- ask-  pure $ StkEl (VTicket ceSelf dat am) :& r+  pure $ StkEl (VTicket (MkAddress ceSelf) dat am) :& r runInstrImpl _ AnnREAD_TICKET{} (te@(StkEl (VTicket addr dat am)) :& r) = do   pure $     StkEl-      (VPair (VAddress (EpAddress addr DefEpName), (VPair (dat, VNat am))))+      (VPair (VAddress (EpAddress' addr DefEpName), (VPair (dat, VNat am))))     :& te :& r runInstrImpl _ AnnSPLIT_TICKET{}     (StkEl tv@(VTicket addr dat am) :&@@ -853,6 +857,11 @@ runInstrImpl _ AnnMIN_BLOCK_TIME{} r = do   ContractEnv{..} <- ask   pure $ StkEl (VNat ceMinBlockTime) :& r+runInstrImpl _ (AnnEMIT _ (unAnnotation -> emTag) mNotes) ((StkEl emValue) :& r) = do+  incrementCounter+  emCounter <- isGlobalCounter <$> getInterpreterState+  let emNotes = fromMaybe starNotes mNotes+  pure $ StkEl (VOp (OpEmit Emit{..})) :& r  -- | Evaluates an arithmetic operation and either fails or proceeds. runArithOp@@ -877,9 +886,9 @@   unpackValue' bs  createOrigOp-  :: (ParameterScope param, StorageScope store)-  => Address-  -> Maybe Alias+  :: (ParameterScope param, StorageScope store, L1AddressKind kind)+  => KindedAddress kind+  -> Maybe ContractAlias   -> Maybe (T.Value 'T.TKeyHash)   -> Mutez   -> Contract param store

@@ -80,4 +80,4 @@   when (tag /= 0x05) . Left . UnpackError $     "Unexpected tag: '" <> (show tag) <> "'. '0x05' tag expected."   expr <- eitherDecodeExpression bs'-  either (Left . UnpackError . pretty) Right $ fromExpression @t expr+  first (UnpackError . pretty) $ fromExpression @t expr

@@ -52,6 +52,7 @@   , ticketOp, readTicketOp, splitTicketOp, joinTicketsOp   , openChestOp   , saplingEmptyStateOp, saplingVerifyUpdateOp, minBlockTimeOp+  , emitOp   ]  -- | Parse a sequence of instructions.@@ -470,3 +471,6 @@  openChestOp :: Parser ParsedInstr openChestOp = word "OPEN_CHEST" OPEN_CHEST <*> noteDef++emitOp :: Parser ParsedInstr+emitOp = word "EMIT" (uncurry EMIT) <*> notesVF <*> optional type_

@@ -24,16 +24,20 @@   , needsParens   , doesntNeedParens   , addParens+  , addParensMultiline   , assertParensNotNeeded   ) where +import Prelude hiding (group)+ import Control.Exception (assert) import Data.Text.Lazy qualified as LT import Data.Text.Lazy.Builder (Builder) import Fmt (Buildable, pretty) import Text.PrettyPrint.Leijen.Text-  (Doc, SimpleDoc, align, braces, displayB, displayT, enclose, encloseSep, hcat, isEmpty, lbracket,-  parens, punctuate, rbracket, renderOneLine, renderPretty, semi, space, text, vcat, (<+>))+  (Doc, SimpleDoc, align, braces, displayB, displayT, enclose, encloseSep, hcat, hsep, isEmpty,+  lbracket, parens, punctuate, rbracket, renderOneLine, renderPretty, semi, sep, space, text, (<+>),+  (<//>))  -- | Environment carried during recursive rendering. newtype RenderContext = RenderContext@@ -91,22 +95,16 @@ renderOps :: (RenderDoc op) => Bool -> NonEmpty op -> Doc renderOps oneLine = renderOpsList oneLine . toList --- | Join a non-empty list of 'Doc' by spaces-spacecat :: NonEmpty Doc -> Doc-spacecat = foldr (<+>) mempty- -- | Render a comma-separated list of items in braces renderOpsList :: (RenderDoc op) => Bool -> [op] -> Doc renderOpsList oneLine ops =   braces $ enclose space space $ renderOpsListNoBraces oneLine ops --- | Render a comma-separated list of items without braces+-- | Render a semi-colon-separated list of items without braces renderOpsListNoBraces :: RenderDoc op => Bool -> [op] -> Doc-renderOpsListNoBraces oneLine ops =-  cat' $ punctuate semi $-    renderDoc doesntNeedParens <$> filter isRenderable ops-  where-    cat' = if oneLine then maybe "" spacecat . nonEmpty else align . vcat+renderOpsListNoBraces oneLine =+  align . (if oneLine then hsep else sep) . punctuate semi .+    fmap (renderDoc doesntNeedParens) . filter isRenderable  -- | Create a specific number of spaces. spaces :: Int -> Doc@@ -128,7 +126,6 @@ buildRenderDocExtended :: RenderDoc a => a -> Builder buildRenderDocExtended = printDocB False . renderDoc doesntNeedParens - -- | Here using a page width of 80 and a ribbon width of 1.0 -- https://hackage.haskell.org/package/wl-pprint-1.2.1/docs/Text-PrettyPrint-Leijen.html doRender :: Bool -> Doc -> SimpleDoc@@ -154,6 +151,12 @@ addParens = \case   RenderContext True -> parens   RenderContext False -> id++-- | Add parentheses if needed, multiline if necessary.+addParensMultiline :: RenderContext -> Doc -> Doc+addParensMultiline pn doc = case pn of+  RenderContext True -> "(" <> doc <//> ")"+  RenderContext False -> doc  -- | Ensure parentheses are not required, for case when you cannot -- sensibly wrap your expression into them.

@@ -18,7 +18,6 @@    -- * Re-exports   , ContractState (..)-  , AddressState (..)   , VotingPowers   , mkVotingPowers   , mkVotingPowersFromMap@@ -55,11 +54,14 @@  import Control.Lens (assign, at, makeLenses, (.=), (<>=)) import Control.Monad.Except (Except, liftEither, runExcept, throwError)+import Data.Constraint (Dict(..), (\\)) import Data.Default (def) import Data.HashSet qualified as HS import Data.Semigroup.Generic (GenericSemigroupMonoid(..))+import Data.Singletons (demote) import Data.Text.IO (getContents) import Data.Text.IO.Utf8 qualified as Utf8 (readFile)+import Data.Type.Equality (pattern Refl) import Fmt (Buildable(build), blockListF, fmt, fmtLn, indentF, nameF, pretty, (+|), (|+)) import Text.Megaparsec (parse) @@ -79,8 +81,9 @@ import Morley.Michelson.Typed.Operation import Morley.Michelson.Untyped (Contract) import Morley.Michelson.Untyped qualified as U-import Morley.Tezos.Address (Address(..), GlobalCounter(..), isKeyAddress)-import Morley.Tezos.Address.Alias (AddressOrAlias(..), Alias)+import Morley.Tezos.Address+import Morley.Tezos.Address.Alias+import Morley.Tezos.Address.Kinds import Morley.Tezos.Core   (Mutez, Timestamp(..), getCurrentTime, unsafeAddMutez, unsafeSubMutez, zeroMutez) import Morley.Tezos.Crypto (KeyHash, parseHash)@@ -105,6 +108,8 @@   -- ^ Transfer tokens to the address.   | SetDelegateOp SetDelegateOperation   -- ^ Set the delegate of a contract.+  | EmitOp EmitOperation+  -- ^ Emit contract event.   deriving stock (Show)  instance Buildable ExecutorOp where@@ -118,6 +123,11 @@     SetDelegateOp SetDelegateOperation{..} ->       "Set delegate of contract " +| sdoContract |+       " to " +| maybe "<nobody>" build sdoDelegate |+ ""+    EmitOp (EmitOperation source T.Emit{..}) ->+      "Emit event " +| emTag |++        " from contract " +| source |++        " with type " +| emNotes |++        " and value " +| emValue |+ ""  -- | Result of a single execution of interpreter. data ExecutorRes = ExecutorRes@@ -143,7 +153,7 @@ data ExecutorState = ExecutorState   { _esGState :: GState   , _esRemainingSteps :: RemainingSteps-  , _esSourceAddress :: Maybe Address+  , _esSourceAddress :: Maybe L1Address   , _esLog :: ExecutorLog   , _esOperationHash :: ~OperationHash   , _esPrevCounters :: HashSet GlobalCounter@@ -171,7 +181,7 @@   | EEInterpreterFailed a                         InterpretError   -- ^ Interpretation of Michelson contract failed.-  | EEUnknownAddressAlias Alias+  | EEUnknownAddressAlias SomeAlias   -- ^ Given alias doesn't refer to any address.   | EEUnknownSender a   -- ^ Sender address is unknown.@@ -199,13 +209,18 @@   -- ^ Type of parameter in transfer to an implicit account is not Unit.   | EEOperationReplay ExecutorOp   -- ^ An attempt to perform the operation duplicated with @DUP@ instruction.-  deriving stock (Show, Functor)+  | EEGlobalOperationSourceNotImplicit Address+  -- ^ Attempted to initiate global operation from a non-implicit address.+  | EEGlobalEmitOp+  -- ^ Trying to run emit operation as a global operation, which should be impossible.+  deriving stock (Show, Functor, Foldable, Traversable)  instance (Buildable a) => Buildable (ExecutorError' a) where   build =     \case-      EEUnknownAddressAlias alias ->-        "The alias " +| alias |+ " doesn't have any associated addresses"+      EEUnknownAddressAlias (SomeAlias (alias :: Alias kind)) ->+        ("The alias " +| alias |+ " doesn't have any associated " +| demote @kind |+ " addresses")+        \\ aliasKindSanity alias       EEUnknownContract addr -> "The contract is not originated " +| addr |+ ""       EEInterpreterFailed addr err ->         "Michelson interpreter failed for contract " +| addr |+ ": " +| err |+ ""@@ -230,6 +245,10 @@         "Bad contract parameter for: " +| addr |+ ""       EEOperationReplay op ->         "Operation replay attempt:\n" +| indentF 2 (build op) |+ ""+      EEGlobalOperationSourceNotImplicit addr ->+        "Attempted to initiate global operation from a non-implicit address " +| addr |+ ""+      EEGlobalEmitOp ->+        "Attempted to run emit event as a global operation, this should be impossible."  type ExecutorError = ExecutorError' Address @@ -274,14 +293,14 @@ originateContract   :: FilePath   -> TypeCheckOptions-  -> Address-  -> Maybe Alias+  -> ImplicitAddress+  -> Maybe ContractAlias   -> Maybe KeyHash   -> Mutez   -> U.Value   -> U.Contract   -> "verbose" :! Bool-  -> IO Address+  -> IO ContractAddress originateContract dbPath tcOpts originator mbAlias delegate balance uStorage uContract verbose = do   origination <- either throwM pure . typeCheckingWith tcOpts $     mkOrigination <$> typeCheckContractAndStorage uContract uStorage@@ -325,8 +344,8 @@     -- Here we are safe to bypass executeGlobalOperations for origination,     -- since origination can't generate more operations.     addr <- executeGlobalOrigination origination-    let transferOp = TransferOp $ TransferOperation addr txData 1-    executeGlobalOperations tcOpts [transferOp]+    let transferOp = TransferOp $ TransferOperation (MkAddress addr) txData 1+    void $ executeGlobalOperations tcOpts [transferOp]     getContractStorage addr   return newSt   where@@ -349,30 +368,29 @@       , ooAlias = Nothing       } -    getContractStorage :: Address -> ExecutorM SomeStorage+    getContractStorage :: ContractAddress -> ExecutorM SomeStorage     getContractStorage addr = do-      addrs <- use (esGState . gsAddressesL)+      addrs <- use (esGState . gsContractAddressesL)       case addrs ^. at addr of         Nothing -> error $ pretty addr <> " is unknown"-        Just (ASSimple {}) -> error $ pretty addr <> " is a simple address"-        Just (ASContract (ContractState{..})) -> return $ SomeStorage csStorage+        Just ContractState{..} -> return $ SomeStorage csStorage  -- | Send a transaction to given address with given parameters.-transfer ::-     Maybe Timestamp+transfer+  :: Maybe Timestamp   -> Maybe Natural   -> Maybe Natural   -> Word64   -> FilePath   -> TypeCheckOptions-  -> AddressOrAlias+  -> AddressOrAlias kind   -> TxData   -> "verbose" :! Bool   -> "dryRun" :? Bool   -> IO () transfer maybeNow maybeLevel maybeMinBlockTime maxSteps dbPath tcOpts destination txData verbose dryRun = do   void $ runExecutorMWithDB maybeNow maybeLevel maybeMinBlockTime dbPath (RemainingSteps maxSteps) verbose dryRun $ do-    destAddr <- resolveAddress destination+    destAddr <- MkAddress <$> resolveAddress destination     executeGlobalOperations tcOpts [TransferOp $ TransferOperation destAddr txData 0]  ----------------------------------------------------------------------------@@ -478,27 +496,31 @@         mapM_ putTextLn logs       putTextLn "" -- extra break line to separate logs from two sequence contracts --- | Resolves 'AddressOrAlias' type to 'Address'-resolveAddress :: AddressOrAlias -> ExecutorM Address+-- | Resolves 'AddressOrAlias' type to 'KindedAddress' of the appropriate kind.+resolveAddress+  :: forall kind. AddressOrAlias kind+  -> ExecutorM (KindedAddress kind) resolveAddress (AddressResolved addr) = pure addr resolveAddress (AddressAlias alias) = do-  addrAliases <- use $ esGState . gsAddressAliasesL-  case lookupAddress alias addrAliases of+  let s :: SingAddressKind kind = T.sing @kind \\ aliasKindSanity alias+  addrMb <- use $ case s of+    SAddressKindImplicit -> esGState . gsImplicitAddressAliasesL . at alias+    SAddressKindContract -> esGState . gsContractAddressAliasesL . at alias+  case addrMb of     Just addr -> pure addr-    Nothing -> throwError $ EEUnknownAddressAlias alias+    Nothing -> throwError $ EEUnknownAddressAlias $ SomeAlias alias --- | Execute a list of global operations, discarding their results.+-- | Execute a list of global operations, returning a list of generated events. executeGlobalOperations   :: TypeCheckOptions   -> [ExecutorOp]-  -> ExecutorM ()-executeGlobalOperations tcOpts = mapM_ $ \op ->-  executeMany (#isGlobalOp :! True) [op]+  -> ExecutorM [EmitOperation]+executeGlobalOperations tcOpts = concatMapM $ \op -> executeMany (#isGlobalOp :! True) [op]   where     -- | Execute a list of operations and additional operations they return, until there are none.-    executeMany :: "isGlobalOp" :! Bool -> [ExecutorOp] -> ExecutorM ()+    executeMany :: "isGlobalOp" :! Bool -> [ExecutorOp] -> ExecutorM [EmitOperation]     executeMany isGlobalOp = \case-        [] -> pass+        [] -> pure []         (op:opsTail) -> do           case op of             OriginateOp origination -> do@@ -510,16 +532,19 @@             TransferOp transferOperation -> do               moreOps <- executeTransfer isGlobalOp Nothing tcOpts transferOperation               executeMany (#isGlobalOp :! False) $ moreOps <> opsTail+            EmitOp emitOperation -> do+              liftM2 (:) (executeEmit isGlobalOp emitOperation) $+                executeMany (#isGlobalOp :! False) opsTail  -- | Execute a global origination operation.-executeGlobalOrigination :: OriginationOperation -> ExecutorM Address+executeGlobalOrigination :: OriginationOperation -> ExecutorM ContractAddress executeGlobalOrigination = executeOrigination ! #isGlobalOp True  -- | Execute an origination operation. executeOrigination   :: "isGlobalOp" :! Bool   -> OriginationOperation-  -> ExecutorM Address+  -> ExecutorM ContractAddress executeOrigination (arg #isGlobalOp -> isGlobalOp) origination@(OriginationOperation{..}) = do   when isGlobalOp $ do     beginGlobalOperation@@ -538,11 +563,12 @@   let contractState = ContractState ooBalance ooContract storageWithIds ooDelegate    let originatorAddress = ooOriginator-  originatorBalance <- case gsAddresses gs ^. at originatorAddress of-    Nothing -> throwError (EEUnknownManager originatorAddress)-    Just (asBalance -> oldBalance)++  originatorBalance <- case lookupBalance originatorAddress gs of+    Nothing -> throwError $ EEUnknownManager $ MkAddress ooOriginator+    Just oldBalance       | oldBalance < ooBalance ->-        throwError $ EENotEnoughFunds originatorAddress oldBalance+        throwError $ EENotEnoughFunds (MkAddress ooOriginator) oldBalance       | otherwise ->         -- Subtraction is safe because we have checked its         -- precondition in guard.@@ -551,8 +577,8 @@     address = mkContractAddress opHash ooCounter     updates =       catMaybes-        [ liftA2 GSAddAddressAlias ooAlias (Just address)-        , Just $ GSAddAddress address (ASContract contractState)+        [ liftA2 GSAddContractAddressAlias ooAlias (Just address)+        , Just $ GSAddContractAddress address contractState         , Just $ GSSetBalance originatorAddress originatorBalance         , Just GSIncrementCounter         , if bigMapCounter0 == bigMapCounter1@@ -573,7 +599,7 @@   :: "isGlobalOp" :! Bool   -> SetDelegateOperation   -> ExecutorM ()-executeDelegation (arg #isGlobalOp -> isGlobalOp) delegation@(SetDelegateOperation{..}) = do+executeDelegation (arg #isGlobalOp -> isGlobalOp) delegation@SetDelegateOperation{..} = do   when isGlobalOp $ do     beginGlobalOperation     assign esOperationHash $ mkDelegationOperationHash delegation@@ -591,6 +617,16 @@        return () +-- | Execute delegation operation.+executeEmit+  :: "isGlobalOp" :! Bool+  -> EmitOperation+  -> ExecutorM EmitOperation+executeEmit (arg #isGlobalOp -> isGlobalOp) op = do+  when isGlobalOp $ throwError EEGlobalEmitOp+  checkOperationReplay $ EmitOp op+  pure op+ -- | Execute a transfer operation. executeTransfer   :: "isGlobalOp" :! Bool@@ -604,7 +640,10 @@   -> TransferOperation   -> ExecutorM [ExecutorOp] executeTransfer (arg #isGlobalOp -> isGlobalOp)-  overrideBalanceMb tcOpts transferOperation@(TransferOperation addr txData _) = do+  overrideBalanceMb tcOpts+    transferOperation@(+      TransferOperation (MkAddress (addr :: KindedAddress kind))+        txData@TxData{tdSenderAddress=MkConstrainedAddress senderAddr,..} _) = do     when isGlobalOp $       beginGlobalOperation @@ -613,186 +652,214 @@     mbt <- view eeMinBlockTime     gs <- use esGState     remainingSteps <- use esRemainingSteps-    mSourceAddr <- use esSourceAddress+    sourceAddr <- fromMaybe (tdSenderAddress txData) <$> use esSourceAddress      let globalCounter = gsCounter gs-    let addresses = gsAddresses gs-    let senderAddr = tdSenderAddress txData-    let sourceAddr = fromMaybe senderAddr mSourceAddr-    let isZeroTransfer = tdAmount txData == zeroMutez+    let addresses :: Map (KindedAddress kind) (AddressStateFam kind)+        addresses = case addr of+          ImplicitAddress{} -> gsImplicitAddresses gs+          ContractAddress{} -> gsContractAddresses gs+          TxRollupAddress{} -> gsTxRollupAddresses gs+    let isZeroTransfer = tdAmount == zeroMutez+    let senderBalance = lookupBalance senderAddr gs      checkOperationReplay $ TransferOp transferOperation      -- Implicit addresses can't be senders with a balance of 0tz even when the transfer amount     -- is zero.-    when (isKeyAddress senderAddr && isNothing overrideBalanceMb) $-      case addresses ^. at senderAddr of-        Nothing -> throwError $ EEEmptyImplicitContract senderAddr-        Just (asBalance -> balance) | balance == zeroMutez ->-          throwError $ EEEmptyImplicitContract senderAddr-        _ -> pass+    case isImplicitAddress senderAddr of+      Nothing -> do+        when (isGlobalOp && not isZeroTransfer) $+          throwError $ EETransactionFromContract (MkAddress senderAddr) tdAmount -    when (badParamToImplicitAccount addr $ tdParameter txData) $-      throwError $ EEWrongParameterType addr+      Just Refl -> do+        when (isNothing overrideBalanceMb) $+          case senderBalance of+            Nothing -> throwError $ EEEmptyImplicitContract $ MkAddress senderAddr+            Just balance | balance == zeroMutez ->+              throwError $ EEEmptyImplicitContract $ MkAddress senderAddr+            _ -> pass -    -- Transferring 0 XTZ to a key address is prohibited.-    when (isZeroTransfer && isKeyAddress addr) $-      throwError $ EEZeroTransaction addr+    case isImplicitAddress addr of+      Nothing -> pass+      Just Refl -> do+        when (badParamToImplicitAccount tdParameter) $+          throwError $ EEWrongParameterType $ MkAddress addr++        -- Transferring 0 XTZ to a key address is prohibited.+        when (isZeroTransfer) $+          throwError $ EEZeroTransaction $ MkAddress addr+     mDecreaseSenderBalance <-       if isNothing overrideBalanceMb && not isZeroTransfer-        then case addresses ^. at senderAddr of-          Nothing -> throwError $ EEUnknownSender senderAddr-          Just (asBalance -> balance)-            | balance < tdAmount txData ->-              throwError $ EENotEnoughFunds senderAddr balance-            | otherwise ->+        then case senderBalance of+          Nothing -> throwError $ EEUnknownSender $ MkAddress senderAddr+          Just balance+            | balance < tdAmount ->+              throwError $ EENotEnoughFunds (MkAddress senderAddr) balance+            | otherwise -> do               -- Subtraction is safe because we have checked its               -- precondition in guard.-              return $ Just $ GSSetBalance senderAddr (balance `unsafeSubMutez` tdAmount txData)+              let newBal = balance `unsafeSubMutez` tdAmount+              pure $ Just $ GSSetBalance senderAddr newBal         else pure Nothing-    when (not (isKeyAddress senderAddr) && isGlobalOp && not isZeroTransfer) $-      throwError $ EETransactionFromContract senderAddr $ tdAmount txData-    let onlyUpdates updates = return (updates, [], Nothing, remainingSteps)-    (otherUpdates, sideEffects, maybeInterpretRes :: Maybe InterpretResult, newRemSteps)-        <- case (addresses ^. at addr, addr) of-      (Nothing, TransactionRollupAddress _) ->-        -- TODO [#838]: support transaction rollups on the emulator-        throwError $ EEUnknownContract addr-      (Nothing, ContractAddress _) ->-        throwError $ EEUnknownContract addr-      (Nothing, KeyAddress _) -> do-        let-          transferAmount = tdAmount txData-          addrState = ASSimple transferAmount-          upd = GSAddAddress addr addrState -        onlyUpdates [upd]-      (Just (ASSimple oldBalance), _) -> do-        let-          -- Calculate the account's new balance, unless `overrideBalanceMb` is used.-          -- Note: `unsafeAddMutez` can't overflow if global state is correct (because we can't-          -- create money out of nowhere)-          newBalance =-            fromMaybe-              (oldBalance `unsafeAddMutez` tdAmount txData)-              overrideBalanceMb-          upd = GSSetBalance addr newBalance-        onlyUpdates [upd]-      (Just (ASContract (ContractState {..})), _) -> do-        let-          existingContracts = extractAllContracts gs-          newBalance =-            -- Calculate the contract's new balance, unless `overrideBalanceMb` is used.-            -- Note: `unsafeAddMutez` can't overflow if global state is correct (because we can't-            -- create money out of nowhere)-            fromMaybe-              (csBalance `unsafeAddMutez` tdAmount txData)-              overrideBalanceMb-          epName = tdEntrypoint txData+    let commonFinishup+          :: Dict (L1AddressKind kind)+          -- NB: this is a Dict and not a constraint because GHC desugars these+          -- let-bindings such that it expects this constraint at the definition+          -- site.+          -> [GStateUpdate]+          -> [T.Operation]+          -> Maybe InterpretResult+          -> RemainingSteps+          -> ExecutorM [ExecutorOp]+        commonFinishup Dict otherUpdates sideEffects maybeInterpretRes newRemSteps = do+          let+            -- According to the reference implementation, counter is incremented for transfers as well.+            updates = (maybe id (:) mDecreaseSenderBalance otherUpdates) ++ [GSIncrementCounter] -        T.MkEntrypointCallRes _ (epc :: EntrypointCallT cp epArg)-          <- T.mkEntrypointCall epName (T.cParamNotes csContract)-             & maybe (throwError $ EEUnknownEntrypoint epName) pure+          newGState <- liftEither $ first EEFailedToApplyUpdates $ applyUpdates updates gs -        -- If the parameter has already been typechecked, simply check if-        -- its type matches the contract's entrypoint's type.-        -- Otherwise (e.g. if it was parsed from stdin via the CLI),-        -- we need to typecheck the parameter.-        typedParameter <--          case tdParameter txData of-            TxTypedParam (typedVal :: T.Value t) -> do-              T.castM @t @epArg typedVal (throwError . EEUnexpectedParameterType addr)-            TxUntypedParam untypedVal ->-              liftEither $ first (EEIllTypedParameter addr) $ typeCheckingWith tcOpts $-                typeVerifyParameter @epArg existingContracts untypedVal+          esGState .= newGState+          esRemainingSteps .= newRemSteps+          esSourceAddress .= Just sourceAddr -        let bigMapCounter0 = gs ^. gsBigMapCounterL-        let (typedParameterWithIds, bigMapCounter1) = runState (assignBigMapIds False typedParameter) bigMapCounter0+          esLog <>= ExecutorLog updates (maybe mempty (one . (MkAddress addr, )) maybeInterpretRes) -        -- I'm not entirely sure why we need to pattern match on `()` here,-        -- but, if we don't, we get a compiler error that I suspect is somehow related-        -- to the existential types we're matching on a few lines above.-        ---        -- • Couldn't match type ‘a0’-        --                  with ‘(InterpretResult, RemainingSteps, [Operation], [GStateUpdate])’-        --     ‘a0’ is untouchable inside the constraints: StorageScope st1-        () <- when isGlobalOp $-          esOperationHash .= mkTransferOperationHash-            addr-            typedParameterWithIds-            (tdEntrypoint txData)-            (tdAmount txData)+          mapM (convertOp addr) $ sideEffects+        onlyUpdates :: Dict (L1AddressKind kind) -> [GStateUpdate] -> ExecutorM [ExecutorOp]+        onlyUpdates dict updates = commonFinishup dict updates [] Nothing remainingSteps -        opHash <- use esOperationHash-        let-          contractEnv = ContractEnv-            { ceNow = now-            , ceMaxSteps = remainingSteps-            , ceBalance = newBalance-            , ceContracts = gsAddresses gs-            , ceSelf = addr-            , ceSource = sourceAddr-            , ceSender = senderAddr-            , ceAmount = tdAmount txData-            , ceVotingPowers = gsVotingPowers gs-            , ceChainId = gsChainId gs-            , ceOperationHash = Just opHash-            , ceLevel = level-            , ceErrorSrcPos = def-            , ceMinBlockTime = mbt-            }+    case addr of+      TxRollupAddress{} ->+        -- TODO [#838]: support transaction rollups on the emulator+        throwError $ EEUnknownContract (MkAddress addr)+      ImplicitAddress{} -> case addresses ^. at addr of+        Nothing -> do+          let+            transferAmount = tdAmount+            addrState = transferAmount+            upd = GSAddImplicitAddress addr addrState -        iur@InterpretResult-          { iurOps = sideEffects-          , iurNewStorage = newValue-          , iurNewState = InterpreterState newRemainingSteps globalCounter2 bigMapCounter2-          }-          <- liftEither $ first (EEInterpreterFailed addr) $-             handleContractReturn $-                interpret-                  csContract-                  epc-                  typedParameterWithIds-                  csStorage-                  (gsCounter gs)-                  bigMapCounter1-                  contractEnv+          onlyUpdates Dict [upd]+        Just oldBalance -> do+          let+            -- Calculate the account's new balance, unless `overrideBalanceMb` is used.+            -- Note: `unsafeAddMutez` can't overflow if global state is correct (because we can't+            -- create money out of nowhere)+            newBalance =+              fromMaybe+                (oldBalance `unsafeAddMutez` tdAmount)+                overrideBalanceMb+            upd = GSSetBalance addr newBalance+          onlyUpdates Dict [upd]+      ContractAddress{} -> case addresses ^. at addr of+        Nothing -> throwError $ EEUnknownContract (MkAddress addr)+        Just ContractState{..} -> do+          let+            existingContracts = extractAllContracts gs+            newBalance =+              -- Calculate the contract's new balance, unless `overrideBalanceMb` is used.+              -- Note: `unsafeAddMutez` can't overflow if global state is correct (because we can't+              -- create money out of nowhere)+              fromMaybe+                (csBalance `unsafeAddMutez` tdAmount)+                overrideBalanceMb+            epName = tdEntrypoint -        let-          updBalance-            | newBalance == csBalance = Nothing-            | otherwise = Just $ GSSetBalance addr newBalance-          updStorage-            | SomeValue newValue == SomeValue csStorage = Nothing-            | otherwise = Just $ GSSetStorageValue addr newValue-          updBigMapCounter-            | bigMapCounter0 == bigMapCounter2 = Nothing-            | otherwise = Just $ GSSetBigMapCounter bigMapCounter2-          updGlobalCounter-            | globalCounter == globalCounter2 = Nothing-            | otherwise = Just $ GSUpdateCounter globalCounter2-          updates = catMaybes-            [ updBalance-            , updStorage-            , updBigMapCounter-            , updGlobalCounter-            ]-        return (updates, sideEffects, Just iur, newRemainingSteps)+          T.MkEntrypointCallRes _ (epc :: EntrypointCallT cp epArg)+            <- T.mkEntrypointCall epName (T.cParamNotes csContract)+              & maybe (throwError $ EEUnknownEntrypoint epName) pure -    let-      -- According to the reference implementation, counter is incremented for transfers as well.-      updates = (maybe id (:) mDecreaseSenderBalance otherUpdates) ++ [GSIncrementCounter]+          -- If the parameter has already been typechecked, simply check if+          -- its type matches the contract's entrypoint's type.+          -- Otherwise (e.g. if it was parsed from stdin via the CLI),+          -- we need to typecheck the parameter.+          typedParameter <-+            case tdParameter of+              TxTypedParam (typedVal :: T.Value t) ->+                T.castM @t @epArg typedVal $+                  throwError . EEUnexpectedParameterType (MkAddress addr)+              TxUntypedParam untypedVal ->+                liftEither $ first (EEIllTypedParameter $ MkAddress addr) $+                  typeCheckingWith tcOpts $+                    typeVerifyParameter @epArg existingContracts untypedVal -    newGState <- liftEither $ first EEFailedToApplyUpdates $ applyUpdates updates gs+          let bigMapCounter0 = gs ^. gsBigMapCounterL+          let (typedParameterWithIds, bigMapCounter1) = runState (assignBigMapIds False typedParameter) bigMapCounter0 -    esGState .= newGState-    esRemainingSteps .= newRemSteps-    esSourceAddress .= Just sourceAddr+          -- I'm not entirely sure why we need to pattern match on `()` here,+          -- but, if we don't, we get a compiler error that I suspect is somehow related+          -- to the existential types we're matching on a few lines above.+          --+          -- • Couldn't match type ‘a0’+          --                  with ‘(InterpretResult, RemainingSteps, [Operation], [GStateUpdate])’+          --     ‘a0’ is untouchable inside the constraints: StorageScope st1+          () <- when isGlobalOp $+            esOperationHash .= mkTransferOperationHash+              addr+              typedParameterWithIds+              tdEntrypoint+              tdAmount -    esLog <>= ExecutorLog updates (maybe mempty (one . (addr, )) maybeInterpretRes)+          opHash <- use esOperationHash+          let+            contractEnv = ContractEnv+              { ceNow = now+              , ceMaxSteps = remainingSteps+              , ceBalance = newBalance+              , ceContracts = gsContractAddresses gs+              , ceSelf = addr+              , ceSource = sourceAddr+              , ceSender = MkConstrainedAddress senderAddr+              , ceAmount = tdAmount+              , ceVotingPowers = gsVotingPowers gs+              , ceChainId = gsChainId gs+              , ceOperationHash = Just opHash+              , ceLevel = level+              , ceErrorSrcPos = def+              , ceMinBlockTime = mbt+              } -    return $ convertOp addr <$> sideEffects+          iur@InterpretResult+            { iurOps = sideEffects+            , iurNewStorage = newValue+            , iurNewState = InterpreterState newRemainingSteps globalCounter2 bigMapCounter2+            }+            <- liftEither $ first (EEInterpreterFailed (MkAddress addr)) $+              handleContractReturn $+                  interpret+                    csContract+                    epc+                    typedParameterWithIds+                    csStorage+                    (gsCounter gs)+                    bigMapCounter1+                    contractEnv +          let+            updBalance+              | newBalance == csBalance = Nothing+              | otherwise = Just $ GSSetBalance addr newBalance+            updStorage+              | SomeValue newValue == SomeValue csStorage = Nothing+              | otherwise = Just $ GSSetStorageValue addr newValue+            updBigMapCounter+              | bigMapCounter0 == bigMapCounter2 = Nothing+              | otherwise = Just $ GSSetBigMapCounter bigMapCounter2+            updGlobalCounter+              | globalCounter == globalCounter2 = Nothing+              | otherwise = Just $ GSUpdateCounter globalCounter2+            updates = catMaybes+              [ updBalance+              , updStorage+              , updBigMapCounter+              , updGlobalCounter+              ]+          commonFinishup Dict updates sideEffects (Just iur) newRemainingSteps++ ---------------------------------------------------------------------------- -- Simple helpers ----------------------------------------------------------------------------@@ -804,21 +871,22 @@       OriginateOp OriginationOperation{..} -> ooCounter       TransferOp TransferOperation{..} -> toCounter       SetDelegateOp SetDelegateOperation{..} -> sdoCounter+      EmitOp (EmitOperation _ T.Emit{..}) -> emCounter   prevCounters <- use esPrevCounters   when (opCounter `HS.member` prevCounters) $     throwError $ EEOperationReplay op   esPrevCounters <>= one opCounter  -- The argument is the address of the contract that generated this operation.-convertOp :: Address -> T.Operation -> ExecutorOp+convertOp :: L1AddressKind kind => KindedAddress kind -> T.Operation -> ExecutorM ExecutorOp convertOp interpretedAddr =   \case     OpTransferTokens tt ->-      case ttContract tt of+      pure $ case ttContract tt of         T.VContract destAddress sepc ->           let txData =                 TxData-                  { tdSenderAddress = interpretedAddr+                  { tdSenderAddress = MkConstrainedAddress interpretedAddr                   , tdEntrypoint = T.sepcName sepc                   , tdParameter = TxTypedParam (ttTransferArgument tt)                   , tdAmount = ttAmount tt@@ -830,31 +898,34 @@                   , toCounter = ttCounter tt                   }           in TransferOp transferOperation-    OpSetDelegate T.SetDelegate{..} -> SetDelegateOp SetDelegateOperation-      { sdoContract = interpretedAddr-      , sdoDelegate = sdMbKeyHash-      , sdoCounter = sdCounter-      }-    OpCreateContract cc ->-      let origination = OriginationOperation-            { ooOriginator = ccOriginator cc-            , ooDelegate = ccDelegate cc-            , ooBalance = ccBalance cc-            , ooStorage = ccStorageVal cc-            , ooContract = ccContract cc-            , ooCounter = ccCounter cc-            , ooAlias = Nothing-            }-       in OriginateOp origination+    OpSetDelegate T.SetDelegate{..} -> case interpretedAddr of+      addr@ContractAddress{} -> pure $ SetDelegateOp SetDelegateOperation+        { sdoContract = addr+        , sdoDelegate = sdMbKeyHash+        , sdoCounter = sdCounter+        }+      _ -> throwError $ EEUnknownContract $ MkAddress interpretedAddr+    OpCreateContract CreateContract{ccOriginator=MkConstrainedAddress ccOriginator, ..} ->+      pure $ OriginateOp OriginationOperation+        { ooOriginator = ccOriginator+        , ooDelegate = ccDelegate+        , ooBalance = ccBalance+        , ooStorage = ccStorageVal+        , ooContract = ccContract+        , ooCounter = ccCounter+        , ooAlias = Nothing+        }+    OpEmit emit -> case interpretedAddr of+      ContractAddress{} -> pure $ EmitOp $ EmitOperation interpretedAddr emit+      _ -> throwError $ EEUnknownContract $ MkAddress interpretedAddr  -- | Reset source address before executing a global operation. beginGlobalOperation :: ExecutorM () beginGlobalOperation =   esSourceAddress .= Nothing --- | Return True if address is an implicit account yet the param is not Unit.-badParamToImplicitAccount :: Address -> TxParam -> Bool-badParamToImplicitAccount (ContractAddress _) _                       = False-badParamToImplicitAccount (KeyAddress _) (TxTypedParam T.VUnit)       = False-badParamToImplicitAccount (KeyAddress _) (TxUntypedParam U.ValueUnit) = False-badParamToImplicitAccount _ _                                         = True+-- | Return True if the param is not Unit.+badParamToImplicitAccount :: TxParam -> Bool+badParamToImplicitAccount (TxTypedParam T.VUnit)       = False+badParamToImplicitAccount (TxUntypedParam U.ValueUnit) = False+badParamToImplicitAccount _ = True

@@ -13,6 +13,7 @@   , dummyGlobalCounter   , dummyOrigination   , dummyMinBlockTime+  , dummySelf   ) where  import Data.Default (def)@@ -22,7 +23,7 @@ import Morley.Michelson.Typed (ParameterScope, StorageScope) import Morley.Michelson.Typed qualified as T import Morley.Michelson.Typed.Operation (OriginationOperation(..))-import Morley.Tezos.Address (GlobalCounter(..))+import Morley.Tezos.Address import Morley.Tezos.Core (Timestamp(..), dummyChainId, tz)  -- | Dummy timestamp, can be used to specify current @NOW@ value or@@ -50,6 +51,9 @@ dummyGlobalCounter :: GlobalCounter dummyGlobalCounter = 0 +dummySelf :: ContractAddress+dummySelf = [ta|KT1AEseqMV6fk2vtvQCVyA7ZCaxv7cpxtXdB|]+ -- | Dummy 'ContractEnv' with some reasonable hardcoded values. You -- can override values you are interested in using record update -- syntax.@@ -59,9 +63,9 @@   , ceMaxSteps = dummyMaxSteps   , ceBalance = [tz|100u|]   , ceContracts = mempty-  , ceSelf = genesisAddress-  , ceSource = genesisAddress-  , ceSender = genesisAddress+  , ceSelf = dummySelf+  , ceSource = MkConstrainedAddress genesisAddress+  , ceSender = MkConstrainedAddress genesisAddress   , ceAmount = [tz|100u|]   , ceVotingPowers = dummyVotingPowers   , ceChainId = dummyChainId

@@ -7,10 +7,6 @@   (     -- * Auxiliary types     ContractState (..)-  , AddressState (..)-  , AddressAliases (..)-  , lookupAddress-  , asBalance   , VotingPowers (..)   , vpPick   , vpTotal@@ -23,11 +19,14 @@   -- * GState   , GState (..)   , gsChainIdL-  , gsAddressesL-  , gsAddressAliasesL+  , gsImplicitAddressesL+  , gsContractAddressesL+  , gsImplicitAddressAliasesL+  , gsContractAddressAliasesL   , gsVotingPowersL   , gsCounterL   , gsBigMapCounterL+  , addressesL   , genesisAddresses   , genesisKeyHashes   , genesisAddress@@ -51,6 +50,8 @@   , applyUpdate   , applyUpdates   , extractAllContracts+  , lookupBalance+  , AddressStateFam   ) where  import Control.Lens (at, makeLenses, (?~))@@ -58,8 +59,6 @@ import Data.Aeson qualified as Aeson import Data.Aeson.Encode.Pretty qualified as Aeson import Data.Aeson.TH (deriveJSON)-import Data.Bimap (Bimap)-import Data.Bimap qualified as Bimap (empty, fromList, insert, lookup, toList) import Data.ByteString.Lazy qualified as LBS import Data.Default (def) import Data.Map.Strict qualified as Map@@ -73,13 +72,16 @@ import Morley.Michelson.Typed.Existential (SomeContractAndStorage(..)) import Morley.Michelson.Typed.Scope import Morley.Michelson.Untyped (Contract, Value)-import Morley.Tezos.Address (Address(..), GlobalCounter(..))-import Morley.Tezos.Address.Alias (Alias)+import Morley.Tezos.Address+import Morley.Tezos.Address.Alias+import Morley.Tezos.Address.Kinds import Morley.Tezos.Core (ChainId, Mutez, divModMutezInt, dummyChainId) import Morley.Tezos.Crypto import Morley.Util.Aeson+import Morley.Util.Bimap (Bimap)+import Morley.Util.Bimap qualified as Bimap import Morley.Util.Lens-import Morley.Util.Peano+import Morley.Util.Peano (ToPeano, type (>)) import Morley.Util.Sing (eqI, eqParamSing, eqParamSing2) import Morley.Util.SizedList qualified as SL import Morley.Util.SizedList.Types@@ -97,6 +99,8 @@   -- ^ Delegate associated with this contract.   } +makeLensesWith postfixLFields ''ContractState+ deriving stock instance Show ContractState  instance Eq ContractState where@@ -137,30 +141,6 @@     "\n  Contract: " +| T.convertContract csContract |+     "\n  Delegate: " +| csDelegate |+ "" --- | State of an arbitrary address.-data AddressState-  = ASSimple Mutez-  -- ^ For contracts without code we store only its balance.-  | ASContract ContractState-  -- ^ For contracts with code we store more state represented by-  -- 'ContractState'.-  deriving stock (Show, Eq, Generic)--instance Buildable AddressState where-  build =-    \case-      ASSimple balance -> "Balance = " +| balance |+ ""-      ASContract cs -> build cs--deriveJSON morleyAesonOptions ''AddressState---- | Extract balance from 'AddressState'.-asBalance :: AddressState -> Mutez-asBalance =-  \case-    ASSimple b -> b-    ASContract cs -> csBalance cs- -- | Distribution of voting power among the contracts. -- -- Voting power reflects the ability of bakers to accept, deny or pass new@@ -208,29 +188,23 @@ data GState = GState   { gsChainId :: ChainId   -- ^ Identifier of chain.-  , gsAddresses :: Map Address AddressState-  -- ^ All known addresses and their state.+  , gsImplicitAddresses :: Map ImplicitAddress Mutez+  -- ^ All known implicit addresses and their state (i.e. balance)+  , gsContractAddresses :: Map ContractAddress ContractState+  -- ^ All known contract addresses and their state.+  , gsTxRollupAddresses :: Map TxRollupAddress ()+  -- ^ All known transaction rollup addresses and their state.   , gsVotingPowers :: VotingPowers   -- ^ Voting power distribution.   , gsCounter :: GlobalCounter   -- ^ Ever increasing operation counter.   , gsBigMapCounter :: BigMapCounter-  , gsAddressAliases :: AddressAliases-  -- ^ Addresses with the associated aliases/names.+  , gsImplicitAddressAliases :: Bimap ImplicitAlias ImplicitAddress+  -- ^ Implicit addresses with the associated aliases/names.+  , gsContractAddressAliases :: Bimap ContractAlias ContractAddress+  -- ^ Contract addresses with the associated aliases/names.   } deriving stock (Show, Eq) -newtype AddressAliases = AddressAliases (Bimap Alias Address)-  deriving stock (Eq, Show)--instance FromJSON AddressAliases where-  parseJSON = fmap (AddressAliases . Bimap.fromList) . parseJSON--instance ToJSON AddressAliases where-  toJSON (AddressAliases aa) = toJSON $ Bimap.toList aa--lookupAddress :: Alias -> AddressAliases -> Maybe Address-lookupAddress alias (AddressAliases aa) = Bimap.lookup alias aa- makeLensesWith postfixLFields ''GState  deriveJSON morleyAesonOptions ''GState@@ -256,15 +230,15 @@ genesisKeyHashes = hashKey . toPublic <$> genesisSecrets  -- | Initially these addresses have a lot of money.-genesisAddresses :: GenesisList Address-genesisAddresses = KeyAddress <$> genesisKeyHashes+genesisAddresses :: GenesisList ImplicitAddress+genesisAddresses = ImplicitAddress <$> genesisKeyHashes  -- | One of genesis key hashes. genesisKeyHash :: KeyHash genesisKeyHash = SL.head genesisKeyHashes  -- | One of genesis addresses.-genesisAddress :: Address+genesisAddress :: ImplicitAddress genesisAddress = SL.head genesisAddresses  -- | Secret key assotiated with 'genesisAddress'.@@ -272,7 +246,7 @@ genesisSecretKey = SL.head genesisSecrets  -- | More genesis addresses-genesisAddress1, genesisAddress2, genesisAddress3 :: Address+genesisAddress1, genesisAddress2, genesisAddress3 :: ImplicitAddress _ :< genesisAddress1 :< genesisAddress2 :< genesisAddress3   :< _ = genesisAddresses @@ -282,7 +256,9 @@ -- -- Note that @'genesisAddress' == genesisAddressN \@0@, @'genesisAddress1' == genesisAddressN \@1@, -- etc.-genesisAddressN :: forall n. (SingIPeano n, ToPeano GenesisAddressesNum > ToPeano n ~ 'True) => Address+genesisAddressN+  :: forall n. (SingIPeano n, ToPeano GenesisAddressesNum > ToPeano n ~ 'True)+  => ImplicitAddress genesisAddressN = SL.index @n genesisAddresses  -- | Dummy 'VotingPowers'. We give all the voting power to two genesis addreses@@ -298,16 +274,19 @@ initGState =   GState   { gsChainId = dummyChainId-  , gsAddresses = Map.fromList-    [ (genesis, ASSimple money)+  , gsImplicitAddresses = Map.fromList+    [ (genesis, money)     | let (money, _) = maxBound @Mutez `divModMutezInt` genesisAddressesNum                     ?: error "Number of genesis addresses is 0"     , genesis <- toList genesisAddresses     ]+  , gsContractAddresses = Map.empty+  , gsTxRollupAddresses = Map.empty   , gsVotingPowers = dummyVotingPowers   , gsCounter = GlobalCounter 0   , gsBigMapCounter = BigMapCounter 0-  , gsAddressAliases = AddressAliases $ Bimap.empty+  , gsImplicitAddressAliases = Bimap.empty+  , gsContractAddressAliases = Bimap.empty   }  data GStateParseError =@@ -342,23 +321,26 @@  -- | Updates that can be applied to 'GState'. data GStateUpdate where-  GSAddAddress :: Address -> AddressState -> GStateUpdate-  GSAddAddressAlias :: Alias -> Address -> GStateUpdate-  GSSetStorageValue :: StorageScope st => Address -> T.Value st -> GStateUpdate-  GSSetBalance :: Address -> Mutez -> GStateUpdate+  GSAddImplicitAddress :: ImplicitAddress -> Mutez -> GStateUpdate+  GSAddContractAddress :: ContractAddress -> ContractState -> GStateUpdate+  GSAddContractAddressAlias :: ContractAlias -> ContractAddress -> GStateUpdate+  GSSetStorageValue :: StorageScope st => ContractAddress -> T.Value st -> GStateUpdate+  GSSetBalance :: L1AddressKind kind => KindedAddress kind -> Mutez -> GStateUpdate   GSIncrementCounter :: GStateUpdate   GSUpdateCounter :: GlobalCounter -> GStateUpdate   GSSetBigMapCounter :: BigMapCounter -> GStateUpdate-  GSSetDelegate :: Address -> Maybe KeyHash -> GStateUpdate+  GSSetDelegate :: ContractAddress -> Maybe KeyHash -> GStateUpdate  deriving stock instance Show GStateUpdate  instance Buildable GStateUpdate where   build =     \case-      GSAddAddress addr st ->-        "Add address " +| addr |+ " with state " +| st |+ ""-      GSAddAddressAlias alias addr ->+      GSAddImplicitAddress addr st ->+        "Add implicit address " +| addr |+ " with balance " +| st |+ ""+      GSAddContractAddress addr st ->+        "Add contract address " +| addr |+ " with state " +| st |+ ""+      GSAddContractAddressAlias alias addr ->         "Add an alias " +| alias |+ " for address " +| addr |+ ""       GSSetStorageValue addr tVal ->         "Set storage value of address " +| addr |+ " to " +| T.untypeValue tVal |+ ""@@ -377,8 +359,8 @@ data GStateUpdateError   = GStateAddressExists Address   | GStateUnknownAddress Address-  | GStateNotContract Address-  | GStateStorageNotMatch Address+  | GStateStorageNotMatch ContractAddress+  | GStateTxRollup TxRollupAddress GStateUpdate   deriving stock (Show)  instance Buildable GStateUpdateError where@@ -386,20 +368,22 @@     \case       GStateAddressExists addr -> "Address already exists: " <> build addr       GStateUnknownAddress addr -> "Unknown address: " <> build addr-      GStateNotContract addr -> "Address doesn't have contract: " <> build addr       GStateStorageNotMatch addr ->         "Storage type does not match the contract in run-time state\         \ when updating new storage value to address: " <> build addr+      GStateTxRollup addr op ->+        "Transaction rollup address " +| addr |+ " doesn't support this operation: " +| op |+ ""  -- | Apply 'GStateUpdate' to 'GState'. applyUpdate :: GStateUpdate -> GState -> Either GStateUpdateError GState applyUpdate =   \case-    GSAddAddress addr st -> addAddress addr st-    GSAddAddressAlias alias addr -> Right . addAddressAlias alias addr+    GSAddImplicitAddress addr st -> addImplicitAddress addr st+    GSAddContractAddress addr st -> addContractAddress addr st+    GSAddContractAddressAlias alias addr -> Right . addContractAddressAlias alias addr     GSSetStorageValue addr newValue ->       setStorageValue addr newValue-    GSSetBalance addr newBalance -> setBalance addr newBalance+    GSSetBalance addr newBalance -> addr `setBalance` newBalance     GSIncrementCounter -> Right . over gsCounterL (+1)     GSUpdateCounter newCounter -> Right . set gsCounterL newCounter     GSSetBigMapCounter bmCounter -> Right . set gsBigMapCounterL bmCounter@@ -410,67 +394,92 @@ applyUpdates = flip (foldM (flip applyUpdate))  -- | Add an address if it hasn't been added before.-addAddress :: Address -> AddressState -> GState -> Either GStateUpdateError GState-addAddress addr st gs-    | addr `Map.member` (gsAddresses gs) = Left $ GStateAddressExists addr-    | otherwise = Right $ gs & gsAddressesL . at addr ?~ st+addImplicitAddress :: ImplicitAddress -> Mutez -> GState -> Either GStateUpdateError GState+addImplicitAddress addr st gs+  | addr `Map.member` (gsImplicitAddresses gs) = Left $ GStateAddressExists (MkAddress addr)+  | otherwise = Right $ gs & gsImplicitAddressesL . at addr ?~ st +-- | Add an address if it hasn't been added before.+addContractAddress :: ContractAddress -> ContractState -> GState -> Either GStateUpdateError GState+addContractAddress addr st gs+  | addr `Map.member` (gsContractAddresses gs) = Left $ GStateAddressExists (MkAddress addr)+  | otherwise = Right $ gs & gsContractAddressesL . at addr ?~ st+ -- | Add an alias for given address, overwriting any existing address for the same alias.-addAddressAlias :: Alias -> Address -> GState -> GState-addAddressAlias alias addr = gsAddressAliasesL %~ insertAddressAlias-  where-    insertAddressAlias (AddressAliases aa) =-      AddressAliases $ Bimap.insert alias addr aa+addContractAddressAlias :: ContractAlias -> ContractAddress -> GState -> GState+addContractAddressAlias alias addr = gsContractAddressAliasesL . at alias ?~ addr  -- | Update storage value associated with given address. setStorageValue :: forall st. (StorageScope st) =>-     Address -> T.Value st -> GState -> Either GStateUpdateError GState+     ContractAddress -> T.Value st -> GState -> Either GStateUpdateError GState setStorageValue addr newValue = updateAddressState addr modifier   where-    modifier :: AddressState -> Either GStateUpdateError AddressState-    modifier (ASSimple _) = Left (GStateNotContract addr)-    modifier (ASContract ContractState{csStorage = _ :: T.Value st', ..}) = do+    modifier :: ContractState -> Either GStateUpdateError ContractState+    modifier ContractState{csStorage = _ :: T.Value st', ..} = do       case eqI @st @st' of-        Just Refl -> Right $ ASContract $ ContractState{csStorage = newValue, ..}+        Just Refl -> Right $ ContractState{csStorage = newValue, ..}         _ -> Left $ GStateStorageNotMatch addr  -- | Update balance value associated with given address.-setBalance :: Address -> Mutez -> GState -> Either GStateUpdateError GState-setBalance addr newBalance = updateAddressState addr $ Right . \case-  ASSimple _ -> ASSimple newBalance-  ASContract cs -> ASContract (cs {csBalance = newBalance})+setBalance+  :: forall kind. L1AddressKind kind+  => KindedAddress kind+  -> Mutez+  -> GState+  -> Either GStateUpdateError GState+setBalance addr newBalance = updateAddressState addr $+  Right . set (balanceLens addr) newBalance +lookupBalance :: forall kind. L1AddressKind kind => KindedAddress kind -> GState -> Maybe Mutez+lookupBalance addr = preview $ addressesL addr . at addr . traverse . balanceLens addr++balanceLens+  :: forall kind. L1AddressKind kind+  => KindedAddress kind+  -> Lens' (AddressStateFam kind) Mutez+balanceLens = \case+  ImplicitAddress{} -> id+  ContractAddress{} -> csBalanceL+  where _ = usingImplicitOrContractKind @kind ()+ -- | Set delegate for a given address-setDelegate :: Address -> Maybe KeyHash -> GState -> Either GStateUpdateError GState-setDelegate addr key = updateAddressState addr \case-  ASSimple _ -> Left $ GStateNotContract addr-  ASContract cs -> Right $ ASContract cs{csDelegate = key}+setDelegate :: ContractAddress -> Maybe KeyHash -> GState -> Either GStateUpdateError GState+setDelegate addr key = updateAddressState addr $ pure . (csDelegateL .~ key) -updateAddressState ::-     Address-  -> (AddressState -> Either GStateUpdateError AddressState)+type family AddressStateFam kind where+  AddressStateFam 'AddressKindImplicit = Mutez+  AddressStateFam 'AddressKindContract = ContractState+  -- TODO [#838]: support transaction rollups on the emulator+  AddressStateFam 'AddressKindTxRollup = ()++updateAddressState+  :: forall kind. KindedAddress kind+  -> (AddressStateFam kind -> Either GStateUpdateError (AddressStateFam kind))   -> GState   -> Either GStateUpdateError GState updateAddressState addr f gs =-  case addresses ^. at addr of-    Nothing -> Left (GStateUnknownAddress addr)+  let addrL :: Lens' GState (Maybe (AddressStateFam kind))+      addrL = addressesL addr . at addr+  in case gs ^. addrL of+    Nothing -> Left $ GStateUnknownAddress $ MkAddress addr     Just as -> do       newState <- f as-      return $ gs { gsAddresses = addresses & at addr .~ Just newState }-  where-    addresses = gsAddresses gs+      return $ gs & addrL .~ Just newState +addressesL+  :: KindedAddress kind+  -> Lens' GState (Map (KindedAddress kind) (AddressStateFam kind))+addressesL = \case+  ImplicitAddress{} -> gsImplicitAddressesL+  ContractAddress{} -> gsContractAddressesL+  TxRollupAddress{} -> gsTxRollupAddressesL+ -- | Retrieve all contracts stored in GState extractAllContracts :: GState -> TcOriginatedContracts-extractAllContracts = Map.fromList . mapMaybe extractContract . toPairs . gsAddresses+extractAllContracts = Map.fromList . mapMaybe extractContract . toPairs . gsContractAddresses  where     extractContract-      :: (Address, AddressState) -> Maybe (ContractHash, SomeParamType)+      :: (ContractAddress, ContractState) -> Maybe (ContractHash, SomeParamType)     extractContract =-      \case (KeyAddress _, ASSimple {}) -> Nothing-            (KeyAddress _, _) -> error "broken GState"-            (ContractAddress ca, ASContract (ContractState{..})) ->+      \case (ContractAddress ca, ContractState{..}) ->               Just (ca, SomeParamType $ T.cParamNotes $ csContract)-            (ContractAddress _, _) -> error "broken GState"-            -- TODO [#838]: support transaction rollups on the emulator-            (TransactionRollupAddress _, _) -> error "broken GState"

@@ -18,7 +18,7 @@ import Morley.Michelson.Typed qualified as T import Morley.Michelson.Untyped (EpName) import Morley.Michelson.Untyped qualified as U-import Morley.Tezos.Address (Address)+import Morley.Tezos.Address import Morley.Tezos.Core (Mutez) import Morley.Util.Lens (postfixLFields) @@ -31,7 +31,7 @@  -- | Data associated with a particular transaction. data TxData = TxData-  { tdSenderAddress :: Address+  { tdSenderAddress :: L1Address   , tdParameter :: TxParam   , tdEntrypoint :: EpName   , tdAmount :: Mutez

@@ -12,6 +12,7 @@   , typeCheckStorage   , typeCheckTopLevelType   , typeCheckValue+  , typeCheckValueRunCodeCompat   , typeVerifyContract   , typeVerifyParameter   , typeVerifyStorage

@@ -27,7 +27,7 @@ import Morley.Michelson.TypeCheck.Types (SomeHST(..)) import Morley.Michelson.Typed qualified as T import Morley.Michelson.Untyped qualified as U-import Morley.Tezos.Address (Address)+import Morley.Tezos.Address import Morley.Tezos.Crypto (CryptoParseError) import Morley.Tezos.Crypto.BLS12381 qualified as BLS import Morley.Util.MismatchError@@ -54,6 +54,7 @@   | FailwithArgument   | TicketsJoin   | ViewBlock+  | EmitArgument   deriving stock (Show, Eq, Generic)   deriving anyclass (NFData) @@ -79,6 +80,7 @@     FailwithArgument -> "argument to FAILWITH"     TicketsJoin -> "join of two tickets"     ViewBlock -> "top-level view block"+    EmitArgument -> "argument to EMIT"  data TopLevelType   = TltParameterType@@ -132,8 +134,10 @@   -- ^ There are not enough items on stack to perform a certain instruction.   | IllegalEntrypoint T.EpNameFromRefAnnError   -- ^ Invalid entrypoint name provided-  | UnknownContract Address+  | UnknownContract ContractAddress   -- ^ Contract with given address is not originated.+  | TxRollupContract TxRollupAddress+  -- ^ Provided txr1 address as contract.   | EntrypointNotFound T.EpName   -- ^ Given entrypoint is not present.   | IllegalParamDecl T.ParamEpError@@ -158,6 +162,13 @@   -- ^ Empty block of code, like ITER body.   | AnyError   -- ^ Generic error when instruction does not match something sensible.+  | InvalidBigMapId Integer+  -- ^ A big_map with the given ID was not found.+  | UnexpectedBigMapType+  -- ^ We found a big_map with the given big_map ID, but+  -- its key and/or value types are not the same as the requested types.+      Integer -- ^ The big_map ID we used to lookup a big_map value.+      (MismatchError T.T)   deriving stock (Show, Eq, Generic)   deriving anyclass (NFData) @@ -194,6 +205,8 @@       "Not enough items on stack"     UnknownContract addr ->       "Contract is not registered:" <+> (renderAnyBuildable addr)+    TxRollupContract addr ->+      "txr1 address can not be used as a contract:" <+> (renderAnyBuildable addr)     IllegalEntrypoint err -> renderDoc context err     EntrypointNotFound ep ->       "No such entrypoint" <+> enclose "`" "`" (renderAnyBuildable ep)@@ -208,6 +221,11 @@       "Cannot use a terminate instruction (like FAILWITH) in this block"     EmptyCode -> "Code block is empty"     AnyError -> "Some of the arguments have invalid types"+    InvalidBigMapId bigMapId ->+      "No big_map with ID" <+> renderAnyBuildable bigMapId <+> "was found."+    UnexpectedBigMapType bigMapId mismatchError ->+      "A big_map with the ID" <+> renderAnyBuildable bigMapId <+> "was found, but it does not have the expected type."+      <$$> renderDoc context mismatchError  -- | Type check error data TCError

@@ -269,7 +269,7 @@   mapMSeq appendTypeComment tcSeq   where     appendTypeComment packedI@(inp :/ iAndOut) = do-      verbose <- lift (asks tcVerbose)+      verbose <- asks' tcVerbose       pure case (verbose, iAndOut) of         (True, i ::: out) -> inp :/ Seq i (stackTypeComment out) ::: out         (True, AnyOutInstr i) -> inp :/ AnyOutInstr (Seq i noStackTypeComment)@@ -279,7 +279,7 @@ prependStackTypeComment   :: SomeInstr inp -> TypeCheckInstrNoExcept (SomeInstr inp) prependStackTypeComment packedInstr@(inp :/ _) = do-  verbose <- lift (asks tcVerbose)+  verbose <- asks' tcVerbose   pure if verbose && (not (isNop' packedInstr))     then mapSomeInstr (Seq (stackTypeComment inp)) packedInstr     else packedInstr

@@ -38,6 +38,7 @@     , typeCheckStorage     , typeCheckTopLevelType     , typeCheckValue+    , typeCheckValueRunCodeCompat     , typeVerifyContract     , typeVerifyParameter     , typeVerifyStorage@@ -47,7 +48,6 @@  import Prelude hiding (EQ, GT, LT) -import Control.Lens ((.=)) import Control.Monad.Except (MonadError, catchError, liftEither, throwError) import Data.Constraint ((\\)) import Data.Default (def)@@ -74,7 +74,7 @@ import Morley.Util.MismatchError import Morley.Util.Peano import Morley.Util.PeanoNatural-import Morley.Util.Sing (SingI1(..))+import Morley.Util.Sing (SingIOne, withSingIOne) import Morley.Util.Type (knownListFromSingI, onFirst, type (++))  import Morley.Michelson.Untyped qualified as U@@ -199,7 +199,7 @@      onFailedCodeTypeCheck :: [TypeCheckedOp] -> TCError -> TypeCheck a     onFailedCodeTypeCheck ops err = do-      verbose <- asks tcVerbose+      verbose <- asks' tcVerbose       throwError if verbose         then TCIncompletelyTyped err U.Contract              { contractParameter = wholeParam@@ -212,7 +212,7 @@      onFailedFullTypeCheck :: [TypeCheckedOp] -> [U.View' TypeCheckedOp] -> TCError -> TypeCheck a     onFailedFullTypeCheck ops views err = do-      verbose <- asks tcVerbose+      verbose <- asks' tcVerbose       throwError if verbose         then TCIncompletelyTyped err U.Contract              { contractParameter = wholeParam@@ -278,7 +278,7 @@     onFailedViewsTypeCheck       :: U.View -> [TypeCheckedOp] -> TCError -> TypeCheck a     onFailedViewsTypeCheck v viewOps err = do-      verbose <- asks tcVerbose+      verbose <- asks' tcVerbose       throwError if verbose         then TCIncompletelyTypedView err v{ U.viewCode = viewOps }         else err@@ -306,7 +306,7 @@     onFailedViewsTypeCheck       :: Seq (U.View' TypeCheckedOp) -> U.View' TypeCheckedOp -> TCError -> TypeCheck a     onFailedViewsTypeCheck processedViews v err = do-      verbose <- asks tcVerbose+      verbose <- asks' tcVerbose       throwError if verbose         then TCIncompletelyTyped err tcCotract              { U.contractViews = toList (processedViews |> v)@@ -326,7 +326,7 @@   => [U.ExpandedOp]   -> HST inp   -> TypeCheck (SomeInstr inp)-typeCheckList = throwingTCError' ... typeCheckListNoExcept+typeCheckList = throwingTCError ... typeCheckListNoExcept  -- | Function @typeCheckListNoExcept@ converts list of Michelson instructions -- given in representation from @Morley.Michelson.Type@ module to representation in a@@ -354,14 +354,24 @@ typeCheckValue   :: forall t. SingI t   => U.Value-  -> TypeCheckInstr (Value t)+  -> TypeCheckResult (Value t) typeCheckValue value = do-  mode <- use tcModeL-  tcModeL .= TypeCheckValue (value, demote @t)-  res <- typeCheckValImpl @t Nothing typeCheckInstr value-  tcModeL .= mode-  pure res+  runTypeCheck (TypeCheckValue (value, demote @t) Nothing) $+    usingReaderT def $+      typeCheckValImpl Nothing typeCheckInstr value +-- | Simulates the typechecking behavior of the RPC's @/run_code@ endpoint.+--+-- If an integer is found where a big_map is expected,+-- we check if a big_map exists with that ID.+-- If it does, and if the big_map's value and key have the expected types, we replace the+-- big_map ID with the corresponding big_map value.+typeCheckValueRunCodeCompat :: forall t. SingI t => BigMapFinder -> U.Value -> TypeCheckResult (Value t)+typeCheckValueRunCodeCompat bigMapFinder val =+  runTypeCheck (TypeCheckValue (val, demote @t) (Just bigMapFinder)) $+    usingReaderT def $+      typeCheckValImpl Nothing typeCheckInstr val+ typeVerifyParameter   :: SingI t   => TcOriginatedContracts -> U.Value -> TypeCheckResult (Value t)@@ -376,7 +386,7 @@   :: forall t. SingI t   => Maybe TcOriginatedContracts -> U.Value -> TypeCheckResult (Value t) typeVerifyTopLevelType mOriginatedContracts valueU =-  runTypeCheck (TypeCheckValue (valueU, demote @t)) $ usingReaderT def $+  runTypeCheck (TypeCheckValue (valueU, demote @t) Nothing) $ usingReaderT def $     typeCheckValImpl mOriginatedContracts typeCheckInstr valueU  -- | Like 'typeCheckValue', but for values to be used as parameter.@@ -596,7 +606,10 @@    (U.PUSH vn mt mval, i) -> workOnInstr uInstr $     withUType mt $ \(nt :: Notes t) -> do-      val <- typeCheckValue @t mval+      -- Locally switch 'TypeCheckMode' to 'TypeCheckValue'.+      val <- local' (tcModeL .~ TypeCheckValue (mval, demote @t) Nothing) $+        typeCheckValImpl @t Nothing typeCheckInstr mval+       proofScope <- onScopeCheckInstrErr @t uInstr (SomeHST i) Nothing         $ checkScope @(ConstantScope t)       case proofScope of@@ -1356,9 +1369,9 @@   (U.VIEW{}, _) -> notEnoughItemsOnStack    (U.SELF vn fn, _) -> workOnInstr uInstr $ withNotInView uInstr do-    mode <- gets tcMode+    mode <- asks' tcMode     case mode of-      TypeCheckValue (value, ty) ->+      TypeCheckValue (value, ty) _ ->         tcFailedOnValue value ty "The SELF instruction cannot appear in a lambda" Nothing       TypeCheckContract (SomeParamType notescp) -> do         let epName = U.epNameFromSelfAnn fn@@ -1605,6 +1618,22 @@     failWithErr $ UnexpectedType $ ("sapling_transaction" :| ["sapling_state"]) :| []   (U.SAPLING_VERIFY_UPDATE _, _) -> notEnoughItemsOnStack +  (U.EMIT{}, SNil) -> notEnoughItemsOnStack++  (U.EMIT va tag mty, ((_ :: SingT t2), Dict) ::& rs) ->+    workOnInstr uInstr do+      Dict <- onScopeCheckInstrErr @t2 uInstr (SomeHST inp) Nothing $+        checkScope @(PackedValScope t2)+      case mty of+        Just (AsUType (ty :: Notes t1)) -> do+          Refl <- errM $ eqType @t1 @t2+          pure $ inp :/ AnnEMIT (Anns1 va) tag (Just ty) ::: ((sing, Dict) ::& rs)+        Nothing ->+          pure $ inp :/ AnnEMIT (Anns1 va) tag Nothing ::: ((sing, Dict) ::& rs)+      where+        errM :: (MonadReader TypeCheckInstrEnv m, MonadError TCError m) => Either TCTypeError a -> m a+        errM = onTypeCheckInstrErr uInstr (SomeHST inp) (Just EmitArgument)+   where     withWTPInstr'       :: forall t inp. SingI t@@ -1629,7 +1658,7 @@     notEnoughItemsOnStack' = failWithErr' NotEnoughItemsOnStack      withNotInView :: U.ExpandedInstr -> (IsNotInView => TypeCheckInstr r) -> TypeCheckInstr r-    withNotInView instr act = gets tcMode >>= \case+    withNotInView instr act = asks' tcMode >>= \case       -- we provide the not-in-view constraint in the isolated mode       TypeCheckTest -> giveNotInView act       _ -> view tcieNotInView >>= \case@@ -1676,7 +1705,7 @@   :: forall c rs.     ( MapOp c     , WellTyped (MapOpInp c)-    , SingI1 (MapOpRes c)+    , SingIOne (MapOpRes c)     )   => ([TypeCheckedOp] -> TypeCheckedInstr)   -> SingT (MapOpInp c)@@ -1696,7 +1725,7 @@             Refl <- onTypeCheckInstrErr instr (SomeHST i) (Just Iteration)               $ eqHST rs rs'             x <- mkRes bn rs'-            pure $ i :/ withSingI1 @(MapOpRes c) @v' (AnnMAP (Anns1 anns) sub ::: x)+            pure $ i :/ withSingIOne @(MapOpRes c) @v' (AnnMAP (Anns1 anns) sub ::: x)           _ -> typeCheckInstrErr instr (SomeHST i) (Just Iteration)       AnyOutInstr _ ->         typeCheckInstrErr' instr (SomeHST i) (Just Iteration) CodeAlwaysFails@@ -1720,8 +1749,8 @@     subI ::: o -> do       Refl <- onTypeCheckInstrErr instr (SomeHST i) (Just Iteration) $ eqHST o rs       pure $ i :/ ITER subI ::: o-    AnyOutInstr _ ->-      typeCheckInstrErr' instr (SomeHST i) (Just Iteration) CodeAlwaysFails+    AnyOutInstr subI ->+      pure $ i :/ ITER subI ::: rs  lamImpl   :: forall it ot ts .

@@ -5,6 +5,7 @@   ( TcInstrHandler   , TcOriginatedContracts   , TypeCheckEnv(..)+  , BigMapFinder   , TypeCheckOptions(..)   , TypeCheck   , TypeCheckNoExcept@@ -13,19 +14,18 @@   , TypeCheckInstr   , TypeCheckInstrNoExcept   , runTypeCheckIsolated-  , runTypeCheckInstrIsolated   , typeCheckingWith   , liftNoExcept-  , liftNoExcept'   , throwingTCError-  , throwingTCError'   , preserving   , preserving'   , guarding   , guarding_   , tcEither+  , ask'+  , asks'+  , local' -  , tcExtFramesL   , tcModeL   , TypeCheckMode(..)   , SomeParamType(..)@@ -36,8 +36,7 @@   ) where  import Control.Lens (makeLenses)-import Control.Monad.Except (Except, mapExceptT, runExcept, throwError)-import Control.Monad.Reader (mapReaderT)+import Control.Monad.Except (Except, MonadError, runExcept, throwError) import Data.Constraint (Dict) import Data.Default (Default(..)) import Fmt (Buildable, build, pretty)@@ -49,29 +48,40 @@   tcsEither) import Morley.Michelson.TypeCheck.Types import Morley.Michelson.Typed qualified as T+import Morley.Michelson.Typed.Existential (SomeVBigMap) import Morley.Michelson.Untyped qualified as U import Morley.Tezos.Address (ContractHash) import Morley.Util.Lens+import Morley.Util.MultiReader -type TypeCheck =-  (ReaderT TypeCheckOptions-    (ExceptT TCError-      (State TypeCheckEnv)))+-- | Environments avaliable during typecheck.+type TCEnvs = '[TypeCheckEnv, TypeCheckOptions] --- | A non-throwing alternative for @TypeCheck@. Mainly meant to be used for--- construction of a partially typed tree (see @TypeCheckedSeq@).-type TypeCheckNoExcept =-  (ReaderT TypeCheckOptions-    (State TypeCheckEnv))+-- | A full type-check monad carrying intermediary context (via 'TypeCheckEnv'),+-- general 'TypeCheckOptions' and throwing 'TCError'.+type TypeCheck = MultiReaderT TCEnvs (Except TCError) +-- | A non-throwing alternative for 'TypeCheck'. Mainly meant to be used for+-- construction of a partially typed tree (see 'TypeCheckedSeq').+type TypeCheckNoExcept = MultiReaderT TCEnvs Identity+ -- | Monad for performing some typechecking operations with the same options. -- -- Unlike 'TypeCheck' monad, this does not carry the context of intra-contract -- or intra-value typechecking.-type TypeCheckResult =-  (ReaderT TypeCheckOptions-    (Except TCError))+type TypeCheckResult = ReaderT TypeCheckOptions (Except TCError) +-- | Environments available during instr typecheck+type TCInstrEnvs = TypeCheckInstrEnv ': TCEnvs++-- | Version of 'TypeCheck' additionally carrying instruction-specific+-- 'TypeCheckInstrEnv'+type TypeCheckInstr = MultiReaderT TCInstrEnvs (Except TCError)++-- | Version of 'TypeCheckNoExcept' additionally carrying instruction-specific+-- 'TypeCheckInstrEnv'+type TypeCheckInstrNoExcept = MultiReaderT TCInstrEnvs Identity+ data SomeParamType = forall t. (T.ParameterScope t) =>   SomeParamType (T.ParamNotes t) @@ -108,16 +118,29 @@ -- | Typechecking mode that tells the type checker whether it is typechecking -- contract code in actual contract, lambda, or test. data TypeCheckMode-  = TypeCheckValue (U.Value, T.T)+  = TypeCheckValue+    -- ^ We're typechecking a value.+      (U.Value, T.T)+      (Maybe BigMapFinder)+      -- ^ When this is a `Just`, we simulate the typechecking behavior of the RPC's @/run_code@ endpoint.+      --+      -- If an integer is found where a big_map is expected,+      -- we use 'BigMapFinder' to check if a big_map exists with that ID.+      -- If it does, and if the big_map's value and key have the expected types, we replace the+      -- big_map ID with the corresponding big_map value.   | TypeCheckContract SomeParamType+    -- ^ We're typechecking a contract.   | TypeCheckTest+    -- ^ We're typechecking a set of instructions in a "test" environment like a REPL,+    -- where the instruction @SELF@ would not make sense.  -- | The typechecking state data TypeCheckEnv = TypeCheckEnv-  { tcExtFrames :: ~TcExtFrames-  , tcMode :: ~TypeCheckMode+  { tcMode :: ~TypeCheckMode   } +type BigMapFinder = Natural -> Maybe SomeVBigMap+ data TypeCheckOptions = TypeCheckOptions   { tcVerbose :: Bool     -- ^ Whether to add stack type comments after every@@ -139,11 +162,16 @@ instance Default TypeCheckOptions where   def = TypeCheckOptions{ tcVerbose = False, tcStrict = True } +data TypeCheckInstrEnv = TypeCheckInstrEnv+  { _tcieErrorPos :: ErrorSrcPos+  , _tcieNotInView :: Maybe (Dict T.IsNotInView)+  }+ makeLensesWith postfixLFields ''TypeCheckEnv+makeLenses ''TypeCheckInstrEnv  runTypeCheck :: TypeCheckMode -> TypeCheck a -> TypeCheckResult a-runTypeCheck mode =-  mapReaderT $ mapExceptT $ evaluatingStateT (TypeCheckEnv [] mode)+runTypeCheck = usingReaderT . TypeCheckEnv  -- | Run type checker as if it worked isolated from other world - -- no access to environment of the current contract is allowed.@@ -153,65 +181,35 @@ -- whatever we typecheck does not depend on the parameter type of the -- contract which is being typechecked (because there is no contract -- that we are typechecking).-runTypeCheckIsolated :: TypeCheck a -> TypeCheckResult a+runTypeCheckIsolated :: TypeCheck (SomeInstr t) -> TypeCheckResult (SomeInstr t) runTypeCheckIsolated = runTypeCheck TypeCheckTest  typeCheckingWith :: TypeCheckOptions -> TypeCheckResult a -> Either TCError a typeCheckingWith options = runExcept . usingReaderT options -type TypeCheckInstr =-  ReaderT TypeCheckInstrEnv TypeCheck--type TypeCheckInstrNoExcept =-  ReaderT TypeCheckInstrEnv TypeCheckNoExcept--data TypeCheckInstrEnv = TypeCheckInstrEnv-  { _tcieErrorPos :: ErrorSrcPos-  , _tcieNotInView :: Maybe (Dict T.IsNotInView)-  }--makeLenses ''TypeCheckInstrEnv- instance Default TypeCheckInstrEnv where   def = TypeCheckInstrEnv def Nothing --- | Similar to 'runTypeCheckIsolated', but for 'TypeCheckInstr.'-runTypeCheckInstrIsolated :: TypeCheckInstr a -> TypeCheckResult a-runTypeCheckInstrIsolated = runTypeCheckIsolated . flip runReaderT def--liftNoExcept :: TypeCheckInstrNoExcept a -> TypeCheckInstr a-liftNoExcept action = (pure action)-                 <**> (usingReaderT <$> ask)-                 <**> (usingReaderT <$> lift ask)-                 <**> (evaluatingState <$> get)--liftNoExcept' :: TypeCheckNoExcept a -> TypeCheck a-liftNoExcept' action = (pure action)-                  <**> (usingReaderT <$> ask)-                  <**> (evaluatingState <$> get)+liftNoExcept+  :: forall m e (a :: Type). MonadMultiReaderT m Identity+  => m a+  -> ChangeMultiReaderBase m (Except e) a+liftNoExcept action = mapMultiReaderT (pure @(Except e) . runIdentity) action  throwingTCError-  :: TypeCheckInstrNoExcept (TypeCheckedSeq inp) -> TypeCheckInstr (SomeInstr inp)-throwingTCError action = liftNoExcept action-  >>= tcsEither (const throwError) (pure)--throwingTCError'-  :: TypeCheckNoExcept (TypeCheckedSeq inp) -> TypeCheck (SomeInstr inp)-throwingTCError' action = liftNoExcept' action-  >>= tcsEither (const throwError) (pure)+  :: ( MonadMultiReaderT m Identity+     , m' ~ ChangeMultiReaderBase m (Except TCError)+     , MonadError TCError m'+     )+  => m (TypeCheckedSeq inp) -> m' (SomeInstr inp)+throwingTCError action = liftNoExcept @_ @TCError action >>= tcsEither (const throwError) (pure)  tcEither   :: (TCError -> TypeCheckInstrNoExcept a) -- ^ Call this if the action throws   -> (b -> TypeCheckInstrNoExcept a) -- ^ Call this if it doesn't   -> TypeCheckInstr b -- ^ The action to perform   -> TypeCheckInstrNoExcept a -- ^ A non-throwing action-tcEither onErr onOk action = do-  res <- (pure action)-    <**> (usingReaderT <$> ask)-    <**> (usingReaderT <$> lift ask)-    <**> (pure runExceptT)-    <**> (evaluatingState <$> get)-  either onErr onOk res+tcEither onErr onOk action = either onErr onOk =<< mapMultiReaderT (pure . runExcept) action  -- | Perform a throwing action on an acquired instruction. Preserve the acquired -- result by embedding it into a type checking tree with a specified parent

@@ -8,7 +8,6 @@     , SomeInstrOut (..)     , SomeInstr (..)     , BoundVars (..)-    , TcExtFrames     , withWTPm     , unsafeWithWTP     , mapSomeContract@@ -174,9 +173,6 @@  noBoundVars :: BoundVars noBoundVars = BoundVars Map.empty Nothing---- | State for type checking @nop@-type TcExtFrames = [BoundVars]  -- | Given a type and an action that requires evidence that the type is well typed, --  generate the evidence and execute the action, or else fail with an error.

@@ -20,14 +20,13 @@ import Morley.Michelson.TypeCheck.Error (TCError(..), TCTypeError(..)) import Morley.Michelson.TypeCheck.Helpers import Morley.Michelson.TypeCheck.TypeCheck-  (SomeParamType(..), TcInstrHandler, TcOriginatedContracts, TypeCheckInstr, TypeCheckOptions(..),-  tcieErrorPos, tcieNotInView, throwingTCError) import Morley.Michelson.TypeCheck.Types-import Morley.Michelson.Typed (EpAddress(..), Notes(..), SingT(..), Value'(..))+import Morley.Michelson.Typed+  (EpAddress(..), Notes(..), SingT(..), SomeVBigMap(..), Value'(..), castM) import Morley.Michelson.Typed qualified as T import Morley.Michelson.Typed.Contract (giveNotInView) import Morley.Michelson.Untyped qualified as U-import Morley.Tezos.Address (Address(..), TxRollupL2Address(..))+import Morley.Tezos.Address import Morley.Tezos.Core import Morley.Tezos.Crypto import Morley.Tezos.Crypto.BLS12381 qualified as BLS@@ -65,225 +64,241 @@ typeCheckValImpl mOriginatedContracts tcDo uv = doTypeCheckVal (uv, sing @ty)   where     doTypeCheckVal :: forall tz. (U.Value, Sing tz) -> TypeCheckInstr (T.Value tz)-    doTypeCheckVal (uvalue, sng) = case (uvalue, sng) of-      (U.ValueInt i, STInt) -> pure $ T.VInt i-      (v@(U.ValueInt i), t@STNat)-        | i >= 0 -> pure $ VNat (fromInteger i)-        | otherwise -> tcFailedOnValue v (fromSing t) "" (Just NegativeNat)-      (v@(U.ValueInt i), t@STMutez) -> case mkMutez i of-        Right m -> pure $ VMutez m-        Left err -> tcFailedOnValue v (fromSing t) err (Just InvalidTimestamp)-      (U.ValueString s, STString) -> pure $ VString s-      (v@(U.ValueString s), t@STAddress) -> case T.parseEpAddress (unMText s) of-        Right addr -> pure $ VAddress addr-        Left err -> tcFailedOnValue v (fromSing t) "" (Just $ InvalidAddress err)-      (v@(U.ValueBytes b), t@STAddress) -> case T.parseEpAddressRaw (U.unInternalByteString b) of-        Right addr -> pure $ VAddress addr-        Left err -> tcFailedOnValue v (fromSing t) "" (Just $ InvalidAddress err)-      (v@(U.ValueString s), t@STKeyHash) -> case parseHash (unMText s)  of-        Right kHash -> pure $ VKeyHash kHash-        Left err -> tcFailedOnValue v (fromSing t) "" (Just $ InvalidKeyHash err)-      (v@(U.ValueBytes b), t@STKeyHash) ->-        case parseKeyHashRaw (U.unInternalByteString b) of+    doTypeCheckVal (uvalue, sng) = do+      typeCheckMode <- asks' tcMode+      case (uvalue, sng) of+        (U.ValueInt i, STInt) -> pure $ T.VInt i+        (v@(U.ValueInt i), t@STNat)+          | i >= 0 -> pure $ VNat (fromInteger i)+          | otherwise -> tcFailedOnValue v (fromSing t) "" (Just NegativeNat)+        (v@(U.ValueInt i), t@STMutez) -> case mkMutez i of+          Right m -> pure $ VMutez m+          Left err -> tcFailedOnValue v (fromSing t) err (Just InvalidTimestamp)++        -- If `tcBigMaps` is a `Just`, then we simulate the behavior of the RPC+        -- @/run_code@ endpoint.+        -- If a value contains a natural number where a big_map is expected,+        -- we assume that number represents a big_map ID and replace it with+        -- the corresponding big_map value (if it exists and has the expected key/value types).+        (U.ValueInt bigMapId, STBigMap {}) | TypeCheckValue _ (Just bigMapFinder) <- typeCheckMode -> do+          let bigMapMaybe = bigMapFinder =<< fromIntegralMaybe @Integer @Natural bigMapId+          case bigMapMaybe of+            Just (SomeVBigMap (bigMap@VBigMap{} :: T.Value actualT)) ->+              withSingI sng $ castM @actualT @tz bigMap $+                tcFailedOnValue uvalue (fromSing sng) "" . Just . UnexpectedBigMapType bigMapId+            Nothing ->+              tcFailedOnValue uvalue (fromSing sng) "" (Just (InvalidBigMapId bigMapId))+        (U.ValueString s, STString) -> pure $ VString s+        (v@(U.ValueString s), t@STAddress) -> case T.parseEpAddress (unMText s) of+          Right addr -> pure $ VAddress addr+          Left err -> tcFailedOnValue v (fromSing t) "" (Just $ InvalidAddress err)+        (v@(U.ValueBytes b), t@STAddress) -> case T.parseEpAddressRaw (U.unInternalByteString b) of+          Right addr -> pure $ VAddress addr+          Left err -> tcFailedOnValue v (fromSing t) "" (Just $ InvalidAddress err)+        (v@(U.ValueString s), t@STKeyHash) -> case parseHash (unMText s)  of           Right kHash -> pure $ VKeyHash kHash           Left err -> tcFailedOnValue v (fromSing t) "" (Just $ InvalidKeyHash err)-      (v@(U.ValueString s), t@STTxRollupL2Address) -> case parseHash (unMText s)  of-        Right kHash -> pure $ VTxRollupL2Address $ TxRollupL2Address kHash-        Left err -> tcFailedOnValue v (fromSing t) "" (Just $ InvalidKeyHash err)-      (v@(U.ValueBytes b), t@STTxRollupL2Address) ->-        case parseKeyHashL2Raw (U.unInternalByteString b) of+        (v@(U.ValueBytes b), t@STKeyHash) ->+          case parseKeyHashRaw (U.unInternalByteString b) of+            Right kHash -> pure $ VKeyHash kHash+            Left err -> tcFailedOnValue v (fromSing t) "" (Just $ InvalidKeyHash err)+        (v@(U.ValueString s), t@STTxRollupL2Address) -> case parseHash (unMText s)  of           Right kHash -> pure $ VTxRollupL2Address $ TxRollupL2Address kHash           Left err -> tcFailedOnValue v (fromSing t) "" (Just $ InvalidKeyHash err)-      (U.ValueInt i, STBls12381Fr) ->-        pure $ VBls12381Fr (fromIntegralOverflowing @Integer @Bls12381Fr i)-      (v@(U.ValueBytes b), t@STBls12381Fr) ->-        case BLS.fromMichelsonBytes (U.unInternalByteString b) of-          Right val -> pure $ VBls12381Fr val-          Left err -> tcFailedOnValue v (fromSing t) "" (Just $ InvalidBls12381Object err)-      (v@(U.ValueBytes b), t@STBls12381G1) ->-        case BLS.fromMichelsonBytes (U.unInternalByteString b) of-          Right val -> pure $ VBls12381G1 val-          Left err -> tcFailedOnValue v (fromSing t) "" (Just $ InvalidBls12381Object err)-      (v@(U.ValueBytes b), t@STBls12381G2) ->-        case BLS.fromMichelsonBytes (U.unInternalByteString b) of-          Right val -> pure $ VBls12381G2 val-          Left err -> tcFailedOnValue v (fromSing t) "" (Just $ InvalidBls12381Object err)-      (v@(U.ValueString s), t@STTimestamp) -> case parseTimestamp $ unMText s of-        Just tstamp -> pure $ VTimestamp tstamp-        Nothing -> tcFailedOnValue v (fromSing t) "" (Just InvalidTimestamp)-      (U.ValueInt i, STTimestamp) -> pure $ VTimestamp (timestampFromSeconds i)-      (U.ValueBytes (U.InternalByteString s), STBytes) -> pure $ VBytes s-      (U.ValueTrue, STBool) -> pure $ VBool True-      (U.ValueFalse, STBool) -> pure $ VBool False+        (v@(U.ValueBytes b), t@STTxRollupL2Address) ->+          case parseKeyHashL2Raw (U.unInternalByteString b) of+            Right kHash -> pure $ VTxRollupL2Address $ TxRollupL2Address kHash+            Left err -> tcFailedOnValue v (fromSing t) "" (Just $ InvalidKeyHash err)+        (U.ValueInt i, STBls12381Fr) ->+          pure $ VBls12381Fr (fromIntegralOverflowing @Integer @Bls12381Fr i)+        (v@(U.ValueBytes b), t@STBls12381Fr) ->+          case BLS.fromMichelsonBytes (U.unInternalByteString b) of+            Right val -> pure $ VBls12381Fr val+            Left err -> tcFailedOnValue v (fromSing t) "" (Just $ InvalidBls12381Object err)+        (v@(U.ValueBytes b), t@STBls12381G1) ->+          case BLS.fromMichelsonBytes (U.unInternalByteString b) of+            Right val -> pure $ VBls12381G1 val+            Left err -> tcFailedOnValue v (fromSing t) "" (Just $ InvalidBls12381Object err)+        (v@(U.ValueBytes b), t@STBls12381G2) ->+          case BLS.fromMichelsonBytes (U.unInternalByteString b) of+            Right val -> pure $ VBls12381G2 val+            Left err -> tcFailedOnValue v (fromSing t) "" (Just $ InvalidBls12381Object err)+        (v@(U.ValueString s), t@STTimestamp) -> case parseTimestamp $ unMText s of+          Just tstamp -> pure $ VTimestamp tstamp+          Nothing -> tcFailedOnValue v (fromSing t) "" (Just InvalidTimestamp)+        (U.ValueInt i, STTimestamp) -> pure $ VTimestamp (timestampFromSeconds i)+        (U.ValueBytes (U.InternalByteString s), STBytes) -> pure $ VBytes s+        (U.ValueTrue, STBool) -> pure $ VBool True+        (U.ValueFalse, STBool) -> pure $ VBool False -      (U.ValueString (parsePublicKey . unMText -> Right s), STKey) ->-        pure $ T.VKey s-      (U.ValueBytes (parsePublicKeyRaw . U.unInternalByteString -> Right s), STKey) ->-        pure $ VKey s+        (U.ValueString (parsePublicKey . unMText -> Right s), STKey) ->+          pure $ T.VKey s+        (U.ValueBytes (parsePublicKeyRaw . U.unInternalByteString -> Right s), STKey) ->+          pure $ VKey s -      (U.ValueString (parseSignature . unMText -> Right s), STSignature) ->-        pure $ VSignature s-      (U.ValueBytes (parseSignatureRaw . U.unInternalByteString  -> Right s), STSignature) ->-        pure $ VSignature s+        (U.ValueString (parseSignature . unMText -> Right s), STSignature) ->+          pure $ VSignature s+        (U.ValueBytes (parseSignatureRaw . U.unInternalByteString  -> Right s), STSignature) ->+          pure $ VSignature s -      (U.ValueString (parseChainId . unMText -> Right ci), STChainId) ->-        pure $ VChainId ci-      (U.ValueBytes (mkChainId . U.unInternalByteString -> Right ci), STChainId) ->-        pure $ VChainId ci+        (U.ValueString (parseChainId . unMText -> Right ci), STChainId) ->+          pure $ VChainId ci+        (U.ValueBytes (mkChainId . U.unInternalByteString -> Right ci), STChainId) ->+          pure $ VChainId ci -      (cv@(U.ValueString (T.parseEpAddress . unMText -> Right addr))-        , STContract pc) -> typecheckContractValue cv addr pc-      (cv@(U.ValueBytes (T.parseEpAddressRaw . U.unInternalByteString -> Right addr))-        , STContract pc) -> typecheckContractValue cv addr pc+        (cv@(U.ValueString (T.parseEpAddress . unMText -> Right addr))+          , STContract pc) -> typecheckContractValue cv addr pc+        (cv@(U.ValueBytes (T.parseEpAddressRaw . U.unInternalByteString -> Right addr))+          , STContract pc) -> typecheckContractValue cv addr pc -      (cv, s@(STTicket vt)) -> lift (asks tcStrict) >>= \case-        -- Note [Tickets forging]-        -- Normally, ticket values cannot be constructed manually (i.e. forged)-        -- by design, and the only valid way to make a ticket is calling-        -- @TICKET@ instruction.-        ---        -- However @tezos-client run@ adds an exception, it allows passing a-        -- manually constructed ticket value as parameter or initial storage.-        True ->-          tcFailedOnValue cv (fromSing sng)-            "ticket values cannot be forged in real operations"-            Nothing-        False -> case cv of-          U.ValuePair addrV (U.ValuePair datV amV) -> withComparable vt cv s $ do-            addrValue <- doTypeCheckVal (addrV, STAddress)-            dat <- doTypeCheckVal (datV, vt)-            amountValue <- doTypeCheckVal (amV, STNat)-            case (addrValue, amountValue) of-              (VAddress (EpAddress addr ep), VNat am) -> do-                unless (U.isDefEpName ep) $-                  tcFailedOnValue cv (fromSing sng)-                    "it is pointless to provide an address with entrypoint as a \-                    \ticketer, we do not support that"-                    Nothing-                -- ↑ Tezos allows passing addresses with entrypoint, but it is-                -- not possible to sanely work with them after that anyway,-                -- since @TICKET@ instruction (the only valid way of constructing-                -- tickets in real run) uses @SELF_ADDRESS@ result as ticketer.-                return $ VTicket addr dat am-          _ ->+        (cv, s@(STTicket vt)) -> asks' tcStrict >>= \case+          -- Note [Tickets forging]+          -- Normally, ticket values cannot be constructed manually (i.e. forged)+          -- by design, and the only valid way to make a ticket is calling+          -- @TICKET@ instruction.+          --+          -- However @tezos-client run@ adds an exception, it allows passing a+          -- manually constructed ticket value as parameter or initial storage.+          True ->             tcFailedOnValue cv (fromSing sng)-              "ticket type expects a value of type `(pair address <data> nat)`"+              "ticket values cannot be forged in real operations"               Nothing+          False -> case cv of+            U.ValuePair addrV (U.ValuePair datV amV) -> withComparable vt cv s $ do+              addrValue <- doTypeCheckVal (addrV, STAddress)+              dat <- doTypeCheckVal (datV, vt)+              amountValue <- doTypeCheckVal (amV, STNat)+              case (addrValue, amountValue) of+                (VAddress (EpAddress' addr ep), VNat am) -> do+                  unless (U.isDefEpName ep) $+                    tcFailedOnValue cv (fromSing sng)+                      "it is pointless to provide an address with entrypoint as a \+                      \ticketer, we do not support that"+                      Nothing+                  -- ↑ Tezos allows passing addresses with entrypoint, but it is+                  -- not possible to sanely work with them after that anyway,+                  -- since @TICKET@ instruction (the only valid way of constructing+                  -- tickets in real run) uses @SELF_ADDRESS@ result as ticketer.+                  pure $ VTicket addr dat am+            _ ->+              tcFailedOnValue cv (fromSing sng)+                "ticket type expects a value of type `(pair address <data> nat)`"+                Nothing -      (U.ValueUnit, STUnit) -> pure $ VUnit-      (U.ValuePair ml mr, STPair lt rt) -> do-        l <- doTypeCheckVal (ml, lt)-        r <- doTypeCheckVal (mr, rt)-        pure $ VPair (l, r)-      (U.ValueLeft ml, STOr lt rt) -> do-        l <- doTypeCheckVal (ml, lt)-        withSingI lt $ withSingI rt $ pure $ VOr (Left l)-      (U.ValueRight mr, STOr lt rt) -> do-        r <- doTypeCheckVal (mr, rt)-        withSingI lt $ withSingI rt $ pure $ VOr (Right r)-      (U.ValueSome mv, STOption op) -> do-        v <- doTypeCheckVal (mv, op)-        withSingI op $ pure $ VOption (Just v)-      (U.ValueNone, STOption op) -> do-        withSingI op $ pure $ VOption Nothing+        (U.ValueUnit, STUnit) -> pure $ VUnit+        (U.ValuePair ml mr, STPair lt rt) -> do+          l <- doTypeCheckVal (ml, lt)+          r <- doTypeCheckVal (mr, rt)+          pure $ VPair (l, r)+        (U.ValueLeft ml, STOr lt rt) -> do+          l <- doTypeCheckVal (ml, lt)+          withSingI lt $ withSingI rt $ pure $ VOr (Left l)+        (U.ValueRight mr, STOr lt rt) -> do+          r <- doTypeCheckVal (mr, rt)+          withSingI lt $ withSingI rt $ pure $ VOr (Right r)+        (U.ValueSome mv, STOption op) -> do+          v <- doTypeCheckVal (mv, op)+          withSingI op $ pure $ VOption (Just v)+        (U.ValueNone, STOption op) -> do+          withSingI op $ pure $ VOption Nothing -      (U.ValueNil, STList l) -> withSingI l $-        pure $ T.VList []+        (U.ValueNil, STList l) -> withSingI l $+          pure $ T.VList [] -      -- If ValueSeq contains at least 2 elements, it can be type checked as a-      -- right combed pair.-      (U.ValueSeq vals@(_ :| (_ : _)), STPair _ _) ->-        doTypeCheckVal (seqToRightCombedPair vals, sng)+        -- If ValueSeq contains at least 2 elements, it can be type checked as a+        -- right combed pair.+        (U.ValueSeq vals@(_ :| (_ : _)), STPair _ _) ->+          doTypeCheckVal (seqToRightCombedPair vals, sng) -      (U.ValueSeq (toList -> mels), STList l) -> do-        els <- typeCheckValsImpl (mels, l)-        withSingI l $ pure $ VList els+        (U.ValueSeq (toList -> mels), STList l) -> do+          els <- typeCheckValsImpl (mels, l)+          withSingI l $ pure $ VList els -      (U.ValueNil, STSet s) -> do-        instrPos <- view tcieErrorPos-        case T.getComparableProofS s of-          Just Dict -> withSingI s $ pure (T.VSet S.empty)-          Nothing -> throwError $ TCFailedOnValue uvalue (fromSing s) "Non comparable types are not allowed in Sets"-            instrPos (Just $ UnsupportedTypeForScope (fromSing s) T.BtNotComparable)+        (U.ValueNil, STSet s) -> do+          instrPos <- view tcieErrorPos+          case T.getComparableProofS s of+            Just Dict -> withSingI s $ pure (T.VSet S.empty)+            Nothing -> throwError $ TCFailedOnValue uvalue (fromSing s) "Non comparable types are not allowed in Sets"+              instrPos (Just $ UnsupportedTypeForScope (fromSing s) T.BtNotComparable) -      (sq@(U.ValueSeq (toList -> mels)), s@(STSet vt)) -> withComparable vt sq s $ do-        instrPos <- view tcieErrorPos+        (sq@(U.ValueSeq (toList -> mels)), s@(STSet vt)) -> withComparable vt sq s $ do+          instrPos <- view tcieErrorPos -        els <- typeCheckValsImpl (mels, vt)-        elsS <- liftEither $ S.fromDistinctAscList <$> ensureDistinctAsc id els-                  `onFirst` \msg -> TCFailedOnValue sq (fromSing vt) msg instrPos Nothing-        withSingI vt $ pure $ VSet elsS+          els <- typeCheckValsImpl (mels, vt)+          elsS <- liftEither $ S.fromDistinctAscList <$> ensureDistinctAsc id els+                    `onFirst` \msg -> TCFailedOnValue sq (fromSing vt) msg instrPos Nothing+          withSingI vt $ pure $ VSet elsS -      (v@U.ValueNil, s@(STMap st vt)) ->-        withSingI st $ withSingI vt $ withComparable st v s $ pure $ T.VMap M.empty+        (v@U.ValueNil, s@(STMap st vt)) ->+          withSingI st $ withSingI vt $ withComparable st v s $ pure $ T.VMap M.empty -      (sq@(U.ValueMap (toList -> mels)), s@(STMap kt vt)) ->-        withComparable kt sq s $ do-          keyOrderedElts <- typeCheckMapVal mels sq kt vt-          withSingI kt $ withSingI vt $-            pure $ VMap (M.fromDistinctAscList keyOrderedElts)+        (sq@(U.ValueMap (toList -> mels)), s@(STMap kt vt)) ->+          withComparable kt sq s $ do+            keyOrderedElts <- typeCheckMapVal mels sq kt vt+            withSingI kt $ withSingI vt $+              pure $ VMap (M.fromDistinctAscList keyOrderedElts) -      (v@U.ValueNil, s@(STBigMap st1 st2)) ->-        withSingI st1 $ withSingI st2 $ withComparable st1 v s $ withBigMapAbsence st2 v s $-          pure $ VBigMap Nothing M.empty+        (v@U.ValueNil, s@(STBigMap st1 st2)) ->+          withSingI st1 $ withSingI st2 $ withComparable st1 v s $ withBigMapAbsence st2 v s $+            pure $ VBigMap Nothing M.empty -      (sq@(U.ValueMap (toList -> mels)), s@(STBigMap kt vt)) ->-        withComparable kt sq s $ withBigMapAbsence vt sq s $ do-          keyOrderedElts <- typeCheckMapVal mels sq kt vt-          withSingI kt $ withSingI vt $-            pure $ VBigMap Nothing (M.fromDistinctAscList keyOrderedElts)+        (sq@(U.ValueMap (toList -> mels)), s@(STBigMap kt vt)) ->+          withComparable kt sq s $ withBigMapAbsence vt sq s $ do+            keyOrderedElts <- typeCheckMapVal mels sq kt vt+            withSingI kt $ withSingI vt $+              pure $ VBigMap Nothing (M.fromDistinctAscList keyOrderedElts) -      -- `{ {} }` can be typechecked either as `VLam` or `VList`.-      (U.ValueLambda s, STList l) ->-        case emptyLambdaAsList s of-          Just xs -> doTypeCheckVal (xs, sng)-          Nothing -> tcFailedOnValue uvalue (fromSing l) "" Nothing+        -- `{ {} }` can be typechecked either as `VLam` or `VList`.+        (U.ValueLambda s, STList l) ->+          case emptyLambdaAsList s of+            Just xs -> doTypeCheckVal (xs, sng)+            Nothing -> tcFailedOnValue uvalue (fromSing l) "" Nothing -      (U.ValueSeq s, STLambda _ _) -> case emptyListAsLambda s of-        Just xs -> doTypeCheckVal (xs, sng)-        Nothing -> tcFailedOnValue uvalue (fromSing sng) "" Nothing+        (U.ValueSeq s, STLambda _ _) -> case emptyListAsLambda s of+          Just xs -> doTypeCheckVal (xs, sng)+          Nothing -> tcFailedOnValue uvalue (fromSing sng) "" Nothing -      (v, STLambda (var :: Sing it) (b :: Sing ot)) -> withSingI var $ withSingI b $ do-        mp <- case v of-          U.ValueNil       -> pure []-          U.ValueLambda mp -> pure $ toList mp-          _ -> tcFailedOnValue v (demote @ty) "unexpected value" Nothing-        _ :/ instr <--          withWTP @it uvalue $ throwingTCError $-            typeCheckImpl-              -- lambdas can contain operations forbidden inside views, hence-              -- we invent a "not in view" constraint here.-              (giveNotInView $ local (set tcieNotInView $ Just Dict) ... tcDo)-              mp-              ((sing @it, Dict) ::& SNil)-        case instr of-          lam ::: (lo :: HST lo) -> withWTP @ot uvalue $ do-            case eqHST1 @ot lo of-              Right Refl -> do-                pure $ T.mkVLam (T.RfNormal lam)-              Left m ->-                tcFailedOnValue v (demote @ty)-                        "wrong output type of lambda's value:" (Just m)-          AnyOutInstr lam ->-            pure $ T.mkVLam (T.RfAlwaysFails lam)+        (v, STLambda (var :: Sing it) (b :: Sing ot)) -> withSingI var $ withSingI b $ do+          mp <- case v of+            U.ValueNil       -> pure []+            U.ValueLambda mp -> pure $ toList mp+            _ -> tcFailedOnValue v (demote @ty) "unexpected value" Nothing+          _ :/ instr <-+            withWTP @it uvalue $ throwingTCError $+              typeCheckImpl+                -- lambdas can contain operations forbidden inside views, hence+                -- we invent a "not in view" constraint here.+                (giveNotInView $ local (set tcieNotInView $ Just Dict) ... tcDo)+                mp+                ((sing @it, Dict) ::& SNil)+          case instr of+            lam ::: (lo :: HST lo) -> withWTP @ot uvalue $ do+              case eqHST1 @ot lo of+                Right Refl -> do+                  pure $ T.mkVLam (T.RfNormal lam)+                Left m ->+                  tcFailedOnValue v (demote @ty)+                          "wrong output type of lambda's value:" (Just m)+            AnyOutInstr lam ->+              pure $ T.mkVLam (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)), 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@(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@(STSaplingState _)) -> tcFailedOnValue v (fromSing t)-        "sapling_state is not supported" Nothing+        (v, t@(STSaplingState _)) -> tcFailedOnValue v (fromSing t)+          "sapling_state is not supported" Nothing -      (v, t@(STSaplingTransaction _)) -> tcFailedOnValue v (fromSing t)-        "sapling_transaction is not supported" Nothing+        (v, t@(STSaplingTransaction _)) -> tcFailedOnValue v (fromSing t)+          "sapling_transaction is not supported" Nothing -      (v, t) -> tcFailedOnValue v (fromSing t) "unknown value" Nothing+        (v, t) -> tcFailedOnValue v (fromSing t) "unknown value" Nothing      seqToRightCombedPair :: (NonEmpty $ U.Value) -> U.Value     seqToRightCombedPair (x :| [y]) = U.ValuePair x y@@ -364,9 +379,9 @@             "Unsupported type in type argument of 'contract' type" instrPos $               Just $ UnsupportedTypeForScope (fromSing pc) reason       case addr of-        KeyAddress _ -> do+        ImplicitAddress _ -> do           Refl <- ensureTypeMatches @'T.TUnit-          pure $ VContract addr T.sepcPrimitive+          pure $ VContract (MkAddress addr) T.sepcPrimitive         ContractAddress ca -> case mOriginatedContracts of           Nothing -> liftEither . Left $ unsupportedType T.BtHasContract           Just originatedContracts -> case M.lookup ca originatedContracts of@@ -378,13 +393,13 @@                   EntrypointNotFound epName                 Just (T.MkEntrypointCallRes (_ :: Notes t') epc) -> do                   Refl <- ensureTypeMatches @t'-                  pure $ VContract addr (T.SomeEpc epc)+                  pure $ VContract (MkAddress addr) (T.SomeEpc epc)             Nothing ->               throwError $ TCFailedOnValue cv (demote @ty) "Contract literal unknown"                 instrPos (Just $ UnknownContract addr)-        TransactionRollupAddress _ ->+        TxRollupAddress _ ->           throwError $ TCFailedOnValue cv (demote @ty) "txr1 address passed as contract"-                instrPos (Just $ UnknownContract addr)+                instrPos (Just $ TxRollupContract addr)  withComparable   :: forall a (t :: T.T) ty. Sing a

@@ -48,7 +48,7 @@ import Morley.Michelson.Typed.View import Morley.Michelson.Untyped qualified as U import Morley.Michelson.Untyped.Annotation (Annotation(unAnnotation))-import Morley.Tezos.Address hiding (ta)+import Morley.Tezos.Address import Morley.Tezos.Core   (ChainId(unChainId), mformatChainId, parseChainId, timestampFromSeconds, timestampToSeconds, tz,   unMutez)@@ -204,15 +204,15 @@   (VContract addr sepc, _) ->     case opts of       Readable  ->-        U.ValueString . mformatEpAddress $ EpAddress addr (sepcName sepc)+        U.ValueString . mformatEpAddress $ EpAddress' addr (sepcName sepc)       _         -> U.ValueBytes . U.InternalByteString . encodeEpAddress $-        EpAddress addr (sepcName sepc)+        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 ->-        let us = untypeValueImpl opts STAddress $ VAddress (EpAddress s DefEpName)+        let us = untypeValueImpl opts STAddress $ VAddress (EpAddress' s DefEpName)             uv = untypeValueImpl opts vt v             ua = untypeValueImpl opts STNat $ VNat a         in case opts of@@ -277,13 +277,13 @@     encodeEpAddress (EpAddress addr epName) =       encodeAddress addr <> encodeEpName epName -    encodeAddress :: Address -> ByteString+    encodeAddress :: KindedAddress kind -> ByteString     encodeAddress = \case-      KeyAddress keyHash ->+      ImplicitAddress keyHash ->         "\x00" <> hashToBytes keyHash       ContractAddress hash ->         "\x01" <> hashToBytes hash <> "\x00"-      TransactionRollupAddress hash ->+      TxRollupAddress hash ->         "\x02" <> hashToBytes hash <> "\x00"      encodeEpName :: EpName -> ByteString@@ -470,6 +470,7 @@         annotateInstr ann U.SAPLING_EMPTY_STATE (singPeanoVal s)       AnnSAPLING_VERIFY_UPDATE ann -> annotateInstr ann U.SAPLING_VERIFY_UPDATE       AnnMIN_BLOCK_TIME ann -> U.MIN_BLOCK_TIME ann+      AnnEMIT va tag ty -> annotateInstr va U.EMIT tag $ mkUType <$> ty  untypeStackRef :: StackRef s -> U.StackRef untypeStackRef (StackRef n) = U.StackRef (fromPeanoNatural n)@@ -582,7 +583,7 @@       dat <- sampleTypedValue t       VNat amount <- sampleTypedValue STNat       case cmpProof of-        Dict -> return $ VTicket (eaAddress sampleAddress) dat amount+        Dict -> return $ VTicket (MkAddress sampleCTAddress) dat amount     STPair t1 t2 -> withSingI t1 $ withSingI t2 $ do       val1 <- sampleTypedValue t1       val2 <- sampleTypedValue t2@@ -610,7 +611,8 @@           pure $ mkVLam $ RfNormal (DROP `Seq` PUSH val)         _ -> pure $ mkVLam $ RfAlwaysFails (PUSH (VString [mt|lambda sample|]) `Seq` FAILWITH)     where-      sampleAddress = (unsafe . parseEpAddress) "KT1AEseqMV6fk2vtvQCVyA7ZCaxv7cpxtXdB"+      sampleCTAddress = [ta|KT1AEseqMV6fk2vtvQCVyA7ZCaxv7cpxtXdB|]+      sampleAddress = unsafe . parseEpAddress $ formatAddress sampleCTAddress       samplePublicKey = fromRight (error "impossible") $ parsePublicKey         "edpkuwTWKgQNnhR5v17H2DYHbfcxYepARyrPGbf1tbMoGQAj8Ljr3V"       sampleSignature = fromRight (error "impossible") $ parseSignature@@ -645,7 +647,7 @@     (VTicket s v a, STTicket tv) -> renderDocSing       needsParens       OpPresent-      (VPair (VAddress (EpAddress s DefEpName), VPair (v, VNat a))+      (VPair (VAddress (EpAddress' s DefEpName), VPair (v, VNat a))         , STPair STAddress (STPair tv STNat))     val@(VPair (_, (VPair (_, _))), _) ->       U.renderValuesList id $ renderLinearizedRightCombValuePair val

@@ -3,7 +3,7 @@  -- | Utilities for lightweight entrypoints support. module Morley.Michelson.Typed.Entrypoints-  ( EpAddress (..)+  ( EpAddress (.., EpAddress)   , ParseEpAddressError (..)   , formatEpAddress   , mformatEpAddress@@ -72,13 +72,18 @@ ----------------------------------------------------------------------------  -- | Address with optional entrypoint name attached to it.-data EpAddress = EpAddress+data EpAddress = EpAddress'   { eaAddress :: Address     -- ^ Address itself   , eaEntrypoint :: EpName     -- ^ Entrypoint name (might be empty)   } deriving stock (Show, Eq, Ord, Generic) +pattern EpAddress :: KindedAddress kind -> EpName -> EpAddress+pattern EpAddress addr name = EpAddress' (MkAddress addr) name++{-# COMPLETE EpAddress #-}+ instance Buildable EpAddress where   build = build . formatEpAddress @@ -130,14 +135,14 @@   in case mannotTxt of     "" -> do       addr <- first ParseEpAddressBadAddress $ parseAddress addrTxt-      return $ EpAddress addr DefEpName+      return $ EpAddress' addr DefEpName     annotTxt' -> do       addr <- first ParseEpAddressBadAddress $ parseAddress addrTxt       annot <- first ParseEpAddressBadRefAnn $ case T.stripPrefix "%" annotTxt' of         Nothing -> error "impossible"         Just a -> mkAnnotation a       epName <- first ParseEpAddressRefAnnError $ epNameFromRefAnn annot-      return $ EpAddress addr epName+      return $ EpAddress' addr epName  -- | Parses byte representation of entrypoint address. --@@ -162,7 +167,7 @@   decodedEntrypoint <- first (ParseEpAddressBadEntryopint raw) $ decodeUtf8' eps   decodedAnnotation <- first ParseEpAddressBadRefAnn $ mkAnnotation decodedEntrypoint   eaEntrypoint <- first ParseEpAddressRefAnnError $ epNameFromRefAnn decodedAnnotation-  pure $ EpAddress {..}+  pure $ EpAddress' {..}  -- ParamNotes ----------------------------------------------------------------------------

@@ -14,6 +14,7 @@   , SomeContract (..)   , SomeContractAndStorage (..)   , SomeIsoValue (..)+  , SomeVBigMap(..)   ) where  import Fmt (Buildable(..))@@ -96,3 +97,6 @@        -> SomeContractAndStorage  deriving stock instance Show SomeContractAndStorage++data SomeVBigMap where+  SomeVBigMap :: forall k v. Value ('TBigMap k v) -> SomeVBigMap

@@ -759,6 +759,12 @@     |]   typeDocDependencies _ = []   typeDocHaskellRep _ _ = Nothing+  typeDocMichelsonRep _ = (Nothing, TKeyHash)+  typeDocMdReference tp _ =+    customTypeDocMdReference+      (typeDocName tp, DType tp)+      []+      (WithinParens False)  instance TypeHasDoc EpAddress where   typeDocName _ = "EntrypointAddress"

@@ -2,7 +2,6 @@ -- SPDX-License-Identifier: LicenseRef-MIT-OA  {-# OPTIONS_GHC -Wno-redundant-constraints #-}-{-# LANGUAGE InstanceSigs #-}  -- | Instructions working on product types derived from Haskell ones. module Morley.Michelson.Typed.Haskell.Instr.Product

@@ -10,10 +10,12 @@   ) where  import Data.Singletons (Demote)-import Data.Type.Bool (If, type (||))+import Data.Type.Bool (type (||)) import GHC.Generics qualified as G import GHC.TypeLits (ErrorMessage(..), Symbol, TypeError) +import Morley.Util.Type (FailUnless, FailUnlessElse)+ -- | Description of constructors and fields of some datatype. -- -- This type is just two nested maps represented as associative lists. It is supposed to@@ -85,24 +87,21 @@ -- otherwise. type family HasAllFields (conName :: Symbol) (fields :: [(Symbol, Symbol)]) (typ :: Type) :: Constraint where   HasAllFields conName fields typ =-    If+    FailUnlessElse       (HasConstructor conName (G.Rep typ))-      (HasAllFieldsImpl conName fields typ)-      (TypeError-        ('Text "No constructor " ':<>: 'ShowType conName ':<>: 'Text " in type " ':<>: 'ShowType typ ':<>: 'Text "." )+      ('Text "No constructor " ':<>: 'ShowType conName ':<>:+      'Text " in type " ':<>: 'ShowType typ ':<>: 'Text "."       )+      (HasAllFieldsImpl conName fields typ)  -- | Actual recursive implementation of 'HasAllFields'. type family HasAllFieldsImpl (conName :: Symbol) (fields :: [(Symbol, Symbol)]) (typ :: Type) :: Constraint where   HasAllFieldsImpl _ '[] _ = ()   HasAllFieldsImpl conName ( '(fieldName, _) ': rest ) typ =-    ( If+    ( FailUnless         (HasField conName fieldName (G.Rep typ))-        (() :: Constraint)-        (TypeError-          ('Text "No field " ':<>: 'ShowType fieldName ':<>: 'Text " in constructor " ':<>:-           'ShowType conName ':<>: 'Text " of type " ':<>: 'ShowType typ ':<>: 'Text "."-          )+        ('Text "No field " ':<>: 'ShowType fieldName ':<>: 'Text " in constructor " ':<>:+        'ShowType conName ':<>: 'Text " of type " ':<>: 'ShowType typ ':<>: 'Text "."         )     , HasAllFieldsImpl conName rest typ     )

@@ -12,7 +12,6 @@   , GIsoValue (GValueType)   , ToT'   , GenericIsoValue-  , WellTypedIsoValue   , WellTypedToT   , HasNoOpToT @@ -56,7 +55,7 @@ import Morley.Michelson.Typed.Scope import Morley.Michelson.Typed.T import Morley.Michelson.Typed.Value-import Morley.Tezos.Address (Address, TxRollupL2Address)+import Morley.Tezos.Address import Morley.Tezos.Core (ChainId, Mutez, Timestamp) import Morley.Tezos.Crypto   (Bls12381Fr, Bls12381G1, Bls12381G2, Chest, ChestKey, KeyHash, PublicKey, Signature)@@ -68,7 +67,7 @@ -- Complex values isomorphism ---------------------------------------------------------------------------- -type KnownIsoT a = SingI (ToT a)+type KnownIsoT a = (IsoValue a, SingI (ToT a))  -- | Isomorphism between Michelson values and plain Haskell types. --@@ -173,7 +172,7 @@  instance IsoValue Address where   type ToT Address = 'TAddress-  toVal addr = VAddress $ EpAddress addr DefEpName+  toVal addr = VAddress $ EpAddress' addr DefEpName   fromVal (VAddress x) = eaAddress x  instance IsoValue EpAddress where@@ -272,11 +271,9 @@  type SomeEntrypointCall arg = SomeEntrypointCallT (ToT arg) -type WellTypedToT a = WellTyped (ToT a)-type WellTypedIsoValue a = (WellTyped (ToT a), IsoValue a)--type HasNoOpToT a = HasNoOp (ToT a)-type HasNoBigMapToT a = HasNoBigMap (ToT a)+type WellTypedToT a = (IsoValue a, WellTyped (ToT a))+type HasNoOpToT a = (IsoValue a, HasNoOp (ToT a))+type HasNoBigMapToT a = (IsoValue a, HasNoBigMap (ToT a))  -- | Since @Contract@ name is used to designate contract code, lets call -- analogy of 'TContract' type as follows.@@ -303,7 +300,7 @@ coerceContractRef ContractRef{..} = ContractRef{..}  contractRefToAddr :: ContractRef cp -> EpAddress-contractRefToAddr ContractRef{..} = EpAddress crAddress (sepcName crEntrypoint)+contractRefToAddr ContractRef{..} = EpAddress' crAddress (sepcName crEntrypoint)  -- | Ticket type. data Ticket (arg :: Type) = Ticket

@@ -98,6 +98,7 @@           , SAPLING_EMPTY_STATE           , SAPLING_VERIFY_UPDATE           , MIN_BLOCK_TIME+          , EMIT           )   , castInstr   , pattern (:#)@@ -159,8 +160,8 @@ import Morley.Util.PeanoNatural import Morley.Util.Sing (eqI) import Morley.Util.TH-import Morley.Util.Type (If, KnownList, type (++))-import Morley.Util.TypeLits (ErrorMessage(ShowType, Text, (:$$:), (:<>:)), TypeErrorUnless)+import Morley.Util.Type (FailUnless, If, KnownList, type (++))+import Morley.Util.TypeLits (ErrorMessage(ShowType, Text, (:$$:), (:<>:)))  {-# ANN module ("HLint: ignore Language.Haskell.TH should be imported post-qualified or with an explicit import list" :: Text) #-} @@ -217,7 +218,7 @@  type ConstraintPairN (n :: Peano) (inp :: [T]) =   ( RequireLongerOrSameLength inp n-  , TypeErrorUnless (n >= ToPeano 2) ('Text "'PAIR n' expects n ≥ 2")+  , FailUnless (n >= ToPeano 2) ('Text "'PAIR n' expects n ≥ 2")   )  type PairN (n :: Peano) (s :: [T]) = (RightComb (Take n s) ': Drop n s)@@ -232,10 +233,10 @@   RightComb (x ': xs) = 'TPair x (RightComb xs)  type ConstraintUnpairN (n :: Peano) (pair :: T) =-  ( TypeErrorUnless (n >= ToPeano 2)+  ( FailUnless (n >= ToPeano 2)       ('Text "'UNPAIR n' expects n ≥ 2") -  , TypeErrorUnless (CombedPairLeafCountIsAtLeast n pair)+  , FailUnless (CombedPairLeafCountIsAtLeast n pair)       (If (IsPair pair)         ('Text "'UNPAIR "           ':<>: 'ShowType (FromPeano n)@@ -265,7 +266,7 @@   UnpairN ('S n)       ('TPair x y) = x : UnpairN n y  type ConstraintGetN (ix :: Peano) (pair :: T) =-  ( TypeErrorUnless (CombedPairNodeIndexIsValid ix pair)+  ( FailUnless (CombedPairNodeIndexIsValid ix pair)       (If (IsPair pair)         ('Text "'GET "           ':<>: 'ShowType (FromPeano ix)@@ -288,7 +289,7 @@   GetN ('S ('S n)) ('TPair _ right) = GetN n right  type ConstraintUpdateN (ix :: Peano) (pair :: T) =-  ( TypeErrorUnless (CombedPairNodeIndexIsValid ix pair)+  ( FailUnless (CombedPairNodeIndexIsValid ix pair)       (If (IsPair pair)         ('Text "'UPDATE "           ':<>: 'ShowType (FromPeano ix)@@ -810,6 +811,12 @@     -> Instr ('TSaplingTransaction n : 'TSaplingState n ': s)              ('TOption ('TPair 'TBytes ('TPair 'TInt ('TSaplingState n))) ': s)   AnnMIN_BLOCK_TIME :: [AnyAnn] -> Instr s ('TNat ': s)+  AnnEMIT+    :: PackedValScope t+    => AnnVar+    -> FieldAnn+    -> Maybe (Notes t)+    -> Instr (t ': s) ('TOperation : s)  castInstr   :: forall inp1 out1 inp2 out2.

@@ -6,6 +6,7 @@   , OriginationOperation (..)   , TransferOperation (..)   , SetDelegateOperation (..)+  , EmitOperation (..)   , mkContractAddress   , mkOriginationOperationHash   , mkTransferOperationHash@@ -16,15 +17,15 @@ import Data.ByteString.Lazy qualified as BSL  import Morley.Michelson.Interpret.Pack (toBinary, toBinary')-import Morley.Michelson.Runtime.TxData (TxData(..))-import Morley.Michelson.Typed (EpName, unContractCode)+import Morley.Michelson.Runtime.TxData (TxData)+import Morley.Michelson.Typed (Emit, EpName(..), Instr, unContractCode) 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.Scope (ParameterScope, StorageScope)-import Morley.Tezos.Address (Address(ContractAddress), GlobalCounter(..))-import Morley.Tezos.Address.Alias (Alias)+import Morley.Michelson.Typed.Scope (PackedValScope, ParameterScope, StorageScope)+import Morley.Tezos.Address+import Morley.Tezos.Address.Alias import Morley.Tezos.Core (Mutez(..)) import Morley.Tezos.Crypto (Hash(..), HashTag(..), KeyHash, blake2b, blake2b160) @@ -47,10 +48,10 @@  -- | Data necessary to originate a contract. data OriginationOperation =-  forall cp st.-  (StorageScope st, ParameterScope cp) =>+  forall cp st kind.+  (StorageScope st, ParameterScope cp, L1AddressKind kind) =>   OriginationOperation-  { ooOriginator :: Address+  { ooOriginator :: KindedAddress kind   -- ^ Originator of the contract.   , ooDelegate :: Maybe KeyHash   -- ^ Optional delegate.@@ -64,7 +65,7 @@   -- ^ The value of the global counter at the time the operation was created.   -- We store it here so that the resulting addresses of @CREATE_CONTRACT@ and   -- performing of origination operation are the same.-  , ooAlias :: Maybe Alias+  , ooAlias :: Maybe ContractAlias   -- ^ An alias to be associated with the originated contract's address.    -- In Tezos each operation also has a special field called @counter@, see here:@@ -112,7 +113,7 @@ mkContractAddress   :: OperationHash   -> GlobalCounter-  -> Address+  -> ContractAddress mkContractAddress (OperationHash opHash) (GlobalCounter counter) =   ContractAddress   $ Hash HashContract@@ -133,7 +134,7 @@  mkTransferOperationHash   :: ParameterScope t-  => Address+  => KindedAddress kind   -> Value t   -> EpName   -> Mutez@@ -157,7 +158,7 @@  -- | Set contract's delegate data SetDelegateOperation = SetDelegateOperation-  { sdoContract :: Address+  { sdoContract :: ContractAddress   -- ^ The contract we're setting delegate of   , sdoDelegate :: Maybe KeyHash   -- ^ The delegate we're setting@@ -173,3 +174,10 @@     --     -- https://gitlab.com/tezos/tezos/-/blob/685227895f48a2564a9de3e1e179e7cd741d52fb/src/proto_010_PtGRANAD/lib_protocol/operation_repr.ml#L354     packedOperation = packMaybe (toBinary' . toVal) sdoDelegate++data EmitOperation = forall t. PackedValScope t => EmitOperation+  { eoSource :: ContractAddress+  , eoEmit :: Emit Instr t+  }++deriving stock instance Show EmitOperation

@@ -132,15 +132,19 @@   , SingI (..)   ) where +import Data.Bool.Singletons (SBool(..)) import Data.Constraint (Dict(..), withDict, (:-)(..), (\\))-import Data.Singletons (Sing, SingI(..), fromSing, withSingI)+import Data.Singletons+  (SLambda(..), Sing, SingI(..), fromSing, type (@@), type (~>), type Apply, withSingI, (@@)) import Data.Type.Bool (Not, type (&&), type (||)) import Fmt (Buildable(..)) import GHC.TypeLits (ErrorMessage(..), TypeError) +import Data.Type.Equality ((:~:)(..)) import Morley.Michelson.Printer.Util (RenderDoc(..), buildRenderDoc) import Morley.Michelson.Typed.Sing (SingT(..)) import Morley.Michelson.Typed.T (T(..))+import Unsafe.Coerce (unsafeCoerce)  ---------------------------------------------------------------------------- -- Constraints@@ -1031,62 +1035,114 @@ -- -- Because of the De Morgan laws @not (a or b)@ implies @(not a) and (not b)@ -- or in our case: @pair@ does not contain @x@ -> @a@ and @b@ don't contain @x@.------ GHC is however not able to prove this, so we need to use another (impossible)--- 'error' to forcefully "prove" the two scopes. class WithDeMorganScope (c :: T -> Constraint) t a b where   withDeMorganScope :: c (t a b) => ((c a, c b) => ret) -> ret --- | Helper to build a 'WithDeMorganScope' by using a 'CheckScope' that we know--- cannot fail.-mkWithDeMorgan-  :: forall scope a b ret. (CheckScope (scope a), CheckScope (scope b))-  => ((scope a, scope b) => ret) -> ret-mkWithDeMorgan f = fromRight (error "impossible") $ do-  Dict <- checkScope @(scope a)-  Dict <- checkScope @(scope b)-  pure f+-- | Produce evidence that the first argument of a disjunction+-- is false if the whole disjunction is false.+orL :: forall a b. (a || b) ~ 'False => Sing a -> a :~: 'False+orL SFalse = Refl+{-# NOINLINE [1] orL #-} -instance (SingI a, SingI b) => WithDeMorganScope HasNoOp 'TPair a b where-  withDeMorganScope = mkWithDeMorgan @HasNoOp @a @b+-- This rule is *slightly* illegitimate, because the right hand side is lazier+-- than the left hand side. In context, this is fine, and we really *want* to+-- do it so we have at least some hope of avoiding building singletons that we+-- don't end up using. We'd get a totally legitimate rule if we used a SingI+-- constraint instead of a Sing argument, but then we'd need to use withSingI,+-- which for some reason doesn't use the newfangled GHC machinery for such and+-- therefore risks gumming up optimization. Of course, we could roll our own+-- withSingI, but that's very hairy and GHC version dependent (the+-- never-really-documented magicDict was recently replaced by withDict, which+-- is documented in ... the type checker source code, apparently).+{-# RULES+"orL" forall s. orL s = unsafeCoerce Refl+ #-} -instance (SingI a, SingI b) => WithDeMorganScope HasNoContract 'TPair a b where-  withDeMorganScope = mkWithDeMorgan @HasNoContract @a @b+-- | When a class looks like+--+-- @+-- class (SomeTypeFamily t ~ 'False, ...) => TheClass t+-- instance (SomeTypeFamily t ~ 'False, ...) => TheClass t+-- @+--+-- and the additional constraints are satisfied by the instance constraints of+-- the 'WithDeMorganScope' instance for @TheClass@, we can use+-- `simpleWithDeMorgan` to define 'withDeMorganScope' for the instance.+simpleWithDeMorgan+  :: forall sym a b ret.+     ((sym @@ a || sym @@ b) ~ 'False, SingI sym, SingI a)+  => (((sym @@ a) ~ 'False, (sym @@ b) ~ 'False) => ret) -> ret+-- Note: If the "orL" rule fires (which it should), we won't actually calculate+-- the (likely recursive) `sing @sym @@ sing @a` at all. If we're lucky, GHC+-- might not build the `SingI a` dictionary either.+simpleWithDeMorgan f+  | Refl <- orL @(sym @@ a) @(sym @@ b) (sing @sym @@ sing @a)+  = f -instance (SingI a, SingI b) => WithDeMorganScope HasNoTicket 'TPair a b where-  withDeMorganScope = mkWithDeMorgan @HasNoTicket @a @b+data ContainsOpSym :: T ~> Bool+type instance Apply ContainsOpSym x = ContainsOp x+instance SingI ContainsOpSym where+  sing = SLambda $ \t -> case checkOpPresence t of+    OpPresent -> STrue+    OpAbsent -> SFalse+instance SingI a => WithDeMorganScope HasNoOp 'TPair a b where+  withDeMorganScope f = simpleWithDeMorgan @ContainsOpSym @a @b f+instance SingI a => WithDeMorganScope HasNoOp 'TOr a b where+  withDeMorganScope f = simpleWithDeMorgan @ContainsOpSym @a @b f+instance SingI k => WithDeMorganScope HasNoOp 'TMap k v where+  withDeMorganScope f = simpleWithDeMorgan @ContainsOpSym @k @v f+instance SingI k => WithDeMorganScope HasNoOp 'TBigMap k v where+  withDeMorganScope f = simpleWithDeMorgan @ContainsOpSym @k @v f -instance (SingI a, SingI b) => WithDeMorganScope HasNoBigMap 'TPair a b where-  withDeMorganScope = mkWithDeMorgan @HasNoBigMap @a @b+data ContainsContractSym :: T ~> Bool+type instance Apply ContainsContractSym x = ContainsContract x+instance SingI ContainsContractSym where+  sing = SLambda $ \t -> case checkContractTypePresence t of+    ContractPresent -> STrue+    ContractAbsent -> SFalse+instance SingI a => WithDeMorganScope HasNoContract 'TPair a b where+  withDeMorganScope f = simpleWithDeMorgan @ContainsContractSym @a @b f+instance SingI a => WithDeMorganScope HasNoContract 'TOr a b where+  withDeMorganScope f = simpleWithDeMorgan @ContainsContractSym @a @b f -instance (SingI a, SingI b) => WithDeMorganScope HasNoNestedBigMaps 'TPair a b where-  withDeMorganScope = mkWithDeMorgan @HasNoNestedBigMaps @a @b+data ContainsTicketSym :: T ~> Bool+type instance Apply ContainsTicketSym x = ContainsTicket x+instance SingI ContainsTicketSym where+  sing = SLambda $ \t -> case checkTicketPresence t of+    TicketPresent -> STrue+    TicketAbsent -> SFalse+instance SingI a => WithDeMorganScope HasNoTicket 'TPair a b where+  withDeMorganScope f = simpleWithDeMorgan @ContainsTicketSym @a @b f+instance SingI a => WithDeMorganScope HasNoTicket 'TOr a b where+  withDeMorganScope f = simpleWithDeMorgan @ContainsTicketSym @a @b f -instance (SingI a, SingI b) => WithDeMorganScope HasNoOp 'TOr a b where-  withDeMorganScope = mkWithDeMorgan @HasNoOp @a @b+data ContainsBigMapSym :: T ~> Bool+type instance Apply ContainsBigMapSym x = ContainsBigMap x+instance SingI ContainsBigMapSym where+  sing = SLambda $ \t -> case checkBigMapPresence t of+    BigMapPresent -> STrue+    BigMapAbsent -> SFalse+instance SingI a => WithDeMorganScope HasNoBigMap 'TPair a b where+  withDeMorganScope f = simpleWithDeMorgan @ContainsBigMapSym @a @b f+instance SingI a => WithDeMorganScope HasNoBigMap 'TOr a b where+  withDeMorganScope f = simpleWithDeMorgan @ContainsBigMapSym @a @b f -instance (SingI a, SingI b) => WithDeMorganScope HasNoContract 'TOr a b where-  withDeMorganScope = mkWithDeMorgan @HasNoContract @a @b+data ContainsNestedBigMapsSym :: T ~> Bool+type instance Apply ContainsNestedBigMapsSym x = ContainsNestedBigMaps x+instance SingI ContainsNestedBigMapsSym where+  sing = SLambda $ \t -> case checkNestedBigMapsPresence t of+    NestedBigMapsPresent -> STrue+    NestedBigMapsAbsent -> SFalse+instance SingI a => WithDeMorganScope HasNoNestedBigMaps 'TPair a b where+  withDeMorganScope f = simpleWithDeMorgan @ContainsNestedBigMapsSym @a @b f+instance SingI a => WithDeMorganScope HasNoNestedBigMaps 'TOr a b where+  withDeMorganScope f = simpleWithDeMorgan @ContainsNestedBigMapsSym @a @b f -instance (SingI a, SingI b) => WithDeMorganScope HasNoTicket 'TOr a b where-  withDeMorganScope = mkWithDeMorgan @HasNoTicket @a @b -instance (SingI a, SingI b) => WithDeMorganScope HasNoBigMap 'TOr a b where-  withDeMorganScope = mkWithDeMorgan @HasNoBigMap @a @b -instance (SingI a, SingI b) => WithDeMorganScope HasNoNestedBigMaps 'TOr a b where-  withDeMorganScope = mkWithDeMorgan @HasNoNestedBigMaps @a @b--instance (SingI k, SingI v) => WithDeMorganScope HasNoOp 'TMap k v where-  withDeMorganScope = mkWithDeMorgan @HasNoOp @k @v--instance (SingI k, SingI v) => WithDeMorganScope HasNoOp 'TBigMap k v where-  withDeMorganScope = mkWithDeMorgan @HasNoOp @k @v- instance   ( WithDeMorganScope HasNoOp t a b   , WithDeMorganScope HasNoNestedBigMaps t a b-  , SingI a, SingI b   , WellTyped a, WellTyped b   ) => WithDeMorganScope ParameterScope t a b where   withDeMorganScope f =@@ -1097,7 +1153,6 @@   ( WithDeMorganScope HasNoOp t a b   , WithDeMorganScope HasNoNestedBigMaps t a b   , WithDeMorganScope HasNoContract t a b-  , SingI a, SingI b   , WellTyped a, WellTyped b   ) => WithDeMorganScope StorageScope t a b where   withDeMorganScope f =@@ -1111,7 +1166,6 @@   , WithDeMorganScope HasNoContract t a b   , WithDeMorganScope HasNoTicket t a b   , WithDeMorganScope HasNoSaplingState t a b-  , SingI a, SingI b   , WellTyped a, WellTyped b   ) => WithDeMorganScope ConstantScope t a b where   withDeMorganScope f =@@ -1126,7 +1180,6 @@   , WithDeMorganScope HasNoBigMap t a b   , WithDeMorganScope HasNoTicket t a b   , WithDeMorganScope HasNoSaplingState t a b-  , SingI a, SingI b   , WellTyped a, WellTyped b   ) => WithDeMorganScope PackedValScope t a b where   withDeMorganScope f =@@ -1138,7 +1191,6 @@ instance   ( WithDeMorganScope PackedValScope t a b   , WithDeMorganScope ConstantScope t a b-  , SingI a, SingI b   , WellTyped a, WellTyped b   ) => WithDeMorganScope UnpackedValScope t a b where   withDeMorganScope f =

@@ -25,7 +25,7 @@ import Morley.Michelson.Printer.Util (RenderDoc(..)) import Morley.Michelson.Typed.T (T(..)) import Morley.Util.MismatchError-import Morley.Util.Sing (SingI1(..), castSing, eqI, genSingletonsType)+import Morley.Util.Sing (castSing, eqI, genSingletonsType) import Morley.Util.TH (deriveGADTNFData)  -- | 'SingI' and 'Data.Singletons.TH.SDecide' instances for the 'T' kind.@@ -45,15 +45,6 @@ --------------------------------------------- -- Singleton-related helpers for T -----------------------------------------------instance SingI1 'TList where-  withSingI1 x = x--instance SingI1 'TOption where-  withSingI1 x = x--instance SingI k => SingI1 ('TMap k) where-  withSingI1 x = x- castSingE   :: forall (a :: T) (b :: T) t. (SingI a, SingI b)   => t a -> Either Text (t b)

@@ -261,6 +261,7 @@     AnnSAPLING_EMPTY_STATE{} -> recursion0 i     AnnSAPLING_VERIFY_UPDATE{} -> recursion0 i     AnnMIN_BLOCK_TIME{} -> recursion0 i+    AnnEMIT{} -> recursion0 i   where     recursion0 ::       forall a b. Instr a b -> m (Instr a b)@@ -454,6 +455,7 @@     i@AnnSAPLING_EMPTY_STATE{} -> RfNormal i     i@AnnSAPLING_VERIFY_UPDATE{} -> RfNormal i     i@AnnMIN_BLOCK_TIME{} -> RfNormal i+    i@AnnEMIT{} -> 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@.@@ -938,6 +940,7 @@   AnnSAPLING_EMPTY_STATE{} -> True   AnnSAPLING_VERIFY_UPDATE{} -> True   AnnMIN_BLOCK_TIME{} -> True+  AnnEMIT{} -> True  -- | A wrapper around either typechecked 'Anns' or unchecked 'NonEmpty' of -- 'AnyAnn'. Annotations on some instructions aren't typechecked, hence these@@ -1069,3 +1072,7 @@   AnnSAPLING_EMPTY_STATE anns _ -> pure $ SomeAnns anns   AnnSAPLING_VERIFY_UPDATE anns -> pure $ SomeAnns anns   AnnMIN_BLOCK_TIME anns -> SomeUncheckedAnns <$> nonEmpty anns+  AnnEMIT anns tag ty -> pure $+    case ty of+      Just ty' -> SomeAnns $ tag `AnnsCons` ty' `AnnsTyCons` anns+      Nothing -> SomeAnns $ tag `AnnsCons` anns

@@ -9,6 +9,7 @@   , Operation' (..)   , SetDelegate (..)   , TransferTokens (..)+  , Emit(..)   , Value' (..)   , RemFail (..)   , mkVLam@@ -31,11 +32,12 @@ import Fmt (Buildable(build), Builder, (+|), (|+))  import Morley.Michelson.Text (MText)+import Morley.Michelson.Typed.Annotation (Notes) import Morley.Michelson.Typed.Contract import Morley.Michelson.Typed.Entrypoints import Morley.Michelson.Typed.Scope import Morley.Michelson.Typed.T (T(..))-import Morley.Tezos.Address (Address, GlobalCounter(..), TxRollupL2Address)+import Morley.Tezos.Address import Morley.Tezos.Core (ChainId, Mutez, Timestamp) import Morley.Tezos.Crypto   (Bls12381Fr, Bls12381G1, Bls12381G2, Chest, ChestKey, KeyHash, PublicKey, Signature)@@ -58,6 +60,7 @@        , Typeable instr, ParameterScope cp, StorageScope st)     => CreateContract instr cp st     -> Operation' instr+  OpEmit :: PackedValScope t => Emit instr t -> Operation' instr  instance Buildable (Operation' instr) where   build =@@ -65,6 +68,7 @@       OpTransferTokens tt -> build tt       OpSetDelegate sd -> build sd       OpCreateContract cc -> build cc+      OpEmit em -> build em  deriving stock instance Show (Operation' instr) @@ -76,6 +80,8 @@     (OpSetDelegate _, _) -> False     (OpCreateContract cc1, OpCreateContract cc2) -> cc1 `eqParamMixed3` cc2     (OpCreateContract _, _) -> False+    (OpEmit em1, OpEmit em2) -> em1 `eqParamSing` em2+    (OpEmit _, _) -> False  data TransferTokens instr p = TransferTokens   { ttTransferArgument :: Value' instr p@@ -104,7 +110,7 @@     , forall i o. Eq (instr i o)     )   => CreateContract-  { ccOriginator :: Address+  { ccOriginator :: L1Address   , ccDelegate :: Maybe KeyHash   , ccBalance :: Mutez   , ccStorageVal :: Value' instr st@@ -121,6 +127,19 @@ deriving stock instance Show (CreateContract instr cp st) deriving stock instance Eq (CreateContract instr cp st) +data Emit instr t = PackedValScope t => Emit+  { emTag :: Text+  , emNotes :: Notes t+  , emValue :: Value' instr t+  , emCounter :: GlobalCounter+  }++deriving stock instance Show (Emit instr t)+deriving stock instance Eq (Emit instr t)++instance Buildable (Emit instr t) where+  build Emit{..} = "Emit contract event with tag " +| emTag |+ " and type " +| emNotes |+ ""+ -- | Wrapper over instruction which remembers whether this instruction -- always fails or not. data RemFail (instr :: k -> k -> Type) (i :: k) (o :: k) where@@ -266,10 +285,10 @@ -- | Make value of @contract@ type which refers to the given address and -- does not call any entrypoint. addressToVContract-  :: forall t instr.+  :: forall t instr kind.       (ParameterScope t, ForbidOr t)-  => Address -> Value' instr ('TContract t)-addressToVContract addr = VContract addr sepcPrimitive+  => KindedAddress kind -> Value' instr ('TContract t)+addressToVContract addr = VContract (MkAddress addr) sepcPrimitive  buildVContract :: Value' instr ('TContract arg) -> Builder buildVContract = \case@@ -364,6 +383,10 @@   , deriveGADTNFData ''Operation'   , deriveGADTNFData ''Value'   ]++instance NFData (Emit instr t) where+  rnf (Emit a b c d) =+    rnf a `seq` rnf b `seq` rnf c `seq` rnf d  instance NFData (TransferTokens instr p) 

@@ -10,14 +10,15 @@   , flattenExpandedOp   ) where -import Prelude hiding (EQ, GT, LT)+import Prelude hiding (EQ, GT, LT, group)  import Data.Aeson.TH (deriveJSON) import Data.Data (Data(..)) import Fmt (Buildable(build), (+|), (|+)) import Generics.SYB (everywhere, mkT) import Text.PrettyPrint.Leijen.Text-  (Doc, align, braces, enclose, indent, integer, line, nest, space, text, (<$$>), (<+>))+  (Doc, align, braces, enclose, group, indent, integer, nest, space, text, (<$$>), (<+>))+import Text.PrettyPrint.Leijen.Text qualified as PP  import Morley.Michelson.ErrorPos (ErrorSrcPos) import Morley.Michelson.Printer.Util@@ -212,6 +213,7 @@   | SAPLING_EMPTY_STATE VarAnn Natural   | SAPLING_VERIFY_UPDATE VarAnn   | MIN_BLOCK_TIME    [AnyAnn]+  | EMIT              VarAnn FieldAnn (Maybe Ty)   deriving stock (Eq, Functor, Data, Generic, Show)  instance NFData op => NFData (InstrAbstract op)@@ -227,20 +229,10 @@     DIG n                   -> "DIG" <+> text (show n)     DUG n                   -> "DUG" <+> text (show n)     PUSH va t v             ->-      let renderConsecutively =-            "PUSH" <+> renderAnnot va <+> renderTy t <+> renderDoc needsParens v-          renderAligned = "PUSH" <+> renderAnnot va <$$> (spaces 2 <> renderTy t)-                                <$$> spaces 2 <> nest 3 (renderDoc needsParens v)-      in case v of-        ValueNil      -> renderConsecutively-        ValueInt{}    -> renderConsecutively-        ValueString{} -> renderConsecutively-        ValueBytes{}  -> renderConsecutively-        ValueUnit     -> renderConsecutively-        ValueTrue     -> renderConsecutively-        ValueFalse    -> renderConsecutively-        ValueNone     -> renderConsecutively-        _             -> renderAligned+      group $ nest 2 $+        text "PUSH" <+> renderAnnot va+        PP.<$> renderTy t+        PP.<$> renderDoc needsParens v     SOME ta va              -> "SOME" <+> renderAnnots [ta] [] [va]     NONE ta va t            -> "NONE" <+> renderAnnots [ta] [] [va] <+> renderTy t     UNIT ta va              -> "UNIT" <+> renderAnnots [ta] [] [va]@@ -276,7 +268,7 @@     EXEC va                 -> "EXEC" <+> renderAnnot va     APPLY va                -> "APPLY" <+> renderAnnot va     DIP s                   -> "DIP" <+> nest 5 (renderOps s)-    DIPN n s                -> "DIP" <+> text (show n) <> line <> indent 4 (renderOps s)+    DIPN n s                -> "DIP" <+> text (show n) PP.<$> indent 4 (renderOps s)     FAILWITH                -> "FAILWITH"     CAST va t               -> "CAST" <+> renderAnnot va <+> renderTy t     RENAME va               -> "RENAME" <+> renderAnnot va@@ -314,32 +306,33 @@     CREATE_CONTRACT va1 va2 contract -> let       body = enclose space space $ align $ (renderDoc doesntNeedParens contract)       in "CREATE_CONTRACT" <+> renderAnnots [] [] [va1, va2] <$$> (indent 2 $ braces $ body)-    IMPLICIT_ACCOUNT va     -> "IMPLICIT_ACCOUNT" <+> renderAnnot va-    NOW va                  -> "NOW" <+> renderAnnot va-    AMOUNT va               -> "AMOUNT" <+> renderAnnot va-    BALANCE va              -> "BALANCE" <+> renderAnnot va-    VOTING_POWER va         -> "VOTING_POWER" <+> renderAnnot va-    TOTAL_VOTING_POWER va   -> "TOTAL_VOTING_POWER" <+> renderAnnot va-    CHECK_SIGNATURE va      -> "CHECK_SIGNATURE" <+> renderAnnot va-    SHA256 va               -> "SHA256" <+> renderAnnot va-    SHA512 va               -> "SHA512" <+> renderAnnot va-    BLAKE2B va              -> "BLAKE2B" <+> renderAnnot va-    SHA3 va                 -> "SHA3" <+> renderAnnot va-    KECCAK va               -> "KECCAK" <+> renderAnnot va-    HASH_KEY va             -> "HASH_KEY" <+> renderAnnot va-    PAIRING_CHECK va        -> "PAIRING_CHECK" <+> renderAnnot va-    SOURCE va               -> "SOURCE" <+> renderAnnot va-    SENDER va               -> "SENDER" <+> renderAnnot va-    ADDRESS va              -> "ADDRESS" <+> renderAnnot va-    CHAIN_ID va             -> "CHAIN_ID" <+> renderAnnot va-    LEVEL va                -> "LEVEL" <+> renderAnnot va-    SELF_ADDRESS va         -> "SELF_ADDRESS" <+> renderAnnot va-    NEVER                   -> "NEVER"-    TICKET va               -> "TICKET" <+> renderAnnot va-    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+    IMPLICIT_ACCOUNT va      -> "IMPLICIT_ACCOUNT" <+> renderAnnot va+    NOW va                   -> "NOW" <+> renderAnnot va+    AMOUNT va                -> "AMOUNT" <+> renderAnnot va+    BALANCE va               -> "BALANCE" <+> renderAnnot va+    VOTING_POWER va          -> "VOTING_POWER" <+> renderAnnot va+    TOTAL_VOTING_POWER va    -> "TOTAL_VOTING_POWER" <+> renderAnnot va+    CHECK_SIGNATURE va       -> "CHECK_SIGNATURE" <+> renderAnnot va+    SHA256 va                -> "SHA256" <+> renderAnnot va+    SHA512 va                -> "SHA512" <+> renderAnnot va+    BLAKE2B va               -> "BLAKE2B" <+> renderAnnot va+    SHA3 va                  -> "SHA3" <+> renderAnnot va+    KECCAK va                -> "KECCAK" <+> renderAnnot va+    HASH_KEY va              -> "HASH_KEY" <+> renderAnnot va+    PAIRING_CHECK va         -> "PAIRING_CHECK" <+> renderAnnot va+    SOURCE va                -> "SOURCE" <+> renderAnnot va+    SENDER va                -> "SENDER" <+> renderAnnot va+    ADDRESS va               -> "ADDRESS" <+> renderAnnot va+    CHAIN_ID va              -> "CHAIN_ID" <+> renderAnnot va+    LEVEL va                 -> "LEVEL" <+> renderAnnot va+    SELF_ADDRESS va          -> "SELF_ADDRESS" <+> renderAnnot va+    NEVER                    -> "NEVER"+    TICKET va                -> "TICKET" <+> renderAnnot va+    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+    EMIT va fa ty            -> "EMIT" <+> renderAnnots [] [fa] [va] <+> maybe mempty renderTy ty     SAPLING_EMPTY_STATE va n -> "SAPLING_EMPTY_STATE" <+> renderAnnot va <+> (integer $ toInteger n)     SAPLING_VERIFY_UPDATE va -> "SAPLING_VERIFY_UPDATE" <+> renderAnnot va     MIN_BLOCK_TIME anns      -> "MIN_BLOCK_TIME" <+> renderAnyAnns anns

@@ -19,6 +19,8 @@   , renderElt'   ) where +import Prelude hiding (group)+ import Data.Aeson (FromJSON(..), ToJSON(..), withText) import Data.Aeson.TH (deriveJSON) import Data.Data (Data(..))@@ -26,10 +28,12 @@ import Fmt (Buildable(build)) import Text.Hex (decodeHex, encodeHex) import Text.PrettyPrint.Leijen.Text-  (Doc, braces, dquotes, enclose, semi, space, text, textStrict, (<+>))+  (Doc, align, dquotes, encloseSep, group, hang, lbrace, rbrace, semi, sep, softline, space, text,+  textStrict, (<+>))+import Text.PrettyPrint.Leijen.Text qualified as PP  import Morley.Michelson.Printer.Util-  (RenderContext, RenderDoc(..), addParens, buildRenderDoc, doesntNeedParens, needsParens,+  (RenderContext, RenderDoc(..), addParensMultiline, buildRenderDoc, doesntNeedParens, needsParens,   renderOps) import Morley.Michelson.Text import Morley.Util.Aeson@@ -99,13 +103,18 @@  -- | Helper functions to render @Value@s renderSome, renderLeft, renderRight :: RenderContext -> (RenderContext -> Doc) -> Doc-renderSome  pn render = addParens pn $ "Some"  <+> render needsParens-renderLeft  pn render = addParens pn $ "Left"  <+> render needsParens-renderRight pn render = addParens pn $ "Right" <+> render needsParens+renderSome  pn render = renderContainer pn $ "Some" PP.<$> render needsParens+renderLeft  pn render = renderContainer pn $ "Left" PP.<$> render needsParens+renderRight pn render = renderContainer pn $ "Right" PP.<$> render needsParens +-- | Helper function to format container values such as @Some@ and @Right@.+renderContainer :: RenderContext -> Doc -> Doc+renderContainer pn doc = addParensMultiline pn $ group $ hang 2 $ doc+ -- | Helper function to render @Pair@ @Value@ renderPair :: RenderContext -> (RenderContext -> Doc) -> (RenderContext -> Doc) -> Doc-renderPair pn l r = addParens pn $ "Pair" <+> l needsParens <+> r needsParens+renderPair pn l r = addParensMultiline pn $ hang 2 $+  sep ["Pair", l needsParens, r needsParens]  -- | Helper function to render @Elt@ renderElt' :: (RenderContext -> Doc) -> (RenderContext -> Doc) -> Doc@@ -126,9 +135,8 @@ -- given a rendering function for a single item. renderValuesList :: (e -> Doc) -> NonEmpty e -> Doc renderValuesList renderElem (toList -> es) =-  braces . enclose space space $-    mconcat . intersperse (semi <> space) $-      renderElem <$> es+  align $ encloseSep (lbrace <> space) (softline <> rbrace) (semi <> space) $+    renderElem <$> es  instance (RenderDoc op) => Buildable (Value' op) where   build = buildRenderDoc

@@ -7,11 +7,19 @@  module Morley.Tezos.Address   ( ContractHash-  , Address (..)+  , KindedAddress (..)   , TxRollupL2Address (..)   , mkKeyAddress   , detGenKeyAddress-  , isKeyAddress+  , isImplicitAddress+  , ImplicitAddress+  , ContractAddress+  , TxRollupAddress+  , L1Address+  , L1AddressKind+  , ConstrainAddressKind+  , Address+  , ConstrainedAddress(.., MkAddress)    , GlobalCounter(..)   , mkContractHashHack@@ -22,16 +30,27 @@   , formatAddress   , mformatAddress   , parseAddressRaw+  , parseKindedAddress   , parseAddress   , ta++  -- * Utilities+  , addressKindSanity+  , usingImplicitOrContractKind   ) where +import Control.Monad.Except (mapExceptT, throwError) import Data.Aeson (FromJSON(..), FromJSONKey, ToJSON(..), ToJSONKey) import Data.Aeson qualified as Aeson import Data.Aeson.Encoding qualified as Aeson import Data.Aeson.Types qualified as AesonTypes+import Data.Binary.Get qualified as Get import Data.ByteString qualified as BS+import Data.ByteString.Lazy qualified as LBS+import Data.Constraint (Dict(..), (\\))+import Data.Singletons (SingI(..)) import Data.Text (strip)+import Data.Type.Equality ((:~:)(..)) import Fmt (Buildable(build), hexF, pretty) import Instances.TH.Lift () import Language.Haskell.TH.Quote qualified as TH@@ -41,42 +60,158 @@  import Morley.Michelson.Printer.Util (RenderDoc(..), buildRenderDoc, renderAnyBuildable) import Morley.Michelson.Text+import Morley.Tezos.Address.Kinds import Morley.Tezos.Crypto+import Morley.Util.Binary import Morley.Util.CLI+import Morley.Util.Sing import Morley.Util.TypeLits --- | Data type corresponding to address structure in Tezos.-data Address-  = KeyAddress KeyHash-  -- ^ @tz1@, @tz2@ or @tz3@ address which is a hash of a public key.-  | ContractAddress ContractHash-  -- ^ @KT@ address which corresponds to a callable contract.-  | TransactionRollupAddress TxRollupHash-  -- ^ @txr1@ address which corresponds to a transaction rollup.-  deriving stock (Show, Eq, Ord, Generic, Lift)+-- | A "kinded" address. This type carries 'AddressKind' on the type-level.+-- Useful in the internal API, not as much when we have to interact with the+-- network. See 'Address' for a type that is isomorphic to a Michelson+-- @address@.+data KindedAddress (kind :: AddressKind) where+  -- | @tz1@, @tz2@ or @tz3@ address which is a hash of a public key.+  ImplicitAddress :: KeyHash -> KindedAddress 'AddressKindImplicit+  -- | @KT1@ address which corresponds to a callable contract.+  ContractAddress :: ContractHash -> KindedAddress 'AddressKindContract+  -- | @txr1@ address which corresponds to a transaction rollup.+  TxRollupAddress :: TxRollupHash -> KindedAddress 'AddressKindTxRollup -instance NFData Address+deriving stock instance Show (KindedAddress kind)+deriving stock instance Eq (KindedAddress kind)+deriving stock instance Ord (KindedAddress kind)+deriving stock instance Lift (KindedAddress kind) +instance NFData (KindedAddress kind) where+  rnf = \case+    ImplicitAddress x -> rnf x+    ContractAddress x -> rnf x+    TxRollupAddress x -> rnf x++-- | A type only allowing v'ImplicitAddress'+type ImplicitAddress = KindedAddress 'AddressKindImplicit++-- | A type only allowing v'ContractAddress'+type ContractAddress = KindedAddress 'AddressKindContract++-- | A type only allowing v'TxRollupAddress'+type TxRollupAddress = KindedAddress 'AddressKindTxRollup++-- | Data type corresponding to @address@ structure in Tezos.+type Address =+  ConstrainedAddress '[ 'AddressKindImplicit, 'AddressKindContract, 'AddressKindTxRollup ]++type family ConstrainAddressKindHelper (ks :: [AddressKind]) kind where+  ConstrainAddressKindHelper (x ': _) x = 'True+  ConstrainAddressKindHelper (_ ': xs) x = ConstrainAddressKindHelper xs x+  ConstrainAddressKindHelper '[] _ = 'False++type family CheckConstrainAddressKindError k b :: Constraint where+  CheckConstrainAddressKindError _ 'True = ()+  CheckConstrainAddressKindError k 'False =+    TypeError ('ShowType k ':<>: 'Text "is forbidden in this context")++-- | Constrain address kind to be one of the kinds in the list.+type ConstrainAddressKind ks k =+  ( CheckConstrainAddressKindError k (ConstrainAddressKindHelper ks k)+  , ConstrainAddressKindHelper ks k ~ 'True)++-- | An existential of 'KindedAddress' constrained by its type argument.+data ConstrainedAddress (ks :: [AddressKind]) =+  forall kind. ConstrainAddressKind ks kind => MkConstrainedAddress (KindedAddress kind)++-- | A convenience synonym for 'ConstrainedAddress' allowing only implicit and+-- contract addresses.+--+-- 'L1Address' is named as such because in addition to implicit and contract+-- addresses, Michelson's @address@ type can contain @txr1@ addresses,+-- identifying transaction rollups. While @txr1@ are technically also level-1+-- (level-2 being @tx_rollup_l2_address@, i.e. @tz4@), in practice it's a+-- level-1 identifier for a bundle of level-2 operations. Hence, to keep type+-- names concise, we use 'L1Address'.+type L1Address =+  ConstrainedAddress '[ 'AddressKindImplicit, 'AddressKindContract ]++-- | Convenience synonym for 'ConstrainAddressKind' allowing only implicit and+-- contract addresses.+--+-- For a note on the naming convention, refer to 'L1Address'.+type L1AddressKind kind =+  ConstrainAddressKind '[ 'AddressKindImplicit, 'AddressKindContract ] kind++-- | A trick to avoid bogus redundant constraint warnings+usingImplicitOrContractKind :: forall kind a. L1AddressKind kind => a -> a+usingImplicitOrContractKind = id+  where _ = Dict :: Dict (L1AddressKind kind)++-- | 'MkConstrainedAddress' specialized to 'Address'+pattern MkAddress :: KindedAddress kind -> Address+pattern MkAddress x <- MkConstrainedAddress x+  where MkAddress x = case x of+          ImplicitAddress{} -> MkConstrainedAddress x+          ContractAddress{} -> MkConstrainedAddress x+          TxRollupAddress{} -> MkConstrainedAddress x++{-# COMPLETE MkAddress #-}++deriving stock instance Show (ConstrainedAddress c)+instance Eq (ConstrainedAddress c) where+  MkConstrainedAddress (addr1 :: KindedAddress kind1)+    == MkConstrainedAddress (addr2 :: KindedAddress kind2) =+    case eqI @kind1 @kind2 \\ addressKindSanity addr1 \\ addressKindSanity addr2 of+      Just Refl -> addr1 == addr2+      Nothing -> False+instance Ord (ConstrainedAddress c) where+  compare (MkConstrainedAddress (a1 :: KindedAddress kind1))+          (MkConstrainedAddress (a2 :: KindedAddress kind2)) =+    case (a1, a2) of+      (k1, k2)+        | Just Refl <- eqI @kind1 @kind2 \\ addressKindSanity k1 \\ addressKindSanity k2+        -> compare k1 k2+      (ImplicitAddress{}, _) -> LT+      (ContractAddress{}, ImplicitAddress{}) -> GT+      (ContractAddress{}, _) -> LT+      (TxRollupAddress{}, ImplicitAddress{}) -> GT+      (TxRollupAddress{}, ContractAddress{}) -> GT+      (TxRollupAddress{}, _) -> LT+deriving stock instance Lift (ConstrainedAddress c)++instance NFData (ConstrainedAddress c) where+  rnf (MkConstrainedAddress x) = rnf x++instance Buildable (ConstrainedAddress c) where+  build (MkConstrainedAddress x) = build x++-- | Given any (non-bottom) 'KindedAddress', prove that @kind@ is well-defined+-- (i.e. has a 'SingI' instance)+addressKindSanity :: KindedAddress kind -> Dict (SingI kind)+addressKindSanity = \case+  ImplicitAddress{} -> Dict+  ContractAddress{} -> Dict+  TxRollupAddress{} -> Dict+ -- | @tz4@ level-2 public key hash address, used with transaction rollups, corresponds -- to @tx_rollup_l2_address@ Michelson type. newtype TxRollupL2Address = TxRollupL2Address KeyHashL2   deriving stock (Show, Eq, Ord, Generic, Lift)   deriving newtype NFData --- | Returns @True@ if given address is implicit.-isKeyAddress :: Address -> Bool-isKeyAddress = \case-  KeyAddress _      -> True-  ContractAddress _ -> False-  TransactionRollupAddress _ -> False+-- | Checks if the provided 'KindedAddress' is an implicit address and returns+-- proof of the fact if it is.+isImplicitAddress :: KindedAddress kind -> Maybe (kind :~: 'AddressKindImplicit)+isImplicitAddress = \case+  ImplicitAddress{} -> Just Refl+  _ -> Nothing --- | Smart constructor for 'KeyAddress'.-mkKeyAddress :: PublicKey -> Address-mkKeyAddress = KeyAddress . hashKey+-- | Smart constructor for t'ImplicitAddress'.+mkKeyAddress :: PublicKey -> ImplicitAddress+mkKeyAddress = ImplicitAddress . hashKey --- | Deterministically generate a random 'KeyAddress' and discard its+-- | Deterministically generate a random t'ImplicitAddress' and discard its -- secret key.-detGenKeyAddress :: ByteString -> Address+detGenKeyAddress :: ByteString -> ImplicitAddress detGenKeyAddress = mkKeyAddress . toPublic . detSecretKey  -- | Represents the network's global counter.@@ -110,17 +245,17 @@ -- Formatting/parsing ---------------------------------------------------------------------------- -formatAddress :: Address -> Text+formatAddress :: KindedAddress kind -> Text formatAddress =   \case-    KeyAddress h -> formatHash h+    ImplicitAddress h -> formatHash h     ContractAddress h -> formatHash h-    TransactionRollupAddress h -> formatHash h+    TxRollupAddress h -> formatHash h -mformatAddress :: Address -> MText+mformatAddress :: KindedAddress kind -> MText mformatAddress = unsafe . mkMText . formatAddress -instance Buildable Address where+instance Buildable (KindedAddress kind) where   build = build . formatAddress  instance Buildable TxRollupL2Address where@@ -152,36 +287,45 @@         mconcat $ "Address failed to parse: " : intersperse ", "           (toList $ renderDoc context <$> pkErr) --- | Parse an address from its human-readable textual representation--- used by Tezos (e. g. "tz1faswCTDciRzE4oJ9jn2Vm2dvjeyA9fUzU"). Or--- fail if it's invalid.-parseAddress :: Text -> Either ParseAddressError Address-parseAddress addressText =-  let implicit = tryParse KeyAddress parseHash handleCrypto-      contract = tryParse ContractAddress parseHash handleCrypto-      txr = tryParse TransactionRollupAddress parseHash handleCrypto-  in implicit `merge` contract `merge` txr+-- | Parse an address of a particular kind from its human-readable textual+-- representation used by Tezos (e. g. "tz1faswCTDciRzE4oJ9jn2Vm2dvjeyA9fUzU").+-- Or fail if it's invalid.+parseKindedAddress :: forall kind. SingI kind => Text -> Either ParseAddressError (KindedAddress kind)+parseKindedAddress addressText = case sing @kind of+  SAddressKindContract -> tryParse ContractAddress+  SAddressKindImplicit -> tryParse ImplicitAddress+  SAddressKindTxRollup -> tryParse TxRollupAddress   where     handleCrypto = \case       CryptoParseWrongBase58Check -> ParseAddressWrongBase58Check       x -> ParseAddressAllFailed $ pure x+    tryParse :: AllHashTags hkind => (Hash hkind -> b) -> Either ParseAddressError b+    tryParse ctor = bimap handleCrypto ctor $ parseHash addressText++-- | Parse an address of arbitrary kind from its human-readable textual+-- representation, or fail if it's invalid.+parseAddress :: Text -> Either ParseAddressError Address+parseAddress x =+          (MkAddress <$> parseKindedAddress @'AddressKindImplicit x)+  `merge` (MkAddress <$> parseKindedAddress @'AddressKindContract x)+  `merge` (MkAddress <$> parseKindedAddress @'AddressKindTxRollup x)+  where     merge :: Semigroup a => Either a b -> Either a b -> Either a b     merge (Left xs) (Left ys) = Left $ xs <> ys     merge r@Right{} _ = r     merge _ r@Right{} = r-    tryParse :: (t -> b) -> (Text -> Either t1 t) -> (t1 -> a) -> Either a b-    tryParse ctor parser handler =-      case parser addressText of-        Left err -> Left $ handler err-        Right res -> Right $ ctor res  data ParseAddressRawError   = ParseAddressRawWrongSize ByteString   -- ^ Raw bytes representation of an address has invalid length.-  | ParseAddressRawInvalidPrefix ByteString+  | ParseAddressRawInvalidPrefix Word8   -- ^ Raw bytes representation of an address has incorrect prefix.-  | ParseAddressRawMalformedSeparator ByteString+  | ParseAddressRawMalformedSeparator Word8   -- ^ Raw bytes representation of an address does not end with "\00".+  | ParseAddressRawBinaryError Text+  -- ^ General binary decoding error.+  | ParseAddressCryptoError CryptoParseError+  -- ^ Crypto error in parsing key hash.   deriving stock (Eq, Show, Generic)  instance NFData ParseAddressRawError@@ -193,8 +337,10 @@         "Invalid prefix for raw address" <+> (dquotes $ renderAnyBuildable $ hexF prefix) <+> "provided"       ParseAddressRawWrongSize addr -> "Given raw address+" <+>         (renderAnyBuildable $ hexF addr) <+> "has invalid length" <+> int (length addr)-      ParseAddressRawMalformedSeparator addr -> "Given raw address+" <+> (renderAnyBuildable $ hexF addr) <+>+      ParseAddressRawMalformedSeparator addr -> "Given raw address" <+> (renderAnyBuildable $ hexF addr) <+>         "does not end with" <+> dquotes (backslash <> "00")+      ParseAddressRawBinaryError err -> "Binary error during decoding address:" <+> renderAnyBuildable err+      ParseAddressCryptoError err -> "Key hash decoding error:" <+> renderAnyBuildable err  instance Buildable ParseAddressRawError where   build = buildRenderDoc@@ -203,32 +349,29 @@ -- (e.g "01521139f84791537d54575df0c74a8084cc68861c00")) . Or fail otherwise -- if it's invalid. parseAddressRaw :: ByteString -> Either ParseAddressRawError Address-parseAddressRaw bytes =-  case BS.splitAt 1 bytes of-    -- key hash address-    ("\00", rest) -> checkHashLength (BS.drop 1 rest) >> case BS.splitAt 1 rest of-      ("\00", addr) -> pure $ KeyAddress $ Hash HashEd25519 addr-      ("\01", addr) -> pure $ KeyAddress $ Hash HashSecp256k1 addr-      ("\02", addr) -> pure $ KeyAddress $ Hash HashP256 addr-      (x, _) -> Left $ ParseAddressRawInvalidPrefix x-    (pfx, rest) -> do-      (address, sep) <- maybe (Left $ ParseAddressRawWrongSize rest) pure $ BS.unsnoc rest-      checkHashLength address-      unless (sep == 0x00) $-        Left $ ParseAddressRawMalformedSeparator rest-      case pfx of-        -- contract address-        "\01" -> pure $ ContractAddress $ Hash HashContract address-        -- transaction rollup address-        "\02" -> pure $ TransactionRollupAddress $ Hash HashTXR address-        x -> Left $ ParseAddressRawInvalidPrefix x+parseAddressRaw bytes+  -- NB: conveniently, the byte count is the same for 'KeyAddress',+  -- 'ContractAddress' and 'TransactionRollupAddress'. However, with+  -- 'KeyAddress' it's two tag bytes, while with the other two it's one tag byte+  -- and one separator byte.+  | BS.length bytes /= hashLengthBytes + 2 = Left $ ParseAddressRawWrongSize bytes+  | otherwise+  = either (Left . ParseAddressRawBinaryError . fromString . view _3) (view _3)+  $ flip Get.runGetOrFail (LBS.fromStrict bytes) $ runExceptT+  $ decodeWithTagM "address" (throwError . ParseAddressRawInvalidPrefix)+      [ 0x00 ##: MkAddress . ImplicitAddress <$> keyHash+      , 0x01 ##: MkAddress . ContractAddress <$> sepHash HashContract+      , 0x02 ##: MkAddress . TxRollupAddress <$> sepHash HashTXR+      ]   where-    checkHashLength addr-      | length addr /= hashLengthBytes-      = Left $ ParseAddressRawWrongSize addr-      | otherwise = pass+    sep = lift Get.getWord8 >>= \case+      0x00 -> pass+      x -> throwError $ ParseAddressRawMalformedSeparator x+    keyHash = mapExceptT (fmap $ first ParseAddressCryptoError) decodeKeyHash+    sepHash :: HashTag kind -> ExceptT ParseAddressRawError Get.Get (Hash kind)+    sepHash kind = Hash kind <$> lift (getByteStringCopy hashLengthBytes) <* sep --- | QuasyQuoter for constructing Tezos addresses.+-- | QuasiQuoter for constructing Tezos addresses. -- -- Validity of result will be checked at compile time. ta :: TH.QuasiQuoter@@ -236,13 +379,13 @@   { TH.quoteExp = \s ->       case parseAddress . strip $ toText s of         Left   err -> fail $ pretty err-        Right addr -> TH.lift addr+        Right (MkAddress addr) -> TH.lift addr   , TH.quotePat = \_ ->-      fail "Cannot use this QuasyQuotation at pattern position"+      fail "Cannot use this QuasiQuotation at pattern position"   , TH.quoteType = \_ ->-      fail "Cannot use this QuasyQuotation at type position"+      fail "Cannot use this QuasiQuotation at type position"   , TH.quoteDec = \_ ->-      fail "Cannot use this QuasyQuotation at declaration position"+      fail "Cannot use this QuasiQuotation at declaration position"   }  @@ -250,7 +393,7 @@     TypeError ('Text "There is no instance defined for (IsString Address)" ':$$:                'Text "Consider using QuasiQuotes: `[ta|some text...|]`"               ) =>-    IsString Address where+    IsString (KindedAddress kind) where   fromString = error "impossible"  @@ -258,24 +401,41 @@ -- Unsafe ---------------------------------------------------------------------------- -instance HasCLReader Address where+instance SingI kind => HasCLReader (KindedAddress kind) where   getReader = eitherReader parseAddrDo     where       parseAddrDo addr =-        either (Left . mappend "Failed to parse address: " . pretty) Right $-        parseAddress $ toText addr+        first (mappend "Failed to parse address: " . pretty) $+        parseKindedAddress $ toText addr   getMetavar = "ADDRESS"  ---------------------------------------------------------------------------- -- Aeson instances ---------------------------------------------------------------------------- -instance ToJSON Address where+instance ToJSON (KindedAddress kind) where   toJSON = Aeson.String . formatAddress   toEncoding = Aeson.text . formatAddress -instance ToJSONKey Address where+instance ToJSONKey (KindedAddress kind) where   toJSONKey = AesonTypes.toJSONKeyText formatAddress++instance SingI kind => FromJSON (KindedAddress kind) where+  parseJSON =+    Aeson.withText "Address" $+    either (fail . pretty) pure . parseKindedAddress++instance SingI kind => FromJSONKey (KindedAddress kind) where+  fromJSONKey =+    AesonTypes.FromJSONKeyTextParser+      (either (fail . pretty) pure . parseKindedAddress)++instance ToJSON (ConstrainedAddress c) where+  toJSON (MkConstrainedAddress addr) = toJSON addr+  toEncoding (MkConstrainedAddress addr) = toEncoding addr++instance ToJSONKey (ConstrainedAddress c) where+  toJSONKey = AesonTypes.toJSONKeyText \(MkConstrainedAddress addr) -> formatAddress addr  instance FromJSON Address where   parseJSON =

@@ -4,43 +4,118 @@ module Morley.Tezos.Address.Alias   ( AddressOrAlias(..)   , Alias(..)+  , SomeAlias(..)+  , SomeAddressOrAlias(..)+  , ImplicitAlias+  , ContractAlias+  , ImplicitAddressOrAlias+  , ContractAddressOrAlias+  , unAlias+  , mkAlias+  , aliasKindSanity   )   where -import Data.Aeson (FromJSON, ToJSON)-import Fmt (Buildable(..))+import Data.Aeson (FromJSON(..), ToJSON(..))+import Data.Constraint (Dict(..), (\\))+import Data.Singletons (SingI(..), demote)+import Data.Type.Equality ((:~:)(..))+import Fmt (Buildable(..), nameF, pretty, (+|), (|+)) import Options.Applicative qualified as Opt -import Morley.Tezos.Address (Address, parseAddress)+import Morley.Tezos.Address+import Morley.Tezos.Address.Kinds import Morley.Util.CLI (HasCLReader(..))+import Morley.Util.Sing  -- | @tezos-client@ can associate addresses with textual aliases. -- This type denotes such an alias.-newtype Alias = Alias-  { unAlias :: Text-    -- ^ Extract 'Text' from 'Alias'.-  }-  deriving stock (Show, Eq, Ord)-  deriving newtype (Buildable, ToJSON, FromJSON)+data Alias (kind :: AddressKind) where+  ImplicitAlias :: Text -> Alias 'AddressKindImplicit+  ContractAlias :: Text -> Alias 'AddressKindContract +-- | A type only allowing v'ImplicitAlias' values.+type ImplicitAlias = Alias 'AddressKindImplicit++-- | A type only allowing v'ContractAlias' values.+type ContractAlias = Alias 'AddressKindContract++deriving stock instance Show (Alias kind)+deriving stock instance Eq (Alias kind)+deriving stock instance Ord (Alias kind)++-- | Get raw alias text from 'Alias'+unAlias :: Alias kind -> Text+unAlias = \case+  ImplicitAlias x -> x+  ContractAlias x -> x++-- | Construct an 'Alias' from alias 'Text'.+mkAlias :: forall kind. (SingI kind, L1AddressKind kind) => Text -> Alias kind+mkAlias = usingImplicitOrContractKind @kind $ case sing @kind of+  SAddressKindImplicit -> ImplicitAlias+  SAddressKindContract -> ContractAlias++instance Buildable (Alias kind) where+  build = build . unAlias++instance ToJSON (Alias kind) where+  toJSON = toJSON . unAlias++instance (SingI kind, L1AddressKind kind) => FromJSON (Alias kind) where+  parseJSON = fmap mkAlias . parseJSON++-- | Existential wrapper over 'Alias'.+data SomeAlias = forall kind. SomeAlias (Alias kind)++deriving stock instance Show SomeAlias++instance Buildable SomeAlias where+  build (SomeAlias x) = build x++-- | Given an 'Alias', prove it's @kind@ is well-defined (i.e. it has a 'SingI'+-- instance and satisfies 'L1AddressKind' constraint)+aliasKindSanity :: Alias kind -> Dict (L1AddressKind kind, SingI kind)+aliasKindSanity = \case+  ImplicitAlias{} -> Dict+  ContractAlias{} -> Dict+ -- | Representation of an address that @tezos-client@ uses. It can be -- an address itself or a textual alias.-data AddressOrAlias-  = AddressResolved Address+data AddressOrAlias kind+  = AddressResolved (KindedAddress kind)   -- ^ Address itself, can be used as is.-  | AddressAlias Alias+  | AddressAlias (Alias kind)   -- ^ Address alias, should be resolved by @tezos-client@.   deriving stock (Show, Eq, Ord) -instance HasCLReader AddressOrAlias where+instance (SingI kind, L1AddressKind kind) => HasCLReader (AddressOrAlias kind) where   getReader =-    Opt.str <&> \addrOrAlias ->+    Opt.str >>= \addrOrAlias ->       case parseAddress addrOrAlias of-        Right addr -> AddressResolved addr-        Left _ -> AddressAlias (Alias addrOrAlias)+        Right (MkAddress (addr :: KindedAddress kind')) ->+          case eqI @kind @kind' \\ addressKindSanity addr of+            Just Refl -> pure $ AddressResolved addr+            Nothing -> Opt.readerError $ pretty $ nameF "Unexpected address kind" $+              "expected " +| demote @kind |+ " address, but got " +| addr |+ ""+        Left _ -> pure $ AddressAlias (mkAlias addrOrAlias)   getMetavar = "ADDRESS OR ALIAS" -instance Buildable AddressOrAlias where+instance Buildable (AddressOrAlias kind) where   build = \case     AddressResolved addr -> build addr     AddressAlias alias -> build alias++-- | Convenience type synonym.+type ImplicitAddressOrAlias = AddressOrAlias 'AddressKindImplicit++-- | Convenience type synonym.+type ContractAddressOrAlias = AddressOrAlias 'AddressKindContract++-- | Existential over 'AddressOrAlias'.+data SomeAddressOrAlias = forall kind. SomeAddressOrAlias (AddressOrAlias kind)++instance Buildable SomeAddressOrAlias where+  build (SomeAddressOrAlias x) = build x++deriving stock instance Show SomeAddressOrAlias

@@ -0,0 +1,33 @@+-- SPDX-FileCopyrightText: 2022 Oxhead Alpha+-- SPDX-License-Identifier: LicenseRef-MIT-OA++-- NB: 'genSingletonsType' creates some unused synonyms and GHC complains. To+-- minimize the impact of this option, this is in a separate module.+{-# OPTIONS_GHC -Wno-unused-top-binds #-}++-- | Address kinds.+module Morley.Tezos.Address.Kinds+  ( AddressKind(..)+  , SingAddressKind(..)+  ) where++import Fmt (Buildable(..))++import Morley.Util.Sing++-- | Address "kind"+data AddressKind+  = AddressKindImplicit+  -- ^ an implicit address, @tz1@-@tz3@+  | AddressKindContract+  -- ^ a contract address, @KT1@+  | AddressKindTxRollup+  -- ^ a transaction rollup address, @txr1@++instance Buildable AddressKind where+  build = \case+    AddressKindImplicit -> "implicit"+    AddressKindContract -> "contract"+    AddressKindTxRollup -> "transaction rollup"++genSingletonsType ''AddressKind

@@ -84,6 +84,7 @@   , hashLengthBytes   , formatSecretKey   , parseSecretKey+  , decodeKeyHash    -- * Hashing   , hashKey@@ -110,9 +111,10 @@   , decodeBase58CheckWithPrefix   , keyDecoders   , keyHashDecoders-  , allHashTags+  , AllHashTags(..)   ) where +import Control.Monad.Except (throwError) import Crypto.Random (MonadRandom) import Data.Aeson (FromJSON(..), FromJSONKey, ToJSON(..), ToJSONKey) import Data.Aeson qualified as Aeson@@ -123,6 +125,7 @@ import Data.ByteString qualified as BS import Data.ByteString.Lazy qualified as LBS import Data.Text qualified as T+import Data.Text.Internal.Builder (Builder) import Fmt (Buildable, build, hexF, pretty) import Instances.TH.Lift () import Language.Haskell.TH.Syntax (Lift)@@ -382,10 +385,8 @@     ])  parsePublicKeyRaw :: ByteString -> Either Text PublicKey-parsePublicKeyRaw ba =-  case Get.runGetOrFail (decodeWithTag "key" keyDecoders) (LBS.fromStrict ba) of-    Right (_, _, result) -> Right result-    Left (_, _, err) -> Left (toText err)+parsePublicKeyRaw ba = bimap (toText . view _3) (view _3) $+  Get.runGetOrFail (decodeWithTag "key" keyDecoders) (LBS.fromStrict ba)  formatSignature :: Signature -> Text formatSignature = \case@@ -469,12 +470,12 @@ instance ToJSONKey (Hash kind) where   toJSONKey = AesonTypes.toJSONKeyText formatHash -instance AllTags kind => FromJSON (Hash kind) where+instance AllHashTags kind => FromJSON (Hash kind) where   parseJSON =     Aeson.withText "Hash" $     either (fail . pretty) pure . parseHash -instance AllTags kind => FromJSONKey (Hash kind) where+instance AllHashTags kind => FromJSONKey (Hash kind) where   fromJSONKey =     AesonTypes.FromJSONKeyTextParser $     either (fail . pretty) pure . parseHash@@ -487,19 +488,19 @@ type KeyHashTag = HashTag 'HashKindPublicKey  -- | List all 'HashTag's for a given 'HashKind'.-class AllTags kind where+class AllHashTags kind where   allHashTags :: NonEmpty (HashTag kind) -instance AllTags 'HashKindPublicKey where+instance AllHashTags 'HashKindPublicKey where   allHashTags = HashEd25519 :| [HashSecp256k1, HashP256] -instance AllTags 'HashKindContract where+instance AllHashTags 'HashKindContract where   allHashTags = pure HashContract -instance AllTags 'HashKindL2PublicKey where+instance AllHashTags 'HashKindL2PublicKey where   allHashTags = pure HashBLS -instance AllTags 'HashKindTxRollup where+instance AllHashTags 'HashKindTxRollup where   allHashTags = pure HashTXR  -- | Blake2b_160 hash of something.@@ -550,7 +551,7 @@   build = build . formatHash  parseHash-  :: AllTags kind+  :: AllHashTags kind   => Text   -> Either CryptoParseError (Hash kind) parseHash txt =@@ -565,24 +566,25 @@    in firstRight $ map parse allHashTags +parseKeyHashHelper+  :: Int+  -> Builder+  -> ExceptT CryptoParseError Get.Get a+  -> ByteString+  -> Either CryptoParseError a+parseKeyHashHelper expectedLength name decoder ba+  | BS.length ba /= expectedLength+  = Left $ CryptoParseUnexpectedLength name (BS.length ba)+  | otherwise+  = either (Left . CryptoParseBinaryError . toText . view _3) (view _3)+  $ flip Get.runGetOrFail (LBS.fromStrict ba) $ runExceptT decoder+ parseKeyHashRaw :: ByteString -> Either CryptoParseError KeyHash-parseKeyHashRaw ba =-  if (BS.length ba - 1 == hashLengthBytes) then-    case Get.runGetOrFail (decodeWithTag "key_hash" keyHashDecoders) (LBS.fromStrict ba) of-      Right (_, _, result) -> Right result-      Left (_, _, err) -> Left $ CryptoParseBinaryError (toText err)-  else-    Left $ CryptoParseUnexpectedLength "key_hash" (BS.length ba)+parseKeyHashRaw = parseKeyHashHelper (hashLengthBytes + 1) "key_hash" decodeKeyHash  parseKeyHashL2Raw :: ByteString -> Either CryptoParseError KeyHashL2-parseKeyHashL2Raw ba =-  if (BS.length ba == hashLengthBytes) then-    case Get.runGetOrFail (Hash HashBLS <$> getByteStringCopy hashLengthBytes)-          (LBS.fromStrict ba) of-      Right (_, _, result) -> Right result-      Left (_, _, err) -> Left $ CryptoParseBinaryError (toText err)-  else-    Left $ CryptoParseUnexpectedLength "tx_rollup_l2_address" (BS.length ba)+parseKeyHashL2Raw = parseKeyHashHelper hashLengthBytes "tx_rollup_l2_address" $+  lift $ Hash HashBLS <$> getByteStringCopy hashLengthBytes  -- | Magic constants used by Tezos to encode hashes with proper prefixes. hashTagBytes :: HashTag kind -> ByteString@@ -601,7 +603,7 @@     HashTXR -> "\001\128\120\031"     -- https://gitlab.com/tezos/tezos/-/blob/0ca82c9dc361a6f223e81221c86bdb95d1a8d91c/src/proto_014_PtKathma/lib_protocol/tx_rollup_prefixes.ml#L35 -instance AllTags kind => HasCLReader (Hash kind) where+instance AllHashTags kind => HasCLReader (Hash kind) where   getReader = eitherReader (first pretty . parseHash . toText)   getMetavar = "KEY_HASH" @@ -615,11 +617,15 @@       (fmap PublicKeyP256 . P256.mkPublicKey)   ] -keyHashDecoders :: [TaggedDecoder KeyHash]+keyHashDecoders :: (Monad (t Get.Get), MonadTrans t) => [TaggedDecoderM t KeyHash] keyHashDecoders =-  [ 0x00 #: Hash HashEd25519 <$> getPayload-  , 0x01 #: Hash HashSecp256k1 <$> getPayload-  , 0x02 #: Hash HashP256 <$> getPayload+  [ 0x00 ##: Hash HashEd25519 <$> getPayload+  , 0x01 ##: Hash HashSecp256k1 <$> getPayload+  , 0x02 ##: Hash HashP256 <$> getPayload   ]   where-    getPayload = getByteStringCopy hashLengthBytes+    getPayload = lift $ getByteStringCopy hashLengthBytes++decodeKeyHash :: ExceptT CryptoParseError Get.Get KeyHash+decodeKeyHash =+  decodeWithTagM "key_hash" (throwError . CryptoParseWrongTag . BS.singleton) keyHashDecoders

@@ -0,0 +1,63 @@+-- SPDX-FileCopyrightText: 2022 Oxhead Alpha+-- SPDX-License-Identifier: LicenseRef-MIT-OA++module Morley.Util.Bimap+  ( Bimap(..)+  , empty+    -- * Optics+  , flipped+  ) where++import Prelude hiding (empty)++import Control.Lens (At(..), Index, Iso, IxValue, Ixed(..), iso)+import Data.Aeson (FromJSON(..), ToJSON(..))+import Data.Bimap qualified as Bimap+import Data.Coerce (coerce)+import GHC.Exts (IsList)++newtype Bimap a b = Bimap { unBimap :: Bimap.Bimap a b }+  deriving newtype (Show, Eq, Ord, IsList)++empty :: Bimap a b+empty = coerce Bimap.empty++type instance Index (Bimap k _) = k+type instance IxValue (Bimap _ v) = v++-- | Left-biased 'Ixed' instance.+-- It assumes the left value @a@ is the key (just like the @Ix (Map k v)@ instance).+--+-- To flip this assumption, use the 'flipped' optic.+instance (Ord k, Ord v) => Ixed (Bimap k v) where+  ix :: k -> Traversal' (Bimap k v) v+  ix k handler (Bimap bmap) =+    case Bimap.lookup k bmap of+     Just v -> handler v <&> \v' -> Bimap $ Bimap.insert k v' bmap+     Nothing -> pure $ Bimap bmap++-- | Left-biased 'At' instance.+-- It assumes the left value @a@ is the key (just like the @At (Map k v)@ instance).+--+-- To flip this assumption, use the 'flipped' optic.+instance (Ord k, Ord v) => At (Bimap k v) where+  at :: k -> Lens' (Bimap k v) (Maybe v)+  at k handler (Bimap bmap) =+    handler currentValueMaybe <&> \newValueMaybe ->+      Bimap $+        case (currentValueMaybe, newValueMaybe) of+          (Nothing, Nothing) -> bmap+          (Just _, Nothing) -> Bimap.delete k bmap+          (_, Just newValue) -> Bimap.insert k newValue bmap+    where+      currentValueMaybe = Bimap.lookup k bmap++-- | Isomorphism between @Bimap a b@ and @Bimap b a@.+flipped :: Iso (Bimap a1 b1) (Bimap a2 b2) (Bimap b1 a1) (Bimap b2 a2)+flipped = iso (coerce Bimap.twist) (coerce Bimap.twist)++instance (Ord a, Ord b, FromJSON a, FromJSON b) => FromJSON (Bimap a b) where+  parseJSON = fmap (Bimap . Bimap.fromList) . parseJSON++instance (ToJSON a, ToJSON b) => ToJSON (Bimap a b) where+  toJSON = toJSON . Bimap.toList . unBimap

@@ -7,10 +7,13 @@   ( UnpackError (..)   , ensureEnd   , launchGet-  , TaggedDecoder(..)+  , TaggedDecoder+  , TaggedDecoderM(..)   , (#:)+  , (##:)   , decodeBytesLike   , decodeWithTag+  , decodeWithTagM   , getByteStringCopy   , getRemainingByteStringCopy   , unknownTag@@ -54,19 +57,27 @@     Left (_remainder, _offset, err) -> Left . UnpackError $ toText err     Right (_remainder, _offset, res) -> Right res --- | Describes how 'decodeWithTag' should decode tag-dependent data.+-- | Specialization of 'TaggedDecoderM' to 'IdentityT' transformer.+type TaggedDecoder a = TaggedDecoderM IdentityT a++-- | Describes how 'decodeWithTagM' should decode tag-dependent data. -- We expect bytes of such structure: 'tdTag' followed by a bytestring -- which will be parsed with 'tdDecoder'.-data TaggedDecoder a = TaggedDecoder+data TaggedDecoderM t a = TaggedDecoder   { tdTag :: Word8-  , tdDecoder :: Get a+  , tdDecoder :: t Get a   } --- | Alias for 'TaggedDecoder' constructor.+-- | Alias for v'TaggedDecoder' constructor specialized to 'Get' (#:) :: Word8 -> Get a -> TaggedDecoder a-(#:) = TaggedDecoder+(#:) t = TaggedDecoder t . lift infixr 0 #: +-- | Alias for v'TaggedDecoder' constructor.+(##:) :: Word8 -> t Get a -> TaggedDecoderM t a+(##:) = TaggedDecoder+infixr 0 ##:+ -- | Get a bytestring of the given length leaving no references to the -- original data in serialized form. getByteStringCopy :: Int -> Get ByteString@@ -92,14 +103,30 @@ unknownTag desc tag =   fail . fmt $ "Unknown " <> build desc <> " tag: 0x" <> hexF tag --- Common decoder for the case when packed data starts with a tag (1--- byte) that specifies how to decode remaining data.+-- | Common decoder for the case when packed data starts with a tag (1 byte)+-- that specifies how to decode remaining data.+--+-- This is a version of 'decodeWithTagM' specialized to naked 'Get' monad. decodeWithTag :: String -> [TaggedDecoder a] -> Get a-decodeWithTag what decoders = do-  tag <- Get.label (what <> " tag") Get.getWord8+decodeWithTag what decoders =+  runIdentityT $ decodeWithTagM what (lift . unknownTag what) decoders++-- | Common decoder for the case when packed data starts with a tag (1 byte)+-- that specifies how to decode remaining data.+--+-- This is a general version of 'decodeWithTag' that allows 'Get' to be wrapped+-- in a monad transformer.+decodeWithTagM+  :: (MonadTrans t, Monad (t Get))+  => String+  -> (Word8 -> t Get a)+  -> [TaggedDecoderM t a]+  -> t Get a+decodeWithTagM what unknownTagFail decoders = do+  tag <- lift $ Get.label (what <> " tag") Get.getWord8   -- Number of decoders is usually small, so linear runtime lookup should be ok.   case List.find ((tag ==) . tdTag) decoders of-    Nothing -> unknownTag what tag+    Nothing -> unknownTagFail tag     Just TaggedDecoder{..} -> tdDecoder  decodeBytesLike

@@ -62,6 +62,7 @@  unescape :: String -> Q String unescape ('\\':'#':xs) = ('\\':) . ('#':) <$> unescape xs+unescape ('\\':'&':xs) = unescape xs unescape xs@('\\':c:cs) = case readP_to_S lexChar xs of   (ch, rest):_ -> (ch :) <$> unescape rest   [] -> do

@@ -0,0 +1,98 @@+-- SPDX-FileCopyrightText: 2022 Oxhead Alpha+-- SPDX-License-Identifier: LicenseRef-MIT-OA++-- | A poor man's extensible reader effects via nested 'ReaderT'.+module Morley.Util.MultiReader+  ( MultiReaderT+  , MonadMultiReaderT+  , ChangeMultiReaderBase+  , asks'+  , ask'+  , local'+  , mapMultiReaderT+  ) where++import Control.Monad.Reader (mapReaderT)+import GHC.TypeLits (ErrorMessage(..), TypeError)++import Morley.Util.Peano++-- | Convenience type family to build a stack of multiple 'ReaderT'.+type family MultiReaderT (xs :: [Type]) (m :: Type -> Type) :: Type -> Type where+  MultiReaderT (x ': xs) m = ReaderT x (MultiReaderT xs m)+  MultiReaderT '[] m = m++-- | Convenience constraint synonym.+--+-- Required for `asks'`, `ask'`, `local'` and 'mapMultiReaderT'+type MonadMultiReaderT m base =+  (m ~ MultiReaderT (MultiReaderIso m) base, MonadMultiReaderMap (MultiReaderIso m))++-- | Replace the base monad for a nested 'ReaderT' stack.+type ChangeMultiReaderBase m newBase = MultiReaderT (MultiReaderIso m) newBase++-- | Find the index of the first occurrence of the first argument in the second+-- argument as a Peano number.+--+-- Essentially a type-level version of 'find'.+--+-- Raises a type error if the element is not found.+type family MultiReaderDepth (r :: Type) (rs :: [Type]) :: Peano where+  MultiReaderDepth r (r ': _) = 'Z+  MultiReaderDepth r (_ ': rs) = 'S (MultiReaderDepth r rs)+  MultiReaderDepth r '[] = TypeError (+    'Text "MultiReaderT does not have a reader environment" ':$$:+    'ShowType r ':$$: 'Text "anywhere in the stack."+    )++-- | Given a transformer stack of nested 'ReaderT', get a list of environments.+-- This type family is essentially a witness of isomorphism between a stack of+-- 'ReaderT' and a type-level list of reader environments.+--+-- This is useful because 'MultiReaderT' can't have an injectivity annotation.+type family MultiReaderIso (m :: Type -> Type) :: [Type] where+  MultiReaderIso (ReaderT r m) = r ': MultiReaderIso m+  MultiReaderIso _ = '[]++-- | Typeclass implementing versions of 'ask' and 'local' that aren't+-- constrained by a functional dependency.+class (Monad m, n ~ MultiReaderDepth r (MultiReaderIso m))+  => MultiReader (n :: Peano) r m where+  -- | Unconstrained version of 'ask'. Lifts the appropriate number of times+  -- depending on the type @r@.+  ask' :: m r++  -- | Unconstrained version of 'local'. Maps the appropriate number of times+  -- depending on the type @r@.+  local' :: (r -> r) -> m a -> m a++instance (Monad m) => MultiReader 'Z x (ReaderT x m) where+  ask' = ask+  local' = local++instance+  ( MultiReader n r m, Monad m, 'S n ~ MultiReaderDepth r (x ': MultiReaderIso m) )+  => MultiReader ('S n) r (ReaderT x m) where+  ask' = lift ask'+  local' = mapReaderT . local'++-- | Class implementing 'mapReaderT' over a stack of 'ReaderT'.+class MonadMultiReaderMap xs where+  -- | 'mapReaderT', only it maps over the whole nested 'ReaderT' stack, and not+  -- just one level.+  mapMultiReaderT+    :: ( m' ~ MultiReaderT xs m+       , n' ~ MultiReaderT xs n+       , xs ~ MultiReaderIso m'+       )+    => (m a -> n b) -> m' a -> n' b++instance MonadMultiReaderMap '[] where+  mapMultiReaderT f = f++instance (MonadMultiReaderMap xs) => MonadMultiReaderMap (x ': xs) where+  mapMultiReaderT f = mapReaderT (mapMultiReaderT f)++-- | Unconstrained version of 'asks'. @asks' f = fmap f ask'@.+asks' :: forall m r (a :: Type) n. MultiReader n r m => (r -> a) -> m a+asks' f = f <$> ask'

@@ -95,7 +95,7 @@ import Unsafe.Coerce (unsafeCoerce)  import Morley.Util.Sing (genSingletonsType)-import Morley.Util.Type (If, MockableConstraint(..))+import Morley.Util.Type (FailUnless, MockableConstraint(..))  -- This is very obviously a false positive. {-# ANN module ("HLint: ignore Use 'natVal' from Universum" :: Text) #-}@@ -130,7 +130,7 @@ -- isomorphism) type IsoNatPeano (n :: GHC.Nat) (p :: Peano) = (n ~ FromPeano p, ToPeano n ~ p) --- | A synonym for @SingI (ToPeano n)@. Essentialy requires that we can construct a 'Peano'+-- | A synonym for @SingI (ToPeano n)@. Essentially requires that we can construct a 'Peano' -- singleton for a given 'Nat' type SingIPeano (n :: GHC.Nat) = SingI (ToPeano n) @@ -327,15 +327,14 @@ -- type family is internal. type family RequireLongerThan' (l :: [k]) (a :: Nat) :: Constraint where   RequireLongerThan' l a =-    If (IsLongerThan l a)-       (() :: Constraint)-       (TypeError-          ('Text "Stack element #" ':<>: 'ShowType (FromPeano a) ':<>:-           'Text " is not accessible" ':$$:-           'Text "Current stack has size of only " ':<>:-           'ShowType (LengthWithTail l) ':<>:-           'Text ":" ':$$: 'ShowType l-           ))+    FailUnless+      (IsLongerThan l a)+      ('Text "Stack element #" ':<>: 'ShowType (FromPeano a) ':<>:+       'Text " is not accessible" ':$$:+       'Text "Current stack has size of only " ':<>:+       'ShowType (LengthWithTail l) ':<>:+       'Text ":" ':$$: 'ShowType l+       )  class (RequireLongerThan' l a, LongerThan l a) =>   RequireLongerThan (l :: [k]) (a :: Peano)@@ -349,14 +348,13 @@ -- GHC and also producess good error messages. type family RequireLongerOrSameLength' (l :: [k]) (a :: Peano) :: Constraint where   RequireLongerOrSameLength' l a =-    If (IsLongerOrSameLength l a)-       (() :: Constraint)-       (TypeError-          ('Text "Expected stack with length >= " ':<>: 'ShowType (FromPeano a) ':$$:-           'Text "Current stack has size of only " ':<>:-           'ShowType (LengthWithTail l) ':<>:-           'Text ":" ':$$: 'ShowType l-           ))+    FailUnless+      (IsLongerOrSameLength l a)+      ('Text "Expected stack with length >= " ':<>: 'ShowType (FromPeano a) ':$$:+       'Text "Current stack has size of only " ':<>:+       'ShowType (LengthWithTail l) ':<>:+       'Text ":" ':$$: 'ShowType l+       )  -- | We can have -- `RequireLongerOrSameLength = (RequireLongerOrSameLength' l a, LongerOrSameLength l a)`,

@@ -8,7 +8,8 @@   , eqParamSing3   , eqParamMixed3   , castSing-  , SingI1(..)+  , SingIOne+  , withSingIOne   , genSingletonsType   ) where @@ -115,9 +116,16 @@   Refl <- sing @a `decideEquality` sing @b   return ca --- Second-order analogue of 'SingI'-class SingI1 f where-  withSingI1 :: forall x r. SingI x => (SingI (f x) => r) -> r+-- | A second-order analogue of 'SingI'. This serves the same purpose as the+-- @"Data.Singletons".'Data.Singletons.SingIOne'@ class. However, the @singletons@+-- version requires a separate instance for each type in order to support GHC+-- versions that don't offer @QuantifiedConstraints@. We only need one instance+-- for all types.+class (forall x. SingI x => SingI (f x)) => SingIOne f+instance (forall x. SingI x => SingI (f x)) => SingIOne f++withSingIOne :: forall f x r. (SingIOne f, SingI x) => (SingI (f x) => r) -> r+withSingIOne f = f  -- | Helper function to generate 'SingI' and 'Data.Singletons.TH.SDecide' instances -- using @Sing@ as prefix for the type names and @S@ for constructors'.

@@ -12,9 +12,16 @@   , IsElem   , type (/)   , type (//)+  , AssertTypesEqual+  , FailUnlessEqual+  , FailUnlessEqualElse   , Guard   , FailWhen+  , FailWhenElse+  , FailWhenElsePoly   , FailUnless+  , FailUnlessElse+  , FailUnlessElsePoly   , failUnlessEvi   , failWhenEvi   , AllUnique@@ -29,8 +36,6 @@   , Some1 (..)   , recordToSomeList -  , reifyTypeEquality-   , ConcatListOfTypesAssociativity   , listOfTypesConcatAssociativityAxiom @@ -41,6 +46,7 @@   ) where  import Data.Constraint (Dict(..), (:-)(..), (\\))+import Data.Eq.Singletons (DefaultEq) import Data.Singletons (SingI(sing)) import Data.Type.Bool (If, Not, type (&&)) import Data.Type.Equality (type (==))@@ -52,6 +58,9 @@ import Prelude.Singletons (SList(..)) import Unsafe.Coerce (unsafeCoerce) +-- $setup+-- >>> import GHC.TypeLits (ErrorMessage (..))+ -- | Equality constraint in form of a typeclass. class a ~ b => IsEq a b instance a ~ b => IsEq a b@@ -76,13 +85,153 @@   Guard 'False _ = 'Nothing   Guard 'True a = 'Just a +-- | Constrain two types to be equal. If they are found not to be, produce+-- an error message. If they are shown to be equal, impose an additional+-- given constraint.+--+-- >>> :k! FailUnlessEqualElse Int Int ('Text "This should not result in a failure") ()+-- FailUnlessEqualElse Int Int ('Text "This should not result in a failure") () :: Constraint+-- = (() :: Constraint, Int ~ Int)+--+-- >>> :k! FailUnlessEqualElse Bool Int ('Text "This should result in a failure") ()+-- FailUnlessEqualElse Bool Int ('Text "This should result in a failure") () :: Constraint+-- = ((TypeError ...), Bool ~ Int)+--+-- the @~@ constraint might seem redundant, but, without it, GHC would reject+--+-- @+-- foo :: FailUnlessEqualElse a b MyError () => a -> b+-- foo = id+-- @+--+-- GHC needs to \"see\" the type equality @~@ in order to actually \"learn\"+-- something from a type family's result.+--+-- We use 'DefaultEq' here, rather than 'Data.Type.Equality.==', so this will+-- work with type variables known to be equal, even if nothing is known about+-- them concretely. For example, the following will compile:+--+-- @+-- foo :: FailUnlessEqualElse a b MyError () => a -> b+-- foo x = x+--+-- bar :: a -> a+-- bar = foo+-- @+--+-- If we used @(==)@, then bar would be rejected.+--+-- @(==)@ has its place (see the comments below it in "Data.Type.Equality")+-- but I don't think it has anything to offer us here. In particular, the equality+-- constraint we bundle up seems to win us all the reasoning power that @(==)@ would+-- provide and more. The following adaptation of the example in the+-- @Data.Type.Equality@ comments compiles:+--+-- @+-- foo :: FailUnlessEqualElse (Maybe a) (Maybe b) ('Text "yo") ()+--          :- FailUnlessEqualElse a b ('Text "heya") ()+-- foo = Sub Dict+-- @+--+-- In this example, the entire consequent follows from the equality constraint+-- in the antecedent; the `FailUnlessElsePoly` part of it is irrelevant, so we+-- don't need to be able to reason from it. If we /were/ reasoning solely using+-- @(==)@, @foo@ would be rejected because the error messages are different.+type FailUnlessEqualElse :: forall k. k -> k -> ErrorMessage -> Constraint -> Constraint+type FailUnlessEqualElse a b err els =+  ( FailUnlessElsePoly (a `DefaultEq` b) err els+  , a ~ b+  )++-- | Constrain two types to be equal, and produce an error message if+-- they are found not to be.+--+-- >>> :k! FailUnlessEqual Int Int ('Text "This should not result in a failure")+-- FailUnlessEqual Int Int ('Text "This should not result in a failure") :: Constraint+-- = (() :: Constraint, Int ~ Int)+--+-- >>> :k! FailUnlessEqual Bool Int ('Text "This should result in a failure")+-- FailUnlessEqual Bool Int ('Text "This should result in a failure") :: Constraint+-- = ((TypeError ...), Bool ~ Int)+type FailUnlessEqual :: forall k. k -> k -> ErrorMessage -> Constraint+type FailUnlessEqual a b err = FailUnlessEqualElse a b err ()++-- | An old name for 'FailUnlessEqual'.+type AssertTypesEqual :: forall k. k -> k -> ErrorMessage -> Constraint+type AssertTypesEqual a b err = FailUnlessEqual a b err++-- | A version of 'FailWhenElsePoly' that imposes an equality constraint on its+-- 'Bool' argument.+type FailWhenElse :: Bool -> ErrorMessage -> Constraint -> Constraint+type FailWhenElse cond msg els = FailUnlessEqualElse cond 'False msg els+ -- | Fail with given error if the condition does not hold.-type family FailUnless (cond :: Bool) (msg :: ErrorMessage) :: Constraint where-  FailUnless 'True _ = ()-  FailUnless 'False msg = TypeError msg+-- Otherwise, return the third argument.+--+-- There is a subtle difference between @FailWhenElsePoly@ and the+-- following type definition:+--+-- @+-- type FailWhenElsePolyAlternative cond msg els =+--   If cond+--      (TypeError msg)+--      els+-- @+--+-- If @cond@ cannot be fully reduced (e.g., it's a stuck type family+-- application or an ambiguous type) then:+--+-- * @FailWhenElsePoly@ will state that the constraint cannot be deduced (and+--   this error message will be suppressed if there are also custom type+--   errors).+--+-- * @FailWhenElsePolyAlternative@ will fail with the given error message,+--   @err@.+--+-- For example:+--+-- @+-- -- Partial function+-- type family IsZero (n :: Peano) :: Bool where+--   IsZero ('S _) = 'False+--+-- f1 :: (IsZero n ~ 'True, FailWhenElsePoly (IsZero n) ('Text "Expected zero") (() :: Constraint)) => ()+-- f1 = ()+--+-- f1 :: (IsZero n ~ 'True, FailWhenElsePolyAlternative (IsZero n) ('Text "Expected zero") (() :: Constraint)) => ()+-- f1 = ()+--+-- f1res == f1 @'Z+-- --  • Couldn't match type ‘IsZero 'Z’ with ‘'True’+--+-- f2res == f2 @'Z+-- --  • Expected zero+-- @+--+-- As you can see, the error message in @f2res@ is misleading (because the type argument+-- actually _is_ zero), so it's preferable to fail with the standard GHC error message.+type FailWhenElsePoly :: forall k. Bool -> ErrorMessage -> k -> k+type family FailWhenElsePoly cond msg els where+  FailWhenElsePoly 'True msg _els = TypeError msg+  FailWhenElsePoly 'False _ els = els +-- | A version of 'FailUnlessElsePoly' that imposes an equality constraint on its+-- 'Bool' argument.+type FailUnlessElse :: Bool -> ErrorMessage -> Constraint -> Constraint+type FailUnlessElse b msg els = FailWhenElse (Not b) msg els++-- | Fail with given error if the condition does not hold. Otherwise,+-- return the third argument.+type FailUnlessElsePoly :: forall k. Bool -> ErrorMessage -> k -> k+type FailUnlessElsePoly b e k = FailWhenElsePoly (Not b) e k++-- | Fail with given error if the condition does not hold.+type FailUnless :: Bool -> ErrorMessage -> Constraint+type FailUnless cond msg = FailUnlessElse cond msg ()+ -- | Fail with given error if the condition holds.-type FailWhen cond msg = FailUnless (Not cond) msg+type FailWhen :: Bool -> ErrorMessage -> Constraint+type FailWhen cond msg = FailWhenElse cond msg ()  -- | A natural conclusion from the fact that an error has not occurred. failUnlessEvi :: forall cond msg. FailUnless cond msg :- (cond ~ 'True)@@ -97,15 +246,15 @@  type RequireAllUnique desc l = RequireAllUnique' desc l l -type family RequireAllUnique' (desc :: Symbol) (l :: [k]) (origL ::[k]) :: Constraint where+type family RequireAllUnique' (desc :: Symbol) (l :: [k]) (origL :: [k]) :: Constraint where   RequireAllUnique' _ '[] _ = ()   RequireAllUnique' desc (x : xs) origL =-    If (IsElem x xs)-       (TypeError ('Text "Duplicated " ':<>: 'Text desc ':<>: 'Text ":" ':$$:-                   'ShowType x ':$$:-                   'Text "Full list: " ':<>:-                   'ShowType origL-                  )+    FailWhenElse+       (IsElem x xs)+       ('Text "Duplicated " ':<>: 'Text desc ':<>: 'Text ":" ':$$:+        'ShowType x ':$$:+        'Text "Full list: " ':<>:+        'ShowType origL        )        (RequireAllUnique' desc xs origL) @@ -129,10 +278,6 @@  instance (c x, ReifyList c xs) => ReifyList c (x ': xs) where   reifyList reifyElem = reifyElem (Proxy @x) : reifyList @_ @c @xs reifyElem---- | Reify type equality from boolean equality.-reifyTypeEquality :: forall a b x. (a == b) ~ 'True => (a ~ b => x) -> x-reifyTypeEquality x = x \\ unsafeProvideConstraint @(a ~ b)  -- | Similar to @SingI []@, but does not require individual elements to be also -- instance of @SingI@.

@@ -15,87 +15,15 @@   , TypeError   , ErrorMessage (..) -  , TypeErrorUnless   , AssertTypesEqual   ) where -import Data.Type.Equality (type (==)) import GHC.TypeLits (AppendSymbol, ErrorMessage(..), KnownSymbol, Symbol, TypeError, symbolVal) +import Morley.Util.Type (AssertTypesEqual)+ symbolValT :: forall s. KnownSymbol s => Proxy s -> Text symbolValT = toText . symbolVal  symbolValT' :: forall s. KnownSymbol s => Text symbolValT' = symbolValT (Proxy @s)---- | Conditional type error.------ There is a very subtle difference between 'TypeErrorUnless' and the following type family:------ > type family TypeErrorUnlessAlternative (cond :: Bool) (err :: ErrorMessage) :: Constraint where--- >   TypeErrorUnlessAlternative cond err =--- >     ( If cond--- >         (() :: Constraint)--- >         (TypeError err)--- >     , cond ~ 'True--- >     )------ If @cond@ cannot be fully reduced (e.g. it's a stuck type family), then:------ * @TypeErrorUnless@ will state that the constraint cannot be deduced.--- * @TypeErrorUnlessAlternative@ will fail with the given error message @err@.------ For example:------ > -- Partial function--- > type family IsZero (n :: Peano) :: Bool where--- >   IsZero ('S _) = 'False--- >--- > f1 :: TypeErrorUnless (IsZero n) ('Text "Expected zero") => ()--- > f1 = ()--- >--- > f2 :: TypeErrorUnlessAlternative (IsZero n) ('Text "Expected zero") => ()--- > f2 = ()--- >--- >--- > f1res = f1 @'Z--- > -- • Couldn't match type ‘IsZero 'Z’ with ‘'True’--- >--- > f2res = f2 @'Z--- > -- • Expected zero------ As you can see, the error message in @f2res@ is misleading (because the type argument--- actually _is_ zero), so it's preferable to fail with the standard GHC error message.-type TypeErrorUnless (cond :: Bool) (err :: ErrorMessage) =-  ( TypeErrorUnlessHelper cond err-  -- Note: the '~' constraint below might seem redundant, but, without it,-  -- GHC would warn that the following pattern match is not exhaustive (even though it is):-  ---  -- > f :: TypeErrorUnless (n >= ToPeano 2) "some err msg" => Sing n -> ()-  -- > f = \case-  -- >   SS (SS SZ) -> ()-  -- >   SS (SS _) -> ()-  ---  -- GHC needs to "see" the type equality '~' in order to actually "learn" something from a-  -- type family's result.-  , cond ~ 'True-  )--type family TypeErrorUnlessHelper (cond :: Bool) (err :: ErrorMessage) :: Constraint where-  TypeErrorUnlessHelper 'True _ = ()-  TypeErrorUnlessHelper 'False err = TypeError err---- | Condition Error helper to check if two types are equal------ >>> :k! AssertTypesEqual Int Int ('Text "This should not result in a failure")--- AssertTypesEqual Int Int ('Text "This should not result in a failure") :: Constraint--- = (() :: Constraint, Int ~ Int)------ >>> :k! AssertTypesEqual Bool Int ('Text "This should result in a failure")--- AssertTypesEqual Bool Int ('Text "This should result in a failure") :: Constraint--- = ((TypeError ...), Bool ~ Int)-type AssertTypesEqual a b (err :: ErrorMessage) =-  ( TypeErrorUnlessHelper (a == b) err-  -- The reasons for the constraint below are the same as those in @TypeErrorUnless@ constructor-  , a ~ b-  )