-- SPDX-FileCopyrightText: 2020 Tocqueville Group
--
-- SPDX-License-Identifier: LicenseRef-MIT-TQ

{- | Module, carrying logic of @UNPACK@ instruction.

This is nearly symmetric to adjacent Pack.hs module.

When implementing this the following sources were used:

* https://pastebin.com/8gfXaRvp

* https://gitlab.com/tezos/tezos/-/blob/767de2b6665ec2cc21e41e6348f8a0b369d26450/src/proto_alpha/lib_protocol/script_ir_translator.ml#L2501

* https://github.com/tezbridge/tezbridge-crypto/blob/f7d93d8d04201557972e839967758cff5bbe5345/PsddFKi3/codec.js#L513

-}
module Michelson.Interpret.Unpack
  ( UnpackError (..)
  , unpackValue
  , unpackValue'
  , unpackInstr'

  -- * Internals
  , decodeContract
  , decodeType
  ) where

import Prelude hiding (EQ, Ordering(..), get)

import Control.Monad.Except (throwError)
import Data.Binary (Get)
import qualified Data.Binary.Get as Get
import qualified Data.Bits as Bits
import qualified Data.ByteString as BS
import qualified Data.ByteString.Lazy as LBS
import Data.Constraint (Dict(..))
import Data.Default (def)
import qualified Data.Kind as Kind
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Singletons (Sing, SingI(..))
import Data.Typeable ((:~:)(..))
import Fmt (Buildable, fmt, hexF, pretty, (+|), (|+))

import Michelson.Parser (Parser, ParserException(..), parseNoEnv)
import qualified Michelson.Parser.Annotations as PA
import Michelson.Text
import Michelson.TypeCheck
  (HST(..), SomeHST(..), SomeInstr(..), SomeInstrOut(..), TCError(..), TypeCheckEnv(..),
  TypeCheckMode(..), TypeContext(..), withWTPm)
import Michelson.TypeCheck.Helpers (ensureDistinctAsc, eqHST1)
import Michelson.TypeCheck.Instr (typeCheckList)
import Michelson.Typed (KnownT, RemFail(..), SingT(..), starNotes)
import qualified Michelson.Typed as T
import Michelson.Typed.Entrypoints
import Michelson.Typed.Scope (UnpackedValScope)
import Michelson.Untyped
import Tezos.Core
import Tezos.Crypto hiding (sign)
import Util.Binary
import Util.Num

----------------------------------------------------------------------------
-- Helpers
----------------------------------------------------------------------------

-- | Alias for label attaching.
(?) :: Get a -> String -> Get a
(?) = flip Get.label
infix 0 ?

