(* Generated by coq-of-rust *)
Require Import CoqOfRust.CoqOfRust.

Module handler.
  Module mainnet.
    Module pre_execution.
      (*
      pub fn load_precompiles<SPEC: Spec, DB: Database>() -> ContextPrecompiles<DB> {
          Precompiles::new(PrecompileSpecId::from_spec_id(SPEC::SPEC_ID))
              .clone()
              .into()
      }
      *)
      Definition load_precompiles (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ SPEC; DB ], [] =>
          ltac:(M.monadic
            (M.call_closure (|
              M.get_trait_method (|
                "core::convert::Into",
                Ty.path "revm_precompile::Precompiles",
                [
                  Ty.apply
                    (Ty.path "revm::context::context_precompiles::ContextPrecompiles")
                    []
                    [ DB ]
                ],
                "into",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.path "revm_precompile::Precompiles",
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "revm_precompile::Precompiles",
                        "new",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "revm_precompile::PrecompileSpecId",
                            "from_spec_id",
                            []
                          |),
                          [
                            M.read (|
                              M.get_constant (| "revm_primitives::specification::Spec::SPEC_ID" |)
                            |)
                          ]
                        |)
                      ]
                    |)
                  ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_load_precompiles :
        M.IsFunction "revm::handler::mainnet::pre_execution::load_precompiles" load_precompiles.
      
      (*
      pub fn load_accounts<SPEC: Spec, EXT, DB: Database>(
          context: &mut Context<EXT, DB>,
      ) -> Result<(), EVMError<DB::Error>> {
          // set journaling state flag.
          context.evm.journaled_state.set_spec_id(SPEC::SPEC_ID);
      
          // load coinbase
          // EIP-3651: Warm COINBASE. Starts the `COINBASE` address warm
          if SPEC::enabled(SHANGHAI) {
              context.evm.inner.journaled_state.initial_account_load(
                  context.evm.inner.env.block.coinbase,
                  &[],
                  &mut context.evm.inner.db,
              )?;
          }
      
          context.evm.load_access_list()?;
          Ok(())
      }
      *)
      Definition load_accounts (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ SPEC; EXT; DB ], [ context ] =>
          ltac:(M.monadic
            (let context := M.alloc (| context |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "revm::journaled_state::JournaledState",
                          "set_spec_id",
                          []
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::deref::DerefMut",
                                Ty.apply
                                  (Ty.path "revm::context::evm_context::EvmContext")
                                  []
                                  [ DB ],
                                [],
                                "deref_mut",
                                []
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| context |),
                                  "revm::context::Context",
                                  "evm"
                                |)
                              ]
                            |),
                            "revm::context::inner_evm_context::InnerEvmContext",
                            "journaled_state"
                          |);
                          M.read (|
                            M.get_constant (| "revm_primitives::specification::Spec::SPEC_ID" |)
                          |)
                        ]
                      |)
                    |) in
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "revm_primitives::specification::Spec",
                                      SPEC,
                                      [],
                                      "enabled",
                                      []
                                    |),
                                    [
                                      Value.StructTuple
                                        "revm_primitives::specification::SpecId::SHANGHAI"
                                        []
                                    ]
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            let~ _ :=
                              M.match_operator (|
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::ops::try_trait::Try",
                                      Ty.apply
                                        (Ty.path "core::result::Result")
                                        []
                                        [
                                          Ty.apply
                                            (Ty.path "&mut")
                                            []
                                            [ Ty.path "revm_primitives::state::Account" ];
                                          Ty.apply
                                            (Ty.path "revm_primitives::result::EVMError")
                                            []
                                            [ Ty.associated ]
                                        ],
                                      [],
                                      "branch",
                                      []
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "revm::journaled_state::JournaledState",
                                          "initial_account_load",
                                          [ DB ]
                                        |),
                                        [
                                          M.SubPointer.get_struct_record_field (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| context |),
                                                "revm::context::Context",
                                                "evm"
                                              |),
                                              "revm::context::evm_context::EvmContext",
                                              "inner"
                                            |),
                                            "revm::context::inner_evm_context::InnerEvmContext",
                                            "journaled_state"
                                          |);
                                          M.read (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (|
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.read (| context |),
                                                        "revm::context::Context",
                                                        "evm"
                                                      |),
                                                      "revm::context::evm_context::EvmContext",
                                                      "inner"
                                                    |),
                                                    "revm::context::inner_evm_context::InnerEvmContext",
                                                    "env"
                                                  |)
                                                |),
                                                "revm_primitives::env::Env",
                                                "block"
                                              |),
                                              "revm_primitives::env::BlockEnv",
                                              "coinbase"
                                            |)
                                          |);
                                          M.alloc (| Value.Array [] |);
                                          M.SubPointer.get_struct_record_field (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| context |),
                                                "revm::context::Context",
                                                "evm"
                                              |),
                                              "revm::context::evm_context::EvmContext",
                                              "inner"
                                            |),
                                            "revm::context::inner_evm_context::InnerEvmContext",
                                            "db"
                                          |)
                                        ]
                                      |)
                                    ]
                                  |)
                                |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ0_0 :=
                                        M.SubPointer.get_struct_tuple_field (|
                                          γ,
                                          "core::ops::control_flow::ControlFlow::Break",
                                          0
                                        |) in
                                      let residual := M.copy (| γ0_0 |) in
                                      M.alloc (|
                                        M.never_to_any (|
                                          M.read (|
                                            M.return_ (|
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::ops::try_trait::FromResidual",
                                                  Ty.apply
                                                    (Ty.path "core::result::Result")
                                                    []
                                                    [
                                                      Ty.tuple [];
                                                      Ty.apply
                                                        (Ty.path
                                                          "revm_primitives::result::EVMError")
                                                        []
                                                        [ Ty.associated ]
                                                    ],
                                                  [
                                                    Ty.apply
                                                      (Ty.path "core::result::Result")
                                                      []
                                                      [
                                                        Ty.path "core::convert::Infallible";
                                                        Ty.apply
                                                          (Ty.path
                                                            "revm_primitives::result::EVMError")
                                                          []
                                                          [ Ty.associated ]
                                                      ]
                                                  ],
                                                  "from_residual",
                                                  []
                                                |),
                                                [ M.read (| residual |) ]
                                              |)
                                            |)
                                          |)
                                        |)
                                      |)));
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ0_0 :=
                                        M.SubPointer.get_struct_tuple_field (|
                                          γ,
                                          "core::ops::control_flow::ControlFlow::Continue",
                                          0
                                        |) in
                                      let val := M.copy (| γ0_0 |) in
                                      val))
                                ]
                              |) in
                            M.alloc (| Value.Tuple [] |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::try_trait::Try",
                            Ty.apply
                              (Ty.path "core::result::Result")
                              []
                              [
                                Ty.tuple [];
                                Ty.apply
                                  (Ty.path "revm_primitives::result::EVMError")
                                  []
                                  [ Ty.associated ]
                              ],
                            [],
                            "branch",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "revm::context::inner_evm_context::InnerEvmContext")
                                  []
                                  [ DB ],
                                "load_access_list",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::deref::DerefMut",
                                    Ty.apply
                                      (Ty.path "revm::context::evm_context::EvmContext")
                                      []
                                      [ DB ],
                                    [],
                                    "deref_mut",
                                    []
                                  |),
                                  [
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| context |),
                                      "revm::context::Context",
                                      "evm"
                                    |)
                                  ]
                                |)
                              ]
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::control_flow::ControlFlow::Break",
                                0
                              |) in
                            let residual := M.copy (| γ0_0 |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  M.return_ (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::ops::try_trait::FromResidual",
                                        Ty.apply
                                          (Ty.path "core::result::Result")
                                          []
                                          [
                                            Ty.tuple [];
                                            Ty.apply
                                              (Ty.path "revm_primitives::result::EVMError")
                                              []
                                              [ Ty.associated ]
                                          ],
                                        [
                                          Ty.apply
                                            (Ty.path "core::result::Result")
                                            []
                                            [
                                              Ty.path "core::convert::Infallible";
                                              Ty.apply
                                                (Ty.path "revm_primitives::result::EVMError")
                                                []
                                                [ Ty.associated ]
                                            ]
                                        ],
                                        "from_residual",
                                        []
                                      |),
                                      [ M.read (| residual |) ]
                                    |)
                                  |)
                                |)
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::control_flow::ControlFlow::Continue",
                                0
                              |) in
                            let val := M.copy (| γ0_0 |) in
                            val))
                      ]
                    |) in
                  M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_load_accounts :
        M.IsFunction "revm::handler::mainnet::pre_execution::load_accounts" load_accounts.
      
      (*
      pub fn deduct_caller_inner<SPEC: Spec>(caller_account: &mut Account, env: &Env) {
          // Subtract gas costs from the caller's account.
          // We need to saturate the gas cost to prevent underflow in case that `disable_balance_check` is enabled.
          let mut gas_cost = U256::from(env.tx.gas_limit).saturating_mul(env.effective_gas_price());
      
          // EIP-4844
          if SPEC::enabled(CANCUN) {
              let data_fee = env.calc_data_fee().expect("already checked");
              gas_cost = gas_cost.saturating_add(data_fee);
          }
      
          // set new caller account balance.
          caller_account.info.balance = caller_account.info.balance.saturating_sub(gas_cost);
      
          // bump the nonce for calls. Nonce for CREATE will be bumped in `handle_create`.
          if matches!(env.tx.transact_to, TransactTo::Call(_)) {
              // Nonce is already checked
              caller_account.info.nonce = caller_account.info.nonce.saturating_add(1);
          }
      
          // touch account so we know it is changed.
          caller_account.mark_touch();
      }
      *)
      Definition deduct_caller_inner (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ SPEC ], [ caller_account; env ] =>
          ltac:(M.monadic
            (let caller_account := M.alloc (| caller_account |) in
            let env := M.alloc (| env |) in
            M.read (|
              let~ gas_cost :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "ruint::Uint")
                        [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                        [],
                      "saturating_mul",
                      []
                    |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "ruint::Uint")
                            [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4
                            ]
                            [],
                          "from",
                          [ Ty.path "u64" ]
                        |),
                        [
                          M.read (|
                            M.SubPointer.get_struct_record_field (|
                              M.SubPointer.get_struct_record_field (|
                                M.read (| env |),
                                "revm_primitives::env::Env",
                                "tx"
                              |),
                              "revm_primitives::env::TxEnv",
                              "gas_limit"
                            |)
                          |)
                        ]
                      |);
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "revm_primitives::env::Env",
                          "effective_gas_price",
                          []
                        |),
                        [ M.read (| env |) ]
                      |)
                    ]
                  |)
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "revm_primitives::specification::Spec",
                                  SPEC,
                                  [],
                                  "enabled",
                                  []
                                |),
                                [
                                  Value.StructTuple
                                    "revm_primitives::specification::SpecId::CANCUN"
                                    []
                                ]
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ data_fee :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "core::option::Option")
                                  []
                                  [
                                    Ty.apply
                                      (Ty.path "ruint::Uint")
                                      [
                                        Value.Integer IntegerKind.Usize 256;
                                        Value.Integer IntegerKind.Usize 4
                                      ]
                                      []
                                  ],
                                "expect",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "revm_primitives::env::Env",
                                    "calc_data_fee",
                                    []
                                  |),
                                  [ M.read (| env |) ]
                                |);
                                M.read (| Value.String "already checked" |)
                              ]
                            |)
                          |) in
                        let~ _ :=
                          M.write (|
                            gas_cost,
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "ruint::Uint")
                                  [
                                    Value.Integer IntegerKind.Usize 256;
                                    Value.Integer IntegerKind.Usize 4
                                  ]
                                  [],
                                "saturating_add",
                                []
                              |),
                              [ M.read (| gas_cost |); M.read (| data_fee |) ]
                            |)
                          |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ _ :=
                M.write (|
                  M.SubPointer.get_struct_record_field (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| caller_account |),
                      "revm_primitives::state::Account",
                      "info"
                    |),
                    "revm_primitives::state::AccountInfo",
                    "balance"
                  |),
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "ruint::Uint")
                        [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                        [],
                      "saturating_sub",
                      []
                    |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| caller_account |),
                            "revm_primitives::state::Account",
                            "info"
                          |),
                          "revm_primitives::state::AccountInfo",
                          "balance"
                        |)
                      |);
                      M.read (| gas_cost |)
                    ]
                  |)
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.match_operator (|
                              M.SubPointer.get_struct_record_field (|
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| env |),
                                  "revm_primitives::env::Env",
                                  "tx"
                                |),
                                "revm_primitives::env::TxEnv",
                                "transact_to"
                              |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ0_0 :=
                                      M.SubPointer.get_struct_tuple_field (|
                                        γ,
                                        "revm_primitives::env::TransactTo::Call",
                                        0
                                      |) in
                                    M.alloc (| Value.Bool true |)));
                                fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
                              ]
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ _ :=
                          M.write (|
                            M.SubPointer.get_struct_record_field (|
                              M.SubPointer.get_struct_record_field (|
                                M.read (| caller_account |),
                                "revm_primitives::state::Account",
                                "info"
                              |),
                              "revm_primitives::state::AccountInfo",
                              "nonce"
                            |),
                            M.call_closure (|
                              M.get_associated_function (| Ty.path "u64", "saturating_add", [] |),
                              [
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| caller_account |),
                                      "revm_primitives::state::Account",
                                      "info"
                                    |),
                                    "revm_primitives::state::AccountInfo",
                                    "nonce"
                                  |)
                                |);
                                Value.Integer IntegerKind.U64 1
                              ]
                            |)
                          |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "revm_primitives::state::Account",
                      "mark_touch",
                      []
                    |),
                    [ M.read (| caller_account |) ]
                  |)
                |) in
              M.alloc (| Value.Tuple [] |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_deduct_caller_inner :
        M.IsFunction
          "revm::handler::mainnet::pre_execution::deduct_caller_inner"
          deduct_caller_inner.
      
      (*
      pub fn deduct_caller<SPEC: Spec, EXT, DB: Database>(
          context: &mut Context<EXT, DB>,
      ) -> Result<(), EVMError<DB::Error>> {
          // load caller's account.
          let (caller_account, _) = context
              .evm
              .inner
              .journaled_state
              .load_account(context.evm.inner.env.tx.caller, &mut context.evm.inner.db)?;
      
          // deduct gas cost from caller's account.
          deduct_caller_inner::<SPEC>(caller_account, &context.evm.inner.env);
      
          Ok(())
      }
      *)
      Definition deduct_caller (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ SPEC; EXT; DB ], [ context ] =>
          ltac:(M.monadic
            (let context := M.alloc (| context |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  M.match_operator (|
                    M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::try_trait::Try",
                            Ty.apply
                              (Ty.path "core::result::Result")
                              []
                              [
                                Ty.tuple
                                  [
                                    Ty.apply
                                      (Ty.path "&mut")
                                      []
                                      [ Ty.path "revm_primitives::state::Account" ];
                                    Ty.path "bool"
                                  ];
                                Ty.apply
                                  (Ty.path "revm_primitives::result::EVMError")
                                  []
                                  [ Ty.associated ]
                              ],
                            [],
                            "branch",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "revm::journaled_state::JournaledState",
                                "load_account",
                                [ DB ]
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| context |),
                                      "revm::context::Context",
                                      "evm"
                                    |),
                                    "revm::context::evm_context::EvmContext",
                                    "inner"
                                  |),
                                  "revm::context::inner_evm_context::InnerEvmContext",
                                  "journaled_state"
                                |);
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| context |),
                                              "revm::context::Context",
                                              "evm"
                                            |),
                                            "revm::context::evm_context::EvmContext",
                                            "inner"
                                          |),
                                          "revm::context::inner_evm_context::InnerEvmContext",
                                          "env"
                                        |)
                                      |),
                                      "revm_primitives::env::Env",
                                      "tx"
                                    |),
                                    "revm_primitives::env::TxEnv",
                                    "caller"
                                  |)
                                |);
                                M.SubPointer.get_struct_record_field (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| context |),
                                      "revm::context::Context",
                                      "evm"
                                    |),
                                    "revm::context::evm_context::EvmContext",
                                    "inner"
                                  |),
                                  "revm::context::inner_evm_context::InnerEvmContext",
                                  "db"
                                |)
                              ]
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::control_flow::ControlFlow::Break",
                                0
                              |) in
                            let residual := M.copy (| γ0_0 |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  M.return_ (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::ops::try_trait::FromResidual",
                                        Ty.apply
                                          (Ty.path "core::result::Result")
                                          []
                                          [
                                            Ty.tuple [];
                                            Ty.apply
                                              (Ty.path "revm_primitives::result::EVMError")
                                              []
                                              [ Ty.associated ]
                                          ],
                                        [
                                          Ty.apply
                                            (Ty.path "core::result::Result")
                                            []
                                            [
                                              Ty.path "core::convert::Infallible";
                                              Ty.apply
                                                (Ty.path "revm_primitives::result::EVMError")
                                                []
                                                [ Ty.associated ]
                                            ]
                                        ],
                                        "from_residual",
                                        []
                                      |),
                                      [ M.read (| residual |) ]
                                    |)
                                  |)
                                |)
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::control_flow::ControlFlow::Continue",
                                0
                              |) in
                            let val := M.copy (| γ0_0 |) in
                            val))
                      ]
                    |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                          let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                          let caller_account := M.copy (| γ0_0 |) in
                          let~ _ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_function (|
                                  "revm::handler::mainnet::pre_execution::deduct_caller_inner",
                                  [ SPEC ]
                                |),
                                [
                                  M.read (| caller_account |);
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.SubPointer.get_struct_record_field (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| context |),
                                          "revm::context::Context",
                                          "evm"
                                        |),
                                        "revm::context::evm_context::EvmContext",
                                        "inner"
                                      |),
                                      "revm::context::inner_evm_context::InnerEvmContext",
                                      "env"
                                    |)
                                  |)
                                ]
                              |)
                            |) in
                          M.alloc (|
                            Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ]
                          |)))
                    ]
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_deduct_caller :
        M.IsFunction "revm::handler::mainnet::pre_execution::deduct_caller" deduct_caller.
    End pre_execution.
  End mainnet.
End handler.
