-- SPDX-FileCopyrightText: 2021 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

module Test.Interpreter.Reference
  ( test_InterpreterWithReferenceImplementation
  , test_Regression688
  ) where

import Data.Default (def)
import Data.Singletons (Sing)
import Data.Typeable ((:~:)(Refl))
import Fmt (pretty)
import Hedgehog (MonadTest, PropertyT, annotate, evalIO, forAll, property, withTests, (===))
import System.IO.Silently (silence)
import Test.Tasty (TestTree, testGroup)
import Test.Tasty.Hedgehog (testProperty)

import Hedgehog.Gen.Michelson.Typed (genValue)
import Morley.AsRPC (AsRPC, MaybeRPC(..), TAsRPC, rpcStorageScopeEvi, valueAsRPC)
import Morley.Client (RunError(..), runMorleyClientM)
import Morley.Client.RPC (RunCodeErrors(..))
import Morley.Client.Util as Reference (RunContractParameters(..), runContract)
import Morley.Michelson.Interpret
  (InterpretError(..), MichelsonFailed(..), MichelsonFailureWithStack(..))
import Morley.Michelson.Runtime as Morley
import Morley.Michelson.Runtime.GState (genesisAddress)
import Morley.Michelson.TypeCheck (TypeCheckOptions(..))
import Morley.Michelson.Typed
  (Contract, Contract'(..), EpAddress(..), SingT(..), SomeConstrainedValue(..), SomeContract(..),
  SomeStorage, Value, Value'(..), dfsMapValue)
import Morley.Michelson.Typed.Arith (ArithError(..), MutezArithErrorType(..))
import Morley.Michelson.Typed.Convert
import Morley.Michelson.Typed.Scope
import Morley.Michelson.Typed.T
import Morley.Michelson.Untyped qualified as U
import Morley.Tezos.Address
import Morley.Tezos.Core (Timestamp(..), dummyChainId, getCurrentTime, zeroMutez)
import Morley.Tezos.Crypto
import Morley.Util.Named
import Morley.Util.Sing (eqI)
import Test.Cleveland (NetworkEnv(neMorleyClientEnv))
import Test.Cleveland.Michelson.Import
import Test.Cleveland.Tasty (whenNetworkEnabled)
import Test.Cleveland.Util (failedTest)
import Test.Util.Contracts (getWellTypedMichelsonContracts)

test_InterpreterWithReferenceImplementation :: IO TestTree
test_InterpreterWithReferenceImplementation = do
  files <- filter (`notElem` excludedContracts) <$> getWellTypedMichelsonContracts

  filesAndContracts :: [(FilePath, SomeContract)] <-
    forM files $ \file -> do
      someContract <- importSomeContract file
      pure (file, someContract)

  pure $
    whenNetworkEnabled $ \withEnv ->
      testGroup "compare interpreter with reference implementation" $
        withFrozenCallStack $ testContract withEnv <$> filesAndContracts
  where
    -- These constracts are currently excluded from the tests since
    -- our or reference implementations doesn't act in an expected way.
    --
    -- Ideally, we should remove the usage of this list one day :coolstory:
    excludedContracts :: [FilePath]
    excludedContracts =
      [ "../../contracts/tezos_examples/mini_scenarios/replay.tz"
      , "../../contracts/replay_origination.tz"
      , "../../contracts/replay_transfer.tz"
      -- ↑ See [#320] and https://gitlab.com/tezos/tezos/-/issues/897
      , "../../contracts/call_self_several_times.tz"
      , "../../contracts/tezos_examples/attic/cps_fact.tz"
      -- ↑ Due to that fact that 'run_code' doesn't perform internal operations in contrary to morley interpreter
      , "../../contracts/tezos_examples/mini_scenarios/multiple_entrypoints_counter.tz"
      , "../../contracts/tezos_examples/mini_scenarios/multiple_en2.tz"
      -- TODO [#699]: find out why these still fail
      -- ↑ 'SELF' and 'SENDER' instruction return same addresses in 'run_code'
      , "../../contracts/tezos_examples/mini_scenarios/lockup.tz"
      , "../../contracts/tezos_examples/attic/forward.tz"
      -- ↑ Reference 'run_code' implementation does something weird to allow transfers with arbitrary
      -- amounts even when BALANCE + AMOUNT < required amount of money that needs to be transfered.
      -- This probably will be resolved in https://gitlab.com/tezos/tezos/-/issues/897, when 'run_code'
      -- will actually try to apply operation instead of running it inside weird environment.
      -- Or in [#406] if the issue turns to be on our side.
      , "../../contracts/voting_powers.tz"
      , "../../contracts/tezos_examples/opcodes/voting_power.tz"
      -- ↑ We cannot predict the total voting power in a real chain.
      -- There is still a similar @voting_power.tz@ that touches only
      -- @VOTING_POWER@ instruction.
      , "../../contracts/tezos_examples/opcodes/level.tz"
      -- ↑ We cannot predict the actual block level in a real chain.
      -- There is another @../../contracts/level.tz@ contract that checks that we can interpret
      -- the @LEVEL@ instruction, without checking its result.
      , "../../contracts/sapling_annot.tz"
      , "../../contracts/sapling_transaction.tz"
      , "../../contracts/tezos_examples/opcodes/sapling_empty_state.tz"
      -- ↑ Sapling types and instructions are supported for typechecking only and not the actual
      -- implementation.
     ]

test_Regression688 :: IO TestTree
test_Regression688 = do
  let file = "../../contracts/tezos_examples/mini_scenarios/xcat_dapp.tz"
      parameter = VOr @_ @('TOr 'TBytes 'TBytes) $ Left $
        VPair
          (VAddress $ EpAddress
            { eaAddress = KeyAddress $ KeyHash
                { khTag = KeyHashEd25519
                , khBytes = "UK\224\155\204\188\151\163%\183I\194*H\252P\246\&4\192\205"
                }
            , eaEntrypoint = U.DefEpName}
          , VPair (VBytes "", VTimestamp $ Timestamp 1225497600)
          )
      storage = VPair (
        VBigMap @'TBytes @('TPair ('TPair 'TAddress 'TAddress) ('TPair 'TMutez 'TTimestamp))
          Nothing mempty,VUnit)

  contract <- importContract file

  pure $
    whenNetworkEnabled $ \withEnv ->
      testProperty "#688 regression test" $ withTests 1 $ property $
        withFrozenCallStack $ compareWithReference withEnv file contract parameter storage

testContract
  :: HasCallStack
  => (forall a. (NetworkEnv -> IO a) -> IO a)
  -> (FilePath, SomeContract) -> TestTree
testContract withEnv (file, someContract) =
  case someContract of
    SomeContract (contract@Contract {} :: Contract cp st) ->
      -- We run each contract 4 times to check that it behaves the same way on different
      -- inputs.
      testProperty ("compare result with morley interpreter for " <> file) $
        withTests 4 $ property $ do
          parameter <- forAll $ genValue @cp
          storage <- forAll $ genValue @st

          compareWithReference withEnv file contract parameter storage

compareWithReference
  :: forall cp st. (ParameterScope cp, StorageScope st)
  => (forall a. (NetworkEnv -> IO a) -> IO a)
  -> FilePath -> Contract cp st -> Value cp -> Value st -> PropertyT IO ()
compareWithReference withEnv file contract parameter storage = do
  (resReference, resMorley) <-
    evalIO $
      withEnv \env -> do
        resReference <- try @_ @RunCodeErrors $
          runMorleyClientM (neMorleyClientEnv env) $
            Reference.runContract @cp @st RunContractParameters
              { rcpContract = contract
              , rcpParameter = NotRPC parameter
              , rcpStorage = NotRPC storage
              , rcpBalance = 4000000000000
              , rcpAmount = zeroMutez
              , rcpSender = Just genesisAddress
              , rcpSource = Just genesisAddress
              }
        currentTimestamp <- getCurrentTime
        -- Reference implementation sends 0,05 tz to implicit contract for this contract
        let amount = if file == "../../contracts/tezos_examples/opcodes/proxy.tz"
                    then 50000 else minBound
        resMorley <- try @_ @ExecutorError $ silence $
          Morley.runContract (Just currentTimestamp) (Just 0) 100500 4000000000000 ""
          tcOptions (untypeValue storage) (convertContract contract)
          (TxData genesisAddress (TxUntypedParam $ untypeValue parameter) U.DefEpName amount)
          (#verbose :! False)
          (#dryRun :! True)

        pure (resReference, resMorley)

  compareResults resReference resMorley parameter storage

tcOptions :: TypeCheckOptions
tcOptions = def
  { -- Since we test against @tezos-client run@
    tcStrict = False
  }

compareResults
      :: forall cp st m.
         (HasCallStack, StorageScope st, MonadTest m)
      => Either RunCodeErrors (AsRPC (Value st))
      -> Either ExecutorError SomeStorage -> Value cp -> Value st -> m ()
compareResults (Left rpcErr) (Left interpreterErr) _ _ = compareErrors rpcErr interpreterErr
compareResults (Left err) (Right _) parameter storage = do
  failedTest . fromString $
    "Morley interpreter unexpectedly didn't fail.\n Passed parameter: " <> pretty parameter <>
    ".\n Passed storage: " <> pretty storage <> ".\n Reference implementation failed with: " <>
    pretty err
compareResults (Right _) (Left err) parameter storage = do
  failedTest . fromString $
    "Morley interpreter unexpectedly failed.\n " <> "Passed parameter: " <> pretty parameter <>
    ".\n Passed storage: " <> pretty storage <> ".\n Morley interpreter failed with: " <>
    displayException err
compareResults (Right st1) (Right (SomeStorage (st2 :: Value st2))) parameter storage =
  withDict (rpcStorageScopeEvi @st) $ do
    case eqI @st @st2 of
      Nothing ->
        failedTest . fromString $ "Result storages have different types.\n" <>
          "Reference implementation returned storage: " <> pretty st1 <> ".\n" <>
          "Morley returned storage: " <> pretty st2
      Just Refl -> do
        annotate $
          ("Both contracts succeeded, but new storages are different.\n Passed parameter: " <>
            pretty parameter <> ".\n Passed storage: " <> pretty storage <> ".\n" <>
            "Reference implementation returned storage: " <> pretty st1 <> ".\n" <>
            "Morley returned storage: " <> pretty st2
          )
        compareValues st1 st2

-- | Compare values with weaken equality requirements, e.g. we don't
-- check that @VAddress@, @VBytes@, @VChainId@ and @VTimestamp@ have same constructor arguments,
-- since they can be different even when both interpreters were successfully run.
--
-- We also don't check big_map contents or their IDs.
--
-- TODO [#604]: compare big_maps' contents.
compareValues :: forall st m. (HasCallStack, MonadTest m, SingI st) => Value (TAsRPC st) -> Value st -> m ()
compareValues storageReference storageMorley =
  preprocessValue storageReference === preprocessValue (valueAsRPC storageMorley)
  where
    preprocessValue :: Value (TAsRPC st) -> Value (TAsRPC st)
    preprocessValue = dfsMapValue placeStubs . scrubBigMapIDs (sing @st)

    placeStubs :: Value t -> Value t
    placeStubs = \case
      VAddress _ -> VAddress $ EpAddress genesisAddress U.DefEpName
      VBytes _ -> VBytes "kek"
      VChainId _ -> VChainId dummyChainId
      VTimestamp _ -> VTimestamp $ Timestamp 100
      v -> v

    -- | Scrub all big_map IDs from a storage value.
    --
    -- The morley interpreter and the RPC might assign different IDs to each big_map,
    -- so we need to scrub all IDs before checking whether the two storages are equivalent.
    scrubBigMapIDs :: forall t. Sing t -> Value (TAsRPC t) -> Value (TAsRPC t)
    scrubBigMapIDs storageSing storage =
      case (storageSing, storage) of
        (STBigMap{}, VNat _) -> VNat 0
        (STOption vSing, VOption v) -> VOption $ scrubBigMapIDs vSing <$> v
        (STList vSing, VList v) -> VList $ scrubBigMapIDs vSing <$> v
        (STPair lSing rSing, VPair v) -> VPair $ bimap (scrubBigMapIDs lSing) (scrubBigMapIDs rSing) v
        (STOr lSing rSing, VOr v) -> VOr $ bimap (scrubBigMapIDs lSing) (scrubBigMapIDs rSing) v
        (STMap _ vSing, VMap v) -> VMap $ scrubBigMapIDs vSing <$> v
        _ -> storage

assertRpcErrs :: (HasCallStack, MonadTest m) => [RunError] -> (RunError -> Bool) -> String -> m ()
assertRpcErrs errs predicate msg =
  if any predicate errs then pass else do failedTest $ fromString msg

-- Note that error comparison can be extended when the new contracts will be added.
compareErrors :: (HasCallStack, MonadTest m) => RunCodeErrors -> ExecutorError -> m ()
compareErrors rpcErr@(RunCodeErrors errs) interpreterErr = case interpreterErr of
  EEInterpreterFailed _ (InterpretError (mfwsFailed -> runtimeErr, _)) -> case runtimeErr of
    MichelsonFailedWith _ ->
      assertRpcErrs errs
      (\case
          ScriptRejected {} -> True
          _ -> False
      ) $ "Morley interpreter failed with FAILWITH, \
          \however reference interpreter failed with:\n" <> displayException rpcErr
    MichelsonArithError arithErr -> case arithErr of
      ShiftArithError {}->
        assertRpcErrs errs
        (\case
            ScriptOverflow -> True
            _ -> False
        ) $ "Morley interpreter failed with shift overflow, \
            \however reference interpreter failed with:\n" <> displayException rpcErr
      MutezArithError AddOverflow _ _ ->
        assertRpcErrs errs
        (\case
            MutezAdditionOverflow {} -> True
            _ -> False
        ) $ "Morley interpreter failed with mutez addition overflow, \
            \however reference interpreter failed with:\n" <> displayException rpcErr
      MutezArithError MulOverflow _ _ ->
        assertRpcErrs errs
        (\case
            MutezMultiplicationOverflow {} -> True
            ScriptOverflow -> True
            _ -> False
        ) $ "Morley interpreter failed with mutez multiplication overflow, \
            \however reference interpreter failed with:\n" <> displayException rpcErr
    MichelsonGasExhaustion ->
      assertRpcErrs errs
      (\case
          GasExhaustedOperation -> True
          _ -> False
      ) $ "Morley interpreter failed due to gas exhaustion, \
          \however reference interpreter failed with:\n" <> displayException rpcErr
    _ -> do
      failedTest . fromString $ "Unexpected morley runtime failure:\n" <> pretty runtimeErr <>
          "\nReference interpreter failed with:\n" <> displayException rpcErr
  EEIllTypedParameter _ _ ->
    assertRpcErrs errs
    (\case
        InconsistentTypes {} -> True
        BadContractParameter {} -> True
        _ -> False
    ) $ "Morley interpreter failed during parmeter typechecking, \
        \however reference interpreter failed with:\n" <> displayException rpcErr
  _ -> do
    failedTest . fromString $ "Unexpected morley interpreter failure:\n" <> displayException interpreterErr <>
      "\nReference interpreter failed with:\n" <> displayException rpcErr