-- | Read a byte and match it against given value.
expectTag :: String -> Word8 -> Get ()
expectTag desc t =
  Get.label desc $ do
    t' <- Get.getWord8
    unless (t == t') $
      fail . fmt $ "Unexpected tag value (expected 0x" +| hexF t |+
                   ", but got 0x" +| hexF t' |+ ")"


-- | Read a byte describing the primitive going further and match it against
-- expected tag in the given conditions.
--
-- Aside of context description, you have to specify number of arguments which
-- given instruction accepts when written in Michelson. For instance, @PUSH@
-- accepts two arguments - type and value.
expectDescTag :: HasCallStack => String -> Word16 -> Get ()
expectDescTag desc argsNum =
  Get.label desc $ do
    tag <- Get.getWord8
    unless (tag == expected) $
      fail . fmt $ "Unexpected preliminary tag: 0x" <> hexF tag
  where
    expected = case argsNum of
      0 -> 0x03
      1 -> 0x05
      2 -> 0x07
      3 -> 0x08
      _ -> error "Bad arguments num"
      -- Intermediate values of tag are also used and designate that annotations
      -- are also attached to the packed data. But they are never produced by
      -- @PACK@, neither @UNPACK@ seem to expect them, so for now we pretend
      -- that annotations do not exist.

-- | Read a byte indicating the number of arguments/annotations of
-- the primitive that follows it.
decodeDescTag :: String -> Get Word8
decodeDescTag desc =
  Get.label desc
    Get.getWord8

-- | Like 'many', but doesn't backtrack if next entry failed to parse
-- yet there are some bytes to consume ahead.
--
-- This function exists primarily for better error messages.
manyForced :: Get a -> Get [a]
manyForced decode = do
  emp <- Get.isEmpty
  if emp
    then return []
    else (:) <$> decode <*> manyForced decode

----------------------------------------------------------------------------
-- Michelson serialisation
----------------------------------------------------------------------------

{- Implementation notes:

* We need to know which exact type we unpack to.
For instance, serialized signatures are indistinguishable from
plain serialized bytes, so if we want to return "Value" (typed or untyped),
we need to know currently expected type. The reference implementation does
the same.

* It occured to be easier to decode to typed values and untyped instructions.
When decoding lambda, we type check given instruction, and when decoding
@PUSH@ call we untype decoded value.
One may say that this gives unreasonable performance overhead, but with the
current definition of "Value" types (typed and untyped) we cannot avoid it
anyway, because when deserializing bytearray-like data (keys, signatures, ...),
we have to convert raw bytes to human-readable 'Text' and later parse them
to bytes back at type check stage.
We console ourselves that lambdas are rarely packed.

-}

-- | Deserialize bytes into the given value.
-- Suitable for @UNPACK@ operation only.
unpackValue
  :: (UnpackedValScope t)
  => LByteString -> Either UnpackError (T.Value t)
unpackValue = launchGet (finalizeDecoder decodeValue)

-- | Like 'unpackValue', for strict byte array.
unpackValue'
  :: (UnpackedValScope t)
  => ByteString -> Either UnpackError (T.Value t)
unpackValue' = unpackValue . LBS.fromStrict

-- | Deserialize an instruction into the given value.
unpackInstr' :: ByteString -> Either UnpackError [ExpandedOp]
unpackInstr' = launchGet (finalizeDecoder decodeOps) . LBS.fromStrict

-- | Turn composable decoder into a final decoder which will be run over data.
finalizeDecoder :: Get a -> Get a
finalizeDecoder decoder =
  expectTag "Packed data start" 0x05 *> decoder <* ensureEnd

decodeValue
  :: forall t.
     (HasCallStack, UnpackedValScope t)
  => Get (T.Value t)
decodeValue = Get.label "Value" $
  case sing @t of
    STKey -> T.VKey <$> decodeAsBytesOrString
      ( decodeWithTag "key" keyDecoders
      , parsePublicKey
      )
    STUnit -> do
      expectDescTag "Unit" 0
      expectTag "Unit" 0x0B
      return T.VUnit
    STSignature -> T.VSignature <$> decodeAsBytesOrString
      ( decodeBytesLikeMaybe "signature wrong size" mkSignature
      , parseSignature
      )
    STChainId -> T.VChainId <$> decodeAsBytesOrString
      ( decodeBytesLikeMaybe "chain_id wrong size" mkChainId
      , parseChainId
      )
    STOption _ -> do
      Get.getByteString 2 >>= \case
        "\x03\x06" -> pure (T.VOption Nothing)
        "\x05\x09" -> T.VOption . Just <$> decodeValue
        other -> fail $ "Unknown option tag: " <> show other
    STList _ -> do
      decodeAsList $ T.VList <$> manyForced decodeValue
    STSet (st :: Sing st) -> withComparable st $ do
      decodeAsList $ do
        vals <- withUnpackedValueScope @st $ manyForced decodeValue
        either (fail . toString) pure $
          T.VSet . Set.fromDistinctAscList <$> ensureDistinctAsc id vals

    STPair (_:: Sing lt) (r :: Sing rt) -> do
      withUnpackedValueScope @rt $ do
        decodeDescTag "Pair" >>= \case
          0x07 -> do
            -- "Normal" pair notation, e.g. `Pair 1 2` or `Pair 1 (Pair 2 3)`
            expectTag "Pair" 0x07
            T.VPair ... (,) <$> decodeValue <*> decodeValue
          0x09 -> do
            -- Right-combed notation, e.g. `Pair 1 2 3`
            expectTag "Pair" 0x07

            -- Find out how many bytes it took to encode the pair's elements, and decode them.
            elemLen <- decodeLength ? "Right-combed pair length"
            val <- Get.isolate elemLen (go @lt @rt r) ? "Right-combed pair elements"

            -- Find out how many bytes it took to encode the pair's annotations - there should be no annotations.
            (decodeLength ? "Right-combed pair annotations' length") >>= \case
              0 -> pass
              _ -> fail "Cannot decode values with annotations"
            pure val
          0x02 -> do
            -- List notation, e.g. `{ 1 ; 2 ; 3 }`
            elemLen <- decodeLength ? "Right-combed pair length"
            Get.isolate elemLen (go @lt @rt r) ? "Right-combed pair elements"
          tag -> fail . fmt $ "Unexpected preliminary tag: 0x" <> hexF tag
      where
        go :: forall l r. (UnpackedValScope l, UnpackedValScope r) => Sing r -> Get (T.Value ('T.TPair l r))
        go singR =
          case singR of
            -- If there are more pairs to the right of the right-combed pair, decode them.
            STPair (_ :: Sing rl) (singRR :: Sing rr) -> do
              withUnpackedValueScope @rr $ do
                T.VPair ... (,) <$> decodeValue @l <*> go @rl @rr singRR
            _ ->
              T.VPair ... (,) <$> decodeValue @l <*> decodeValue @r
    STOr (_ :: Sing lt) _ ->
      withUnpackedValueScope @lt $ do
        expectDescTag "Or" 1
        Get.getWord8 >>= \case
          0x05 -> T.VOr . Left <$> decodeValue
          0x08 -> T.VOr . Right <$> decodeValue
          other -> unknownTag "or constructor" other
    STLambda (_ :: Sing t1) (_ :: Sing t2) -> do
      uinstr <- decodeOps
      withWTPm @t2 $
        withWTPm @t1 (T.VLam <$> decodeTypeCheckLam uinstr)
    STMap (st :: Sing st) (_ :: Sing sv) ->
      withUnpackedValueScope @st $
        withComparable st $ T.VMap <$> decodeMap

    STInt -> do
      expectTag "Int" 0x00
      T.VInt <$> decodeInt
    STNat -> do
      expectTag "Nat" 0x00
      T.VNat <$> decodeInt
    STString -> do
      expectTag "String" 0x01
      T.VString <$> decodeString
    STBytes -> do
      expectTag "Bytes" 0x0a
      T.VBytes <$> decodeBytes
    STMutez -> do
      expectTag "Mutez" 0x00
      mmutez <- mkMutez <$> decodeInt
      maybe (fail "Negative mutez") (pure . T.VMutez) mmutez
    STBool -> do
      expectDescTag "Bool" 0
      Get.getWord8 >>= \case
        0x0A -> pure (T.VBool True)
        0x03 -> pure (T.VBool False)
        other -> unknownTag "bool" other
    STKeyHash -> T.VKeyHash <$> decodeAsBytesOrString
      ( decodeWithTag "key_hash" keyHashDecoders
      , parseKeyHash
      )
    STTimestamp -> Get.label "Timestamp" $ Get.getWord8 >>= \case
      0x00 -> do
        T.VTimestamp . timestampFromSeconds <$> decodeInt
      0x01 -> do
        str <- decodeString
        maybe (fail $ toString $ "failed to parse timestamp from " <> unMText str)
          (pure . T.VTimestamp) $ parseTimestamp $ unMText str
      other -> unknownTag "int or string" other
    STAddress ->
      T.VAddress <$> decodeAsBytesOrString
      ( decodeBytesLike "EpAddress" parseEpAddressRaw
      , parseEpAddress
      )

withUnpackedValueScope
  :: forall a v m. (KnownT a, MonadFail m)
  => (T.UnpackedValScope a => m v)
  -> m v
withUnpackedValueScope act = case T.checkScope @(T.UnpackedValScope a) of
  Right Dict -> act
  _ -> fail "Unpackable value is required here"

withComparable
  :: forall a v m. (MonadFail m)
  => Sing a
  -> (T.Comparable a => m v)
  -> m v
withComparable a act = case T.getComparableProofS a of
  Just Dict -> act
  Nothing -> fail "Comparable type is required here"

-- | Read length of something (list, string, ...).
decodeLength :: Get Int
decodeLength = Get.label "Length" $ do
  len <- Get.getWord32be
  -- @martoon: I'm not sure whether returning 'Int' is valid here.
  -- Strictly speaking, it may be 'Word32', but there seems to be no easy way
  -- to check the reference implementation on that.
  -- One more reason to go with just 'Int' for now is that we need to be able to
  -- deserialize byte arrays, and 'BS.ByteString' keeps length of type 'Int'
  -- inside.
  fromIntegralChecked len
    & either (fail . toString) pure
    ? "Length"

decodeAsListRaw :: Get a -> Get a
decodeAsListRaw getElems = do
  l <- decodeLength ? "List length"
  Get.isolate l (getElems ? "List content")

-- | Given decoder for list content, get a whole list decoder.
decodeAsList :: Get a -> Get a
decodeAsList getElems = do
  expectTag "List" 0x02
  decodeAsListRaw getElems

decodeString :: Get MText
decodeString = do
  l <- decodeLength ? "String length"
  ss <- replicateM l Get.getWord8 ? "String content"
  ss' <- decodeUtf8' (BS.pack ss)
    & either (fail . show) pure
    ? "String UTF-8 decoding"
  mkMText ss'
    & either (fail . show) pure
    ? "Michelson string validity analysis"

decodeAsBytesRaw :: (Int -> Get a) -> Get a
decodeAsBytesRaw decode = do
  l <- decodeLength ? "Byte array length"
  decode l

decodeAsBytesOrString :: Buildable e => (Get a, Text -> Either e a) -> Get a
decodeAsBytesOrString (bytesDecoder, strParser) =
  Get.getWord8 >>= \case
    0x01 -> do
      str <- decodeString
      either (fail . pretty) pure $ strParser $ unMText str
    0x0A -> do
      decodeAsBytesRaw $ \l ->
        Get.isolate l bytesDecoder ? "Binary content"
    other -> unknownTag "text or string" other


decodeBytesLikeMaybe
  :: String -> (ByteString -> Maybe a) -> Get a
decodeBytesLikeMaybe onErr constructor = do
  bs <- getRemainingByteStringCopy
  case constructor bs of
    Nothing -> fail onErr
    Just res -> pure res

decodeBytes :: Get ByteString
decodeBytes =
  decodeAsBytesRaw $ Get.label "Bytes payload" . getByteStringCopy

decodeMap
  :: forall k v.(UnpackedValScope k, UnpackedValScope v)
  => Get $ Map (T.Value k) (T.Value v)
decodeMap = withComparable (sing @k) $ Get.label "Map" $
  decodeAsList $ do
    es <- manyForced $ do
      expectDescTag "Elt" 2
      expectTag "Elt" 0x04
      (,) <$> decodeValue <*> decodeValue
    either (fail . toString) pure $
      Map.fromDistinctAscList <$> ensureDistinctAsc fst es

-- | Read a numeric value.
decodeInt :: (Integral i, Bits.Bits i) => Get i
decodeInt = (Bits.toIntegralSized @Integer <$> loop 0 0 ? "Number")
            >>= maybe (fail "Value doesn't satisfy type ranges") pure
  where
    loop !offset !acc = do
      byte <- Get.getWord8

      let hasCont = Bits.testBit byte 7
      let doCont shft = if hasCont then loop (shft + offset) else pure
      let addAndCont shft bytePayload =
            doCont shft $ acc + Bits.shiftL (fromIntegral bytePayload) offset

      let payload = Bits.clearBit byte 7
      if offset > 0
        then addAndCont 7 payload
        else do
          let sign = if Bits.testBit byte 6 then -1 else 1
          let upayload = Bits.clearBit payload 6
          (sign *) <$> addAndCont 6 upayload

-- | Type check instruction occured from a lambda.
decodeTypeCheckLam
  :: forall inp out m.
     (T.WellTyped inp, T.WellTyped out, MonadFail m)
  => [ExpandedOp]
  -> m (RemFail T.Instr '[inp] '[out])
decodeTypeCheckLam uinstr =
  either tcErrToFail pure . run $ do
    let inp = (starNotes, Dict, noAnn) ::& SNil
    _ :/ instr' <- typeCheckList uinstr inp
    case instr' of
      instr ::: out' ->
        case eqHST1 @out out' of
          Right Refl ->
            pure $ RfNormal instr
          Left err ->
                -- dummy types, we have no full information to build untyped
                -- 'T' anyway
            let tinp = Type TUnit noAnn
                tout = Type TUnit noAnn
            in throwError $
              TCFailedOnInstr (LAMBDA noAnn tinp tout uinstr) (SomeHST inp) def
              (Just LambdaCode) (Just err)
      AnyOutInstr instr ->
        return $ RfAlwaysFails instr
  where
    run = evaluatingState tcInitEnv . runExceptT . usingReaderT def
    tcErrToFail err = fail $ "Type check failed: " +| err |+ ""
    tcInitEnv =
      TypeCheckEnv
      { tcExtFrames = error "runInstrImpl(UNPACK): tcExtFrames touched"
        --- ^ This is safe because @UNPACK@ never produces Ext instructions
      , tcMode = TypeCheckPack
      }

decodeInstr :: Get ExpandedInstr
decodeInstr = Get.label "Instruction" $ do
  pretag <- Get.getWord8 ? "Pre instr tag"
  tag <- Get.getWord8 ? "Instr tag"
  case (pretag, tag) of
    (0x03, 0x20) -> pure $ DROP
    (0x05, 0x20) -> DROPN <$> (expectTag "'DROP n' parameter" 0x00 *> decodeInt)
    (0x03, 0x21) -> DUP <$> decodeNoAnn
    (0x03, 0x4C) -> pure $ SWAP
    (0x05, 0x70) -> DIG <$> (expectTag "'DIG n' parameter" 0x00 *> decodeInt)
    (0x05, 0x71) -> DUG <$> (expectTag "'DUG n' parameter" 0x00 *> decodeInt)
    (0x07, 0x43) -> do
      (typ, val) <- decodePushVal
      an <- decodeNoAnn
      return $ PUSH an typ val
    (0x03, 0x46) -> SOME <$> decodeNoAnn <*> decodeNoAnn
    (0x05, 0x3E) -> NONE <$> decodeNoAnn <*> decodeNoAnn <*> decodeType
    (0x03, 0x4F) -> UNIT <$> decodeNoAnn <*> decodeNoAnn
    (0x07, 0x2F) -> IF_NONE <$> decodeOps <*> decodeOps
    (0x03, 0x42) -> PAIR <$> decodeNoAnn <*> decodeNoAnn <*> decodeNoAnn <*> decodeNoAnn
    (0x03, 0x16) -> CAR <$> decodeNoAnn <*> decodeNoAnn
    (0x03, 0x17) -> CDR <$> decodeNoAnn <*> decodeNoAnn
    (0x05, 0x33) -> LEFT <$> decodeNoAnn <*> decodeNoAnn <*> decodeNoAnn <*> decodeNoAnn
                         <*> decodeType
    (0x05, 0x44) -> RIGHT <$> decodeNoAnn <*> decodeNoAnn <*> decodeNoAnn <*> decodeNoAnn
                          <*> decodeType
    (0x07, 0x2E) -> IF_LEFT <$> decodeOps  <*> decodeOps
    (0x05, 0x3D) -> NIL <$> decodeNoAnn <*> decodeNoAnn <*> decodeType
    (0x03, 0x1B) -> CONS <$> decodeNoAnn
    (0x07, 0x2D) -> IF_CONS <$> decodeOps  <*> decodeOps
    (0x03, 0x45) -> SIZE <$> decodeNoAnn
    (0x05, 0x24) -> EMPTY_SET <$> decodeNoAnn <*> decodeNoAnn <*> decodeComparable
    (0x07, 0x23) -> EMPTY_MAP <$> decodeNoAnn <*> decodeNoAnn <*> decodeComparable
                              <*> decodeType
    (0x07, 0x72) -> EMPTY_BIG_MAP <$> decodeNoAnn <*> decodeNoAnn <*> decodeComparable
                                  <*> decodeType
    (0x05, 0x38) -> MAP <$> decodeNoAnn <*> decodeOps
    (0x05, 0x52) -> ITER <$> decodeOps
    (0x03, 0x39) -> MEM <$> decodeNoAnn
    (0x03, 0x29) -> GET <$> decodeNoAnn
    (0x03, 0x50) -> UPDATE <$> decodeNoAnn
    (0x07, 0x2C) -> IF <$> decodeOps  <*> decodeOps
    (0x05, 0x34) -> LOOP <$> decodeOps
    (0x05, 0x53) -> LOOP_LEFT <$> decodeOps
    (0x09, 0x31) -> do
      (ti, to, ops) <- decodeAsListRaw $
        (,,) <$> decodeType <*> decodeType <*> decodeOps
      vAnn <- decodeVAnnDef
      return $ LAMBDA vAnn ti to ops
    (0x03, 0x26) -> EXEC <$> decodeNoAnn
    (0x03, 0x73) -> APPLY <$> decodeNoAnn
    (0x05, 0x1F) -> DIP <$> decodeOps
    (0x07, 0x1F) ->
      DIPN <$> (expectTag "'DIP n' parameter" 0x00 *> decodeInt) <*> decodeOps
    (0x03, 0x27) -> pure FAILWITH
    (0x05, 0x57) -> CAST <$> decodeNoAnn <*> decodeType
    (0x03, 0x58) -> RENAME <$> decodeNoAnn
    (0x03, 0x0C) -> PACK <$> decodeNoAnn
    (0x05, 0x0D) -> UNPACK <$> decodeNoAnn <*> decodeNoAnn <*> decodeType
    (0x03, 0x1A) -> CONCAT <$> decodeNoAnn
    (0x03, 0x6F) -> SLICE <$> decodeNoAnn
    (0x03, 0x56) -> ISNAT <$> decodeNoAnn
    (0x03, 0x12) -> ADD <$> decodeNoAnn
    (0x03, 0x4B) -> SUB <$> decodeNoAnn
    (0x03, 0x3A) -> MUL <$> decodeNoAnn
    (0x03, 0x22) -> EDIV <$> decodeNoAnn
    (0x03, 0x11) -> ABS <$> decodeNoAnn
    (0x03, 0x3B) -> NEG <$> decodeNoAnn
    (0x03, 0x35) -> LSL <$> decodeNoAnn
    (0x03, 0x36) -> LSR <$> decodeNoAnn
    (0x03, 0x41) -> OR <$> decodeNoAnn
    (0x03, 0x14) -> AND <$> decodeNoAnn
    (0x03, 0x51) -> XOR <$> decodeNoAnn
    (0x03, 0x3F) -> NOT <$> decodeNoAnn
    (0x03, 0x19) -> COMPARE <$> decodeNoAnn
    (0x03, 0x25) -> EQ <$> decodeNoAnn
    (0x03, 0x3C) -> NEQ <$> decodeNoAnn
    (0x03, 0x37) -> LT <$> decodeNoAnn
    (0x03, 0x2A) -> GT <$> decodeNoAnn
    (0x03, 0x32) -> LE <$> decodeNoAnn
    (0x03, 0x28) -> GE <$> decodeNoAnn
    (0x03, 0x30) -> INT <$> decodeNoAnn
    (0x05, 0x55) -> CONTRACT <$> decodeNoAnn <*> decodeNoAnn <*> decodeType
    (0x03, 0x4D) -> TRANSFER_TOKENS <$> decodeNoAnn
    (0x03, 0x4E) -> SET_DELEGATE <$> decodeNoAnn
    (0x05, 0x1D) -> do
      contract <- decodeContract
      CREATE_CONTRACT <$> decodeNoAnn <*> decodeNoAnn <*> pure contract
    (0x03, 0x1E) -> IMPLICIT_ACCOUNT <$> decodeNoAnn
    (0x03, 0x40) -> NOW <$> decodeNoAnn
    (0x03, 0x13) -> AMOUNT <$> decodeNoAnn
    (0x03, 0x15) -> BALANCE <$> decodeNoAnn
    (0x03, 0x18) -> CHECK_SIGNATURE <$> decodeNoAnn
    (0x03, 0x0F) -> SHA256 <$> decodeNoAnn
    (0x03, 0x10) -> SHA512 <$> decodeNoAnn
    (0x03, 0x0E) -> BLAKE2B <$> decodeNoAnn
    (0x03, 0x7E) -> SHA3 <$> decodeNoAnn
    (0x03, 0x7D) -> KECCAK <$> decodeNoAnn
    (0x03, 0x2B) -> HASH_KEY <$> decodeNoAnn
    (0x03, 0x47) -> SOURCE <$> decodeNoAnn
    (0x03, 0x48) -> SENDER <$> decodeNoAnn
    (0x03, 0x49) -> SELF <$> decodeNoAnn <*> decodeNoAnn
    (0x03, 0x54) -> ADDRESS <$> decodeNoAnn
    (0x03, 0x75) -> CHAIN_ID <$> decodeNoAnn
    (0x03, 0x76) -> LEVEL <$> decodeNoAnn
    -- Instructions with annotations from here on
    (0x04, 0x21) -> DUP <$> decodeVAnn
    (0x08, 0x43) -> do
      (typ, val) <- decodePushVal
      an <- decodeVAnn
      return $ PUSH an typ val
    (0x04, 0x46) -> decodeWithTVAnns SOME
    (0x06, 0x3E) -> do
      t <- decodeType
      decodeWithTVAnns NONE <*> pure t
    (0x04, 0x4F) -> decodeWithTVAnns UNIT
    (0x04, 0x42) -> decodeWithTVF2Anns PAIR
    (0x04, 0x16) -> decodeWithVFAnns CAR
    (0x04, 0x17) -> decodeWithVFAnns CDR
    (0x06, 0x33) -> do
      t <- decodeType
      decodeWithTVF2Anns LEFT <*> pure t
    (0x06, 0x44) -> do
      t <- decodeType
      decodeWithTVF2Anns RIGHT <*> pure t
    (0x06, 0x3D) -> do
      t <- decodeType
      decodeWithTVAnns NIL <*> pure t
    (0x04, 0x1B) -> CONS <$> decodeVAnn
    (0x04, 0x45) -> SIZE<$> decodeVAnn
    (0x06, 0x24) -> do
      c <- decodeComparable
      decodeWithTVAnns EMPTY_SET <*> pure c
    (0x08, 0x23) -> do
      c <- decodeComparable
      t <- decodeType
      decodeWithTVAnns EMPTY_MAP <*> pure c <*> pure t
    (0x08, 0x72) -> do
      c <- decodeComparable
      t <- decodeType
      decodeWithTVAnns EMPTY_BIG_MAP <*> pure c <*> pure t
    (0x06, 0x38) -> do
      o <- decodeOps
      MAP <$> decodeVAnn <*> pure o
    (0x04, 0x39) -> MEM <$> decodeVAnn
    (0x04, 0x29) -> GET <$> decodeVAnn
    (0x04, 0x50) -> UPDATE <$> decodeVAnn
    (0x04, 0x26) -> EXEC <$> decodeVAnn
    (0x04, 0x73) -> APPLY <$> decodeVAnn
    (0x06, 0x57) -> do
      t <- decodeType
      CAST <$> decodeVAnn <*> pure t
    (0x04, 0x58) -> RENAME <$> decodeVAnn
    (0x04, 0x0C) -> PACK <$> decodeVAnn
    (0x06, 0x0D) -> do
      t <- decodeType
      decodeWithTVAnns UNPACK <*> pure t
    (0x04, 0x1A) -> CONCAT <$> decodeVAnn
    (0x04, 0x6F) -> SLICE <$> decodeVAnn
    (0x04, 0x56) -> ISNAT <$> decodeVAnn
    (0x04, 0x12) -> ADD <$> decodeVAnn
    (0x04, 0x4B) -> SUB <$> decodeVAnn
    (0x04, 0x3A) -> MUL <$> decodeVAnn
    (0x04, 0x22) -> EDIV <$> decodeVAnn
    (0x04, 0x11) -> ABS <$> decodeVAnn
    (0x04, 0x3B) -> NEG <$> decodeVAnn
    (0x04, 0x35) -> LSL <$> decodeVAnn
    (0x04, 0x36) -> LSR <$> decodeVAnn
    (0x04, 0x41) -> OR <$> decodeVAnn
    (0x04, 0x14) -> AND <$> decodeVAnn
    (0x04, 0x51) -> XOR <$> decodeVAnn
    (0x04, 0x3F) -> NOT <$> decodeVAnn
    (0x04, 0x19) -> COMPARE <$> decodeVAnn
    (0x04, 0x25) -> EQ <$> decodeVAnn
    (0x04, 0x3C) -> NEQ <$> decodeVAnn
    (0x04, 0x37) -> LT <$> decodeVAnn
    (0x04, 0x2A) -> GT <$> decodeVAnn
    (0x04, 0x32) -> LE <$> decodeVAnn
    (0x04, 0x28) -> GE <$> decodeVAnn
    (0x04, 0x30) -> INT <$> decodeVAnn
    (0x06, 0x55) -> do
      t <- decodeType
      decodeWithVFAnns CONTRACT <*> pure t
    (0x04, 0x4D) -> TRANSFER_TOKENS <$> decodeVAnn
    (0x04, 0x4E) -> SET_DELEGATE <$> decodeVAnn
    (0x06, 0x1D) -> do
      contract <- decodeContract
      decodeWithV2Anns CREATE_CONTRACT <*> pure contract
    (0x04, 0x1E) -> IMPLICIT_ACCOUNT <$> decodeVAnn
    (0x04, 0x40) -> NOW <$> decodeVAnn
    (0x04, 0x13) -> AMOUNT <$> decodeVAnn
    (0x04, 0x15) -> BALANCE <$> decodeVAnn
    (0x04, 0x18) -> CHECK_SIGNATURE <$> decodeVAnn
    (0x04, 0x0F) -> SHA256 <$> decodeVAnn
    (0x04, 0x10) -> SHA512 <$> decodeVAnn
    (0x04, 0x0E) -> BLAKE2B <$> decodeVAnn
    (0x04, 0x7E) -> SHA3 <$> decodeVAnn
    (0x04, 0x7D) -> KECCAK <$> decodeVAnn
    (0x04, 0x2B) -> HASH_KEY <$> decodeVAnn
    (0x04, 0x47) -> SOURCE <$> decodeVAnn
    (0x04, 0x48) -> SENDER <$> decodeVAnn
    (0x04, 0x49) -> decodeWithVFAnns SELF
    (0x04, 0x54) -> ADDRESS <$> decodeVAnn
    (0x04, 0x75) -> CHAIN_ID <$> decodeVAnn
    (0x04, 0x76) -> LEVEL <$> decodeVAnn
    (other1, other2) -> fail $ "Unknown instruction tag: 0x" +|
                        hexF other1 |+ hexF other2 |+ ""

decodePushVal :: Get (Type, Value)
decodePushVal = do
  typ <- decodeType
  T.withSomeSingT (T.fromUType typ) $ \(_ :: Sing t) ->
    case T.checkScope @(T.ConstantScope t) of
      Left bt -> fail $ "Type can not appear in PUSH because it " <> pretty bt
      Right Dict -> do
        tval <- decodeValue @t
        pure $ (typ, T.untypeValue tval)

decodeContract :: Get Contract
decodeContract = decodeAsList $ do
  result <- contractTuple
  case orderContractBlock result of
    Just contract' -> do
      pure contract'
    Nothing ->
      fail "Duplicate contract field."
  where
    decodeParamsBlock = CBParam <$> do
      expectTag "Pre contract parameter" 0x05
      expectTag "Contract parameter" 0x00
      (t, ta, root) <- decodeTWithAnns
      pure $ ParameterType (Type t ta) root
    decodeStorageBlock = CBStorage <$> do
      expectTag "Pre contract storage" 0x05
      expectTag "Contract storage" 0x01
      decodeType
    decodeCodeBlock = CBCode <$> do
      expectTag "Pre contract code" 0x05
      expectTag "Contract code" 0x02
      decodeOps

    contractBlock = decodeParamsBlock <|> decodeStorageBlock <|> decodeCodeBlock

    contractTuple = do
      result1 <- contractBlock
      result2 <- contractBlock
      result3 <- contractBlock
      pure (result1, result2, result3)


decodeOp :: Get ExpandedOp
decodeOp = Get.label "Op" $ do
  tag <- Get.lookAhead Get.getWord8
  if tag == 0x02
    then SeqEx <$> decodeOps ? "Ops seq"
    else PrimEx <$> decodeInstr ? "One op"

decodeOps :: Get [ExpandedOp]
decodeOps = decodeAsList $ manyForced decodeOp

decodeComparable :: Get Type
decodeComparable = do
  (ct, tAnn, fAnn) <- decodeComparableTWithAnns
  if fAnn == noAnn
    then pure $ Type ct tAnn
    else fail "This Comparable should not have a Field annotation"

decodeType :: Get Type
decodeType = do
  (t, tAnn, fAnn) <- decodeTWithAnns
  if fAnn == noAnn
    then pure $ Type t tAnn
    else fail "This Type should not have a Field annotation"

decodeComparableTWithAnns :: Get (T, TypeAnn, FieldAnn)
decodeComparableTWithAnns = Get.label "Comparable primitive type" $ do
  pretag <- Get.getWord8 ? "Pre simple comparable type tag"
  tag <- Get.getWord8 ? "Simple comparable type tag"
  let failMessage = "Unknown primitive tag: 0x" +| hexF pretag |+ hexF tag |+ ""
  ct <- case tag of
    0x5B -> pure TInt
    0x62 -> pure TNat
    0x68 -> pure TString
    0x69 -> pure TBytes
    0x6A -> pure TMutez
    0x59 -> pure TBool
    0x5D -> pure TKeyHash
    0x6B -> pure TTimestamp
    0x6E -> pure TAddress
    0x65 ->
      case pretag of
        0x07 -> decodeTPair
        0x08 -> decodeTPair
        0x09 -> decodeTPairN
        _ -> fail failMessage
    _ -> fail failMessage
  case pretag of
    0x03 -> (ct,,) <$> decodeNoAnn <*> decodeNoAnn
    0x04 -> decodeWithTFAnns (ct,,)
    0x05 -> decodeWithTFAnns (ct,,)
    0x07 -> (ct,,) <$> decodeNoAnn <*> decodeNoAnn
    0x08 -> decodeWithTFAnns (ct,,)
    0x09 -> decodeWithTFAnns (ct,,)
    _ -> fail failMessage

{-# ANN decodeTWithAnns ("HLint: ignore Redundant <$>" :: Text) #-}
decodeTWithAnns :: Get (T, TypeAnn, FieldAnn)
decodeTWithAnns = doDecode <|> decodeComparableTWithAnns ? "Type"
  where
    doDecode = do
      pretag <- Get.getWord8 ? "Pre complex type tag"
      tag <- Get.getWord8 ? "Complex type tag"
      case (pretag, tag) of
        (0x03, 0x5C) ->
          (,,) <$> pure TKey <*> decodeNoAnn <*> decodeNoAnn
        (0x03, 0x6C) ->
          (,,) <$> pure TUnit <*> decodeNoAnn <*> decodeNoAnn
        (0x03, 0x67) ->
          (,,) <$> pure TSignature <*> decodeNoAnn <*> decodeNoAnn
        (0x03, 0x74) ->
          (,,) <$> pure TChainId <*> decodeNoAnn <*> decodeNoAnn
        (0x05, 0x63) ->
          (,,) <$> (TOption <$> decodeType) <*> decodeNoAnn <*> decodeNoAnn
        (0x05, 0x5F) ->
          (,,) <$> (TList <$> decodeType) <*> decodeNoAnn <*> decodeNoAnn
        (0x05, 0x66) ->
          (,,) <$> (TSet <$> decodeComparable) <*> decodeNoAnn <*> decodeNoAnn
        (0x03, 0x6D) ->
          (,,) <$> pure TOperation <*> decodeNoAnn <*> decodeNoAnn
        (0x05, 0x5A) ->
          (,,) <$> (TContract <$> decodeType) <*> decodeNoAnn <*> decodeNoAnn
        (0x07, 0x64) -> do
          t <- decodeTOr
          (,,) <$> pure t <*> decodeNoAnn <*> decodeNoAnn
        (0x07, 0x5E) ->
          (,,) <$> (TLambda <$> decodeType <*> decodeType) <*> decodeNoAnn <*> decodeNoAnn
        (0x07, 0x60) ->
          (,,) <$> (TMap <$> decodeComparable <*> decodeType) <*> decodeNoAnn <*> decodeNoAnn
        (0x07, 0x61) ->
          (,,) <$> (TBigMap <$> decodeComparable <*> decodeType) <*> decodeNoAnn <*> decodeNoAnn
        -- T with annotations from here on
        (0x04, 0x5C) -> decodeWithTFAnns (TKey,,)
        (0x04, 0x6C) -> decodeWithTFAnns (TUnit,,)
        (0x04, 0x67) -> decodeWithTFAnns (TSignature,,)
        (0x04, 0x74) -> decodeWithTFAnns (TChainId,,)
        (0x06, 0x63) -> do
          t <- TOption <$> decodeType
          decodeWithTFAnns (t,,)
        (0x06, 0x5F) -> do
          t <- TList <$> decodeType
          decodeWithTFAnns (t,,)
        (0x06, 0x66) -> do
          t <- TSet <$> decodeComparable
          decodeWithTFAnns (t,,)
        (0x04, 0x6D) -> decodeWithTFAnns (TOperation,,)
        (0x06, 0x5A) -> do
          t <- TContract <$> decodeType
          decodeWithTFAnns (t,,)
        (0x08, 0x64) -> do
          t <- decodeTOr
          decodeWithTFAnns (t,,)
        (0x08, 0x5E) -> do
          t <- TLambda <$> decodeType <*> decodeType
          decodeWithTFAnns (t,,)
        (0x08, 0x60) -> do
          t <- TMap <$> decodeComparable <*> decodeType
          decodeWithTFAnns (t,,)
        (0x08, 0x61) -> do
          t <- TBigMap <$> decodeComparable <*> decodeType
          decodeWithTFAnns (t,,)
        (other1, other2) -> fail $ "Unknown primitive tag: 0x" +|
                            hexF other1 |+ hexF other2 |+ ""

-- | "Normal" pair notation, e.g. `pair int int` or `pair int (pair int int)`
decodeTPair :: Get T
decodeTPair = do
  (t1, tAnn1, fAnn1) <- decodeTWithAnns
  (t2, tAnn2, fAnn2) <- decodeTWithAnns
  pure $ TPair fAnn1 fAnn2 (Type t1 tAnn1) (Type t2 tAnn2)

-- | Right-combed notation, e.g. `pair int int int`
decodeTPairN :: Get T
decodeTPairN = do
  -- Find out how many bytes it took to encode the pair's fields, and decode them.
  fieldsLen <- decodeLength ? "'pair' number of type arguments"
  fields <- Get.isolate fieldsLen (manyForced decodeTWithAnns) ? "'pair' type arguments"
  go fields
  where
    go :: [(T, TypeAnn, FieldAnn)] -> Get T
    go = \case
      [] -> fail "The 'pair' type expects at least 2 type arguments, but 0 were given."
      [(t, _, _)] -> fail $ "The 'pair' type expects at least 2 type arguments, but only 1 was given: '" <> pretty t <> "'."
      [(t1, tAnn1, fAnn1), (t2, tAnn2, fAnn2)] ->
        pure $ TPair fAnn1 fAnn2 (Type t1 tAnn1) (Type t2 tAnn2)
      (t1, t1Ann1, fAnn1) : fields -> do
        rightCombedT <- go fields
        pure $ TPair fAnn1 noAnn (Type t1 t1Ann1) (Type rightCombedT noAnn)

decodeTOr :: Get T
decodeTOr = do
  (t1, tAnn1, fAnn1) <- decodeTWithAnns
  (t2, tAnn2, fAnn2) <- decodeTWithAnns
  pure $ TOr fAnn1 fAnn2 (Type t1 tAnn1) (Type t2 tAnn2)

----------------------------------------------------------------------------
-- Annotations
----------------------------------------------------------------------------

-- | Utility function to fill a constructor with an empty annotation
decodeNoAnn :: forall (t :: Kind.Type). Get (Annotation t)
decodeNoAnn = pure noAnn

-- | Decodes an annotations' string and uses the provided `Parser` to parse
-- untyped annotations from it. This has to produce at least one annotation
-- (Annotations' String parsing will fail otherwise)
decodeAnns :: Parser a -> Get a
decodeAnns annsParser = do
  l <- decodeLength ? "Annotations' String length"
  ss <- replicateM l Get.getWord8 ? "Annotations' String content"
  s <- decodeUtf8' (BS.pack ss)
    & either (fail . show) pure
    ? "Annotations' String UTF-8 decoding"
  either (fail . displayException . ParserException) pure $ parseNoEnv annsParser "" s

decodeVAnn :: Get VarAnn
decodeVAnn = decodeAnns PA.noteV

decodeVAnnDef :: Get VarAnn
decodeVAnnDef = decodeAnns PA.noteDef

decodeWithTVAnns :: (TypeAnn -> VarAnn -> a) -> Get a
decodeWithTVAnns f = do
  (tAnn, vAnn) <- decodeAnns PA.notesTV
  pure $ f tAnn vAnn

decodeWithTVF2Anns :: (TypeAnn -> VarAnn -> FieldAnn -> FieldAnn -> a) -> Get a
decodeWithTVF2Anns f = do
  (tAnn, vAnn, (fAnn1, fAnn2)) <- decodeAnns PA.notesTVF2Def
  pure $ f tAnn vAnn fAnn1 fAnn2

decodeWithTFAnns :: (TypeAnn -> FieldAnn -> a) -> Get a
decodeWithTFAnns f =  do
  (tAnn, fAnn) <- decodeAnns PA.notesTF
  pure $ f tAnn fAnn

decodeWithV2Anns :: (VarAnn -> VarAnn -> a) -> Get a
decodeWithV2Anns f = do
  (vAnn1, vAnn2) <- decodeAnns PA.noteV2Def
  pure $ f vAnn1 vAnn2

decodeWithVFAnns :: (VarAnn -> FieldAnn -> a) -> Get a
decodeWithVFAnns f = do
  (vAnn, fAnn) <- decodeAnns PA.notesVF
  pure $ f vAnn fAnn