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

Module handler.
  Module mainnet.
    Module execution.
      (*
      pub fn frame_return_with_refund_flag<SPEC: Spec>(
          env: &Env,
          frame_result: &mut FrameResult,
          refund_enabled: bool,
      ) {
          let instruction_result = frame_result.interpreter_result().result;
          let gas = frame_result.gas_mut();
          let remaining = gas.remaining();
          let refunded = gas.refunded();
      
          // Spend the gas limit. Gas is reimbursed when the tx returns successfully.
          *gas = Gas::new_spent(env.tx.gas_limit);
      
          match instruction_result {
              return_ok!() => {
                  gas.erase_cost(remaining);
                  gas.record_refund(refunded);
              }
              return_revert!() => {
                  gas.erase_cost(remaining);
              }
              _ => {}
          }
      
          // Calculate gas refund for transaction.
          // If config is set to disable gas refund, it will return 0.
          // If spec is set to london, it will decrease the maximum refund amount to 5th part of
          // gas spend. (Before london it was 2th part of gas spend)
          if refund_enabled {
              // EIP-3529: Reduction in refunds
              gas.set_final_refund(SPEC::SPEC_ID.is_enabled_in(SpecId::LONDON));
          }
      }
      *)
      Definition frame_return_with_refund_flag
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        match ε, τ, α with
        | [], [ SPEC ], [ env; frame_result; refund_enabled ] =>
          ltac:(M.monadic
            (let env := M.alloc (| env |) in
            let frame_result := M.alloc (| frame_result |) in
            let refund_enabled := M.alloc (| refund_enabled |) in
            M.read (|
              let~ instruction_result :=
                M.copy (|
                  M.SubPointer.get_struct_record_field (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "revm::frame::FrameResult",
                        "interpreter_result",
                        []
                      |),
                      [ M.read (| frame_result |) ]
                    |),
                    "revm_interpreter::interpreter::InterpreterResult",
                    "result"
                  |)
                |) in
              let~ gas :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "revm::frame::FrameResult",
                      "gas_mut",
                      []
                    |),
                    [ M.read (| frame_result |) ]
                  |)
                |) in
              let~ remaining :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "revm_interpreter::gas::Gas",
                      "remaining",
                      []
                    |),
                    [ M.read (| gas |) ]
                  |)
                |) in
              let~ refunded :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "revm_interpreter::gas::Gas",
                      "refunded",
                      []
                    |),
                    [ M.read (| gas |) ]
                  |)
                |) in
              let~ _ :=
                M.write (|
                  M.read (| gas |),
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "revm_interpreter::gas::Gas",
                      "new_spent",
                      []
                    |),
                    [
                      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"
                        |)
                      |)
                    ]
                  |)
                |) in
              let~ _ :=
                M.match_operator (|
                  instruction_result,
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (M.find_or_pattern (|
                          γ,
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm_interpreter::instruction_result::InstructionResult::Continue"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm_interpreter::instruction_result::InstructionResult::Stop"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm_interpreter::instruction_result::InstructionResult::Return"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm_interpreter::instruction_result::InstructionResult::SelfDestruct"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm_interpreter::instruction_result::InstructionResult::ReturnContract"
                                  |) in
                                Value.Tuple []))
                          ],
                          M.closure
                            (fun γ =>
                              ltac:(M.monadic
                                match γ with
                                | [] =>
                                  ltac:(M.monadic
                                    (let~ _ :=
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "revm_interpreter::gas::Gas",
                                            "erase_cost",
                                            []
                                          |),
                                          [ M.read (| gas |); M.read (| remaining |) ]
                                        |)
                                      |) in
                                    let~ _ :=
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "revm_interpreter::gas::Gas",
                                            "record_refund",
                                            []
                                          |),
                                          [ M.read (| gas |); M.read (| refunded |) ]
                                        |)
                                      |) in
                                    M.alloc (| Value.Tuple [] |)))
                                | _ => M.impossible "wrong number of arguments"
                                end))
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.find_or_pattern (|
                          γ,
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm_interpreter::instruction_result::InstructionResult::Revert"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm_interpreter::instruction_result::InstructionResult::CallTooDeep"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm_interpreter::instruction_result::InstructionResult::OutOfFunds"
                                  |) in
                                Value.Tuple []))
                          ],
                          M.closure
                            (fun γ =>
                              ltac:(M.monadic
                                match γ with
                                | [] =>
                                  ltac:(M.monadic
                                    (let~ _ :=
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "revm_interpreter::gas::Gas",
                                            "erase_cost",
                                            []
                                          |),
                                          [ M.read (| gas |); M.read (| remaining |) ]
                                        |)
                                      |) in
                                    M.alloc (| Value.Tuple [] |)))
                                | _ => M.impossible "wrong number of arguments"
                                end))
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.use refund_enabled in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      let~ _ :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "revm_interpreter::gas::Gas",
                              "set_final_refund",
                              []
                            |),
                            [
                              M.read (| gas |);
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "revm_primitives::specification::SpecId",
                                  "is_enabled_in",
                                  []
                                |),
                                [
                                  M.read (|
                                    M.get_constant (|
                                      "revm_primitives::specification::Spec::SPEC_ID"
                                    |)
                                  |);
                                  Value.StructTuple
                                    "revm_primitives::specification::SpecId::LONDON"
                                    []
                                ]
                              |)
                            ]
                          |)
                        |) in
                      M.alloc (| Value.Tuple [] |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_frame_return_with_refund_flag :
        M.IsFunction
          "revm::handler::mainnet::execution::frame_return_with_refund_flag"
          frame_return_with_refund_flag.
      
      (*
      pub fn last_frame_return<SPEC: Spec, EXT, DB: Database>(
          context: &mut Context<EXT, DB>,
          frame_result: &mut FrameResult,
      ) -> Result<(), EVMError<DB::Error>> {
          frame_return_with_refund_flag::<SPEC>(&context.evm.env, frame_result, true);
          Ok(())
      }
      *)
      Definition last_frame_return (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ SPEC; EXT; DB ], [ context; frame_result ] =>
          ltac:(M.monadic
            (let context := M.alloc (| context |) in
            let frame_result := M.alloc (| frame_result |) in
            M.read (|
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "revm::handler::mainnet::execution::frame_return_with_refund_flag",
                      [ SPEC ]
                    |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::deref::Deref",
                              Ty.apply (Ty.path "revm::context::evm_context::EvmContext") [] [ DB ],
                              [],
                              "deref",
                              []
                            |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| context |),
                                "revm::context::Context",
                                "evm"
                              |)
                            ]
                          |),
                          "revm::context::inner_evm_context::InnerEvmContext",
                          "env"
                        |)
                      |);
                      M.read (| frame_result |);
                      Value.Bool true
                    ]
                  |)
                |) in
              M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_last_frame_return :
        M.IsFunction "revm::handler::mainnet::execution::last_frame_return" last_frame_return.
      
      (*
      pub fn call<SPEC: Spec, EXT, DB: Database>(
          context: &mut Context<EXT, DB>,
          inputs: Box<CallInputs>,
      ) -> Result<FrameOrResult, EVMError<DB::Error>> {
          context.evm.make_call_frame(&inputs)
      }
      *)
      Definition call (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ SPEC; EXT; DB ], [ context; inputs ] =>
          ltac:(M.monadic
            (let context := M.alloc (| context |) in
            let inputs := M.alloc (| inputs |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "revm::context::evm_context::EvmContext") [] [ DB ],
                "make_call_frame",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| context |),
                  "revm::context::Context",
                  "evm"
                |);
                M.read (| inputs |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_call : M.IsFunction "revm::handler::mainnet::execution::call" call.
      
      (*
      pub fn call_return<EXT, DB: Database>(
          context: &mut Context<EXT, DB>,
          frame: Box<CallFrame>,
          interpreter_result: InterpreterResult,
      ) -> Result<CallOutcome, EVMError<DB::Error>> {
          context
              .evm
              .call_return(&interpreter_result, frame.frame_data.checkpoint);
          Ok(CallOutcome::new(
              interpreter_result,
              frame.return_memory_range,
          ))
      }
      *)
      Definition call_return (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ EXT; DB ], [ context; frame; interpreter_result ] =>
          ltac:(M.monadic
            (let context := M.alloc (| context |) in
            let frame := M.alloc (| frame |) in
            let interpreter_result := M.alloc (| interpreter_result |) in
            M.read (|
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "revm::context::inner_evm_context::InnerEvmContext")
                        []
                        [ DB ],
                      "call_return",
                      []
                    |),
                    [
                      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"
                          |)
                        ]
                      |);
                      interpreter_result;
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| frame |),
                            "revm::frame::CallFrame",
                            "frame_data"
                          |),
                          "revm::frame::FrameData",
                          "checkpoint"
                        |)
                      |)
                    ]
                  |)
                |) in
              M.alloc (|
                Value.StructTuple
                  "core::result::Result::Ok"
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "revm_interpreter::interpreter_action::call_outcome::CallOutcome",
                        "new",
                        []
                      |),
                      [
                        M.read (| interpreter_result |);
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| frame |),
                            "revm::frame::CallFrame",
                            "return_memory_range"
                          |)
                        |)
                      ]
                    |)
                  ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_call_return :
        M.IsFunction "revm::handler::mainnet::execution::call_return" call_return.
      
      (*
      pub fn insert_call_outcome<EXT, DB: Database>(
          context: &mut Context<EXT, DB>,
          frame: &mut Frame,
          shared_memory: &mut SharedMemory,
          outcome: CallOutcome,
      ) -> Result<(), EVMError<DB::Error>> {
          context.evm.take_error()?;
          frame
              .frame_data_mut()
              .interpreter
              .insert_call_outcome(shared_memory, outcome);
          Ok(())
      }
      *)
      Definition insert_call_outcome (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ EXT; DB ], [ context; frame; shared_memory; outcome ] =>
          ltac:(M.monadic
            (let context := M.alloc (| context |) in
            let frame := M.alloc (| frame |) in
            let shared_memory := M.alloc (| shared_memory |) in
            let outcome := M.alloc (| outcome |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  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 ],
                                "take_error",
                                []
                              |),
                              [
                                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
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "revm_interpreter::interpreter::Interpreter",
                          "insert_call_outcome",
                          []
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "revm::frame::Frame",
                                "frame_data_mut",
                                []
                              |),
                              [ M.read (| frame |) ]
                            |),
                            "revm::frame::FrameData",
                            "interpreter"
                          |);
                          M.read (| shared_memory |);
                          M.read (| outcome |)
                        ]
                      |)
                    |) in
                  M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_insert_call_outcome :
        M.IsFunction "revm::handler::mainnet::execution::insert_call_outcome" insert_call_outcome.
      
      (*
      pub fn create<SPEC: Spec, EXT, DB: Database>(
          context: &mut Context<EXT, DB>,
          inputs: Box<CreateInputs>,
      ) -> Result<FrameOrResult, EVMError<DB::Error>> {
          context.evm.make_create_frame(SPEC::SPEC_ID, &inputs)
      }
      *)
      Definition create (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ SPEC; EXT; DB ], [ context; inputs ] =>
          ltac:(M.monadic
            (let context := M.alloc (| context |) in
            let inputs := M.alloc (| inputs |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "revm::context::inner_evm_context::InnerEvmContext") [] [ DB ],
                "make_create_frame",
                []
              |),
              [
                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"
                    |)
                  ]
                |);
                M.read (| M.get_constant (| "revm_primitives::specification::Spec::SPEC_ID" |) |);
                M.read (| inputs |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_create : M.IsFunction "revm::handler::mainnet::execution::create" create.
      
      (*
      pub fn create_return<SPEC: Spec, EXT, DB: Database>(
          context: &mut Context<EXT, DB>,
          frame: Box<CreateFrame>,
          mut interpreter_result: InterpreterResult,
      ) -> Result<CreateOutcome, EVMError<DB::Error>> {
          context.evm.create_return::<SPEC>(
              &mut interpreter_result,
              frame.created_address,
              frame.frame_data.checkpoint,
          );
          Ok(CreateOutcome::new(
              interpreter_result,
              Some(frame.created_address),
          ))
      }
      *)
      Definition create_return (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ SPEC; EXT; DB ], [ context; frame; interpreter_result ] =>
          ltac:(M.monadic
            (let context := M.alloc (| context |) in
            let frame := M.alloc (| frame |) in
            let interpreter_result := M.alloc (| interpreter_result |) in
            M.read (|
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "revm::context::inner_evm_context::InnerEvmContext")
                        []
                        [ DB ],
                      "create_return",
                      [ SPEC ]
                    |),
                    [
                      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"
                          |)
                        ]
                      |);
                      interpreter_result;
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| frame |),
                          "revm::frame::CreateFrame",
                          "created_address"
                        |)
                      |);
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| frame |),
                            "revm::frame::CreateFrame",
                            "frame_data"
                          |),
                          "revm::frame::FrameData",
                          "checkpoint"
                        |)
                      |)
                    ]
                  |)
                |) in
              M.alloc (|
                Value.StructTuple
                  "core::result::Result::Ok"
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path
                          "revm_interpreter::interpreter_action::create_outcome::CreateOutcome",
                        "new",
                        []
                      |),
                      [
                        M.read (| interpreter_result |);
                        Value.StructTuple
                          "core::option::Option::Some"
                          [
                            M.read (|
                              M.SubPointer.get_struct_record_field (|
                                M.read (| frame |),
                                "revm::frame::CreateFrame",
                                "created_address"
                              |)
                            |)
                          ]
                      ]
                    |)
                  ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_create_return :
        M.IsFunction "revm::handler::mainnet::execution::create_return" create_return.
      
      (*
      pub fn insert_create_outcome<EXT, DB: Database>(
          context: &mut Context<EXT, DB>,
          frame: &mut Frame,
          outcome: CreateOutcome,
      ) -> Result<(), EVMError<DB::Error>> {
          context.evm.take_error()?;
          frame
              .frame_data_mut()
              .interpreter
              .insert_create_outcome(outcome);
          Ok(())
      }
      *)
      Definition insert_create_outcome (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ EXT; DB ], [ context; frame; outcome ] =>
          ltac:(M.monadic
            (let context := M.alloc (| context |) in
            let frame := M.alloc (| frame |) in
            let outcome := M.alloc (| outcome |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  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 ],
                                "take_error",
                                []
                              |),
                              [
                                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
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "revm_interpreter::interpreter::Interpreter",
                          "insert_create_outcome",
                          []
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "revm::frame::Frame",
                                "frame_data_mut",
                                []
                              |),
                              [ M.read (| frame |) ]
                            |),
                            "revm::frame::FrameData",
                            "interpreter"
                          |);
                          M.read (| outcome |)
                        ]
                      |)
                    |) in
                  M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_insert_create_outcome :
        M.IsFunction
          "revm::handler::mainnet::execution::insert_create_outcome"
          insert_create_outcome.
      
      (*
      pub fn eofcreate<SPEC: Spec, EXT, DB: Database>(
          context: &mut Context<EXT, DB>,
          inputs: Box<EOFCreateInput>,
      ) -> Result<FrameOrResult, EVMError<DB::Error>> {
          context.evm.make_eofcreate_frame(SPEC::SPEC_ID, &inputs)
      }
      *)
      Definition eofcreate (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ SPEC; EXT; DB ], [ context; inputs ] =>
          ltac:(M.monadic
            (let context := M.alloc (| context |) in
            let inputs := M.alloc (| inputs |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "revm::context::inner_evm_context::InnerEvmContext") [] [ DB ],
                "make_eofcreate_frame",
                []
              |),
              [
                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"
                    |)
                  ]
                |);
                M.read (| M.get_constant (| "revm_primitives::specification::Spec::SPEC_ID" |) |);
                M.read (| inputs |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_eofcreate :
        M.IsFunction "revm::handler::mainnet::execution::eofcreate" eofcreate.
      
      (*
      pub fn eofcreate_return<SPEC: Spec, EXT, DB: Database>(
          context: &mut Context<EXT, DB>,
          frame: Box<EOFCreateFrame>,
          mut interpreter_result: InterpreterResult,
      ) -> Result<EOFCreateOutcome, EVMError<DB::Error>> {
          context.evm.eofcreate_return::<SPEC>(
              &mut interpreter_result,
              frame.created_address,
              frame.frame_data.checkpoint,
          );
          Ok(EOFCreateOutcome::new(
              interpreter_result,
              frame.created_address,
              frame.return_memory_range,
          ))
      }
      *)
      Definition eofcreate_return (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ SPEC; EXT; DB ], [ context; frame; interpreter_result ] =>
          ltac:(M.monadic
            (let context := M.alloc (| context |) in
            let frame := M.alloc (| frame |) in
            let interpreter_result := M.alloc (| interpreter_result |) in
            M.read (|
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "revm::context::inner_evm_context::InnerEvmContext")
                        []
                        [ DB ],
                      "eofcreate_return",
                      [ SPEC ]
                    |),
                    [
                      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"
                          |)
                        ]
                      |);
                      interpreter_result;
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| frame |),
                          "revm::frame::EOFCreateFrame",
                          "created_address"
                        |)
                      |);
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| frame |),
                            "revm::frame::EOFCreateFrame",
                            "frame_data"
                          |),
                          "revm::frame::FrameData",
                          "checkpoint"
                        |)
                      |)
                    ]
                  |)
                |) in
              M.alloc (|
                Value.StructTuple
                  "core::result::Result::Ok"
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path
                          "revm_interpreter::interpreter_action::eof_create_outcome::EOFCreateOutcome",
                        "new",
                        []
                      |),
                      [
                        M.read (| interpreter_result |);
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| frame |),
                            "revm::frame::EOFCreateFrame",
                            "created_address"
                          |)
                        |);
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| frame |),
                            "revm::frame::EOFCreateFrame",
                            "return_memory_range"
                          |)
                        |)
                      ]
                    |)
                  ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_eofcreate_return :
        M.IsFunction "revm::handler::mainnet::execution::eofcreate_return" eofcreate_return.
      
      (*
      pub fn insert_eofcreate_outcome<EXT, DB: Database>(
          context: &mut Context<EXT, DB>,
          frame: &mut Frame,
          outcome: EOFCreateOutcome,
      ) -> Result<(), EVMError<DB::Error>> {
          core::mem::replace(&mut context.evm.error, Ok(()))?;
          frame
              .frame_data_mut()
              .interpreter
              .insert_eofcreate_outcome(outcome);
          Ok(())
      }
      *)
      Definition insert_eofcreate_outcome
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        match ε, τ, α with
        | [], [ EXT; DB ], [ context; frame; outcome ] =>
          ltac:(M.monadic
            (let context := M.alloc (| context |) in
            let frame := M.alloc (| frame |) in
            let outcome := M.alloc (| outcome |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  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_function (|
                                "core::mem::replace",
                                [
                                  Ty.apply
                                    (Ty.path "core::result::Result")
                                    []
                                    [
                                      Ty.tuple [];
                                      Ty.apply
                                        (Ty.path "revm_primitives::result::EVMError")
                                        []
                                        [ Ty.associated ]
                                    ]
                                ]
                              |),
                              [
                                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",
                                  "error"
                                |);
                                Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ]
                              ]
                            |)
                          ]
                        |)
                      |),
                      [
                        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
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "revm_interpreter::interpreter::Interpreter",
                          "insert_eofcreate_outcome",
                          []
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "revm::frame::Frame",
                                "frame_data_mut",
                                []
                              |),
                              [ M.read (| frame |) ]
                            |),
                            "revm::frame::FrameData",
                            "interpreter"
                          |);
                          M.read (| outcome |)
                        ]
                      |)
                    |) in
                  M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_insert_eofcreate_outcome :
        M.IsFunction
          "revm::handler::mainnet::execution::insert_eofcreate_outcome"
          insert_eofcreate_outcome.
    End execution.
  End mainnet.
End handler.
