content: {-# LANGUAGE ImplicitParams #-}
  
  module EVM.Format
    ( formatExpr
    , formatSomeExpr
    , formatPartial
    , formatPartialDetailed
    , formatProp
    , formatState
    , formatError
    , contractNamePart
    , contractPathPart
    , showError
    , showTree
    , showTraceTree
    , showTraceTree'
    , showValues
    , prettyvmresult
    , showCall
    , showWordExact
    , showWordExplanation
    , parenthesise
    , showValue
    , textValues
    , showAbiValue
    , prettyIfConcreteWord
    , formatBytes
    , formatBinary
    , indent
    , strip0x
    , strip0x'
    , hexByteString
    , hexText
    , showVal
    ) where
  
  import Prelude hiding (LT, GT)
  
  import EVM (traceForest, traceForest', traceContext, cheatCode)
  import EVM.ABI (getAbiSeq, parseTypeName, AbiValue(..), AbiType(..), SolError(..), Indexed(..), Event(..))
  import EVM.Dapp (DappContext(..), DappInfo(..), findSrc, showTraceLocation)
  import EVM.Expr qualified as Expr
  import EVM.Solidity (SolcContract(..), Method(..), SrcMap (..), WarningData (..), SourceCache(..))
  import EVM.Types
  import EVM.Expr (maybeLitWordSimp, maybeLitAddrSimp)
  
  import Control.Arrow ((>>>))
  import Optics.Core
  import Data.Binary.Get (runGetOrFail)
  import Data.Bits (shiftR)
  import Data.ByteString (ByteString)
  import Data.ByteString qualified as BS
  import Data.ByteString.Char8 qualified as Char8
  import Data.ByteString.Base16 qualified as BS16
  import Data.ByteString.Builder (byteStringHex, toLazyByteString)
  import Data.ByteString.Lazy (toStrict, fromStrict)
  import Data.Char qualified as Char
  import Data.DoubleWord (signedWord)
  import Data.Foldable (toList)
  import Data.List (isPrefixOf, sort)
  import Data.Map qualified as Map
  import Data.Maybe (catMaybes, fromMaybe, listToMaybe)
  import Data.Text (Text, pack, unpack, intercalate, dropEnd, splitOn)
  import Data.Text qualified as T
  import Data.Text.Encoding qualified as T
  import Data.Tree.View (showTree)
  import Data.Vector (Vector)
  import Hexdump (prettyHex)
  import Numeric (showHex)
  import Witch (into, unsafeInto, tryFrom)
  import Data.Vector.Storable qualified as VS
  import Data.Sequence qualified as Seq
  
  data Signedness = Signed | Unsigned
    deriving (Show)
  
  showDec :: Signedness -> W256 -> Text
  showDec signed (W256 w)
    | Right i' <- tryFrom i, LitAddr i' == cheatCode = "<hevm cheat address>"
    | (i :: Integer) == 2 ^ (256 :: Integer) - 1 = "MAX_UINT256"
    | otherwise = T.pack (show (i :: Integer))
    where
      i = case signed of
            Signed   -> into (signedWord w)
            Unsigned -> into w
  
  showWordExact :: Integral i => i -> Text
  showWordExact w = humanizeInteger (toInteger w)
  
  showWordExplanation :: W256 -> DappInfo -> Text
  showWordExplanation w _ | w > 0xffffffff = showDec Unsigned w
  showWordExplanation w dapp =
    case Map.lookup (unsafeInto w) dapp.abiMap of
      Nothing -> showDec Unsigned w
      Just x  -> "keccak(\"" <> x.methodSignature <> "\")"
  
  humanizeInteger :: (Num a, Integral a, Show a) => a -> Text
  humanizeInteger =
    T.intercalate ","
    . reverse
    . map T.reverse
    . T.chunksOf 3
    . T.reverse
    . T.pack
    . show
  
  prettyIfConcreteWord :: Expr EWord -> Text
  prettyIfConcreteWord = \case
    Lit w -> T.pack $ "0x" <> showHex w ""
    w -> T.pack $ show w
  
  showAbiValue :: (?context :: DappContext) => AbiValue -> Text
  showAbiValue (AbiString bs) = formatBytes bs
  showAbiValue (AbiBytesDynamic bs) = formatBytes bs
  showAbiValue (AbiBytes _ bs) = formatBytes bs
  showAbiValue (AbiAddress addr) = ppAddr (LitAddr addr) False
  showAbiValue v = pack $ show v
  
  textAbiValues :: (?context :: DappContext) => Vector AbiValue -> [Text]
  textAbiValues vs = toList (fmap showAbiValue vs)
  
  textValues :: (?context :: DappContext) => [AbiType] -> Expr Buf -> [Text]
  textValues ts (ConcreteBuf bs) =
    case runGetOrFail (getAbiSeq (length ts) ts) (fromStrict bs) of
      Right (_, _, xs) -> textAbiValues xs
      Left (_, _, _)   -> [formatBinary bs]
  textValues ts _ = fmap (const "<symbolic>") ts
  
  textValue :: (?context :: DappContext) => AbiType -> Expr Buf -> Text
  textValue ts (ConcreteBuf bs) =
    case runGetOrFail (getAbiSeq 1 [ts]) (fromStrict bs) of
      Right (_, _, xs) -> fromMaybe (internalError "impossible empty list") $ listToMaybe $ textAbiValues xs
      Left (_, _, _)   -> formatBinary bs
  textValue _ _ = "<symbolic>"
  
  parenthesise :: [Text] -> Text
  parenthesise ts = "(" <> intercalate ", " ts <> ")"
  
  showValues :: (?context :: DappContext) => [AbiType] -> Expr Buf -> Text
  showValues ts b = parenthesise $ textValues ts b
  
  showValue :: (?context :: DappContext) => AbiType -> Expr Buf -> Text
  showValue t b = textValue t b
  
  showCall :: (?context :: DappContext) => [AbiType] -> Expr Buf -> Text
  showCall ts (ConcreteBuf bs) = showValues ts $ ConcreteBuf (BS.drop 4 bs)
  showCall _ _ = "(<symbolic>)"
  
  showError :: (?context :: DappContext) => Expr Buf -> Text
  showError (ConcreteBuf bs) =
    let dappinfo = ?context.info
        bs4 = BS.take 4 bs
    in case Map.lookup (word bs4) dappinfo.errorMap of
        Just (SolError errName ts) -> errName <> " " <> showCall ts (ConcreteBuf bs)
        Nothing -> case bs4 of
                    -- Method ID for Error(string)
                    "\b\195y\160" -> showCall [AbiStringType] (ConcreteBuf bs)
                    -- Method ID for Panic(uint256)
                    "NH{q"        -> "Panic" <> parenthesise [formatBinary bs]
                    _             -> formatBinary bs
  showError b = T.pack $ show b
  
  -- the conditions under which bytes will be decoded and rendered as a string
  isPrintable :: ByteString -> Bool
  isPrintable =
    T.decodeUtf8' >>>
      either
        (const False)
        (T.all (\c-> Char.isPrint c && (not . Char.isControl) c))
  
  formatBytes :: ByteString -> Text
  formatBytes b =
    let (s, _) = BS.spanEnd (== 0) b
    in
      if isPrintable s
      then formatBString s
      else formatBinary b
  
  -- a string that came from bytes, displayed with special quotes
  formatBString :: ByteString -> Text
  formatBString b = mconcat [ "«",  T.dropAround (=='"') (pack $ formatString b), "»" ]
  
  formatBinary :: ByteString -> Text
  formatBinary =
    (<>) "0x" . T.decodeUtf8 . toStrict . toLazyByteString . byteStringHex
  
  formatSBinary :: Expr Buf -> Text
  formatSBinary e = format $ Expr.concKeccakSimpExpr e
    where
      format (ConcreteBuf bs) = formatBinary bs
      format (AbstractBuf t) = "<" <> t <> " abstract buf>"
      format e2 = T.pack $ "Symbolic expression: " <> show e2
  
  showTraceTree :: DappInfo -> VM t s -> Text
  showTraceTree dapp vm =
    let ?context = DappContext { info = dapp
                               , contracts = vm.env.contracts
                               , labels = vm.labels }
    in let forest = traceForest vm
           traces = fmap (fmap (unpack . showTrace)) forest
    in pack $ concatMap showTree traces
  
  showTraceTree' :: DappInfo -> Expr End -> Text
  showTraceTree' _ (ITE {}) = internalError "ITE does not contain a trace"
  showTraceTree' dapp leaf =
    let ?context = DappContext { info = dapp, contracts, labels }
    in let forest = traceForest' leaf
           traces = fmap (fmap (unpack . showTrace)) forest
    in pack $ concatMap showTree traces
    where TraceContext { contracts, labels } = traceContext leaf
  
  showTrace :: (?context :: DappContext) => Trace -> Text
  showTrace trace =
    let
      dapp = ?context.info
      pos =
        case showTraceLocation dapp trace of
          Left x -> " \x1b[1m" <> x <> "\x1b[0m"
          Right x -> " \x1b[1m(" <> x <> ")\x1b[0m"
    in case trace.tracedata of
      EventTrace _ bytes topics ->
        case topics of
          [] ->
            logn
          firstTopic:restTopics ->
            case maybeLitWordSimp firstTopic of
              Just topic ->
                case Map.lookup topic dapp.eventMap of
                  Just (Event name _ argInfos) ->
                    showEvent name argInfos restTopics
                  Nothing ->
                    case topics of
                      [_, t2, _, _] ->
                        -- check for ds-note logs.. possibly catching false positives
                        -- event LogNote(
                        --     bytes4   indexed  sig,
                        --     address  indexed  usr,
                        --     bytes32  indexed  arg1,
                        --     bytes32  indexed  arg2,
                        --     bytes             data
                        -- ) anonymous;
                        let
                          sig = unsafeInto $ shiftR topic 224 :: FunctionSelector
                          usr = case maybeLitWordSimp t2 of
                            Just w ->
                              pack $ show (unsafeInto w :: Addr)
                            Nothing  ->
                              "<symbolic>"
                        in
                          case Map.lookup sig dapp.abiMap of
                            Just m ->
                              lognote m.methodSignature usr
                            Nothing ->
                              logn
                      _ ->
                        logn
              Nothing ->
                logn
        where
          logn = mconcat
            [ "\x1b[36m"
            , "log" <> (pack (show (length topics)))
            , parenthesise ((map (pack . show) topics) ++ [formatSBinary bytes])
            , "\x1b[0m"
            ] <> pos
  
          showEvent eventName argInfos indexedTopics = mconcat
            [ "emit "
            , "\x1b[36m"
            , eventName
            , "\x1b[0m"
            , parenthesise (snd <$> sort (unindexedArgs <> indexedArgs))
            ] <> pos
            where
            -- We maintain the original position of event arguments since indexed
            -- and not indexed arguments can be interleaved.
            unindexedArgs :: [(Int, Text)]
            unindexedArgs =
              let (positions, names, abiTypes) = unzip3 (filterArgInfos NotIndexed)
              in zip positions (zipWith withName names (textValues abiTypes bytes))
  
            indexedArgs :: [(Int, Text)]
            indexedArgs =
              let (positions, names, abiTypes) = unzip3 (filterArgInfos Indexed)
              in zip positions (zipWith withName names (zipWith showTopic abiTypes indexedTopics))
              where
              showTopic :: AbiType -> Expr EWord -> Text
              showTopic abiType topic =
                case maybeLitWordSimp (Expr.concKeccakSimpExpr topic) of
                  Just w -> textValue abiType (ConcreteBuf (word256Bytes w))
                  _ -> "<symbolic>"
  
            withName :: Text -> Text -> Text
            withName "" value = value
            withName argName value = argName <> "=" <> value
  
            filterArgInfos :: Indexed -> [(Int, Text, AbiType)]
            filterArgInfos which =
              [ (i, argName, argType) | (i, (argName, argType, indexed)) <- zip [0..] argInfos
                                      , indexed == which
              ]
  
          lognote sig usr = mconcat
            [ "\x1b[36m"
            , "LogNote"
            , parenthesise [sig, usr, "..."]
            , "\x1b[0m"
            ] <> pos
  
      ErrorTrace e ->
        case e of
          Revert out ->
            "\x1b[91merror\x1b[0m " <> "Revert " <> showError out <> pos
          _ ->
            "\x1b[91merror\x1b[0m " <> pack (show e) <> pos
  
      ReturnTrace out (CallContext { abi = Just abi }) ->
        "← " <>
          case Map.lookup (unsafeInto abi) dapp.abiMap of
            Just m  ->
              case unzip m.output of
                ([], []) ->
                  formatSBinary out
                (_, ts) ->
                  showValues ts out
            Nothing ->
              formatSBinary out
      ReturnTrace out (CallContext {}) ->
        "← " <> formatSBinary out
      ReturnTrace out (CreationContext {}) ->
        let l = Expr.bufLength out
        in "← " <> formatExpr l <> " bytes of code"
      EntryTrace t ->
        t
      FrameTrace (CreationContext { address }) ->
        "create "
        <> ppAddr address True
        <> pos
      FrameTrace (CallContext { target, context, abi, calldata }) ->
        let calltype = if target == context
                       then "call "
                       else "delegatecall "
        in
        calltype
        <> ppAddr target False
        <> "::"
        <> case findSrcFromAddr target of
          Nothing ->
            case Map.lookup (unsafeInto (fromMaybe 0x00 abi)) dapp.abiMap of
              Just m  ->
                "\x1b[1m"
                <> m.name
                <> "\x1b[0m"
                <> showCall (catMaybes (getAbiTypes m.methodSignature)) calldata
              Nothing ->
                formatSBinary calldata
            <> pos
  
          Just solc ->
            maybe "[fallback function]"
                   (fromMaybe "[unknown method]" . maybeAbiName solc)
                   abi
            <> maybe ("(" <> formatSBinary calldata <> ")")
                     (\x -> showCall (catMaybes x) calldata)
                     (abi >>= fmap getAbiTypes . maybeAbiName solc)
            <> pos
      where
      findSrcFromAddr addr = do
        contract <- Map.lookup addr ?context.contracts
        findSrc contract ?context.info
  
  ppAddr :: (?context :: DappContext) => Expr EAddr -> Bool -> Text
  ppAddr addr alwaysShowAddr =
    let
      sourceName = case Map.lookup addr ?context.contracts of
        Nothing ->
          case addr of
            LitAddr 0x7109709ECfa91a80626fF3989D68f67F5b1DD12D -> Just "HEVM"
            _ -> Nothing
        Just contract ->
          case (findSrc contract ?context.info) of
            Just x -> Just (contractNamePart x.contractName)
            Nothing -> Nothing
      label = case do litAddr <- maybeLitAddrSimp addr
                      Map.lookup litAddr ?context.labels of
                Nothing -> ""
                Just l -> "[" <> "\x1b[1m" <> l <> "\x1b[0m" <> "]"
      name = maybe "" (\n -> "\x1b[1m" <> n <> "\x1b[0m") sourceName <> label
    in
      if name == "" then
        formatAddr addr
      else if alwaysShowAddr then
        name <> "@" <> formatAddr addr
      else
        name
  
  formatAddr :: Expr EAddr -> Text
  formatAddr = \case
    LitAddr a -> pack (show a)
    SymAddr a -> "symbolic(" <> a <> ")"
    GVar _ -> internalError "Unexpected GVar"
  
  getAbiTypes :: Text -> [Maybe AbiType]
  getAbiTypes abi = map (parseTypeName mempty) types
    where
      types =
        filter (/= "") $
          splitOn "," (dropEnd 1 (last (splitOn "(" abi)))
  
  maybeAbiName :: SolcContract -> W256 -> Maybe Text
  maybeAbiName solc abi = Map.lookup (unsafeInto abi) solc.abiMap <&> (.methodSignature)
  
  contractNamePart :: Text -> Text
  contractNamePart x = T.split (== ':') x !! 1
  
  contractPathPart :: Text -> Text
  contractPathPart x = T.split (== ':') x !! 0
  
  prettyError :: EvmError -> String
  prettyError = \case
    IllegalOverflow -> "Illegal overflow"
    SelfDestruction -> "Self destruct"
    StackLimitExceeded -> "Stack limit exceeded"
    InvalidMemoryAccess -> "Invalid memory access"
    BadJumpDestination -> "Bad jump destination"
    StackUnderrun -> "Stack underrun"
    BalanceTooLow a b -> "Balance too low. value: " <> show a <> " balance: " <> show b
    UnrecognizedOpcode a -> "Unrecognized opcode: " <> show a
    Revert (ConcreteBuf msg) -> "Revert: " <> (T.unpack $ formatBinary msg)
    Revert _ -> "Revert: <symbolic>"
    OutOfGas a b -> "Out of gas: have: " <> show a <> " need: " <> show b
    StateChangeWhileStatic -> "State change while static"
    CallDepthLimitReached -> "Call depth limit reached"
    MaxCodeSizeExceeded a b -> "Max code size exceeded: max: " <> show a <> " actual: " <> show b
    MaxInitCodeSizeExceeded a b -> "Max init code size exceeded: max: " <> show a <> " actual: " <> show b
    InvalidFormat -> "Invalid Format"
    PrecompileFailure -> "Precompile failure"
    NonexistentPrecompile a -> "Precompile at address " <> show a <> " does not exist"
    ReturnDataOutOfBounds -> "Return data out of bounds"
    NonceOverflow -> "Nonce overflow"
    BadCheatCode reason a -> "Bad cheat code: " <>  reason <> " sig: " <> show a
    NonexistentFork a -> "Fork ID does not exist: " <> show a
  
  prettyvmresult :: Expr End -> String
  prettyvmresult (Failure _ _ (Revert (ConcreteBuf ""))) = "Revert"
  prettyvmresult (Success _ _ (ConcreteBuf msg) _) =
    if BS.null msg
    then "Stop"
    else "Return: " <> show (ByteStringS msg)
  prettyvmresult (Success _ _ _ _) =
    "Return: <symbolic>"
  prettyvmresult (Failure _ _ err) = prettyError err
  prettyvmresult (Partial _ _ p) = T.unpack $ formatPartial p
  prettyvmresult r = internalError $ "Invalid result: " <> show r
  
  indent :: Int -> Text -> Text
  indent n = rstrip . T.unlines . fmap (T.replicate n (T.pack [' ']) <>) . T.lines
  
  rstrip :: Text -> Text
  rstrip = T.reverse . T.dropWhile (=='\n') . T.reverse
  
  formatError :: EvmError -> Text
  formatError = \case
    Revert buf -> T.unlines
      [ "(Revert"
      , indent 2 $ formatExpr buf
      , ")"
      ]
    e -> T.pack $ show e
  
  formatPartial :: PartialExec -> Text
  formatPartial = \case
    UnexpectedSymbolicArg pc addr opcode msg args -> T.unlines
      [ "Unexpected symbolic arguments to opcode."
      , indent 2 $ T.unlines
        [ "msg: " <> T.pack (show msg)
        , "contract addr: " <> pack (show addr)
        , "program counter: " <> T.pack (show pc)
        , "opcode: " <> T.pack opcode
        , "arguments: "
        , indent 2 $ T.unlines . fmap formatSomeExpr $ args
        ]
      ]
    MaxIterationsReached pc addr -> T.unlines
      ["Max iterations reached."
      , indent 2 $ T.unlines
        [ "contract addr: " <> T.pack (show addr)
        , "program counter: " <> T.pack (show pc)
        ]
      ]
    JumpIntoSymbolicCode pc addr idx -> T.unlines
      ["Encountered a jump into a symbolic code region."
      , indent 2 $ T.unlines
        [ "contract addr: " <> T.pack (show addr)
        , "program counter: " <> T.pack (show pc)
        , "jump dst: " <> pack (show idx)
        ]
      ]
    CheatCodeMissing pc addr selector -> T.unlines
      [ "Cheat code not recognized."
      , indent 2 $ T.unlines
        [ "contract addr: " <> T.pack (show addr)
        , "program counter: " <> T.pack (show pc)
        , "function selector: " <> T.pack (show selector)
        ]
      ]
    BranchTooDeep pc addr -> T.unlines
      ["Branch too deep."
      , indent 2 $ T.unlines
        [ "contract addr: " <> pack (show addr)
        , "program counter: " <> pack (show pc)]
      ]
  
    PrecompileMissing pc addr preAddr -> T.unlines
      ["Precompile does not exist"
      , indent 2 $ T.unlines
        [ "precompile addr: " <> pack (show preAddr)
        , "contract addr: " <> pack (show addr)
        , "program counter: " <> pack (show pc)]
      ]
  
  
  formatPartialDetailed :: Maybe (WarningData s t) -> PartialExec -> Text
  formatPartialDetailed warnData p =
    let toTxt addr pc = pack $ getSrcInfo warnData addr pc
    in case p of
      UnexpectedSymbolicArg {..} -> "Unexpected symbolic arguments to opcode: " <> T.pack opcode <> toTxt addr pc
      MaxIterationsReached {..}  -> "Max iterations reached" <> toTxt addr pc
      JumpIntoSymbolicCode {..}  -> "Encountered a jump into a symbolic code" <> toTxt addr pc
      CheatCodeMissing {..}      -> "Cheat code not recognized: " <> T.pack (show selector) <> toTxt addr pc
      PrecompileMissing {..}     -> "Precompile at address " <> pack (show preAddr) <> " does not exist, called from" <> toTxt addr pc
      BranchTooDeep {..}         -> "Branches too deep" <> toTxt addr pc
  
  getSrcInfo :: Maybe (WarningData s t) -> Expr EAddr -> Int -> String
  getSrcInfo Nothing addr pc = " at addr: " <> show addr <> " at pc: " <> show pc
  getSrcInfo (Just dat) addr pc = fromMaybe (getSrcInfo Nothing addr pc) $ do
    contr <- Map.lookup addr dat.vm.env.contracts
    pcOp <- contr.opIxMap VS.!? pc
    sMap <- Seq.lookup pcOp dat.solcContr.runtimeSrcmap
    (fname, fcontent) <- Map.lookup sMap.file dat.sourceCache.files
    let eols = BS.count 10 $ BS.take sMap.offset fcontent  -- 10 is \n
    let str = " in file \"" <> fname <> "\" on line " <> show (eols+1)
    case (BS.length fcontent > (sMap.offset + sMap.length)) of
      False -> pure str
      True  -> let relevant = BS.take sMap.length $ BS.drop sMap.offset fcontent
        in pure $ str <> " : " <> show relevant
  
  formatSomeExpr :: SomeExpr -> Text
  formatSomeExpr (SomeExpr e) = formatExpr $ Expr.simplify e
  
  formatState :: Map.Map (Expr EAddr) (Expr EContract) -> Text
  formatState store = indent 2 $ T.unlines (fmap (\(k,v) ->
                T.unlines
                  [ formatExpr k <> ":"
                  , indent 2 $ formatExpr v
                  ]) (Map.toList store))
  
  formatExpr :: Expr a -> Text
  formatExpr = go
    where
      go :: Expr a -> Text
      go x = T.stripEnd $ case x of
        Lit w -> T.pack $ show (into w :: Integer)
        (Var v) -> "(Var " <> T.pack (show v) <> ")"
        (GVar v) -> "(GVar " <> T.pack (show v) <> ")"
        LitByte w -> T.pack $ show w
  
        ITE c t f -> T.unlines
          [ "(ITE"
          , indent 2 $ T.unlines
            [ formatExpr c
            , formatExpr t
            , formatExpr f
            ]
          , ")"]
        Success asserts _ buf store -> T.unlines
          [ "(Success"
          , indent 2 $ T.unlines
            [ "Data:" , indent 2 $ formatExpr buf
            , ""
            , "State:", formatState store
            , "Assertions:", indent 2 . T.unlines $ fmap formatProp asserts
            ]
          , ")"
          ]
        Partial asserts _ err -> T.unlines
          [ "(Partial"
          , indent 2 $ T.unlines
            [ "Reason:"
            , indent 2 $ formatPartial err
            , "Assertions:"
            , indent 2 . T.unlines $ fmap formatProp asserts
            ]
          , ")"
          ]
        Failure asserts _ err -> T.unlines
          [ "(Failure"
          , indent 2 $ T.unlines
            [ "Error:"
            , indent 2 $ formatError err
            , "Assertions:"
            , indent 2 . T.unlines $ fmap formatProp asserts
            ]
          , ")"
          ]
  
        IndexWord idx val -> T.unlines
          [ "(IndexWord"
          , indent 2 $ T.unlines
            [ "idx:"
            , indent 2 $ formatExpr idx
            , "val: "
            , indent 2 $ formatExpr val
            ]
          , ")"
          ]
        ReadWord idx buf -> T.unlines
          [ "(ReadWord"
          , indent 2 $ T.unlines
            [ "idx:"
            , indent 2 $ formatExpr idx
            , "buf: "
            , indent 2 $ formatExpr buf
            ]
          , ")"
          ]
        ReadByte idx buf -> T.unlines
          [ "(ReadByte"
          , indent 2 $ T.unlines
            [ "idx:"
            , indent 2 $ formatExpr idx
            , "buf: "
            , indent 2 $ formatExpr buf
            ]
          , ")"
          ]
  
        Add a b -> fmt "Add" [a, b]
        Sub a b -> fmt "Sub" [a, b]
        Mul a b -> fmt "Mul" [a, b]
        Div a b -> fmt "Div" [a, b]
        SDiv a b -> fmt "SDiv" [a, b]
        Mod a b -> fmt "Mod" [a, b]
        SMod a b -> fmt "SMod" [a, b]
        AddMod a b c -> fmt "AddMod" [a, b, c]
        MulMod a b c -> fmt "MulMod" [a, b, c]
        Exp a b -> fmt "Exp" [a, b]
        SEx a b -> fmt "SEx" [a, b]
        Min a b -> fmt "Min" [a, b]
        Max a b -> fmt "Max" [a, b]
  
        LT a b -> fmt "LT" [a, b]
        GT a b -> fmt "GT" [a, b]
        LEq a b -> fmt "LEq" [a, b]
        GEq a b -> fmt "GEq" [a, b]
        SLT a b -> fmt "SLT" [a, b]
        SGT a b -> fmt "SGT" [a, b]
        Eq a b -> fmt "Eq" [a, b]
        EqByte a b -> fmt "EqByte" [a, b]
        IsZero a -> fmt "IsZero" [a]
  
        And a b -> fmt "And" [a, b]
        Or a b -> fmt "Or" [a, b]
        Xor a b -> fmt "Xor" [a, b]
        Not a -> fmt "Not" [a]
        SHL a b -> fmt "SHL" [a, b]
        SHR a b -> fmt "SHR" [a, b]
        SAR a b -> fmt "SAR" [a, b]
  
        e@Origin -> T.pack (show e)
        e@Coinbase -> T.pack (show e)
        e@Timestamp -> T.pack (show e)
        e@BlockNumber -> T.pack (show e)
        e@PrevRandao -> T.pack (show e)
        e@GasLimit -> T.pack (show e)
        e@ChainId -> T.pack (show e)
        e@BaseFee -> T.pack (show e)
        e@TxValue -> T.pack (show e)
        e@(Gas {}) -> "(" <> T.pack (show e) <> ")"
  
        BlockHash a -> fmt "BlockHash" [a]
        Balance a -> fmt "Balance" [a]
        CodeSize a -> fmt "CodeSize" [a]
        CodeHash a -> fmt "CodeHash" [a]
  
  
        JoinBytes zero one two three four five six seven eight nine
          ten eleven twelve thirteen fourteen fifteen sixteen seventeen
          eighteen nineteen twenty twentyone twentytwo twentythree twentyfour
          twentyfive twentysix twentyseven twentyeight twentynine thirty thirtyone -> fmt "JoinBytes"
          [ zero
          , one
          , two
          , three
          , four
          , five
          , six
          , seven
          , eight
          , nine
          , ten
          , eleven
          , twelve
          , thirteen
          , fourteen
          , fifteen
          , sixteen
          , seventeen
          , eighteen
          , nineteen
          , twenty
          , twentyone
          , twentytwo
          , twentythree
          , twentyfour
          , twentyfive
          , twentysix
          , twentyseven
          , twentyeight
          , twentynine
          , thirty
          , thirtyone
          ]
  
        LogEntry addr dat topics -> T.unlines
          [ "(LogEntry"
          , indent 2 $ T.unlines
            [ "addr:"
            , indent 2 $ formatExpr addr
            , "data:"
            , indent 2 $ formatExpr dat
            , "topics:"
            , indent 2 . T.unlines $ fmap formatExpr topics
            ]
          , ")"
          ]
  
        a@(SymAddr {}) -> "(" <> T.pack (show a) <> ")"
        LitAddr a -> T.pack (show a)
        WAddr a -> fmt "WAddr" [a]
  
        BufLength b -> fmt "BufLength" [b]
  
        C code store tStore bal nonce -> T.unlines
          [ "(Contract"
          , indent 2 $ T.unlines
            [ "code:"
            , indent 2 $ formatCode code
            , "storage:"
            , indent 2 $ formatExpr store
            , "tStorage:"
            , indent 2 $ formatExpr tStore
            , "balance:"
            , indent 2 $ formatExpr bal
            , "nonce:"
            , indent 2 $ formatNonce nonce
            ]
          , ")"
          ]
  
        -- Stores
        SLoad slot storage -> T.unlines
          [ "(SLoad"
          , indent 2 $ T.unlines
            [ "slot:"
            , indent 2 $ formatExpr slot
            , "storage:"
            , indent 2 $ formatExpr storage
            ]
          , ")"
          ]
        SStore slot val prev -> T.unlines
          [ "(SStore"
          , indent 2 $ T.unlines
            [ "slot:"
            , indent 2 $ formatExpr slot
            , "val:"
            , indent 2 $ formatExpr val
            , "store:"
            , indent 2 $ formatExpr prev
            ]
          , ")"
          ]
        AbstractStore a idx ->
          "(AbstractStore " <> formatExpr a <> " " <> T.pack (show idx) <> ")"
        ConcreteStore s -> if null s
          then "(ConcreteStore <empty>)"
          else T.unlines
            [ "(ConcreteStore"
            , indent 2 $ T.unlines
              [ "vals:"
              , indent 2 $ T.unlines $ fmap (T.pack . show) $ Map.toList s
              ]
            , ")"
            ]
  
        -- Buffers
  
        CopySlice srcOff dstOff size src dst -> T.unlines
          [ "(CopySlice"
          , indent 2 $ T.unlines
            [ "srcOffset: " <> formatExpr srcOff
            , "dstOffset: " <> formatExpr dstOff
            , "size:      " <> formatExpr size
            , "src:"
            , indent 2 $ formatExpr src
            , "dst:"
            , indent 2 $ formatExpr dst
            ]
          , ")"
          ]
        WriteWord idx val buf -> T.unlines
          [ "(WriteWord"
          , indent 2 $ T.unlines
            [ "idx:"
            , indent 2 $ formatExpr idx
            , "val:"
            , indent 2 $ formatExpr val
            , "buf:"
            , indent 2 $ formatExpr buf
            ]
          , ")"
          ]
        WriteByte idx val buf -> T.unlines
          [ "(WriteByte"
          , indent 2 $ T.unlines
            [ "idx: " <> formatExpr idx
            , "val: " <> formatExpr val
            , "buf: " <> formatExpr buf
            ]
          , ")"
          ]
        ConcreteBuf bs -> case bs of
          "" -> "(ConcreteBuf \"\")"
          _ -> T.unlines
            [ "(ConcreteBuf"
            , indent 2 $ T.pack $ prettyHex bs
            , ")"
            ]
        b@(AbstractBuf _) -> "(" <> T.pack (show b) <> ")"
  
        -- Hashes
        Keccak b -> fmt "Keccak" [b]
        SHA256 b -> fmt "SHA256" [b]
        where
          fmt nm args = T.unlines
            [ "(" <> nm
            , indent 2 $ T.unlines $ fmap formatExpr args
            , ")"
            ]
  
  formatProp :: Prop -> Text
  formatProp x = T.stripEnd $ case x of
    PEq a b -> fmt "PEq" [a, b]
    PLT a b -> fmt "PLT" [a, b]
    PGT a b -> fmt "PGT" [a, b]
    PGEq a b -> fmt "PGEq" [a, b]
    PLEq a b -> fmt "PLEq" [a, b]
    PNeg a -> fmt' "PNeg" [a]
    PAnd a b -> fmt' "PAnd" [a, b]
    POr a b -> fmt' "POr" [a, b]
    PImpl a b -> fmt' "PImpl" [a, b]
    PBool a -> T.pack (show a)
    where
      fmt nm args = T.unlines
        [ "(" <> nm
        , indent 2 $ T.unlines $ fmap formatExpr args
        , ")"
        ]
      fmt' nm args = T.unlines
        [ "(" <> nm
        , indent 2 $ T.unlines $ fmap formatProp args
        , ")"
        ]
  
  formatNonce :: Maybe W64 -> Text
  formatNonce = \case
    Just w -> T.pack $ show w
    Nothing -> "symbolic"
  
  formatCode :: ContractCode -> Text
  formatCode = \case
    UnknownCode _ -> "Unknown"
    InitCode c d -> T.unlines
      [ "(InitCode"
      , indent 2 $ T.unlines
        [ "code: " <> T.pack (bsToHex c)
        , "data: " <> formatExpr d
        ]
      , ")"
      ]
    RuntimeCode (ConcreteRuntimeCode c)
      -> "(RuntimeCode " <> T.pack (bsToHex c) <> ")"
    RuntimeCode (SymbolicRuntimeCode bs)
      -> "(RuntimeCode " <> T.pack (show (fmap formatExpr bs)) <> ")"
  
  
  strip0x :: ByteString -> ByteString
  strip0x bs = if "0x" `Char8.isPrefixOf` bs then Char8.drop 2 bs else bs
  
  strip0x' :: String -> String
  strip0x' s = if "0x" `isPrefixOf` s then drop 2 s else s
  
  hexByteString :: ByteString -> Maybe ByteString
  hexByteString bs =
    case BS16.decodeBase16Untyped bs of
      Right x -> pure x
      Left _ -> Nothing
  
  hexText :: Text -> ByteString
  hexText t =
    case BS16.decodeBase16Untyped (T.encodeUtf8 (T.drop 2 t)) of
      Right x -> x
      _ -> internalError $ "invalid hex bytestring " ++ show t
  
  showVal :: AbiValue -> Text
  showVal (AbiBytes _ bs) = formatBytes bs
  showVal (AbiAddress addr) = T.pack  . show $ addr
  showVal v = T.pack . show $ v
  