diff --git a/CHANGES.md b/CHANGES.md
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,3 +1,17 @@
+1.6.0
+=====
+* [!323](https://gitlab.com/morley-framework/morley/-/merge_requests/323)
+  Add `parseSecretKey` which allows parsing all types of `SecretKey`.
+* [!537](https://gitlab.com/morley-framework/morley/-/merge_requests/537)
+  Permit `SELF %default` instruction.
+* [!522](https://gitlab.com/morley-framework/morley/-/merge_requests/522)
+  + allow calling the interpreter with a typed transfer parameter and
+  avoid unnecessary typechecking.
+* [!495](https://gitlab.com/morley-framework/morley/-/merge_requests/495)
+  Add source location to typed `Instr` AST.
+* [!521](https://gitlab.com/morley-framework/morley/-/merge_requests/521)
+  Document generater can now generate table of contents.
+
 1.5.0
 =====
 * [!509](https://gitlab.com/morley-framework/morley/-/merge_requests/509)
diff --git a/morley.cabal b/morley.cabal
--- a/morley.cabal
+++ b/morley.cabal
@@ -4,10 +4,10 @@
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: baa867af7f9b3c6cbf4de3c7d9746427b24b2cca6f9c9cb9025ad098b40ef60e
+-- hash: e9b0b7602aa9e3fa21558643cd50b0071708c46a024ce35930b662fbec21b73e
 
 name:           morley
-version:        1.5.0
+version:        1.6.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
diff --git a/src/Michelson/Doc.hs b/src/Michelson/Doc.hs
--- a/src/Michelson/Doc.hs
+++ b/src/Michelson/Doc.hs
@@ -11,7 +11,9 @@
   , docItemPosition
   , DocItemId (..)
   , DocItemPlacementKind (..)
+  , DocItemPos (..)
   , DocItemRef (..)
+  , DocItemReferencedKind
   , DocSectionNameStyle (..)
   , SomeDocItem (..)
   , SomeDocDefinitionItem (..)
@@ -30,8 +32,10 @@
   , docItemToBlock
   , lookupDocBlockSection
   , contractDocToMarkdown
+  , contractDocToToc
   , docGroupContent
   , docDefinitionRef
+  , mdTocFromRef
 
   , DGeneralInfoSection (..)
   , DName (..)
@@ -42,8 +46,11 @@
   , morleyRepoSettings
   , DComment (..)
   , DAnchor (..)
+  , DToc (..)
   ) where
 
+import Control.Lens.Cons (_head)
+import Data.Char (toLower)
 import qualified Data.Map as M
 import qualified Data.Map.Merge.Strict as M
 import qualified Data.Set as S
@@ -123,15 +130,20 @@
   type DocItemPlacement d :: DocItemPlacementKind
   type DocItemPlacement d = 'DocItemInlined
 
+  type DocItemReferenced d :: DocItemReferencedKind
+  type DocItemReferenced d = 'False
+
   -- | Defines a function which constructs an unique identifier of given doc item,
   -- if it has been decided to put the doc item into definitions section.
   --
   -- Identifier should be unique both among doc items of the same type and items
   -- of other types. Thus, consider using "typeId-contentId" pattern.
-  docItemRef :: d -> DocItemRef (DocItemPlacement d)
+  docItemRef :: d -> DocItemRef (DocItemPlacement d) (DocItemReferenced d)
   default docItemRef
-    :: (DocItemPlacement d ~ 'DocItemInlined)
-    => d -> DocItemRef (DocItemPlacement d)
+    :: ( DocItemPlacement d ~ 'DocItemInlined
+       , DocItemReferenced d ~ 'False
+       )
+    => d -> DocItemRef (DocItemPlacement d) (DocItemReferenced d)
   docItemRef _ = DocItemNoRef
 
   -- | Render given doc item to Markdown, preferably one line,
@@ -142,6 +154,10 @@
   -- headers thus delivering mess).
   docItemToMarkdown :: HeaderLevel -> d -> Markdown
 
+  -- | Render table of contents entry for given doc item to Markdown.
+  docItemToToc :: HeaderLevel -> d -> Markdown
+  docItemToToc _ _ = ""
+
   -- | All doc items which this doc item refers to.
   --
   -- They will automatically be put to definitions as soon as given doc item
@@ -161,8 +177,16 @@
     [] -> []
     docItems@(someDocItem : _) -> case docItemRef someDocItem of
       DocItemNoRef -> docItems
-      DocItemRef _ -> docItemsOrderById docItems
+      DocItemRef _ ->
+        docItemsOrderById docItems
+      DocItemRefInlined _ ->
+        docItems
 
+-- | Generate 'DToc' entry anchor from 'docItemRef'.
+mdTocFromRef :: (DocItem d, DocItemReferenced d ~ 'True) => HeaderLevel -> Markdown -> d -> Markdown
+mdTocFromRef lvl text d =
+  mdToc lvl text (toAnchor $ docItemRef d)
+
 -- | Get doc item position at term-level.
 docItemPosition :: forall d. DocItem d => DocItemPos
 docItemPosition = DocItemPos (docItemPos @d, show (typeRep $ Proxy @d))
@@ -174,6 +198,7 @@
   where
     manchor = case docItemRef d of
       DocItemRef docItemId -> mdAnchor docItemId
+      DocItemRefInlined docItemId -> mdAnchor docItemId
       DocItemNoRef -> ""
 
 -- | Order items by their 'docItemId'.
@@ -213,13 +238,17 @@
   | DocItemInDefinitions
     -- ^ Placed in dedicated definitions section; can later be referenced.
 
--- | Defines an identifier which given doc item can be referenced with.
-data DocItemRef (p :: DocItemPlacementKind) where
-  DocItemRef :: DocItemId -> DocItemRef 'DocItemInDefinitions
-  DocItemNoRef :: DocItemRef 'DocItemInlined
+-- | Type-level check whether or not a doc item can be referenced.
+type DocItemReferencedKind = Bool
 
-instance ToAnchor (DocItemRef 'DocItemInDefinitions) where
+data DocItemRef (p :: DocItemPlacementKind) (r :: DocItemReferencedKind) where
+  DocItemRef        :: DocItemId -> DocItemRef 'DocItemInDefinitions 'True
+  DocItemRefInlined :: DocItemId -> DocItemRef 'DocItemInlined 'True
+  DocItemNoRef      :: DocItemRef 'DocItemInlined 'False
+
+instance ToAnchor (DocItemRef d 'True) where
   toAnchor (DocItemRef ref) = toAnchor ref
+  toAnchor (DocItemRefInlined ref) = toAnchor ref
 
 -- | How to render section name.
 data DocSectionNameStyle
@@ -342,6 +371,24 @@
        then ""
        else sectionNameFull <> sectionDescFull <> content
 
+-- | Render a part of table of contents from 'DocBlock'.
+docBlockToToc :: HeaderLevel -> DocBlock -> Markdown
+docBlockToToc hl block =
+  mconcat $ M.elems block <&> \(DocSection items@((_ :: DocElem di) :| _)) ->
+    let sectionName = docItemSectionName @di
+        (sectionNameFull, headerLevelDelta) =
+          case sectionName of
+            Nothing -> ("", id)
+            Just "Table of contents" -> ("", id)
+            Just sn ->
+              (mdToc hl (build sn) (over _head toLower $ sn), nextHeaderLevel)
+        resItems = docItemsOrder $ map deItem (toList items)
+        content =
+          mconcat $ resItems <&> docItemToToc (headerLevelDelta hl)
+    in if null resItems
+       then ""
+       else sectionNameFull <> content
+
 -- | Lift a doc item to a block, be it atomic doc item or grouping one.
 docItemToBlockGeneral :: forall di. DocItem di => di -> Maybe SubDoc -> DocBlock
 docItemToBlockGeneral di msub =
@@ -372,6 +419,10 @@
 subDocToMarkdown :: HeaderLevel -> SubDoc -> Markdown
 subDocToMarkdown hl (SubDoc d) = docBlockToMarkdown hl d
 
+-- | Render documentation for 'SubDoc'.
+subDocToToc :: HeaderLevel -> SubDoc -> Markdown
+subDocToToc hl (SubDoc d) = docBlockToToc hl d
+
 -- | Keeps documentation gathered for some piece of contract code.
 --
 -- Used for building documentation of a contract.
@@ -426,6 +477,7 @@
         case docItemRef di of
           DocItemNoRef -> False
           DocItemRef docItemId -> docItemId `S.member` defs
+          DocItemRefInlined docItemId -> docItemId `S.member` defs
 
 instance Monoid ContractDoc where
   mempty = ContractDoc
@@ -448,6 +500,18 @@
     total = fmt (contents <> definitions)
   in LT.strip total <> "\n"
 
+contractDocToToc :: ContractDoc -> Markdown
+contractDocToToc ContractDoc{..} =
+  let
+    contents =
+      docBlockToToc (HeaderLevel 1) cdContents
+
+    definitions
+      | null cdDefinitions = ""
+      | otherwise = "\n**[Definitions](#definitions)**\n\n"
+          +| docBlockToToc (HeaderLevel 2) cdDefinitions
+  in contents <> definitions <> "\n"
+
 -- | A function which groups a piece of doc under one doc item.
 type DocGrouping = SubDoc -> SomeDocItem
 
@@ -479,6 +543,8 @@
   docItemSectionName = Nothing
   docItemToMarkdown lvl (DGeneralInfoSection subDoc) =
     subDocToMarkdown lvl subDoc
+  docItemToToc lvl (DGeneralInfoSection subDoc) =
+    subDocToToc lvl subDoc
 
 -- | Give a name to document block.
 data DName = DName Text SubDoc
@@ -489,6 +555,8 @@
   docItemToMarkdown lvl (DName name doc) =
     mdHeader lvl (build name) <>
     subDocToMarkdown (nextHeaderLevel lvl) doc
+  docItemToToc lvl (DName _ doc) =
+    subDocToToc (nextHeaderLevel lvl) doc
 
 -- | Description of something.
 data DDescription = DDescription Markdown
@@ -577,6 +645,18 @@
   docItemSectionName = Nothing
   docItemToMarkdown _ (DComment commentText) =
     "<!---\n" +| commentText |+ "\n-->"
+
+-- | @Table of contents@ to be inserted into the doc in an ad-hoc way.
+--
+-- It is not intended to be inserted manually. See 'attachToc' to understand
+-- how this works.
+--
+data DToc = DToc Markdown
+
+instance DocItem DToc where
+  docItemPos = 11
+  docItemSectionName = Just "Table of contents"
+  docItemToMarkdown _ (DToc toc) = toc
 
 -- | A hand-made anchor.
 data DAnchor = DAnchor Anchor
diff --git a/src/Michelson/Interpret.hs b/src/Michelson/Interpret.hs
--- a/src/Michelson/Interpret.hs
+++ b/src/Michelson/Interpret.hs
@@ -331,6 +331,7 @@
 -- | Function to interpret Michelson instruction(s) against given stack.
 runInstrImpl :: EvalM m => InstrRunner m -> InstrRunner m
 runInstrImpl runner (Seq i1 i2) r = runner i1 r >>= \r' -> runner i2 r'
+runInstrImpl runner (WithLoc _ i) r = runInstrImpl runner i r
 runInstrImpl runner (InstrWithNotes _ i) r = runner i r
 runInstrImpl runner (InstrWithVarNotes _ i) r = runner i r
 runInstrImpl runner (FrameInstr (_ :: Proxy s) i) r = do
@@ -381,7 +382,7 @@
 runInstrImpl _ UNIT r = pure $ VUnit :& r
 runInstrImpl runner (IF_NONE _bNone bJust) (VOption (Just a) :& r) = runner bJust (a :& r)
 runInstrImpl runner (IF_NONE bNone _bJust) (VOption Nothing :& r) = runner bNone r
-runInstrImpl _ PAIR (a :& b :& r) = pure $ VPair (a, b) :& r
+runInstrImpl _ (AnnPAIR{}) (a :& b :& r) = pure $ VPair (a, b) :& r
 runInstrImpl _ (AnnCAR _) (VPair (a, _b) :& r) = pure $ a :& r
 runInstrImpl _ (AnnCDR _) (VPair (_a, b) :& r) = pure $ b :& r
 runInstrImpl _ LEFT (a :& r) =
@@ -541,7 +542,7 @@
               -- context, therefore we generate dummy contract address with its own origination
               -- operation and counter set to 0.
               originationNonce
-  let resEpAddr = EpAddress resAddr def
+  let resEpAddr = EpAddress resAddr DefEpName
   let resOp = CreateContract originator (unwrapMbKeyHash mbKeyHash) m g ops
   pure $ VOp (OpCreateContract resOp)
       :& (VAddress resEpAddr)
@@ -565,10 +566,10 @@
 runInstrImpl _ HASH_KEY (VKey k :& r) = pure $ (VKeyHash $ hashKey k) :& r
 runInstrImpl _ SOURCE r = do
   ContractEnv{..} <- ask
-  pure $ (VAddress $ EpAddress ceSource def) :& r
+  pure $ (VAddress $ EpAddress ceSource DefEpName) :& r
 runInstrImpl _ SENDER r = do
   ContractEnv{..} <- ask
-  pure $ (VAddress $ EpAddress ceSender def) :& r
+  pure $ (VAddress $ EpAddress ceSender DefEpName) :& r
 runInstrImpl _ ADDRESS (VContract a sepc :& r) =
   pure $ (VAddress $ EpAddress a (sepcName sepc)) :& r
 runInstrImpl _ CHAIN_ID r = do
diff --git a/src/Michelson/Interpret/Pack.hs b/src/Michelson/Interpret/Pack.hs
--- a/src/Michelson/Interpret/Pack.hs
+++ b/src/Michelson/Interpret/Pack.hs
@@ -10,6 +10,7 @@
   , packT'
   , packValue
   , packValue'
+  , packValuePrefix
     -- * Serializers used in morley-client
   , encodeValue'
   , packNotedT'
@@ -39,9 +40,13 @@
 import qualified Tezos.Crypto.Secp256k1 as Secp256k1
 import Util.Peano (peanoValSing)
 
+-- | Prefix prepended to the binary representation of a value.
+packValuePrefix :: IsString s => s
+packValuePrefix = "\x05"
+
 -- | Serialize a value given to @PACK@ instruction.
 packValue :: PackedValScope t => Value t -> LByteString
-packValue x = "\x05" <> encodeValue x
+packValue x = packValuePrefix <> encodeValue x
 
 -- | Same as 'packValue', for strict bytestring.
 packValue' :: PackedValScope t => Value t -> ByteString
@@ -191,6 +196,8 @@
 -- | Encode an instruction.
 encodeInstr :: forall inp out. Instr inp out -> LByteString
 encodeInstr = \case
+  WithLoc _ i ->
+    encodeInstr i
   InstrWithNotes n a ->
     encodeNotedInstr a n []
   InstrWithVarNotes varNotes a ->
@@ -229,8 +236,8 @@
     "\x03\x4f"
   IF_NONE a b ->
     "\x07\x2f" <> encodeInstrs a <> encodeInstrs b
-  PAIR ->
-    "\x03\x42"
+  AnnPAIR tn fn1 fn2 ->
+    encodeWithAnns [tn] [fn1, fn2] [] "\x03\x42"
   (AnnCAR fn) ->
     encodeWithAnns [] [fn] [] "\x03\x16"
   (AnnCDR fn) ->
@@ -407,14 +414,14 @@
 encodeNotedInstr
   :: forall inp out. Instr inp out -> PackedNotes out -> [VarAnn] -> LByteString
 encodeNotedInstr a (PackedNotes n) vns = case (a, Proxy @out, n) of
+  (WithLoc _ a0, _, _) ->
+    encodeNotedInstr a0 (PackedNotes n) vns
   (SOME, _, NTOption tn _ns) ->
     encodeWithAnns [tn] [] vns $ encodeInstr a
   (NONE, _ :: Proxy ('TOption t ': s), NTOption tn ns) ->
     encodeWithAnns [tn] [] vns $ "\x05\x3e" <> encodeNotedT' @t ns
   (UNIT, _, NTUnit tn) ->
     encodeWithAnns [tn] [] vns $ encodeInstr a
-  (PAIR, _, NTPair tn fn1 fn2 _ns1 _ns2) ->
-    encodeWithAnns [tn] [fn1, fn2] vns $ encodeInstr a
   (LEFT, _ :: Proxy ('TOr l r ': s), NTOr tn fn1 fn2 _ns1 ns2) ->
     encodeWithAnns [tn] [fn1, fn2] vns $ "\x05\x33" <> encodeNotedT' @r ns2
   (RIGHT, _ :: Proxy ('TOr l r ': s), NTOr tn fn1 fn2 ns1 _ns2) ->
diff --git a/src/Michelson/Interpret/Unpack.hs b/src/Michelson/Interpret/Unpack.hs
--- a/src/Michelson/Interpret/Unpack.hs
+++ b/src/Michelson/Interpret/Unpack.hs
@@ -238,9 +238,14 @@
       ( decodeWithTag "key_hash" keyHashDecoders
       , parseKeyHash
       )
-    STTimestamp -> do
-      expectTag "Timestamp" 0x00
-      T.VTimestamp . timestampFromSeconds <$> decodeInt
+    STTimestamp -> Get.label "Timestamp" $ Get.getWord8 >>= \case
+      0x00 -> do
+        T.VTimestamp . timestampFromSeconds <$> decodeInt
+      0x01 -> do
+        str <- decodeString
+        maybe (fail $ toString $ "failed to parse timestamp from " <> unMText str)
+          (pure . T.VTimestamp) $ parseTimestamp $ unMText str
+      other -> unknownTag "int or string" other
     STAddress ->
       T.VAddress <$> decodeAsBytesOrString
       ( decodeBytesLike "EpAddress" parseEpAddressRaw
diff --git a/src/Michelson/Optimizer.hs b/src/Michelson/Optimizer.hs
--- a/src/Michelson/Optimizer.hs
+++ b/src/Michelson/Optimizer.hs
@@ -24,11 +24,13 @@
 
 import Prelude hiding (EQ)
 
+import Data.Constraint (Dict(..))
 import Data.Default (Default(def))
 import Data.Singletons (sing)
 
 import Michelson.Interpret.Pack (packValue')
 import Michelson.Typed.Aliases (Value)
+import Michelson.Typed.Arith
 import Michelson.Typed.Instr
 import Michelson.Typed.Scope (PackedValScope)
 import Michelson.Typed.Sing
@@ -95,8 +97,10 @@
     `orSimpleRule` internalNop
     `orSimpleRule` simpleDips
     `orSimpleRule` adjacentDips
+    `orSimpleRule` adjacentDrops
     `orSimpleRule` specificPush
     `orSimpleRule` pairUnpair
+    `orSimpleRule` swapBeforeCommutative
 
 -- | We do not enable 'pushPack' rule by default because it is
 -- potentially dangerous.
@@ -264,9 +268,24 @@
 adjacentDips :: Rule
 adjacentDips = \case
   Seq (DIP f) (DIP g) -> Just (DIP (Seq f g))
+  Seq (DIP f) (Seq (DIP g) c) -> Just (DIP (Seq f g) `Seq` c)
 
   _ -> Nothing
 
+-- TODO (#299): optimize sequences of more than 2 DROPs.
+-- | Sequences of @DROP@s can be turned into single @DROP n@.
+-- When @n@ is greater than 2 it saves size and gas.
+-- When @n@ is 2 it saves gas only.
+adjacentDrops :: Rule
+adjacentDrops = \case
+  Seq DROP DROP -> Just (DROPN (SS $ SS SZ))
+  Seq DROP (Seq DROP c) -> Just (DROPN (SS $ SS SZ) `Seq` c)
+
+  -- Does not compile, need to do something smart
+  -- Seq (DROPN (SS (SS SZ))) DROP -> Just (DROPN (SS $ SS $ SS SZ))
+
+  _ -> Nothing
+
 specificPush :: Rule
 specificPush = \case
   push@PUSH{} -> optimizePush push
@@ -300,6 +319,23 @@
 
   UNPAIR_c (Seq PAIR c) -> Just c
   UNPAIR_c      PAIR    -> Just Nop
+
+  _ -> Nothing
+
+commuteArith ::
+  forall n m s out. Instr (n ': m ': s) out -> Maybe (Instr (m ': n ': s) out)
+commuteArith = \case
+  ADD -> do Dict <- commutativityProof @Add @n @m; Just ADD
+  MUL -> do Dict <- commutativityProof @Mul @n @m; Just MUL
+  OR -> do Dict <- commutativityProof @Or @n @m; Just OR
+  AND -> do Dict <- commutativityProof @And @n @m; Just AND
+  XOR -> do Dict <- commutativityProof @Xor @n @m; Just XOR
+  _ -> Nothing
+
+swapBeforeCommutative :: Rule
+swapBeforeCommutative = \case
+  Seq SWAP (Seq i c) -> (`Seq` c) <$> commuteArith i
+  Seq SWAP i -> commuteArith i
 
   _ -> Nothing
 
diff --git a/src/Michelson/Parser.hs b/src/Michelson/Parser.hs
--- a/src/Michelson/Parser.hs
+++ b/src/Michelson/Parser.hs
@@ -43,12 +43,13 @@
 import Prelude hiding (try)
 
 import qualified Language.Haskell.TH.Quote as TH
-import Text.Megaparsec
-  (Parsec, choice, eitherP, eof, errorBundlePretty, getSourcePos, lookAhead, parse, try)
+import Text.Megaparsec (Parsec, choice, customFailure, eitherP, eof, errorBundlePretty,
+  getSourcePos, lookAhead, parse, try)
 import Text.Megaparsec.Pos (SourcePos(..), unPos)
 
 import Michelson.ErrorPos (SrcPos(..), mkPos)
 import Michelson.Macro (LetMacro, Macro(..), ParsedInstr, ParsedOp(..), ParsedValue, expandValue)
+import Michelson.Parser.Annotations (noteF)
 import Michelson.Parser.Error
 import Michelson.Parser.Ext
 import Michelson.Parser.Instr
@@ -92,8 +93,17 @@
 
 cbParameter :: Parser ParameterType
 cbParameter = do
-  (fieldAnn, t) <- symbol "parameter" *> field
-  pure $ ParameterType t (convAnn fieldAnn)
+  symbol "parameter"
+  prefixRootAnn <- optional noteF
+  (inTypeRootAnn, t) <- field
+  rootAnn <- case (prefixRootAnn, inTypeRootAnn) of
+    -- TODO: [#310] Handle cases where there are 2 empty root annotations.
+    -- For example: root % (unit %) which should throw the error.
+    (Just "", "") -> pure noAnn
+    (Just a, "") -> pure a
+    (Nothing, b) -> pure b
+    (Just _, _) -> customFailure MultiRootAnnotationException
+  pure $ ParameterType t (convAnn rootAnn)
 
 cbStorage :: Parser Type
 cbStorage = symbol "storage" *> type_
diff --git a/src/Michelson/Parser/Error.hs b/src/Michelson/Parser/Error.hs
--- a/src/Michelson/Parser/Error.hs
+++ b/src/Michelson/Parser/Error.hs
@@ -28,6 +28,7 @@
   | WrongAccessArgs Natural Positive
   | WrongSetArgs Natural Positive
   | ExcessFieldAnnotation
+  | MultiRootAnnotationException
   deriving stock (Eq, Data, Ord, Show, Generic)
 
 instance NFData CustomParserException
@@ -37,6 +38,7 @@
   showErrorComponent (StringLiteralException e) = showErrorComponent e
   showErrorComponent OddNumberBytesException = "odd number bytes"
   showErrorComponent ExcessFieldAnnotation = "excess field annotation"
+  showErrorComponent MultiRootAnnotationException = "unexpected multiple root annotations"
   showErrorComponent (WrongTagArgs idx size) =
     "TAG: too large index: " +| idx |+ " \
            \exceedes union size " +| size |+ ""
diff --git a/src/Michelson/Runtime.hs b/src/Michelson/Runtime.hs
--- a/src/Michelson/Runtime.hs
+++ b/src/Michelson/Runtime.hs
@@ -21,6 +21,7 @@
   , ContractState (..)
   , AddressState (..)
   , TxData (..)
+  , TxParam (..)
 
   -- * For testing
   , ExecutorOp (..)
@@ -55,6 +56,8 @@
 import Named ((:!), (:?), arg, argDef, defaults, (!))
 import Text.Megaparsec (parse)
 
+import Data.Singletons (demote)
+import Data.Typeable (gcast)
 import Michelson.Interpret
   (ContractEnv(..), InterpretError(..), InterpretResult(..), InterpreterState(..), MorleyLogs(..),
   RemainingSteps(..), handleContractReturn, interpret)
@@ -64,7 +67,7 @@
 import Michelson.Runtime.TxData
 import Michelson.TypeCheck (TCError, typeVerifyParameter)
 import Michelson.Typed
-  (CreateContract(..), EpName, Operation'(..), SomeValue'(..), TransferTokens(..),
+  (CreateContract(..), EntrypointCallT, EpName, Operation'(..), SomeValue'(..), TransferTokens(..),
   convertContractCode, untypeValue)
 import qualified Michelson.Typed as T
 import Michelson.Untyped
@@ -164,6 +167,9 @@
   -- ^ Contract storage is ill-typed.
   | EEIllTypedParameter !TCError
   -- ^ Contract parameter is ill-typed.
+  | EEUnexpectedParameterType T.T T.T
+  -- ^ Contract parameter is well-typed, but its type does
+  -- not match the entrypoint's type.
   | EEUnknownEntrypoint EpName
   -- ^ Specified entrypoint to run is not found.
   deriving stock (Show, Functor)
@@ -188,6 +194,10 @@
       EEIllTypedContract err -> "The contract is ill-typed: " +| err |+ ""
       EEIllTypedStorage err -> "The contract storage is ill-typed: " +| err |+ ""
       EEIllTypedParameter err -> "The contract parameter is ill-typed: " +| err |+ ""
+      EEUnexpectedParameterType expectedT actualT ->
+        "The contract parameter is well-typed, but did not match the contract's entrypoint's type.\n" <>
+        "Expected: " +| expectedT |+ "\n" <>
+        "Got: " +| actualT |+ ""
       EEUnknownEntrypoint epName -> "The contract does not contain entrypoint '" +| epName |+ "'"
 
 type ExecutorError = ExecutorError' Address
@@ -529,11 +539,23 @@
             }
           epName = tdEntrypoint txData
 
-        T.MkEntrypointCallRes _ epc
+        T.MkEntrypointCallRes _ (epc :: EntrypointCallT cp epArg)
           <- T.mkEntrypointCall epName (T.cParamNotes csContract)
              & maybe (throwError $ EEUnknownEntrypoint epName) pure
-        typedParameter <- liftEither $ first EEIllTypedParameter $
-           typeVerifyParameter existingContracts (tdParameter txData)
+
+        -- 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) ->
+              maybe (throwError $ EEUnexpectedParameterType (demote @epArg) (demote @t)) pure $
+                gcast @t @epArg typedVal
+            TxUntypedParam untypedVal ->
+              liftEither $ first EEIllTypedParameter $
+                typeVerifyParameter @epArg existingContracts untypedVal
+
         iur@InterpretResult
           { iurOps = sideEffects
           , iurNewStorage = newValue
@@ -597,7 +619,7 @@
                 TxData
                   { tdSenderAddress = interpretedAddr
                   , tdEntrypoint = T.sepcName sepc
-                  , tdParameter = untypeValue (ttTransferArgument tt)
+                  , tdParameter = TxTypedParam (ttTransferArgument tt)
                   , tdAmount = ttAmount tt
                   }
           in Just (TransferOp destAddress txData)
diff --git a/src/Michelson/Runtime/GState.hs b/src/Michelson/Runtime/GState.hs
--- a/src/Michelson/Runtime/GState.hs
+++ b/src/Michelson/Runtime/GState.hs
@@ -117,9 +117,9 @@
 
 instance Buildable ContractState where
   build ContractState{..} =
-    "Contractstate:\n csBalance: " +| csBalance |+
-    "\n  csContract: " +| T.untypeValue csStorage ||+
-    "\n  csStorage: " +| T.convertContract csContract ||+ ""
+    "Contractstate:\n Balance: " +| csBalance |+
+    "\n  Storage: " +| T.untypeValue csStorage ||+
+    "\n  Contract: " +| T.convertContract csContract ||+ ""
 
 -- | State of an arbitrary address.
 data AddressState
@@ -159,9 +159,6 @@
 makeLensesWith postfixLFields ''GState
 
 deriveJSON morleyAesonOptions ''GState
-
-
-
 
 -- | Number of genesis addresses.
 genesisAddressesNum :: Word
diff --git a/src/Michelson/Runtime/TxData.hs b/src/Michelson/Runtime/TxData.hs
--- a/src/Michelson/Runtime/TxData.hs
+++ b/src/Michelson/Runtime/TxData.hs
@@ -6,6 +6,7 @@
 
 module Michelson.Runtime.TxData
        ( TxData (..)
+       , TxParam(..)
        , tdSenderAddressL
        , tdParameterL
        , tdEntrypointL
@@ -13,21 +14,36 @@
        ) where
 
 import Control.Lens (makeLensesWith)
-import Data.Aeson.TH (deriveJSON)
+import Data.Aeson (ToJSON(toJSON))
+import Data.Aeson.TH (deriveToJSON)
 
-import Michelson.Untyped (EpName, Value)
+import Michelson.Typed (ParameterScope)
+import qualified Michelson.Typed as T
+import Michelson.Untyped (EpName)
+import qualified Michelson.Untyped as U
 import Tezos.Address (Address)
 import Tezos.Core (Mutez)
 import Util.Aeson (morleyAesonOptions)
 import Util.Lens (postfixLFields)
 
+-- | A parameter associated with a particular transaction.
+data TxParam where
+  TxTypedParam :: forall t. ParameterScope t => T.Value t -> TxParam
+  TxUntypedParam :: U.Value -> TxParam
+
+deriving stock instance Show TxParam
+
+instance ToJSON TxParam where
+  toJSON (TxTypedParam val) = toJSON $ T.untypeValue val
+  toJSON (TxUntypedParam val) = toJSON val
+
 -- | Data associated with a particular transaction.
 data TxData = TxData
   { tdSenderAddress :: Address
-  , tdParameter :: Value
+  , tdParameter :: TxParam
   , tdEntrypoint :: EpName
   , tdAmount :: Mutez
-  } deriving stock (Show, Eq)
+  } deriving stock Show
 
 makeLensesWith postfixLFields ''TxData
-deriveJSON morleyAesonOptions ''TxData
+deriveToJSON morleyAesonOptions ''TxData
diff --git a/src/Michelson/TypeCheck/Helpers.hs b/src/Michelson/TypeCheck/Helpers.hs
--- a/src/Michelson/TypeCheck/Helpers.hs
+++ b/src/Michelson/TypeCheck/Helpers.hs
@@ -269,13 +269,19 @@
     Un.SeqEx sq : rs                 -> typeCheckSeq Nothing sq rs
     []                               -> pure $ a :/ Nop ::: a
   where
-    typeCheckPrim (Just cs) i [] = local (const cs) $ tcInstr i t
-    typeCheckPrim (Just cs) i rs = local (const cs) $ typeCheckImplDo (tcInstr i t) id rs
+    -- If we know source location from the untyped instruction, keep it in the typed one.
+    typeCheckPrim (Just cs) i [] = local (const cs) $ (tcInstr i t <&> wrapWithLoc cs)
+    typeCheckPrim (Just cs) i rs = local (const cs) $ typeCheckImplDo (tcInstr i t <&> wrapWithLoc cs) id rs
     typeCheckPrim Nothing i [] = tcInstr i t
     typeCheckPrim Nothing i rs = typeCheckImplDo (tcInstr i t) id rs
 
     typeCheckSeq (Just cs) sq = local (const cs) . typeCheckImplDo (typeCheckImpl tcInstr sq t) Nested
     typeCheckSeq Nothing sq = typeCheckImplDo (typeCheckImpl tcInstr sq t) Nested
+
+    wrapWithLoc :: InstrCallStack -> SomeInstr inp -> SomeInstr inp
+    wrapWithLoc _ si@(_ :/ (WithLoc _ _) ::: _) = si
+    wrapWithLoc cs (inp :/ instr ::: out) = inp :/ WithLoc cs instr ::: out
+    wrapWithLoc _ si = si
 
     typeCheckImplDo
       :: TypeCheckInstr (SomeInstr inp)
diff --git a/src/Michelson/TypeCheck/Instr.hs b/src/Michelson/TypeCheck/Instr.hs
--- a/src/Michelson/TypeCheck/Instr.hs
+++ b/src/Michelson/TypeCheck/Instr.hs
@@ -341,7 +341,8 @@
   (U.PAIR tn vn pfn qfn, (an, _, avn) ::& (bn, _, bvn) ::& rs) -> do
     let (vn', pfn', qfn') = deriveSpecialFNs pfn qfn avn bvn
     case NTPair tn pfn' qfn' an bn of
-      (ns :: Notes ('TPair a b)) -> withWTPInstr @('TPair a b) $ pure (inp :/ PAIR ::: ((ns, Dict, vn `orAnn` vn') ::& rs))
+      (ns :: Notes ('TPair a b)) -> withWTPInstr @('TPair a b) $
+        pure (inp :/ AnnPAIR tn pfn qfn ::: ((ns, Dict, vn `orAnn` vn') ::& rs))
 
   (U.PAIR {}, _) -> notEnoughItemsOnStack
 
@@ -918,8 +919,7 @@
         TypeCheckValue (value, ty) ->
           tcFailedOnValue value ty "The SELF instruction cannot appear in a lambda." Nothing
         TypeCheckContract (SomeParamType _ notescp) -> do
-          epName <- onTypeCheckInstrErr uInstr (SomeHST inp) Nothing $
-                      epNameFromRefAnn fn `onLeft` IllegalEntrypoint
+          let epName = U.epNameFromSelfAnn fn
           MkEntrypointCallRes (argNotes :: Notes arg) epc <-
             mkEntrypointCall epName notescp
               & maybeToRight (EntrypointNotFound epName)
diff --git a/src/Michelson/Typed/Annotation.hs b/src/Michelson/Typed/Annotation.hs
--- a/src/Michelson/Typed/Annotation.hs
+++ b/src/Michelson/Typed/Annotation.hs
@@ -2,8 +2,6 @@
 --
 -- SPDX-License-Identifier: LicenseRef-MIT-TQ
 
-{-# LANGUAGE DataKinds, GADTs #-}
-
 -- | Module, providing @Notes t@ data type, which holds annotations for a
 -- given type @t@.
 --
diff --git a/src/Michelson/Typed/Arith.hs b/src/Michelson/Typed/Arith.hs
--- a/src/Michelson/Typed/Arith.hs
+++ b/src/Michelson/Typed/Arith.hs
@@ -2,8 +2,6 @@
 --
 -- SPDX-License-Identifier: LicenseRef-MIT-TQ
 
-{-# LANGUAGE DataKinds, MultiParamTypeClasses, TypeFamilies #-}
-
 -- | Module, containing some boilerplate for support of
 -- arithmetic operations in Michelson language.
 
@@ -11,7 +9,8 @@
   ( ArithOp (..)
   , UnaryArithOp (..)
   , ArithError (..)
-  , ArithErrorType (..)
+  , ShiftArithErrorType (..)
+  , MutezArithErrorType (..)
   , Add
   , Sub
   , Mul
@@ -34,13 +33,14 @@
   ) where
 
 import Data.Bits (complement, shift, (.&.), (.|.))
+import Data.Constraint (Dict(..))
 import Data.Singletons (Sing, SingI(..))
 import Fmt (Buildable(build))
 
 import Michelson.Typed.Annotation (AnnConvergeError, Notes(..), converge, convergeAnns, starNotes)
 import Michelson.Typed.Sing (SingT(..))
 import Michelson.Typed.T (T(..))
-import Michelson.Typed.Value (Comparable, Comparability(..), checkComparability, Value'(..))
+import Michelson.Typed.Value (Comparability(..), Comparable, Value'(..), checkComparability)
 import Tezos.Core (addMutez, mulMutez, subMutez, timestampFromSeconds, timestampToSeconds)
 
 -- | Class for binary arithmetic operation.
@@ -71,21 +71,36 @@
     -> Value' instr m
     -> Either (ArithError (Value' instr n) (Value' instr m)) (Value' instr (ArithRes aop n m))
 
--- | Denotes the error type occured in the arithmetic operation.
-data ArithErrorType
+  -- | An operation can marked as commutative, it does not affect its
+  -- runtime behavior, but enables certain optimization in the optimizer.
+  -- We conservatively consider operations non-commutative by default.
+  --
+  -- Note that there is one unusual case: @AND@ works with @int : nat@
+  -- but not with @nat : int@. That's how it's specified in Michelson.
+  commutativityProof :: Maybe $ Dict (ArithRes aop n m ~ ArithRes aop m n, ArithOp aop m n)
+  commutativityProof = Nothing
+
+-- | Denotes the error type occurred in the arithmetic shift operation.
+data ShiftArithErrorType
+  = LslOverflow
+  | LsrUnderflow
+  deriving stock (Show, Eq, Ord, Generic)
+
+instance NFData ShiftArithErrorType
+
+-- | Denotes the error type occurred in the arithmetic operation involving mutez.
+data MutezArithErrorType
   = AddOverflow
   | MulOverflow
   | SubUnderflow
-  | LslOverflow
-  | LsrUnderflow
   deriving stock (Show, Eq, Ord, Generic)
 
-instance NFData ArithErrorType
+instance NFData MutezArithErrorType
 
 -- | Represents an arithmetic error of the operation.
 data ArithError n m
-  = MutezArithError ArithErrorType n m
-  | ShiftArithError ArithErrorType n m
+  = MutezArithError MutezArithErrorType n m
+  | ShiftArithError ShiftArithErrorType n m
   deriving stock (Show, Eq, Ord, Generic)
 
 instance (NFData n, NFData m) => NFData (ArithError n m)
@@ -120,34 +135,41 @@
   type ArithRes Add 'TNat 'TInt = 'TInt
   convergeArith _ _ n2 = Right n2
   evalOp _ (VNat i) (VInt j) = Right $ VInt (toInteger i + j)
+  commutativityProof = Just Dict
 instance ArithOp Add 'TInt 'TNat where
   type ArithRes Add 'TInt 'TNat = 'TInt
   convergeArith _ n1 _ = Right n1
   evalOp _ (VInt i) (VNat j) = Right $ VInt (i + toInteger j)
+  commutativityProof = Just Dict
 instance ArithOp Add 'TNat 'TNat where
   type ArithRes Add 'TNat 'TNat = 'TNat
   convergeArith _ n1 n2 = converge n1 n2
   evalOp _ (VNat i) (VNat j) = Right $ VNat (i + j)
+  commutativityProof = Just Dict
 instance ArithOp Add 'TInt 'TInt where
   type ArithRes Add 'TInt 'TInt = 'TInt
   convergeArith _ n1 n2 = converge n1 n2
   evalOp _ (VInt i) (VInt j) = Right $ VInt (i + j)
+  commutativityProof = Just Dict
 instance ArithOp Add 'TTimestamp 'TInt where
   type ArithRes Add 'TTimestamp 'TInt = 'TTimestamp
   convergeArith _ n1 _ = Right n1
   evalOp _ (VTimestamp i) (VInt j) =
     Right $ VTimestamp $ timestampFromSeconds $ timestampToSeconds i + j
+  commutativityProof = Just Dict
 instance ArithOp Add 'TInt 'TTimestamp where
   type ArithRes Add 'TInt 'TTimestamp = 'TTimestamp
   convergeArith _ _ n2 = Right n2
   evalOp _ (VInt i) (VTimestamp j) =
     Right $ VTimestamp $ timestampFromSeconds $ timestampToSeconds j + i
+  commutativityProof = Just Dict
 instance ArithOp Add 'TMutez 'TMutez where
   type ArithRes Add 'TMutez 'TMutez = 'TMutez
   convergeArith _ n1 n2 = converge n1 n2
   evalOp _ n@(VMutez i) m@(VMutez j) = res
     where
       res = maybe (Left $ MutezArithError AddOverflow n m) (Right . VMutez) $ i `addMutez` j
+  commutativityProof = Just Dict
 
 instance ArithOp Sub 'TNat 'TInt where
   type ArithRes Sub 'TNat 'TInt = 'TInt
@@ -187,30 +209,36 @@
   type ArithRes Mul 'TNat 'TInt = 'TInt
   convergeArith _ _ n2 = Right n2
   evalOp _ (VNat i) (VInt j) = Right $ VInt (toInteger i * j)
+  commutativityProof = Just Dict
 instance ArithOp Mul 'TInt 'TNat where
   type ArithRes Mul 'TInt 'TNat = 'TInt
   convergeArith _ n1 _ = Right n1
   evalOp _ (VInt i) (VNat j) = Right $ VInt (i * toInteger j)
+  commutativityProof = Just Dict
 instance ArithOp Mul 'TNat 'TNat where
   type ArithRes Mul 'TNat 'TNat = 'TNat
   convergeArith _ n1 n2 = converge n1 n2
   evalOp _ (VNat i) (VNat j) = Right $ VNat (i * j)
+  commutativityProof = Just Dict
 instance ArithOp Mul 'TInt 'TInt where
   type ArithRes Mul 'TInt 'TInt = 'TInt
   convergeArith _ n1 n2 = converge n1 n2
   evalOp _ (VInt i) (VInt j) = Right $ VInt (i * j)
+  commutativityProof = Just Dict
 instance ArithOp Mul 'TNat 'TMutez where
   type ArithRes Mul 'TNat 'TMutez = 'TMutez
   convergeArith _ _ n2 = Right n2
   evalOp _ n@(VNat i) m@(VMutez j) = res
     where
       res = maybe (Left $ MutezArithError MulOverflow n m) (Right . VMutez) $ j `mulMutez` i
+  commutativityProof = Just Dict
 instance ArithOp Mul 'TMutez 'TNat where
   type ArithRes Mul 'TMutez 'TNat = 'TMutez
   convergeArith _ n1 _ = Right n1
   evalOp _ n@(VMutez i) m@(VNat j) = res
     where
       res = maybe (Left $ MutezArithError MulOverflow n m) (Right . VMutez) $ i `mulMutez` j
+  commutativityProof = Just Dict
 
 instance UnaryArithOp Abs 'TInt where
   type UnaryArithRes Abs 'TInt = 'TNat
@@ -227,10 +255,12 @@
   type ArithRes Or 'TNat 'TNat = 'TNat
   convergeArith _ n1 n2 = converge n1 n2
   evalOp _ (VNat i) (VNat j) = Right $ VNat (i .|. j)
+  commutativityProof = Just Dict
 instance ArithOp Or 'TBool 'TBool where
   type ArithRes Or 'TBool 'TBool = 'TBool
   convergeArith _ n1 n2 = converge n1 n2
   evalOp _ (VBool i) (VBool j) = Right $ VBool (i .|. j)
+  commutativityProof = Just Dict
 
 instance ArithOp And 'TInt 'TNat where
   type ArithRes And 'TInt 'TNat = 'TNat
@@ -240,19 +270,23 @@
   type ArithRes And 'TNat 'TNat = 'TNat
   convergeArith _ n1 n2 = converge n1 n2
   evalOp _ (VNat i) (VNat j) = Right $ VNat (i .&. j)
+  commutativityProof = Just Dict
 instance ArithOp And 'TBool 'TBool where
   type ArithRes And 'TBool 'TBool = 'TBool
   convergeArith _ n1 n2 = converge n1 n2
   evalOp _ (VBool i) (VBool j) = Right $ VBool (i .&. j)
+  commutativityProof = Just Dict
 
 instance ArithOp Xor 'TNat 'TNat where
   type ArithRes Xor 'TNat 'TNat = 'TNat
   convergeArith _ n1 n2 = converge n1 n2
   evalOp _ (VNat i) (VNat j) = Right $ VNat (i `xor` j)
+  commutativityProof = Just Dict
 instance ArithOp Xor 'TBool 'TBool where
   type ArithRes Xor 'TBool 'TBool = 'TBool
   convergeArith _ n1 n2 = converge n1 n2
   evalOp _ (VBool i) (VBool j) = Right $ VBool (i `xor` j)
+  commutativityProof = Just Dict
 
 instance ArithOp Lsl 'TNat 'TNat where
   type ArithRes Lsl 'TNat 'TNat = 'TNat
@@ -325,13 +359,16 @@
   evalUnaryArithOp _ (VInt i) = VBool (i >= 0)
 
 
-instance Buildable ArithErrorType where
+instance Buildable ShiftArithErrorType where
   build = \case
+    LslOverflow -> "lsl overflow"
+    LsrUnderflow -> "lsr underflow"
+
+instance Buildable MutezArithErrorType where
+  build = \case
     AddOverflow -> "add overflow"
     MulOverflow -> "mul overflow"
     SubUnderflow -> "sub overflow"
-    LslOverflow -> "lsl overflow"
-    LsrUnderflow -> "lsr underflow"
 
 instance (Show n, Show m) => Buildable (ArithError n m) where
   build (MutezArithError errType n m) = "Mutez "
diff --git a/src/Michelson/Typed/Convert.hs b/src/Michelson/Typed/Convert.hs
--- a/src/Michelson/Typed/Convert.hs
+++ b/src/Michelson/Typed/Convert.hs
@@ -9,24 +9,31 @@
   , convertContract
   , instrToOps
   , untypeValue
+
+  -- Helper for generating documentation
+  , sampleValueFromUntype
   ) where
 
+import Data.Constraint (Dict(..))
 import qualified Data.Map as Map
-import Data.Singletons (demote)
+import qualified Data.Set as Set
+import Data.Singletons (Sing, demote)
 import Fmt (Buildable(..), pretty)
 
 import Michelson.Text
+import Michelson.Typed.Aliases
 import Michelson.Typed.Annotation (Notes(..))
 import Michelson.Typed.Entrypoints
-import Michelson.Typed.Extract (mkUType, toUType)
+import Michelson.Typed.Extract (fromUType, mkUType, toUType)
 import Michelson.Typed.Instr as Instr
 import Michelson.Typed.Scope
-import Michelson.Typed.Sing (SingT(..))
+import Michelson.Typed.Sing (SingT(..), withSomeSingT)
 import Michelson.Typed.T (T(..))
 import Michelson.Typed.Value
 import qualified Michelson.Untyped as U
-import Tezos.Core (mformatChainId, unMutez)
-import Tezos.Crypto (mformatKeyHash, mformatPublicKey, mformatSignature)
+import Tezos.Core
+  (mformatChainId, parseChainId, timestampFromSeconds, unMutez, unsafeMkMutez)
+import Tezos.Crypto
 import Util.Peano
 import Util.Typeable
 
@@ -133,12 +140,16 @@
   DocGroup _ sq -> instrToOps sq
   Ext (ext :: ExtInstr inp) -> (U.PrimEx . U.EXT) <$> extInstrToOps ext
   FrameInstr _ i -> instrToOps i
+  -- TODO [#283] After representation of locations is polished,
+  -- this place should be updated to pass it from typed to untyped ASTs.
+  WithLoc _ i -> instrToOps i
   InstrWithNotes n i -> case i of
     Nop -> instrToOps i
     Seq _ _ -> instrToOps i
     Nested _ -> instrToOps i
     DocGroup _ _ -> instrToOps i
     Ext _ -> instrToOps i
+    WithLoc _ i0 -> instrToOps (InstrWithNotes n i0)
     InstrWithNotes _ _ -> instrToOps i
     InstrWithVarNotes _ _ -> instrToOps i
     -- For inner instruction, filter out values that we don't want to apply
@@ -152,12 +163,11 @@
     Nested _ -> instrToOps i
     DocGroup _ _ -> instrToOps i
     Ext _ -> instrToOps i
+    WithLoc _ i0 -> instrToOps (InstrWithVarNotes n i0)
     InstrWithNotes _ _ -> instrToOps i
     InstrWithVarNotes _ _ -> instrToOps i
     _ -> [U.PrimEx $ handleInstrVarNotes i n]
   i -> [U.PrimEx $ handleInstr i]
-  -- TODO pva701: perphaps, typed instr has to hold a position too
-  -- to make it possible to report a precise location of a runtime error
   where
     handleInstrAnnotate
       :: forall inp' out' . HasCallStack
@@ -173,7 +183,7 @@
             (_, U.SOME _ va, NTOption ta _) -> U.SOME ta va
             (STOption _, U.NONE _ va _, NTOption ta nt) -> U.NONE ta va (mkUType nt)
             (_, U.UNIT _ va, NTUnit ta) -> U.UNIT ta va
-            (_, U.PAIR _ va _ _, NTPair ta f1 f2 _ _) -> U.PAIR ta va f1 f2
+            (_, U.PAIR ta va f1 f2, _) -> U.PAIR ta va f1 f2
             (_, U.CAR va f1, _) -> U.CAR va f1
             (_, U.CDR va f1, _) -> U.CDR va f1
             (STOr _ _, U.LEFT _ va _ _ _, NTOr ta f1 f2 _ n2) ->
@@ -350,6 +360,7 @@
 
     handleInstr :: Instr inp out -> U.ExpandedInstr
     handleInstr = \case
+      (WithLoc _ _) -> error "impossible"
       (InstrWithNotes _ _) -> error "impossible"
       (InstrWithVarNotes _ _) -> error "impossible"
       (FrameInstr _ _) -> error "impossible"
@@ -372,7 +383,7 @@
       SOME -> U.SOME U.noAnn U.noAnn
       UNIT -> U.UNIT U.noAnn U.noAnn
       (IF_NONE i1 i2) -> U.IF_NONE (instrToOps i1) (instrToOps i2)
-      PAIR -> U.PAIR U.noAnn U.noAnn U.noAnn U.noAnn
+      AnnPAIR tn fn1 fn2 -> U.PAIR tn U.noAnn fn1 fn2
       (AnnCAR fn) -> U.CAR U.noAnn fn
       (AnnCDR fn) -> U.CDR U.noAnn fn
       i@LEFT | _ :: Instr (a ': s) ('TOr a b ': s) <- i ->
@@ -510,3 +521,86 @@
 
 instance (SingI t, HasNoOp t) => Buildable (Value' Instr t) where
   build = build . untypeValue
+
+-- | Get 'sampleTypedValue' from untyped value.
+--
+-- Throw error if @U.Type@ contains @TOperation@.
+sampleValueFromUntype :: HasCallStack => U.Type -> U.Value' U.ExpandedOp
+sampleValueFromUntype ty = withSomeSingT (fromUType ty) $ \(_ :: Sing t) ->
+  case checkScope @(ParameterScope t) of
+    Left bt -> error $ "Scope error: " <> pretty bt
+    Right Dict -> untypeValue $ sampleTypedValue @t
+
+-- | Sample values used for generating examples of entrypoint parameter in documentation.
+sampleTypedValue :: forall t. (HasCallStack, ParameterScope t) => Value t
+sampleTypedValue = case sing @t of
+    STInt              -> VInt -1
+    STNat              -> VNat 0
+    STString           -> VString [mt|hello|]
+    STMutez            -> VMutez (unsafeMkMutez 100)
+    STBool             -> VBool True
+    STKey              -> VKey samplePublicKey
+    STKeyHash          -> VKeyHash $ hashKey samplePublicKey
+    STTimestamp        -> VTimestamp $ timestampFromSeconds 1564142952
+    STBytes            -> VBytes "\10"
+    STAddress          -> VAddress $ sampleAddress
+    STUnit             -> VUnit
+    STSignature        -> VSignature $ sampleSignature
+    STChainId          -> VChainId sampleChainId
+    STOption (_ :: Sing t2) -> VOption $ Just $ sampleTypedValue @t2
+    STList (_ :: Sing t2) -> VList [sampleTypedValue @t2]
+    STSet (s2 :: Sing t2) ->
+      case ( checkComparability s2
+           , checkNestedBigMapsPresence s2
+           ) of
+        (CanBeCompared, NestedBigMapsAbsent) ->
+          VSet $ Set.fromList [sampleTypedValue @t2]
+        _ -> error $ "Error generating sample value: scope error"
+    STContract _ ->
+      VContract (eaAddress sampleAddress) $ SomeEpc epcCallRootUnsafe
+    STPair (s2 :: Sing t2) (s3 :: Sing t3) ->
+      case ( checkOpPresence s2
+           , checkNestedBigMapsPresence s2
+           , checkOpPresence s3
+           , checkNestedBigMapsPresence s3
+           ) of
+        (OpAbsent, NestedBigMapsAbsent, OpAbsent, NestedBigMapsAbsent) ->
+          VPair (sampleTypedValue @t2, sampleTypedValue @t3)
+    STOr (s2 :: Sing t2) _ ->
+      case (checkNestedBigMapsPresence s2, checkOpPresence s2) of
+        (NestedBigMapsAbsent, OpAbsent) ->
+          VOr $ Left $ sampleTypedValue @t2
+    STMap (s2 :: Sing t2) (s3 :: Sing t3) ->
+      case ( checkNestedBigMapsPresence s2
+           , checkComparability s2
+           , checkOpPresence s2
+           , checkNestedBigMapsPresence s3
+           ) of
+        (NestedBigMapsAbsent, CanBeCompared, OpAbsent, NestedBigMapsAbsent) ->
+            VMap $ Map.fromList [(sampleTypedValue @t2, sampleTypedValue @t3)]
+        _ -> error $ "Error generating sample value: scope error"
+    STBigMap (s2 :: Sing t2) (s3 :: Sing t3) ->
+      case ( checkNestedBigMapsPresence s2
+           , checkComparability s2
+           , checkOpPresence s2
+           , checkNestedBigMapsPresence s3
+           ) of
+        (NestedBigMapsAbsent, CanBeCompared, OpAbsent, NestedBigMapsAbsent) ->
+            VBigMap $ Map.fromList [(sampleTypedValue @t2, sampleTypedValue @t3)]
+        _ -> error $ "Error generating sample value: scope error"
+    STLambda (_ :: Sing t2) (s3 :: Sing t3) ->
+      case ( checkNestedBigMapsPresence s3
+           , checkBigMapPresence s3
+           , checkContractTypePresence s3
+           , checkOpPresence s3
+           ) of
+        (NestedBigMapsAbsent, BigMapAbsent, ContractAbsent, OpAbsent) ->
+          VLam $ RfNormal (DROP `Seq` PUSH (sampleTypedValue @t3))
+        _ -> VLam $ RfAlwaysFails (PUSH (VString [mt|lambda sample|]) `Seq` FAILWITH)
+    where
+      sampleAddress =  unsafeParseEpAddress "KT1AEseqMV6fk2vtvQCVyA7ZCaxv7cpxtXdB"
+      samplePublicKey = fromRight (error "impossible") $ parsePublicKey
+        "edpkuwTWKgQNnhR5v17H2DYHbfcxYepARyrPGbf1tbMoGQAj8Ljr3V"
+      sampleSignature = fromRight (error "impossible") $ parseSignature
+        "edsigtrs8bK7vNfiR4Kd9dWasVa1bAWaQSu2ipnmLGZuwQa8ktCEMYVKqbWsbJ7zTS8dgYT9tiSUKorWCPFHosL5zPsiDwBQ6vb"
+      sampleChainId = fromRight (error "impossible") $ parseChainId "NetXUdfLh6Gm88t"
diff --git a/src/Michelson/Typed/Doc.hs b/src/Michelson/Typed/Doc.hs
--- a/src/Michelson/Typed/Doc.hs
+++ b/src/Michelson/Typed/Doc.hs
@@ -37,6 +37,8 @@
   () <- case docItemRef di of
     DocItemNoRef ->
       modify (<> mempty{ cdContents = docItemToBlock di })
+    DocItemRefInlined{} ->
+      modify (<> mempty{ cdContents = docItemToBlock di })
     DocItemRef{} ->
       someDefinitionDocItemToContractDoc (SomeDocDefinitionItem di)
   forM_ @_ @_ @() (docItemDependencies di) $ \(SomeDocDefinitionItem dep) ->
@@ -57,10 +59,19 @@
   DGitRevisionUnknown -> Just gitRev
   _ -> Nothing
 
+attachToc :: DToc -> Instr inp out -> Instr inp out
+attachToc toc = modifyInstrDoc $ \case
+  DToc "" -> Just $ toc
+  _ -> Nothing
+
 -- | Assemble contract documentation with the revision of the contract.
 buildInstrDocWithGitRev :: DGitRevision -> Instr inp out -> ContractDoc
 buildInstrDocWithGitRev gitRev contract =
-  buildInstrDoc $ attachGitInfo gitRev contract
+  let toc = DToc $ contractDocToToc $ buildInstrDoc contract
+      c = contract
+            & attachGitInfo gitRev
+            & attachToc toc
+  in buildInstrDoc c
 
 -- | Assemble contract documentation.
 buildInstrDoc :: Instr inp out -> ContractDoc
diff --git a/src/Michelson/Typed/Entrypoints.hs b/src/Michelson/Typed/Entrypoints.hs
--- a/src/Michelson/Typed/Entrypoints.hs
+++ b/src/Michelson/Typed/Entrypoints.hs
@@ -48,7 +48,6 @@
 import Control.Monad.Except (throwError)
 import qualified Data.ByteString as BS
 import Data.Constraint (Dict(..))
-import Data.Default (Default(..))
 import qualified Data.List.NonEmpty as NE
 import qualified Data.Text as T
 import Fmt (Buildable(..), hexF, pretty, (+|), (|+))
@@ -92,7 +91,7 @@
 
 formatEpAddress :: EpAddress -> Text
 formatEpAddress (EpAddress addr ep)
-  | ep == def = formatAddress addr
+  | isDefEpName ep = formatAddress addr
   | otherwise = formatAddress addr <> "%" <> pretty ep
 
 mformatEpAddress :: EpAddress -> MText
@@ -133,7 +132,7 @@
   in case mannotTxt of
     "" -> do
       addr <- first ParseEpAddressBadAddress $ parseAddress addrTxt
-      return $ EpAddress addr def
+      return $ EpAddress addr DefEpName
     annotTxt' -> do
       addr <- first ParseEpAddressBadAddress $ parseAddress addrTxt
       annot <- first ParseEpAddressBadRefAnn $ case T.stripPrefix "%" annotTxt' of
@@ -278,8 +277,8 @@
         haveDefLL <- first (AcLeft  :) $ ensureAllCallable l
         haveDefRR <- first (AcRight :) $ ensureAllCallable r
 
-        let haveDefL = or [haveDefLL, epNameL == Just (def @EpName)]
-        let haveDefR = or [haveDefRR, epNameR == Just (def @EpName)]
+        let haveDefL = or [haveDefLL, maybe False isDefEpName epNameL]
+        let haveDefR = or [haveDefRR, maybe False isDefEpName epNameR]
 
         when haveDefL $ first (AcRight :) $ checkAllEpsNamed epNameR r
         when haveDefR $ first (AcLeft  :) $ checkAllEpsNamed epNameL l
@@ -360,7 +359,7 @@
 -- Validity of such operation is not ensured.
 epcCallRootUnsafe :: ParameterScope param => EntrypointCallT param param
 epcCallRootUnsafe = EntrypointCall
-  { epcName = def
+  { epcName = DefEpName
   , epcParamProxy = Proxy
   , epcLiftSequence = EplArgHere
   }
@@ -482,9 +481,9 @@
         , epcParamProxy = Proxy
         , epcLiftSequence = liftSeq
         }
-  , guard (epName == def) $>
+  , guard (isDefEpName epName) $>
       MkEntrypointCallRes paramNotes EntrypointCall
-        { epcName = def
+        { epcName = epName
         , epcParamProxy = Proxy
         , epcLiftSequence = EplArgHere
         }
@@ -502,11 +501,3 @@
 -- duplicate entrypoints are handled.
 flattenEntrypoints :: SingI t => ParamNotes t -> Map EpName U.Type
 flattenEntrypoints (pnNotes -> notes) = mkEntrypointsMap (mkUType notes)
-
--- TODO [#35]: Root annotation is currently support as a dedicated field
--- in 'ParamNotes'.
---
--- Also it would be nice to automatically add @%root@ annotation in each parameter
--- declaration when compiling Lorentz to Michelson.
--- In addition to this, we should actually use @%root@ annotation in the entrypoint engine
--- and not just store it.
diff --git a/src/Michelson/Typed/Haskell/Doc.hs b/src/Michelson/Typed/Haskell/Doc.hs
--- a/src/Michelson/Typed/Haskell/Doc.hs
+++ b/src/Michelson/Typed/Haskell/Doc.hs
@@ -318,6 +318,7 @@
 
 instance DocItem DType where
   type DocItemPlacement DType = 'DocItemInDefinitions
+  type DocItemReferenced DType = 'True
   docItemPos = 5000
 
   docItemSectionName = Just "Types"
@@ -359,6 +360,9 @@
         in rendered <> "\n\n"
     ]
 
+  docItemToToc lvl d@(DType ap') =
+    mdTocFromRef lvl (build $ typeDocName ap') d
+
 -- | Create a 'DType' in form suitable for putting to 'typeDocDependencies'.
 dTypeDep :: forall (t :: Kind.Type). TypeHasDoc t => SomeDocDefinitionItem
 dTypeDep = SomeDocDefinitionItem (DType (Proxy @t))
@@ -372,12 +376,19 @@
 
 -- | Doc element with description of contract storage type.
 newtype DStorageType = DStorageType DType
-  deriving stock Generic
+  deriving stock (Generic, Eq, Ord)
 
 instance DocItem DStorageType where
+  type DocItemPlacement DStorageType = 'DocItemInlined
+  type DocItemReferenced DStorageType = 'True
+
+  docItemRef (DStorageType (DType a)) = DocItemRefInlined $
+    DocItemId ("storage-" <> typeDocName a)
   docItemPos = 835
   docItemSectionName = Just "Storage"
   docItemToMarkdown lvl (DStorageType t) = docItemToMarkdown lvl t
+  docItemToToc lvl d@(DStorageType (DType a)) =
+    mdTocFromRef lvl (build $ typeDocName a) d
   docItemDependencies (DStorageType t) = docItemDependencies t
 
 -- Default implementations
diff --git a/src/Michelson/Typed/Haskell/Value.hs b/src/Michelson/Typed/Haskell/Value.hs
--- a/src/Michelson/Typed/Haskell/Value.hs
+++ b/src/Michelson/Typed/Haskell/Value.hs
@@ -151,7 +151,7 @@
 
 instance IsoValue Address where
   type ToT Address = 'TAddress
-  toVal addr = VAddress $ EpAddress addr def
+  toVal addr = VAddress $ EpAddress addr DefEpName
   fromVal (VAddress x) = eaAddress x
 
 instance IsoValue EpAddress where
diff --git a/src/Michelson/Typed/Instr.hs b/src/Michelson/Typed/Instr.hs
--- a/src/Michelson/Typed/Instr.hs
+++ b/src/Michelson/Typed/Instr.hs
@@ -20,6 +20,7 @@
   , mapEntriesOrdered
   , pattern CAR
   , pattern CDR
+  , pattern PAIR
   , pattern UNPAIR
   , PackedNotes(..)
   , ConstraintDIPN
@@ -36,6 +37,7 @@
 import qualified Text.Show
 
 import Michelson.Doc
+import Michelson.ErrorPos
 import Michelson.Printer.Util (RenderDoc(..), buildRenderDoc, needsParens, printDocS)
 import Michelson.Typed.Annotation (Notes(..))
 import Michelson.Typed.Arith
@@ -45,7 +47,7 @@
 import Michelson.Typed.Sing (KnownT)
 import Michelson.Typed.T (T(..))
 import Michelson.Typed.Value (Comparable, ContractInp, ContractOut, Value'(..))
-import Michelson.Untyped (Annotation(..), EntriesOrder(..), FieldAnn, VarAnn, entriesOrderToInt)
+import Michelson.Untyped (Annotation(..), EntriesOrder(..), FieldAnn, TypeAnn, VarAnn, entriesOrderToInt)
 import Util.Peano
 import Util.TH
 import Util.Type (type (++), KnownList)
@@ -116,6 +118,11 @@
 -- Type parameter @out@ states for output stack type or type
 -- of stack that will be left after instruction's execution.
 data Instr (inp :: [T]) (out :: [T]) where
+  -- | A wrapper carrying original source location of the instruction.
+  --
+  -- TODO [#283]: replace this wrapper with something more clever and abstract.
+  WithLoc :: InstrCallStack -> Instr a b -> Instr a b
+
   -- | A wrapper for instruction that also contain annotations for the
   -- top type on the result stack.
   --
@@ -197,7 +204,10 @@
     :: Instr s s'
     -> Instr (a ': s) s'
     -> Instr ('TOption a ': s) s'
-  PAIR :: Instr (a ': b ': s) ('TPair a b ': s)
+  -- | Annotations for PAIR instructions can be different from notes presented on the stack
+  -- in case of special field annotations, so we carry annotations for instruction
+  -- separately from notes.
+  AnnPAIR :: TypeAnn -> FieldAnn -> FieldAnn -> Instr (a ': b ': s) ('TPair a b ': s)
   LEFT :: forall b a s . KnownT b => Instr (a ': s) ('TOr a b ': s)
   RIGHT :: forall a b s . KnownT a => Instr (b ': s) ('TOr a b ': s)
   IF_LEFT
@@ -378,6 +388,9 @@
 
 pattern UNPAIR :: () => (i ~ ('TPair a b : s), o ~ (a : b : s)) => Instr i o
 pattern UNPAIR = Seq DUP (Seq CAR (DIP CDR))
+
+pattern PAIR :: () => (i ~ (a ': b ': s), o ~ ('TPair a b ': s)) => Instr i o
+pattern PAIR = AnnPAIR (AnnotationUnsafe "") (AnnotationUnsafe "") (AnnotationUnsafe "")
 
 data TestAssert (s :: [T]) where
   TestAssert
diff --git a/src/Michelson/Typed/T.hs b/src/Michelson/Typed/T.hs
--- a/src/Michelson/Typed/T.hs
+++ b/src/Michelson/Typed/T.hs
@@ -2,8 +2,6 @@
 --
 -- SPDX-License-Identifier: LicenseRef-MIT-TQ
 
-{-# LANGUAGE DataKinds #-}
-
 -- | Module, providing 'T' data type, representing Michelson
 -- language types without annotations.
 module Michelson.Typed.T
diff --git a/src/Michelson/Typed/Util.hs b/src/Michelson/Typed/Util.hs
--- a/src/Michelson/Typed/Util.hs
+++ b/src/Michelson/Typed/Util.hs
@@ -91,6 +91,7 @@
 dfsInstr settings@DfsSettings{..} step i =
   case i of
     Seq i1 i2 -> recursion2 Seq i1 i2
+    WithLoc loc i1 -> recursion1 (WithLoc loc) i1
     InstrWithNotes notes i1 -> recursion1 (InstrWithNotes notes) i1
     InstrWithVarNotes varNotes i1 -> recursion1 (InstrWithVarNotes varNotes) i1
     FrameInstr p i1 -> recursion1 (FrameInstr p) i1
@@ -155,7 +156,7 @@
     SOME{} -> step i
     NONE{} -> step i
     UNIT{} -> step i
-    PAIR{} -> step i
+    AnnPAIR{} -> step i
     LEFT{} -> step i
     RIGHT{} -> step i
     NIL{} -> step i
@@ -274,6 +275,10 @@
   where
   go :: Instr i o -> RemFail Instr i o
   go = \case
+    WithLoc loc i -> case go i of
+      RfNormal i0 ->
+        RfNormal (WithLoc loc i0)
+      r -> r
     InstrWithNotes pn i -> case go i of
       RfNormal i0 ->
         RfNormal (InstrWithNotes pn i0)
@@ -320,7 +325,7 @@
     i@SOME{} -> RfNormal i
     i@NONE{} -> RfNormal i
     i@UNIT{} -> RfNormal i
-    i@PAIR{} -> RfNormal i
+    i@AnnPAIR{} -> RfNormal i
     i@LEFT{} -> RfNormal i
     i@RIGHT{} -> RfNormal i
     i@NIL{} -> RfNormal i
diff --git a/src/Michelson/Untyped/Entrypoints.hs b/src/Michelson/Untyped/Entrypoints.hs
--- a/src/Michelson/Untyped/Entrypoints.hs
+++ b/src/Michelson/Untyped/Entrypoints.hs
@@ -5,9 +5,11 @@
 module Michelson.Untyped.Entrypoints
   ( EpName (..)
   , pattern DefEpName
+  , isDefEpName
   , epNameFromParamAnn
   , epNameToParamAnn
   , epNameFromRefAnn
+  , epNameFromSelfAnn
   , epNameToRefAnn
   , EpNameFromRefAnnError (..)
   , buildEpName
@@ -16,7 +18,6 @@
   ) where
 
 import Data.Aeson.TH (deriveJSON)
-import Data.Default (Default(..))
 import qualified Data.Map as Map
 import Fmt (Buildable(..), pretty, (+|), (|+))
 import Test.QuickCheck (Arbitrary(..), suchThatMap)
@@ -28,9 +29,31 @@
 
 -- | Entrypoint name.
 --
--- Empty if this entrypoint is default one.
--- Cannot be equal to "default", the reference implementation forbids that.
--- Also, set of allowed characters should be the same as in annotations.
+-- There are two properties we care about:
+--
+-- 1. Special treatment of the @default@ entrypoint name.
+-- @default@ is prohibited in the @CONTRACT@ instruction and in
+-- values of @address@ and @contract@ types.
+-- However, it is not prohibited in the @SELF@ instruction.
+-- Hence, the value inside @EpName@ __can__ be @"default"@, so that
+-- we can distinguish @SELF@ and @SELF %default@. It is important
+-- to distinguish them because their binary representation that is
+-- inserted into blockchain is different. For example, typechecking
+-- @SELF %default@ consumes more gas than @SELF@.
+-- In this module, we provide several smart constructors with different
+-- handling of @default@, please use the appropriate one for your use case.
+-- 2. The set of permitted characters. Intuitively, an entrypoint name should
+-- be valid only if it is a valid annotation (because entrypoints are defined
+-- using field annotations). However, it is not enforced in Tezos.
+-- It is not clear whether this behavior is intended. There is an upstream
+-- [issue](https://gitlab.com/tezos/tezos/-/issues/851) which received @bug@
+-- label, so probably it is considered a bug. Currently we treat it as a bug
+-- and deviate from upstream implementation by probiting entrypoint names that
+-- are not valid annotations. If Tezos developers fix it soon, we will be happy.
+-- If they don't, we should (maybe temporarily) remove this limitation from our
+-- code. There is an
+-- [issue](https://gitlab.com/morley-framework/morley/-/issues/275) in our
+-- repo as well.
 newtype EpName = EpNameUnsafe { unEpName :: Text }
   deriving stock (Show, Eq, Ord, Generic)
 
@@ -38,17 +61,32 @@
 
 deriveJSON morleyAesonOptions ''EpName
 
+-- | This is a bidirectional pattern that can be used for two purposes:
+--
+-- 1. Construct an 'EpName' referring to the default entrypoint.
+-- 2. Use it in pattern-matching or in equality comparison to check whether
+-- 'EpName' refers to the default entrypoint. This is trickier because there
+-- are two possible 'EpName' values referring to the default entrypoints.
+-- 'DefEpName' will match only the most common one (no entrypoint).
+-- However, there is a special case: @SELF@ instruction can have explicit
+-- @%default@ reference. For this reason, it is recommended to use
+-- 'isDefEpName' instead. Pattern-matching on 'DefEpName' is still permitted
+-- for backwards compatibility and for the cases when you are sure that
+-- 'EpName' does not come from the @SELF@ instruction.
 pattern DefEpName :: EpName
 pattern DefEpName = EpNameUnsafe ""
 
+-- | Check whether given 'EpName' refers to the default entrypoint.
+-- Unlike 'DefEpName' pattern, this function correctly handles all cases,
+-- including the @SELF@ instruction.
+isDefEpName :: EpName -> Bool
+isDefEpName epName = epName == DefEpName || epName == EpNameUnsafe "default"
+
 instance Buildable EpName where
   build = \case
     DefEpName -> "<default>"
     EpNameUnsafe name -> build name
 
-instance Default EpName where
-  def = EpNameUnsafe ""
-
 -- | Make up 'EpName' from annotation in parameter type declaration.
 --
 -- Returns 'Nothing' if no entrypoint is assigned here.
@@ -75,19 +113,34 @@
     InEpNameBadAnnotation (Annotation an) ->
       "Invalid entrypoint reference `" +| an |+ "`"
 
--- | Make up 'EpName' from annotation which is reference to an entrypoint
--- (e.g. annotation in @CONTRACT@ instruction).
+-- | Make up 'EpName' from annotation which is reference to an entrypoint.
+-- Note that it's more common for Michelson to prohibit explicit @default@
+-- entrypoint reference.
 --
--- Fails if annotation is invalid.
+-- Specifically, @%default@ annotation is probitited in values of @address@
+-- and @contract@ types. It's also prohibited in the @CONTRACT@ instruction.
+-- However, there is an exception: @SELF %default@ is a perfectly valid
+-- instruction. Hence, when you construct an 'EpName' from an annotation
+-- that's part of @SELF@, you should use 'epNameFromSelfAnn' instead.
 epNameFromRefAnn :: FieldAnn -> Either EpNameFromRefAnnError EpName
 epNameFromRefAnn an@(Annotation a)
   | a == "default" = Left $ InEpNameBadAnnotation an
   | otherwise = Right $ EpNameUnsafe a
 
+-- | Make up an 'EpName' from an annotation which is part of the
+-- @SELF@ instruction.
+epNameFromSelfAnn :: FieldAnn -> EpName
+epNameFromSelfAnn (Annotation a) = EpNameUnsafe a
+
 -- | Turn entrypoint name into annotation used as reference to entrypoint.
 epNameToRefAnn :: EpName -> FieldAnn
 epNameToRefAnn (EpNameUnsafe name) = ann name
 
+-- | Make a valid entrypoint name from an arbitrary text. This
+-- function prohibits explicit @default@ entrypoint name which is
+-- permitted by Michelson inside the @SELF@ instruction. This
+-- limitation shouldn't be restrictive because @SELF@ is equivalent to
+-- @SELF %default@.
 buildEpName :: Text -> Either String EpName
 buildEpName txt = do
   annotation <-
@@ -96,7 +149,8 @@
   epNameFromRefAnn annotation
     & first pretty
 
-unsafeBuildEpName :: Text -> EpName
+-- | Partial version of 'buildEpName'.
+unsafeBuildEpName :: HasCallStack => Text -> EpName
 unsafeBuildEpName = either (error . pretty) id . buildEpName
 
 instance Arbitrary FieldAnn => Arbitrary EpName where
diff --git a/src/Morley/CLI.hs b/src/Morley/CLI.hs
--- a/src/Morley/CLI.hs
+++ b/src/Morley/CLI.hs
@@ -32,7 +32,7 @@
 import Options.Applicative.Help.Pretty (Doc)
 
 import qualified Michelson.Parser as P
-import Michelson.Runtime (TxData(..))
+import Michelson.Runtime (TxData(..), TxParam(..))
 import Michelson.Runtime.GState (genesisAddress)
 import Michelson.Text (MText)
 import Michelson.Untyped (EpName)
@@ -118,7 +118,7 @@
     mkTxData addr param amount epName =
       TxData
         { tdSenderAddress = addr
-        , tdParameter = param
+        , tdParameter = TxUntypedParam param
         , tdEntrypoint = epName
         , tdAmount = amount
         }
diff --git a/src/Tezos/Crypto.hs b/src/Tezos/Crypto.hs
--- a/src/Tezos/Crypto.hs
+++ b/src/Tezos/Crypto.hs
@@ -65,6 +65,8 @@
   , parseKeyHash
   , parseKeyHashRaw
   , keyHashLengthBytes
+  , formatSecretKey
+  , parseSecretKey
 
   -- * Hashing
   , hashKey
@@ -89,6 +91,7 @@
 import qualified Data.ByteArray as BA
 import qualified Data.ByteString as BS
 import qualified Data.ByteString.Lazy as LBS
+import qualified Data.Text as T
 import Fmt (Buildable, build, hexF, pretty)
 import Test.QuickCheck (Arbitrary(..), elements, oneof)
 
@@ -345,6 +348,33 @@
     , fmap SignatureP256 . P256.parseSignature
     , parseImpl genericSignatureTag (pure . SignatureGeneric)
     ])
+
+formatSecretKey :: SecretKey -> Text
+formatSecretKey = \case
+  SecretKeyEd25519 sig -> Ed25519.formatSecretKey sig
+  SecretKeySecp256k1 sig -> Secp256k1.formatSecretKey sig
+  SecretKeyP256 sig -> P256.formatSecretKey sig
+
+instance Buildable SecretKey where
+  build = build . formatSecretKey
+
+-- | Parse __unencrypted__ secret key. It accepts formats containing
+-- either with or without the @unecrypted@ prefix.
+parseSecretKey :: Text -> Either CryptoParseError SecretKey
+parseSecretKey txt =
+  firstRight $ map (\f -> f $ removePrefix txt)
+    ( fmap SecretKeyEd25519 . Ed25519.parseSecretKey :|
+    [ fmap SecretKeySecp256k1 . Secp256k1.parseSecretKey
+    , fmap SecretKeyP256 . P256.parseSecretKey
+    ])
+  where
+    removePrefix :: Text -> Text
+    removePrefix input =
+      let unencrypted = "unencrypted:"
+          (prefix, payload) = T.splitAt (length unencrypted) input
+      in case prefix == unencrypted of
+        True -> payload
+        False -> input
 
 ----------------------------------------------------------------------------
 -- JSON encoding/decoding
diff --git a/src/Tezos/Crypto/P256.hs b/src/Tezos/Crypto/P256.hs
--- a/src/Tezos/Crypto/P256.hs
+++ b/src/Tezos/Crypto/P256.hs
@@ -28,6 +28,8 @@
   , formatSignature
   , mformatSignature
   , parseSignature
+  , formatSecretKey
+  , parseSecretKey
 
   -- * Signing
   , sign
@@ -138,6 +140,14 @@
 signatureLengthBytes :: Integral n => n
 signatureLengthBytes = signatureLengthBytes_ curve
 
+mkSecretKey :: ByteArray ba => ba -> Either CryptoParseError SecretKey
+mkSecretKey = Right . SecretKey . mkSecretKey_ curve
+
+-- | Convert a 'PublicKey' to raw bytes.
+secretKeyToBytes :: ByteArray ba => SecretKey -> ba
+secretKeyToBytes (SecretKey kp) =
+  secretKeyToBytes_ kp
+
 ----------------------------------------------------------------------------
 -- Magic bytes
 ----------------------------------------------------------------------------
@@ -145,6 +155,10 @@
 publicKeyTag :: ByteString
 publicKeyTag = "\003\178\139\127"
 
+-- | Base16 format is @1051eebd@
+secretKeyTag :: ByteString
+secretKeyTag = "\016\081\238\189"
+
 signatureTag :: ByteString
 signatureTag = "\054\240\044\052"
 
@@ -175,6 +189,15 @@
 
 parseSignature :: Text -> Either CryptoParseError Signature
 parseSignature = parseImpl signatureTag mkSignature
+
+formatSecretKey :: SecretKey -> Text
+formatSecretKey = formatImpl @ByteString secretKeyTag . secretKeyToBytes
+
+instance Buildable SecretKey where
+  build = build . formatSecretKey
+
+parseSecretKey :: Text -> Either CryptoParseError SecretKey
+parseSecretKey = parseImpl secretKeyTag mkSecretKey
 
 ----------------------------------------------------------------------------
 -- Signing
diff --git a/src/Tezos/Crypto/Secp256k1.hs b/src/Tezos/Crypto/Secp256k1.hs
--- a/src/Tezos/Crypto/Secp256k1.hs
+++ b/src/Tezos/Crypto/Secp256k1.hs
@@ -28,6 +28,8 @@
   , formatSignature
   , mformatSignature
   , parseSignature
+  , formatSecretKey
+  , parseSecretKey
 
   -- * Signing
   , sign
@@ -138,6 +140,14 @@
 signatureLengthBytes :: Integral n => n
 signatureLengthBytes = signatureLengthBytes_ curve
 
+mkSecretKey :: ByteArray ba => ba -> Either CryptoParseError SecretKey
+mkSecretKey = Right . SecretKey . mkSecretKey_ curve
+
+-- | Convert a 'PublicKey' to raw bytes.
+secretKeyToBytes :: ByteArray ba => SecretKey -> ba
+secretKeyToBytes (SecretKey kp) =
+  secretKeyToBytes_ kp
+
 ----------------------------------------------------------------------------
 -- Magic bytes
 ----------------------------------------------------------------------------
@@ -145,6 +155,10 @@
 publicKeyTag :: ByteString
 publicKeyTag = "\003\254\226\086"
 
+-- | Base16 format is @11a2e0c9@
+secretKeyTag :: ByteString
+secretKeyTag = "\017\162\224\201"
+
 signatureTag :: ByteString
 signatureTag = "\013\115\101\019\063"
 
@@ -175,6 +189,15 @@
 
 parseSignature :: Text -> Either CryptoParseError Signature
 parseSignature = parseImpl signatureTag mkSignature
+
+formatSecretKey :: SecretKey -> Text
+formatSecretKey = formatImpl @ByteString secretKeyTag . secretKeyToBytes
+
+instance Buildable SecretKey where
+  build = build . formatSecretKey
+
+parseSecretKey :: Text -> Either CryptoParseError SecretKey
+parseSecretKey = parseImpl secretKeyTag mkSecretKey
 
 ----------------------------------------------------------------------------
 -- Signing
diff --git a/src/Tezos/Crypto/Util.hs b/src/Tezos/Crypto/Util.hs
--- a/src/Tezos/Crypto/Util.hs
+++ b/src/Tezos/Crypto/Util.hs
@@ -19,6 +19,8 @@
   , rnfCurve
   , publicKeyLengthBytes_
   , mkSignature_
+  , mkSecretKey_
+  , secretKeyToBytes_
   , signatureToBytes_
   , mkPublicKey_
   , publicKeyToBytes_
@@ -30,6 +32,7 @@
 import Crypto.Number.ModArithmetic (squareRoot)
 import Crypto.Random (ChaChaDRG, MonadPseudoRandom, drgNewSeed, seedFromInteger, withDRG)
 import qualified Crypto.PubKey.ECC.ECDSA as ECDSA
+import qualified Crypto.PubKey.ECC.Generate as ECC.Generate
 import Crypto.PubKey.ECC.Types
   (Curve(..), CurveCommon(..), CurvePrime(..), Point(..), curveSizeBits)
 import qualified Data.Binary.Get as Get
@@ -222,6 +225,11 @@
 signatureToBytes_ curve (ECDSA.Signature r s) =
   coordToBytes curve r <> coordToBytes curve s
 
+-- | Convert a 'PublicKey' to raw bytes.
+secretKeyToBytes_ :: BA.ByteArray ba => ECDSA.KeyPair -> ba
+secretKeyToBytes_ (ECDSA.KeyPair c _ s) =
+  coordToBytes c s
+
 -- | Make a 'Signature' from raw bytes.
 mkSignature_ :: BA.ByteArray ba => Curve -> ba -> Either CryptoParseError ECDSA.Signature
 mkSignature_ curve ba
@@ -232,3 +240,10 @@
     Left $ CryptoParseUnexpectedLength "signature" l
   where
     l = BA.length ba
+
+-- | Make a 'SecretKey' from raw bytes.
+mkSecretKey_ :: BA.ByteArray ba => Curve -> ba -> ECDSA.KeyPair
+mkSecretKey_ c ba =
+  let s = os2ip ba
+      p = ECC.Generate.generateQ c s
+  in ECDSA.KeyPair c p s
diff --git a/src/Util/Markdown.hs b/src/Util/Markdown.hs
--- a/src/Util/Markdown.hs
+++ b/src/Util/Markdown.hs
@@ -10,6 +10,7 @@
   , ToAnchor (..)
   , nextHeaderLevel
   , mdHeader
+  , mdToc
   , mdSubsection
   , mdSubsectionTitle
   , mdBold
@@ -17,6 +18,7 @@
   , mdTicked
   , mdRef
   , mdLocalRef
+  , mdEscapeAnchor
   , mdAnchor
   , mdSeparator
   , mdSpoiler
@@ -27,6 +29,7 @@
 import qualified Data.String.Interpolate.IsString as Interpolate
 import Data.String.Interpolate.Util (unindent)
 import Fmt (Builder, build, (+|), (|+))
+
 import Language.Haskell.TH.Quote (QuasiQuoter(..))
 
 -- | A piece of markdown document.
@@ -61,6 +64,11 @@
 mdHeader :: HeaderLevel -> Markdown -> Markdown
 mdHeader (HeaderLevel lvl) text =
   mconcat (replicate lvl "#") +| " " +| text |+ "\n\n"
+
+mdToc :: ToAnchor anchor => HeaderLevel -> Markdown -> anchor -> Markdown
+mdToc (HeaderLevel lvl) text anchor =
+  mconcat (replicate (lvl - 2) "  ") +|
+    "- " +| mdLocalRef text anchor |+ "\n"
 
 mdSubsectionTitle :: Markdown -> Markdown
 mdSubsectionTitle title = mdBold (title <> ":")