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

Module context.
  Module evm_context.
    (* StructRecord
      {
        name := "EvmContext";
        const_params := [];
        ty_params := [ "DB" ];
        fields :=
          [
            ("inner",
              Ty.apply (Ty.path "revm::context::inner_evm_context::InnerEvmContext") [] [ DB ]);
            ("precompiles",
              Ty.apply (Ty.path "revm::context::context_precompiles::ContextPrecompiles") [] [ DB ])
          ];
      } *)
    
    Module Impl_core_clone_Clone_where_revm_primitives_db_Database_DB_where_core_clone_Clone_DB_where_core_clone_Clone_associated_type_for_revm_context_evm_context_EvmContext_DB.
      Definition Self (DB : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "revm::context::evm_context::EvmContext") [] [ DB ].
      
      (*
          fn clone(&self) -> Self {
              Self {
                  inner: self.inner.clone(),
                  precompiles: ContextPrecompiles::default(),
              }
          }
      *)
      Definition clone (DB : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self DB in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            Value.StructRecord
              "revm::context::evm_context::EvmContext"
              [
                ("inner",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::clone::Clone",
                      Ty.apply
                        (Ty.path "revm::context::inner_evm_context::InnerEvmContext")
                        []
                        [ DB ],
                      [],
                      "clone",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm::context::evm_context::EvmContext",
                        "inner"
                      |)
                    ]
                  |));
                ("precompiles",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::default::Default",
                      Ty.apply
                        (Ty.path "revm::context::context_precompiles::ContextPrecompiles")
                        []
                        [ DB ],
                      [],
                      "default",
                      []
                    |),
                    []
                  |))
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (DB : Ty.t),
        M.IsTraitInstance
          "core::clone::Clone"
          (Self DB)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("clone", InstanceField.Method (clone DB)) ].
    End Impl_core_clone_Clone_where_revm_primitives_db_Database_DB_where_core_clone_Clone_DB_where_core_clone_Clone_associated_type_for_revm_context_evm_context_EvmContext_DB.
    
    Module Impl_core_fmt_Debug_where_revm_primitives_db_Database_DB_where_core_fmt_Debug_DB_where_core_fmt_Debug_associated_type_for_revm_context_evm_context_EvmContext_DB.
      Definition Self (DB : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "revm::context::evm_context::EvmContext") [] [ DB ].
      
      (*
          fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
              f.debug_struct("EvmContext")
                  .field("inner", &self.inner)
                  .field("precompiles", &self.inner)
                  .finish_non_exhaustive()
          }
      *)
      Definition fmt (DB : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self DB in
        match ε, τ, α with
        | [], [], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "core::fmt::builders::DebugStruct",
                "finish_non_exhaustive",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "core::fmt::builders::DebugStruct",
                    "field",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "core::fmt::builders::DebugStruct",
                        "field",
                        []
                      |),
                      [
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Formatter",
                              "debug_struct",
                              []
                            |),
                            [ M.read (| f |); M.read (| Value.String "EvmContext" |) ]
                          |)
                        |);
                        M.read (| Value.String "inner" |);
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::context::evm_context::EvmContext",
                          "inner"
                        |)
                      ]
                    |);
                    M.read (| Value.String "precompiles" |);
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm::context::evm_context::EvmContext",
                      "inner"
                    |)
                  ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (DB : Ty.t),
        M.IsTraitInstance
          "core::fmt::Debug"
          (Self DB)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method (fmt DB)) ].
    End Impl_core_fmt_Debug_where_revm_primitives_db_Database_DB_where_core_fmt_Debug_DB_where_core_fmt_Debug_associated_type_for_revm_context_evm_context_EvmContext_DB.
    
    Module Impl_core_ops_deref_Deref_where_revm_primitives_db_Database_DB_for_revm_context_evm_context_EvmContext_DB.
      Definition Self (DB : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "revm::context::evm_context::EvmContext") [] [ DB ].
      
      (*     type Target = InnerEvmContext<DB>; *)
      Definition _Target (DB : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "revm::context::inner_evm_context::InnerEvmContext") [] [ DB ].
      
      (*
          fn deref(&self) -> &Self::Target {
              &self.inner
          }
      *)
      Definition deref (DB : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self DB in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.SubPointer.get_struct_record_field (|
              M.read (| self |),
              "revm::context::evm_context::EvmContext",
              "inner"
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (DB : Ty.t),
        M.IsTraitInstance
          "core::ops::deref::Deref"
          (Self DB)
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Target", InstanceField.Ty (_Target DB)); ("deref", InstanceField.Method (deref DB)) ].
    End Impl_core_ops_deref_Deref_where_revm_primitives_db_Database_DB_for_revm_context_evm_context_EvmContext_DB.
    
    Module Impl_core_ops_deref_DerefMut_where_revm_primitives_db_Database_DB_for_revm_context_evm_context_EvmContext_DB.
      Definition Self (DB : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "revm::context::evm_context::EvmContext") [] [ DB ].
      
      (*
          fn deref_mut(&mut self) -> &mut Self::Target {
              &mut self.inner
          }
      *)
      Definition deref_mut (DB : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self DB in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.SubPointer.get_struct_record_field (|
              M.read (| self |),
              "revm::context::evm_context::EvmContext",
              "inner"
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (DB : Ty.t),
        M.IsTraitInstance
          "core::ops::deref::DerefMut"
          (Self DB)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("deref_mut", InstanceField.Method (deref_mut DB)) ].
    End Impl_core_ops_deref_DerefMut_where_revm_primitives_db_Database_DB_for_revm_context_evm_context_EvmContext_DB.
    
    Module Impl_revm_context_evm_context_EvmContext_DB.
      Definition Self (DB : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "revm::context::evm_context::EvmContext") [] [ DB ].
      
      (*
          pub fn new(db: DB) -> Self {
              Self {
                  inner: InnerEvmContext::new(db),
                  precompiles: ContextPrecompiles::default(),
              }
          }
      *)
      Definition new (DB : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self DB in
        match ε, τ, α with
        | [], [], [ db ] =>
          ltac:(M.monadic
            (let db := M.alloc (| db |) in
            Value.StructRecord
              "revm::context::evm_context::EvmContext"
              [
                ("inner",
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "revm::context::inner_evm_context::InnerEvmContext")
                        []
                        [ DB ],
                      "new",
                      []
                    |),
                    [ M.read (| db |) ]
                  |));
                ("precompiles",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::default::Default",
                      Ty.apply
                        (Ty.path "revm::context::context_precompiles::ContextPrecompiles")
                        []
                        [ DB ],
                      [],
                      "default",
                      []
                    |),
                    []
                  |))
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_new :
        forall (DB : Ty.t),
        M.IsAssociatedFunction (Self DB) "new" (new DB).
      
      (*
          pub fn new_with_env(db: DB, env: Box<Env>) -> Self {
              Self {
                  inner: InnerEvmContext::new_with_env(db, env),
                  precompiles: ContextPrecompiles::default(),
              }
          }
      *)
      Definition new_with_env
          (DB : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self DB in
        match ε, τ, α with
        | [], [], [ db; env ] =>
          ltac:(M.monadic
            (let db := M.alloc (| db |) in
            let env := M.alloc (| env |) in
            Value.StructRecord
              "revm::context::evm_context::EvmContext"
              [
                ("inner",
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "revm::context::inner_evm_context::InnerEvmContext")
                        []
                        [ DB ],
                      "new_with_env",
                      []
                    |),
                    [ M.read (| db |); M.read (| env |) ]
                  |));
                ("precompiles",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::default::Default",
                      Ty.apply
                        (Ty.path "revm::context::context_precompiles::ContextPrecompiles")
                        []
                        [ DB ],
                      [],
                      "default",
                      []
                    |),
                    []
                  |))
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_new_with_env :
        forall (DB : Ty.t),
        M.IsAssociatedFunction (Self DB) "new_with_env" (new_with_env DB).
      
      (*
          pub fn with_db<ODB: Database>(self, db: ODB) -> EvmContext<ODB> {
              EvmContext {
                  inner: self.inner.with_db(db),
                  precompiles: ContextPrecompiles::default(),
              }
          }
      *)
      Definition with_db (DB : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self DB in
        match ε, τ, α with
        | [], [ ODB ], [ self; db ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let db := M.alloc (| db |) in
            Value.StructRecord
              "revm::context::evm_context::EvmContext"
              [
                ("inner",
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "revm::context::inner_evm_context::InnerEvmContext")
                        []
                        [ DB ],
                      "with_db",
                      [ ODB ]
                    |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "revm::context::evm_context::EvmContext",
                          "inner"
                        |)
                      |);
                      M.read (| db |)
                    ]
                  |));
                ("precompiles",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::default::Default",
                      Ty.apply
                        (Ty.path "revm::context::context_precompiles::ContextPrecompiles")
                        []
                        [ ODB ],
                      [],
                      "default",
                      []
                    |),
                    []
                  |))
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_with_db :
        forall (DB : Ty.t),
        M.IsAssociatedFunction (Self DB) "with_db" (with_db DB).
      
      (*
          pub fn set_precompiles(&mut self, precompiles: ContextPrecompiles<DB>) {
              // set warm loaded addresses.
              self.journaled_state.warm_preloaded_addresses =
                  precompiles.addresses().copied().collect::<HashSet<_>>();
              self.precompiles = precompiles;
          }
      *)
      Definition set_precompiles
          (DB : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self DB in
        match ε, τ, α with
        | [], [], [ self; precompiles ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let precompiles := M.alloc (| precompiles |) in
            M.read (|
              let~ _ :=
                M.write (|
                  M.SubPointer.get_struct_record_field (|
                    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.read (| self |) ]
                      |),
                      "revm::context::inner_evm_context::InnerEvmContext",
                      "journaled_state"
                    |),
                    "revm::journaled_state::JournaledState",
                    "warm_preloaded_addresses"
                  |),
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::iterator::Iterator",
                      Ty.apply
                        (Ty.path "core::iter::adapters::copied::Copied")
                        []
                        [ Ty.associated ],
                      [],
                      "collect",
                      [
                        Ty.apply
                          (Ty.path "std::collections::hash::set::HashSet")
                          []
                          [
                            Ty.path "alloy_primitives::bits::address::Address";
                            Ty.path "std::hash::random::RandomState"
                          ]
                      ]
                    |),
                    [
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::iter::traits::iterator::Iterator",
                          Ty.associated,
                          [],
                          "copied",
                          [ Ty.path "alloy_primitives::bits::address::Address" ]
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "revm::context::context_precompiles::ContextPrecompiles")
                                []
                                [ DB ],
                              "addresses",
                              []
                            |),
                            [ precompiles ]
                          |)
                        ]
                      |)
                    ]
                  |)
                |) in
              let~ _ :=
                M.write (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm::context::evm_context::EvmContext",
                    "precompiles"
                  |),
                  M.read (| precompiles |)
                |) in
              M.alloc (| Value.Tuple [] |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_set_precompiles :
        forall (DB : Ty.t),
        M.IsAssociatedFunction (Self DB) "set_precompiles" (set_precompiles DB).
      
      (*
          fn call_precompile(
              &mut self,
              address: Address,
              input_data: &Bytes,
              gas: Gas,
          ) -> Option<InterpreterResult> {
              let out = self
                  .precompiles
                  .call(address, input_data, gas.limit(), &mut self.inner)?;
      
              let mut result = InterpreterResult {
                  result: InstructionResult::Return,
                  gas,
                  output: Bytes::new(),
              };
      
              match out {
                  Ok((gas_used, data)) => {
                      if result.gas.record_cost(gas_used) {
                          result.result = InstructionResult::Return;
                          result.output = data;
                      } else {
                          result.result = InstructionResult::PrecompileOOG;
                      }
                  }
                  Err(e) => {
                      result.result = if e == crate::precompile::Error::OutOfGas {
                          InstructionResult::PrecompileOOG
                      } else {
                          InstructionResult::PrecompileError
                      };
                  }
              }
              Some(result)
          }
      *)
      Definition call_precompile
          (DB : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self DB in
        match ε, τ, α with
        | [], [], [ self; address; input_data; gas ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let address := M.alloc (| address |) in
            let input_data := M.alloc (| input_data |) in
            let gas := M.alloc (| gas |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ out :=
                    M.copy (|
                      M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::try_trait::Try",
                              Ty.apply
                                (Ty.path "core::option::Option")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "core::result::Result")
                                    []
                                    [
                                      Ty.tuple
                                        [ Ty.path "u64"; Ty.path "alloy_primitives::bytes_::Bytes"
                                        ];
                                      Ty.path "revm_primitives::precompile::PrecompileError"
                                    ]
                                ],
                              [],
                              "branch",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path
                                      "revm::context::context_precompiles::ContextPrecompiles")
                                    []
                                    [ DB ],
                                  "call",
                                  []
                                |),
                                [
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "revm::context::evm_context::EvmContext",
                                    "precompiles"
                                  |);
                                  M.read (| address |);
                                  M.read (| input_data |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "revm_interpreter::gas::Gas",
                                      "limit",
                                      []
                                    |),
                                    [ gas ]
                                  |);
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "revm::context::evm_context::EvmContext",
                                    "inner"
                                  |)
                                ]
                              |)
                            ]
                          |)
                        |),
                        [
                          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::option::Option")
                                            []
                                            [
                                              Ty.path
                                                "revm_interpreter::interpreter::InterpreterResult"
                                            ],
                                          [
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [ Ty.path "core::convert::Infallible" ]
                                          ],
                                          "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~ result :=
                    M.alloc (|
                      Value.StructRecord
                        "revm_interpreter::interpreter::InterpreterResult"
                        [
                          ("result",
                            Value.StructTuple
                              "revm_interpreter::instruction_result::InstructionResult::Return"
                              []);
                          ("gas", M.read (| gas |));
                          ("output",
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "alloy_primitives::bytes_::Bytes",
                                "new",
                                []
                              |),
                              []
                            |))
                        ]
                    |) in
                  let~ _ :=
                    M.match_operator (|
                      out,
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::result::Result::Ok",
                                0
                              |) in
                            let γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                            let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                            let gas_used := M.copy (| γ1_0 |) in
                            let data := M.copy (| γ1_1 |) in
                            M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "revm_interpreter::gas::Gas",
                                              "record_cost",
                                              []
                                            |),
                                            [
                                              M.SubPointer.get_struct_record_field (|
                                                result,
                                                "revm_interpreter::interpreter::InterpreterResult",
                                                "gas"
                                              |);
                                              M.read (| gas_used |)
                                            ]
                                          |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    let~ _ :=
                                      M.write (|
                                        M.SubPointer.get_struct_record_field (|
                                          result,
                                          "revm_interpreter::interpreter::InterpreterResult",
                                          "result"
                                        |),
                                        Value.StructTuple
                                          "revm_interpreter::instruction_result::InstructionResult::Return"
                                          []
                                      |) in
                                    let~ _ :=
                                      M.write (|
                                        M.SubPointer.get_struct_record_field (|
                                          result,
                                          "revm_interpreter::interpreter::InterpreterResult",
                                          "output"
                                        |),
                                        M.read (| data |)
                                      |) in
                                    M.alloc (| Value.Tuple [] |)));
                                fun γ =>
                                  ltac:(M.monadic
                                    (let~ _ :=
                                      M.write (|
                                        M.SubPointer.get_struct_record_field (|
                                          result,
                                          "revm_interpreter::interpreter::InterpreterResult",
                                          "result"
                                        |),
                                        Value.StructTuple
                                          "revm_interpreter::instruction_result::InstructionResult::PrecompileOOG"
                                          []
                                      |) in
                                    M.alloc (| Value.Tuple [] |)))
                              ]
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::result::Result::Err",
                                0
                              |) in
                            let e := M.copy (| γ0_0 |) in
                            let~ _ :=
                              M.write (|
                                M.SubPointer.get_struct_record_field (|
                                  result,
                                  "revm_interpreter::interpreter::InterpreterResult",
                                  "result"
                                |),
                                M.read (|
                                  M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ :=
                                            M.use
                                              (M.alloc (|
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::cmp::PartialEq",
                                                    Ty.path
                                                      "revm_primitives::precompile::PrecompileError",
                                                    [
                                                      Ty.path
                                                        "revm_primitives::precompile::PrecompileError"
                                                    ],
                                                    "eq",
                                                    []
                                                  |),
                                                  [
                                                    e;
                                                    M.alloc (|
                                                      Value.StructTuple
                                                        "revm_primitives::precompile::PrecompileError::OutOfGas"
                                                        []
                                                    |)
                                                  ]
                                                |)
                                              |)) in
                                          let _ :=
                                            M.is_constant_or_break_match (|
                                              M.read (| γ |),
                                              Value.Bool true
                                            |) in
                                          M.alloc (|
                                            Value.StructTuple
                                              "revm_interpreter::instruction_result::InstructionResult::PrecompileOOG"
                                              []
                                          |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (M.alloc (|
                                            Value.StructTuple
                                              "revm_interpreter::instruction_result::InstructionResult::PrecompileError"
                                              []
                                          |)))
                                    ]
                                  |)
                                |)
                              |) in
                            M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  M.alloc (|
                    Value.StructTuple "core::option::Option::Some" [ M.read (| result |) ]
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_call_precompile :
        forall (DB : Ty.t),
        M.IsAssociatedFunction (Self DB) "call_precompile" (call_precompile DB).
      
      (*
          pub fn make_call_frame(
              &mut self,
              inputs: &CallInputs,
          ) -> Result<FrameOrResult, EVMError<DB::Error>> {
              let gas = Gas::new(inputs.gas_limit);
      
              let return_result = |instruction_result: InstructionResult| {
                  Ok(FrameOrResult::new_call_result(
                      InterpreterResult {
                          result: instruction_result,
                          gas,
                          output: Bytes::new(),
                      },
                      inputs.return_memory_offset.clone(),
                  ))
              };
      
              // Check depth
              if self.journaled_state.depth() > CALL_STACK_LIMIT {
                  return return_result(InstructionResult::CallTooDeep);
              }
      
              let (account, _) = self
                  .inner
                  .journaled_state
                  .load_code(inputs.bytecode_address, &mut self.inner.db)?;
              let code_hash = account.info.code_hash();
              let bytecode = account.info.code.clone().unwrap_or_default();
      
              // Create subroutine checkpoint
              let checkpoint = self.journaled_state.checkpoint();
      
              // Touch address. For "EIP-158 State Clear", this will erase empty accounts.
              match inputs.value {
                  // if transfer value is zero, do the touch.
                  CallValue::Transfer(value) if value == U256::ZERO => {
                      self.load_account(inputs.target_address)?;
                      self.journaled_state.touch(&inputs.target_address);
                  }
                  CallValue::Transfer(value) => {
                      // Transfer value from caller to called account
                      if let Some(result) = self.inner.journaled_state.transfer(
                          &inputs.caller,
                          &inputs.target_address,
                          value,
                          &mut self.inner.db,
                      )? {
                          self.journaled_state.checkpoint_revert(checkpoint);
                          return return_result(result);
                      }
                  }
                  _ => {}
              };
      
              if let Some(result) = self.call_precompile(inputs.bytecode_address, &inputs.input, gas) {
                  if matches!(result.result, return_ok!()) {
                      self.journaled_state.checkpoint_commit();
                  } else {
                      self.journaled_state.checkpoint_revert(checkpoint);
                  }
                  Ok(FrameOrResult::new_call_result(
                      result,
                      inputs.return_memory_offset.clone(),
                  ))
              } else if !bytecode.is_empty() {
                  let contract =
                      Contract::new_with_context(inputs.input.clone(), bytecode, Some(code_hash), inputs);
                  // Create interpreter and executes call and push new CallStackFrame.
                  Ok(FrameOrResult::new_call_frame(
                      inputs.return_memory_offset.clone(),
                      checkpoint,
                      Interpreter::new(contract, gas.limit(), inputs.is_static),
                  ))
              } else {
                  self.journaled_state.checkpoint_commit();
                  return_result(InstructionResult::Stop)
              }
          }
      *)
      Definition make_call_frame
          (DB : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self DB in
        match ε, τ, α with
        | [], [], [ self; inputs ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let inputs := M.alloc (| inputs |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ gas :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "revm_interpreter::gas::Gas",
                          "new",
                          []
                        |),
                        [
                          M.read (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| inputs |),
                              "revm_interpreter::interpreter_action::call_inputs::CallInputs",
                              "gas_limit"
                            |)
                          |)
                        ]
                      |)
                    |) in
                  let~ return_result :=
                    M.alloc (|
                      M.closure
                        (fun γ =>
                          ltac:(M.monadic
                            match γ with
                            | [ α0 ] =>
                              ltac:(M.monadic
                                (M.match_operator (|
                                  M.alloc (| α0 |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let instruction_result := M.copy (| γ |) in
                                        Value.StructTuple
                                          "core::result::Result::Ok"
                                          [
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.path "revm::frame::FrameOrResult",
                                                "new_call_result",
                                                []
                                              |),
                                              [
                                                Value.StructRecord
                                                  "revm_interpreter::interpreter::InterpreterResult"
                                                  [
                                                    ("result", M.read (| instruction_result |));
                                                    ("gas", M.read (| gas |));
                                                    ("output",
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path "alloy_primitives::bytes_::Bytes",
                                                          "new",
                                                          []
                                                        |),
                                                        []
                                                      |))
                                                  ];
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::clone::Clone",
                                                    Ty.apply
                                                      (Ty.path "core::ops::range::Range")
                                                      []
                                                      [ Ty.path "usize" ],
                                                    [],
                                                    "clone",
                                                    []
                                                  |),
                                                  [
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| inputs |),
                                                      "revm_interpreter::interpreter_action::call_inputs::CallInputs",
                                                      "return_memory_offset"
                                                    |)
                                                  ]
                                                |)
                                              ]
                                            |)
                                          ]))
                                  ]
                                |)))
                            | _ => M.impossible "wrong number of arguments"
                            end))
                    |) in
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  BinOp.gt (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "revm::journaled_state::JournaledState",
                                        "depth",
                                        []
                                      |),
                                      [
                                        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.read (| self |) ]
                                          |),
                                          "revm::context::inner_evm_context::InnerEvmContext",
                                          "journaled_state"
                                        |)
                                      ]
                                    |),
                                    M.read (| M.get_constant (| "revm::evm::CALL_STACK_LIMIT" |) |)
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  M.return_ (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::ops::function::Fn",
                                        Ty.function
                                          [
                                            Ty.tuple
                                              [
                                                Ty.path
                                                  "revm_interpreter::instruction_result::InstructionResult"
                                              ]
                                          ]
                                          (Ty.apply
                                            (Ty.path "core::result::Result")
                                            []
                                            [
                                              Ty.path "revm::frame::FrameOrResult";
                                              Ty.apply
                                                (Ty.path "revm_primitives::result::EVMError")
                                                []
                                                [ Ty.associated ]
                                            ]),
                                        [
                                          Ty.tuple
                                            [
                                              Ty.path
                                                "revm_interpreter::instruction_result::InstructionResult"
                                            ]
                                        ],
                                        "call",
                                        []
                                      |),
                                      [
                                        return_result;
                                        Value.Tuple
                                          [
                                            Value.StructTuple
                                              "revm_interpreter::instruction_result::InstructionResult::CallTooDeep"
                                              []
                                          ]
                                      ]
                                    |)
                                  |)
                                |)
                              |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  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_code",
                                [ DB ]
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "revm::context::evm_context::EvmContext",
                                    "inner"
                                  |),
                                  "revm::context::inner_evm_context::InnerEvmContext",
                                  "journaled_state"
                                |);
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| inputs |),
                                    "revm_interpreter::interpreter_action::call_inputs::CallInputs",
                                    "bytecode_address"
                                  |)
                                |);
                                M.SubPointer.get_struct_record_field (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "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.path "revm::frame::FrameOrResult";
                                            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 account := M.copy (| γ0_0 |) in
                          let~ code_hash :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "revm_primitives::state::AccountInfo",
                                  "code_hash",
                                  []
                                |),
                                [
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| account |),
                                    "revm_primitives::state::Account",
                                    "info"
                                  |)
                                ]
                              |)
                            |) in
                          let~ bytecode :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "core::option::Option")
                                    []
                                    [ Ty.path "revm_primitives::bytecode::Bytecode" ],
                                  "unwrap_or_default",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::clone::Clone",
                                      Ty.apply
                                        (Ty.path "core::option::Option")
                                        []
                                        [ Ty.path "revm_primitives::bytecode::Bytecode" ],
                                      [],
                                      "clone",
                                      []
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| account |),
                                          "revm_primitives::state::Account",
                                          "info"
                                        |),
                                        "revm_primitives::state::AccountInfo",
                                        "code"
                                      |)
                                    ]
                                  |)
                                ]
                              |)
                            |) in
                          let~ checkpoint :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "revm::journaled_state::JournaledState",
                                  "checkpoint",
                                  []
                                |),
                                [
                                  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.read (| self |) ]
                                    |),
                                    "revm::context::inner_evm_context::InnerEvmContext",
                                    "journaled_state"
                                  |)
                                ]
                              |)
                            |) in
                          let~ _ :=
                            M.match_operator (|
                              M.SubPointer.get_struct_record_field (|
                                M.read (| inputs |),
                                "revm_interpreter::interpreter_action::call_inputs::CallInputs",
                                "value"
                              |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ0_0 :=
                                      M.SubPointer.get_struct_tuple_field (|
                                        γ,
                                        "revm_interpreter::interpreter_action::call_inputs::CallValue::Transfer",
                                        0
                                      |) in
                                    let value := M.copy (| γ0_0 |) in
                                    let γ :=
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::cmp::PartialEq",
                                            Ty.apply
                                              (Ty.path "ruint::Uint")
                                              [
                                                Value.Integer IntegerKind.Usize 256;
                                                Value.Integer IntegerKind.Usize 4
                                              ]
                                              [],
                                            [
                                              Ty.apply
                                                (Ty.path "ruint::Uint")
                                                [
                                                  Value.Integer IntegerKind.Usize 256;
                                                  Value.Integer IntegerKind.Usize 4
                                                ]
                                                []
                                            ],
                                            "eq",
                                            []
                                          |),
                                          [ value; M.get_constant (| "ruint::ZERO" |) ]
                                        |)
                                      |) 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.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.apply
                                                    (Ty.path
                                                      "revm::context::inner_evm_context::InnerEvmContext")
                                                    []
                                                    [ DB ],
                                                  "load_account",
                                                  []
                                                |),
                                                [
                                                  M.call_closure (|
                                                    M.get_trait_method (|
                                                      "core::ops::deref::DerefMut",
                                                      Ty.apply
                                                        (Ty.path
                                                          "revm::context::evm_context::EvmContext")
                                                        []
                                                        [ DB ],
                                                      [],
                                                      "deref_mut",
                                                      []
                                                    |),
                                                    [ M.read (| self |) ]
                                                  |);
                                                  M.read (|
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| inputs |),
                                                      "revm_interpreter::interpreter_action::call_inputs::CallInputs",
                                                      "target_address"
                                                    |)
                                                  |)
                                                ]
                                              |)
                                            ]
                                          |)
                                        |),
                                        [
                                          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.path "revm::frame::FrameOrResult";
                                                              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::journaled_state::JournaledState",
                                            "touch",
                                            []
                                          |),
                                          [
                                            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.read (| self |) ]
                                              |),
                                              "revm::context::inner_evm_context::InnerEvmContext",
                                              "journaled_state"
                                            |);
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| inputs |),
                                              "revm_interpreter::interpreter_action::call_inputs::CallInputs",
                                              "target_address"
                                            |)
                                          ]
                                        |)
                                      |) in
                                    M.alloc (| Value.Tuple [] |)));
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ0_0 :=
                                      M.SubPointer.get_struct_tuple_field (|
                                        γ,
                                        "revm_interpreter::interpreter_action::call_inputs::CallValue::Transfer",
                                        0
                                      |) in
                                    let value := M.copy (| γ0_0 |) in
                                    M.match_operator (|
                                      M.alloc (| Value.Tuple [] |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (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 "core::option::Option")
                                                            []
                                                            [
                                                              Ty.path
                                                                "revm_interpreter::instruction_result::InstructionResult"
                                                            ];
                                                          Ty.apply
                                                            (Ty.path
                                                              "revm_primitives::result::EVMError")
                                                            []
                                                            [ Ty.associated ]
                                                        ],
                                                      [],
                                                      "branch",
                                                      []
                                                    |),
                                                    [
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path
                                                            "revm::journaled_state::JournaledState",
                                                          "transfer",
                                                          [ DB ]
                                                        |),
                                                        [
                                                          M.SubPointer.get_struct_record_field (|
                                                            M.SubPointer.get_struct_record_field (|
                                                              M.read (| self |),
                                                              "revm::context::evm_context::EvmContext",
                                                              "inner"
                                                            |),
                                                            "revm::context::inner_evm_context::InnerEvmContext",
                                                            "journaled_state"
                                                          |);
                                                          M.SubPointer.get_struct_record_field (|
                                                            M.read (| inputs |),
                                                            "revm_interpreter::interpreter_action::call_inputs::CallInputs",
                                                            "caller"
                                                          |);
                                                          M.SubPointer.get_struct_record_field (|
                                                            M.read (| inputs |),
                                                            "revm_interpreter::interpreter_action::call_inputs::CallInputs",
                                                            "target_address"
                                                          |);
                                                          M.read (| value |);
                                                          M.SubPointer.get_struct_record_field (|
                                                            M.SubPointer.get_struct_record_field (|
                                                              M.read (| self |),
                                                              "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.path
                                                                        "revm::frame::FrameOrResult";
                                                                      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 γ0_0 :=
                                              M.SubPointer.get_struct_tuple_field (|
                                                γ,
                                                "core::option::Option::Some",
                                                0
                                              |) in
                                            let result := M.copy (| γ0_0 |) in
                                            M.alloc (|
                                              M.never_to_any (|
                                                M.read (|
                                                  let~ _ :=
                                                    M.alloc (|
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path
                                                            "revm::journaled_state::JournaledState",
                                                          "checkpoint_revert",
                                                          []
                                                        |),
                                                        [
                                                          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.read (| self |) ]
                                                            |),
                                                            "revm::context::inner_evm_context::InnerEvmContext",
                                                            "journaled_state"
                                                          |);
                                                          M.read (| checkpoint |)
                                                        ]
                                                      |)
                                                    |) in
                                                  M.return_ (|
                                                    M.call_closure (|
                                                      M.get_trait_method (|
                                                        "core::ops::function::Fn",
                                                        Ty.function
                                                          [
                                                            Ty.tuple
                                                              [
                                                                Ty.path
                                                                  "revm_interpreter::instruction_result::InstructionResult"
                                                              ]
                                                          ]
                                                          (Ty.apply
                                                            (Ty.path "core::result::Result")
                                                            []
                                                            [
                                                              Ty.path "revm::frame::FrameOrResult";
                                                              Ty.apply
                                                                (Ty.path
                                                                  "revm_primitives::result::EVMError")
                                                                []
                                                                [ Ty.associated ]
                                                            ]),
                                                        [
                                                          Ty.tuple
                                                            [
                                                              Ty.path
                                                                "revm_interpreter::instruction_result::InstructionResult"
                                                            ]
                                                        ],
                                                        "call",
                                                        []
                                                      |),
                                                      [
                                                        return_result;
                                                        Value.Tuple [ M.read (| result |) ]
                                                      ]
                                                    |)
                                                  |)
                                                |)
                                              |)
                                            |)));
                                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                      ]
                                    |)));
                                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                              ]
                            |) in
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path "revm::context::evm_context::EvmContext")
                                            []
                                            [ DB ],
                                          "call_precompile",
                                          []
                                        |),
                                        [
                                          M.read (| self |);
                                          M.read (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| inputs |),
                                              "revm_interpreter::interpreter_action::call_inputs::CallInputs",
                                              "bytecode_address"
                                            |)
                                          |);
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| inputs |),
                                            "revm_interpreter::interpreter_action::call_inputs::CallInputs",
                                            "input"
                                          |);
                                          M.read (| gas |)
                                        ]
                                      |)
                                    |) in
                                  let γ0_0 :=
                                    M.SubPointer.get_struct_tuple_field (|
                                      γ,
                                      "core::option::Option::Some",
                                      0
                                    |) in
                                  let result := M.copy (| γ0_0 |) 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 (|
                                                    result,
                                                    "revm_interpreter::interpreter::InterpreterResult",
                                                    "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
                                                                    (M.alloc (| Value.Bool true |)))
                                                                | _ =>
                                                                  M.impossible
                                                                    "wrong number of arguments"
                                                                end))
                                                        |)));
                                                    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.alloc (|
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.path "revm::journaled_state::JournaledState",
                                                    "checkpoint_commit",
                                                    []
                                                  |),
                                                  [
                                                    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.read (| self |) ]
                                                      |),
                                                      "revm::context::inner_evm_context::InnerEvmContext",
                                                      "journaled_state"
                                                    |)
                                                  ]
                                                |)
                                              |) in
                                            M.alloc (| Value.Tuple [] |)));
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let~ _ :=
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.path "revm::journaled_state::JournaledState",
                                                    "checkpoint_revert",
                                                    []
                                                  |),
                                                  [
                                                    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.read (| self |) ]
                                                      |),
                                                      "revm::context::inner_evm_context::InnerEvmContext",
                                                      "journaled_state"
                                                    |);
                                                    M.read (| checkpoint |)
                                                  ]
                                                |)
                                              |) in
                                            M.alloc (| Value.Tuple [] |)))
                                      ]
                                    |) in
                                  M.alloc (|
                                    Value.StructTuple
                                      "core::result::Result::Ok"
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "revm::frame::FrameOrResult",
                                            "new_call_result",
                                            []
                                          |),
                                          [
                                            M.read (| result |);
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::clone::Clone",
                                                Ty.apply
                                                  (Ty.path "core::ops::range::Range")
                                                  []
                                                  [ Ty.path "usize" ],
                                                [],
                                                "clone",
                                                []
                                              |),
                                              [
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| inputs |),
                                                  "revm_interpreter::interpreter_action::call_inputs::CallInputs",
                                                  "return_memory_offset"
                                                |)
                                              ]
                                            |)
                                          ]
                                        |)
                                      ]
                                  |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ :=
                                            M.use
                                              (M.alloc (|
                                                UnOp.not (|
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.path "revm_primitives::bytecode::Bytecode",
                                                      "is_empty",
                                                      []
                                                    |),
                                                    [ bytecode ]
                                                  |)
                                                |)
                                              |)) in
                                          let _ :=
                                            M.is_constant_or_break_match (|
                                              M.read (| γ |),
                                              Value.Bool true
                                            |) in
                                          let~ contract :=
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path
                                                    "revm_interpreter::interpreter::contract::Contract",
                                                  "new_with_context",
                                                  []
                                                |),
                                                [
                                                  M.call_closure (|
                                                    M.get_trait_method (|
                                                      "core::clone::Clone",
                                                      Ty.path "alloy_primitives::bytes_::Bytes",
                                                      [],
                                                      "clone",
                                                      []
                                                    |),
                                                    [
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.read (| inputs |),
                                                        "revm_interpreter::interpreter_action::call_inputs::CallInputs",
                                                        "input"
                                                      |)
                                                    ]
                                                  |);
                                                  M.read (| bytecode |);
                                                  Value.StructTuple
                                                    "core::option::Option::Some"
                                                    [ M.read (| code_hash |) ];
                                                  M.read (| inputs |)
                                                ]
                                              |)
                                            |) in
                                          M.alloc (|
                                            Value.StructTuple
                                              "core::result::Result::Ok"
                                              [
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.path "revm::frame::FrameOrResult",
                                                    "new_call_frame",
                                                    []
                                                  |),
                                                  [
                                                    M.call_closure (|
                                                      M.get_trait_method (|
                                                        "core::clone::Clone",
                                                        Ty.apply
                                                          (Ty.path "core::ops::range::Range")
                                                          []
                                                          [ Ty.path "usize" ],
                                                        [],
                                                        "clone",
                                                        []
                                                      |),
                                                      [
                                                        M.SubPointer.get_struct_record_field (|
                                                          M.read (| inputs |),
                                                          "revm_interpreter::interpreter_action::call_inputs::CallInputs",
                                                          "return_memory_offset"
                                                        |)
                                                      ]
                                                    |);
                                                    M.read (| checkpoint |);
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.path
                                                          "revm_interpreter::interpreter::Interpreter",
                                                        "new",
                                                        []
                                                      |),
                                                      [
                                                        M.read (| contract |);
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.path "revm_interpreter::gas::Gas",
                                                            "limit",
                                                            []
                                                          |),
                                                          [ gas ]
                                                        |);
                                                        M.read (|
                                                          M.SubPointer.get_struct_record_field (|
                                                            M.read (| inputs |),
                                                            "revm_interpreter::interpreter_action::call_inputs::CallInputs",
                                                            "is_static"
                                                          |)
                                                        |)
                                                      ]
                                                    |)
                                                  ]
                                                |)
                                              ]
                                          |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let~ _ :=
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path "revm::journaled_state::JournaledState",
                                                  "checkpoint_commit",
                                                  []
                                                |),
                                                [
                                                  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.read (| self |) ]
                                                    |),
                                                    "revm::context::inner_evm_context::InnerEvmContext",
                                                    "journaled_state"
                                                  |)
                                                ]
                                              |)
                                            |) in
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::ops::function::Fn",
                                                Ty.function
                                                  [
                                                    Ty.tuple
                                                      [
                                                        Ty.path
                                                          "revm_interpreter::instruction_result::InstructionResult"
                                                      ]
                                                  ]
                                                  (Ty.apply
                                                    (Ty.path "core::result::Result")
                                                    []
                                                    [
                                                      Ty.path "revm::frame::FrameOrResult";
                                                      Ty.apply
                                                        (Ty.path
                                                          "revm_primitives::result::EVMError")
                                                        []
                                                        [ Ty.associated ]
                                                    ]),
                                                [
                                                  Ty.tuple
                                                    [
                                                      Ty.path
                                                        "revm_interpreter::instruction_result::InstructionResult"
                                                    ]
                                                ],
                                                "call",
                                                []
                                              |),
                                              [
                                                return_result;
                                                Value.Tuple
                                                  [
                                                    Value.StructTuple
                                                      "revm_interpreter::instruction_result::InstructionResult::Stop"
                                                      []
                                                  ]
                                              ]
                                            |)
                                          |)))
                                    ]
                                  |)))
                            ]
                          |)))
                    ]
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_make_call_frame :
        forall (DB : Ty.t),
        M.IsAssociatedFunction (Self DB) "make_call_frame" (make_call_frame DB).
    End Impl_revm_context_evm_context_EvmContext_DB.
  End evm_context.
End context.
