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

Module context.
  Module inner_evm_context.
    (* StructRecord
      {
        name := "InnerEvmContext";
        const_params := [];
        ty_params := [ "DB" ];
        fields :=
          [
            ("env",
              Ty.apply
                (Ty.path "alloc::boxed::Box")
                []
                [ Ty.path "revm_primitives::env::Env"; Ty.path "alloc::alloc::Global" ]);
            ("journaled_state", Ty.path "revm::journaled_state::JournaledState");
            ("db", DB);
            ("error",
              Ty.apply
                (Ty.path "core::result::Result")
                []
                [
                  Ty.tuple [];
                  Ty.apply (Ty.path "revm_primitives::result::EVMError") [] [ Ty.associated ]
                ])
          ];
      } *)
    
    Module Impl_core_fmt_Debug_where_core_fmt_Debug_DB_where_revm_primitives_db_Database_DB_where_core_fmt_Debug_associated_type_for_revm_context_inner_evm_context_InnerEvmContext_DB.
      Definition Self (DB : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "revm::context::inner_evm_context::InnerEvmContext") [] [ DB ].
      
      (* Debug *)
      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::Formatter",
                "debug_struct_field4_finish",
                []
              |),
              [
                M.read (| f |);
                M.read (| Value.String "InnerEvmContext" |);
                M.read (| Value.String "env" |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm::context::inner_evm_context::InnerEvmContext",
                  "env"
                |);
                M.read (| Value.String "journaled_state" |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm::context::inner_evm_context::InnerEvmContext",
                  "journaled_state"
                |);
                M.read (| Value.String "db" |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm::context::inner_evm_context::InnerEvmContext",
                  "db"
                |);
                M.read (| Value.String "error" |);
                M.alloc (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm::context::inner_evm_context::InnerEvmContext",
                    "error"
                  |)
                |)
              ]
            |)))
        | _, _, _ => 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_core_fmt_Debug_DB_where_revm_primitives_db_Database_DB_where_core_fmt_Debug_associated_type_for_revm_context_inner_evm_context_InnerEvmContext_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_inner_evm_context_InnerEvmContext_DB.
      Definition Self (DB : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "revm::context::inner_evm_context::InnerEvmContext") [] [ DB ].
      
      (*
          fn clone(&self) -> Self {
              Self {
                  env: self.env.clone(),
                  journaled_state: self.journaled_state.clone(),
                  db: self.db.clone(),
                  error: self.error.clone(),
                  #[cfg(feature = "optimism")]
                  l1_block_info: self.l1_block_info.clone(),
              }
          }
      *)
      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::inner_evm_context::InnerEvmContext"
              [
                ("env",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::clone::Clone",
                      Ty.apply
                        (Ty.path "alloc::boxed::Box")
                        []
                        [ Ty.path "revm_primitives::env::Env"; Ty.path "alloc::alloc::Global" ],
                      [],
                      "clone",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm::context::inner_evm_context::InnerEvmContext",
                        "env"
                      |)
                    ]
                  |));
                ("journaled_state",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::clone::Clone",
                      Ty.path "revm::journaled_state::JournaledState",
                      [],
                      "clone",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm::context::inner_evm_context::InnerEvmContext",
                        "journaled_state"
                      |)
                    ]
                  |));
                ("db",
                  M.call_closure (|
                    M.get_trait_method (| "core::clone::Clone", DB, [], "clone", [] |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm::context::inner_evm_context::InnerEvmContext",
                        "db"
                      |)
                    ]
                  |));
                ("error",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::clone::Clone",
                      Ty.apply
                        (Ty.path "core::result::Result")
                        []
                        [
                          Ty.tuple [];
                          Ty.apply
                            (Ty.path "revm_primitives::result::EVMError")
                            []
                            [ Ty.associated ]
                        ],
                      [],
                      "clone",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm::context::inner_evm_context::InnerEvmContext",
                        "error"
                      |)
                    ]
                  |))
              ]))
        | _, _, _ => 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_inner_evm_context_InnerEvmContext_DB.
    
    Module Impl_revm_context_inner_evm_context_InnerEvmContext_DB.
      Definition Self (DB : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "revm::context::inner_evm_context::InnerEvmContext") [] [ DB ].
      
      (*
          pub fn new(db: DB) -> Self {
              Self {
                  env: Box::default(),
                  journaled_state: JournaledState::new(SpecId::LATEST, HashSet::new()),
                  db,
                  error: Ok(()),
                  #[cfg(feature = "optimism")]
                  l1_block_info: None,
              }
          }
      *)
      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::inner_evm_context::InnerEvmContext"
              [
                ("env",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::default::Default",
                      Ty.apply
                        (Ty.path "alloc::boxed::Box")
                        []
                        [ Ty.path "revm_primitives::env::Env"; Ty.path "alloc::alloc::Global" ],
                      [],
                      "default",
                      []
                    |),
                    []
                  |));
                ("journaled_state",
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "revm::journaled_state::JournaledState",
                      "new",
                      []
                    |),
                    [
                      Value.StructTuple "revm_primitives::specification::SpecId::LATEST" [];
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "std::collections::hash::set::HashSet")
                            []
                            [
                              Ty.path "alloy_primitives::bits::address::Address";
                              Ty.path "std::hash::random::RandomState"
                            ],
                          "new",
                          []
                        |),
                        []
                      |)
                    ]
                  |));
                ("db", M.read (| db |));
                ("error", Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ])
              ]))
        | _, _, _ => 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 {
                  env,
                  journaled_state: JournaledState::new(SpecId::LATEST, HashSet::new()),
                  db,
                  error: Ok(()),
                  #[cfg(feature = "optimism")]
                  l1_block_info: None,
              }
          }
      *)
      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::inner_evm_context::InnerEvmContext"
              [
                ("env", M.read (| env |));
                ("journaled_state",
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "revm::journaled_state::JournaledState",
                      "new",
                      []
                    |),
                    [
                      Value.StructTuple "revm_primitives::specification::SpecId::LATEST" [];
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "std::collections::hash::set::HashSet")
                            []
                            [
                              Ty.path "alloy_primitives::bits::address::Address";
                              Ty.path "std::hash::random::RandomState"
                            ],
                          "new",
                          []
                        |),
                        []
                      |)
                    ]
                  |));
                ("db", M.read (| db |));
                ("error", Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ])
              ]))
        | _, _, _ => 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) -> InnerEvmContext<ODB> {
              InnerEvmContext {
                  env: self.env,
                  journaled_state: self.journaled_state,
                  db,
                  error: Ok(()),
                  #[cfg(feature = "optimism")]
                  l1_block_info: self.l1_block_info,
              }
          }
      *)
      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::inner_evm_context::InnerEvmContext"
              [
                ("env",
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      self,
                      "revm::context::inner_evm_context::InnerEvmContext",
                      "env"
                    |)
                  |));
                ("journaled_state",
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      self,
                      "revm::context::inner_evm_context::InnerEvmContext",
                      "journaled_state"
                    |)
                  |));
                ("db", M.read (| db |));
                ("error", Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ])
              ]))
        | _, _, _ => 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 const fn spec_id(&self) -> SpecId {
              self.journaled_state.spec
          }
      *)
      Definition spec_id (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.read (|
              M.SubPointer.get_struct_record_field (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm::context::inner_evm_context::InnerEvmContext",
                  "journaled_state"
                |),
                "revm::journaled_state::JournaledState",
                "spec"
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_spec_id :
        forall (DB : Ty.t),
        M.IsAssociatedFunction (Self DB) "spec_id" (spec_id DB).
      
      (*
          pub fn load_access_list(&mut self) -> Result<(), EVMError<DB::Error>> {
              for (address, slots) in self.env.tx.access_list.iter() {
                  self.journaled_state
                      .initial_account_load( *address, slots, &mut self.db)?;
              }
              Ok(())
          }
      *)
      Definition load_access_list
          (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.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    M.use
                      (M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::iter::traits::collect::IntoIterator",
                              Ty.apply
                                (Ty.path "core::slice::iter::Iter")
                                []
                                [
                                  Ty.tuple
                                    [
                                      Ty.path "alloy_primitives::bits::address::Address";
                                      Ty.apply
                                        (Ty.path "alloc::vec::Vec")
                                        []
                                        [
                                          Ty.apply
                                            (Ty.path "ruint::Uint")
                                            [
                                              Value.Integer IntegerKind.Usize 256;
                                              Value.Integer IntegerKind.Usize 4
                                            ]
                                            [];
                                          Ty.path "alloc::alloc::Global"
                                        ]
                                    ]
                                ],
                              [],
                              "into_iter",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "slice")
                                    []
                                    [
                                      Ty.tuple
                                        [
                                          Ty.path "alloy_primitives::bits::address::Address";
                                          Ty.apply
                                            (Ty.path "alloc::vec::Vec")
                                            []
                                            [
                                              Ty.apply
                                                (Ty.path "ruint::Uint")
                                                [
                                                  Value.Integer IntegerKind.Usize 256;
                                                  Value.Integer IntegerKind.Usize 4
                                                ]
                                                [];
                                              Ty.path "alloc::alloc::Global"
                                            ]
                                        ]
                                    ],
                                  "iter",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::ops::deref::Deref",
                                      Ty.apply
                                        (Ty.path "alloc::vec::Vec")
                                        []
                                        [
                                          Ty.tuple
                                            [
                                              Ty.path "alloy_primitives::bits::address::Address";
                                              Ty.apply
                                                (Ty.path "alloc::vec::Vec")
                                                []
                                                [
                                                  Ty.apply
                                                    (Ty.path "ruint::Uint")
                                                    [
                                                      Value.Integer IntegerKind.Usize 256;
                                                      Value.Integer IntegerKind.Usize 4
                                                    ]
                                                    [];
                                                  Ty.path "alloc::alloc::Global"
                                                ]
                                            ];
                                          Ty.path "alloc::alloc::Global"
                                        ],
                                      [],
                                      "deref",
                                      []
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| self |),
                                              "revm::context::inner_evm_context::InnerEvmContext",
                                              "env"
                                            |)
                                          |),
                                          "revm_primitives::env::Env",
                                          "tx"
                                        |),
                                        "revm_primitives::env::TxEnv",
                                        "access_list"
                                      |)
                                    ]
                                  |)
                                ]
                              |)
                            ]
                          |)
                        |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let iter := M.copy (| γ |) in
                              M.loop (|
                                ltac:(M.monadic
                                  (let~ _ :=
                                    M.match_operator (|
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::iter::traits::iterator::Iterator",
                                            Ty.apply
                                              (Ty.path "core::slice::iter::Iter")
                                              []
                                              [
                                                Ty.tuple
                                                  [
                                                    Ty.path
                                                      "alloy_primitives::bits::address::Address";
                                                    Ty.apply
                                                      (Ty.path "alloc::vec::Vec")
                                                      []
                                                      [
                                                        Ty.apply
                                                          (Ty.path "ruint::Uint")
                                                          [
                                                            Value.Integer IntegerKind.Usize 256;
                                                            Value.Integer IntegerKind.Usize 4
                                                          ]
                                                          [];
                                                        Ty.path "alloc::alloc::Global"
                                                      ]
                                                  ]
                                              ],
                                            [],
                                            "next",
                                            []
                                          |),
                                          [ iter ]
                                        |)
                                      |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let _ :=
                                              M.is_struct_tuple (|
                                                γ,
                                                "core::option::Option::None"
                                              |) in
                                            M.alloc (|
                                              M.never_to_any (| M.read (| M.break (||) |) |)
                                            |)));
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ0_0 :=
                                              M.SubPointer.get_struct_tuple_field (|
                                                γ,
                                                "core::option::Option::Some",
                                                0
                                              |) in
                                            let γ0_0 := M.read (| γ0_0 |) in
                                            let γ2_0 :=
                                              M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                                            let γ2_1 :=
                                              M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                                            let address := M.alloc (| γ2_0 |) in
                                            let slots := M.alloc (| γ2_1 |) in
                                            let~ _ :=
                                              M.match_operator (|
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_trait_method (|
                                                      "core::ops::try_trait::Try",
                                                      Ty.apply
                                                        (Ty.path "core::result::Result")
                                                        []
                                                        [
                                                          Ty.apply
                                                            (Ty.path "&mut")
                                                            []
                                                            [
                                                              Ty.path
                                                                "revm_primitives::state::Account"
                                                            ];
                                                          Ty.apply
                                                            (Ty.path
                                                              "revm_primitives::result::EVMError")
                                                            []
                                                            [ Ty.associated ]
                                                        ],
                                                      [],
                                                      "branch",
                                                      []
                                                    |),
                                                    [
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path
                                                            "revm::journaled_state::JournaledState",
                                                          "initial_account_load",
                                                          [ DB ]
                                                        |),
                                                        [
                                                          M.SubPointer.get_struct_record_field (|
                                                            M.read (| self |),
                                                            "revm::context::inner_evm_context::InnerEvmContext",
                                                            "journaled_state"
                                                          |);
                                                          M.read (| M.read (| address |) |);
                                                          M.call_closure (|
                                                            M.get_trait_method (|
                                                              "core::ops::deref::Deref",
                                                              Ty.apply
                                                                (Ty.path "alloc::vec::Vec")
                                                                []
                                                                [
                                                                  Ty.apply
                                                                    (Ty.path "ruint::Uint")
                                                                    [
                                                                      Value.Integer
                                                                        IntegerKind.Usize
                                                                        256;
                                                                      Value.Integer
                                                                        IntegerKind.Usize
                                                                        4
                                                                    ]
                                                                    [];
                                                                  Ty.path "alloc::alloc::Global"
                                                                ],
                                                              [],
                                                              "deref",
                                                              []
                                                            |),
                                                            [ M.read (| slots |) ]
                                                          |);
                                                          M.SubPointer.get_struct_record_field (|
                                                            M.read (| self |),
                                                            "revm::context::inner_evm_context::InnerEvmContext",
                                                            "db"
                                                          |)
                                                        ]
                                                      |)
                                                    ]
                                                  |)
                                                |),
                                                [
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ0_0 :=
                                                        M.SubPointer.get_struct_tuple_field (|
                                                          γ,
                                                          "core::ops::control_flow::ControlFlow::Break",
                                                          0
                                                        |) in
                                                      let residual := M.copy (| γ0_0 |) in
                                                      M.alloc (|
                                                        M.never_to_any (|
                                                          M.read (|
                                                            M.return_ (|
                                                              M.call_closure (|
                                                                M.get_trait_method (|
                                                                  "core::ops::try_trait::FromResidual",
                                                                  Ty.apply
                                                                    (Ty.path "core::result::Result")
                                                                    []
                                                                    [
                                                                      Ty.tuple [];
                                                                      Ty.apply
                                                                        (Ty.path
                                                                          "revm_primitives::result::EVMError")
                                                                        []
                                                                        [ Ty.associated ]
                                                                    ],
                                                                  [
                                                                    Ty.apply
                                                                      (Ty.path
                                                                        "core::result::Result")
                                                                      []
                                                                      [
                                                                        Ty.path
                                                                          "core::convert::Infallible";
                                                                        Ty.apply
                                                                          (Ty.path
                                                                            "revm_primitives::result::EVMError")
                                                                          []
                                                                          [ Ty.associated ]
                                                                      ]
                                                                  ],
                                                                  "from_residual",
                                                                  []
                                                                |),
                                                                [ M.read (| residual |) ]
                                                              |)
                                                            |)
                                                          |)
                                                        |)
                                                      |)));
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ0_0 :=
                                                        M.SubPointer.get_struct_tuple_field (|
                                                          γ,
                                                          "core::ops::control_flow::ControlFlow::Continue",
                                                          0
                                                        |) in
                                                      let val := M.copy (| γ0_0 |) in
                                                      val))
                                                ]
                                              |) in
                                            M.alloc (| Value.Tuple [] |)))
                                      ]
                                    |) in
                                  M.alloc (| Value.Tuple [] |)))
                              |)))
                        ]
                      |)) in
                  M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_load_access_list :
        forall (DB : Ty.t),
        M.IsAssociatedFunction (Self DB) "load_access_list" (load_access_list DB).
      
      (*
          pub fn env(&mut self) -> &mut Env {
              &mut self.env
          }
      *)
      Definition env (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.read (|
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "revm::context::inner_evm_context::InnerEvmContext",
                "env"
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_env :
        forall (DB : Ty.t),
        M.IsAssociatedFunction (Self DB) "env" (env DB).
      
      (*
          pub fn take_error(&mut self) -> Result<(), EVMError<DB::Error>> {
              core::mem::replace(&mut self.error, Ok(()))
          }
      *)
      Definition take_error (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.call_closure (|
              M.get_function (|
                "core::mem::replace",
                [
                  Ty.apply
                    (Ty.path "core::result::Result")
                    []
                    [
                      Ty.tuple [];
                      Ty.apply (Ty.path "revm_primitives::result::EVMError") [] [ Ty.associated ]
                    ]
                ]
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm::context::inner_evm_context::InnerEvmContext",
                  "error"
                |);
                Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ]
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_take_error :
        forall (DB : Ty.t),
        M.IsAssociatedFunction (Self DB) "take_error" (take_error DB).
      
      (*
          pub fn block_hash(&mut self, number: U256) -> Result<B256, EVMError<DB::Error>> {
              self.db.block_hash(number).map_err(EVMError::Database)
          }
      *)
      Definition block_hash (DB : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self DB in
        match ε, τ, α with
        | [], [], [ self; number ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let number := M.alloc (| number |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "core::result::Result")
                  []
                  [
                    Ty.apply
                      (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                      [ Value.Integer IntegerKind.Usize 32 ]
                      [];
                    Ty.associated
                  ],
                "map_err",
                [
                  Ty.apply (Ty.path "revm_primitives::result::EVMError") [] [ Ty.associated ];
                  Ty.function
                    [ Ty.associated ]
                    (Ty.apply (Ty.path "revm_primitives::result::EVMError") [] [ Ty.associated ])
                ]
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "revm_primitives::db::Database",
                    DB,
                    [],
                    "block_hash",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm::context::inner_evm_context::InnerEvmContext",
                      "db"
                    |);
                    M.read (| number |)
                  ]
                |);
                M.constructor_as_closure "revm_primitives::result::EVMError::Database"
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_block_hash :
        forall (DB : Ty.t),
        M.IsAssociatedFunction (Self DB) "block_hash" (block_hash DB).
      
      (*
          pub fn touch(&mut self, address: &Address) {
              self.journaled_state.touch(address);
          }
      *)
      Definition touch (DB : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self DB in
        match ε, τ, α with
        | [], [], [ self; address ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let address := M.alloc (| address |) in
            M.read (|
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "revm::journaled_state::JournaledState",
                      "touch",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm::context::inner_evm_context::InnerEvmContext",
                        "journaled_state"
                      |);
                      M.read (| address |)
                    ]
                  |)
                |) in
              M.alloc (| Value.Tuple [] |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_touch :
        forall (DB : Ty.t),
        M.IsAssociatedFunction (Self DB) "touch" (touch DB).
      
      (*
          pub fn load_account(
              &mut self,
              address: Address,
          ) -> Result<(&mut Account, bool), EVMError<DB::Error>> {
              self.journaled_state.load_account(address, &mut self.db)
          }
      *)
      Definition load_account
          (DB : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self DB in
        match ε, τ, α with
        | [], [], [ self; address ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let address := M.alloc (| address |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "revm::journaled_state::JournaledState",
                "load_account",
                [ DB ]
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm::context::inner_evm_context::InnerEvmContext",
                  "journaled_state"
                |);
                M.read (| address |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm::context::inner_evm_context::InnerEvmContext",
                  "db"
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_load_account :
        forall (DB : Ty.t),
        M.IsAssociatedFunction (Self DB) "load_account" (load_account DB).
      
      (*
          pub fn load_account_exist(
              &mut self,
              address: Address,
          ) -> Result<LoadAccountResult, EVMError<DB::Error>> {
              self.journaled_state
                  .load_account_exist(address, &mut self.db)
          }
      *)
      Definition load_account_exist
          (DB : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self DB in
        match ε, τ, α with
        | [], [], [ self; address ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let address := M.alloc (| address |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "revm::journaled_state::JournaledState",
                "load_account_exist",
                [ DB ]
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm::context::inner_evm_context::InnerEvmContext",
                  "journaled_state"
                |);
                M.read (| address |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm::context::inner_evm_context::InnerEvmContext",
                  "db"
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_load_account_exist :
        forall (DB : Ty.t),
        M.IsAssociatedFunction (Self DB) "load_account_exist" (load_account_exist DB).
      
      (*
          pub fn balance(&mut self, address: Address) -> Result<(U256, bool), EVMError<DB::Error>> {
              self.journaled_state
                  .load_account(address, &mut self.db)
                  .map(|(acc, is_cold)| (acc.info.balance, is_cold))
          }
      *)
      Definition balance (DB : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self DB in
        match ε, τ, α with
        | [], [], [ self; address ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let address := M.alloc (| address |) in
            M.call_closure (|
              M.get_associated_function (|
                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 ]
                  ],
                "map",
                [
                  Ty.tuple
                    [
                      Ty.apply
                        (Ty.path "ruint::Uint")
                        [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                        [];
                      Ty.path "bool"
                    ];
                  Ty.function
                    [
                      Ty.tuple
                        [
                          Ty.tuple
                            [
                              Ty.apply
                                (Ty.path "&mut")
                                []
                                [ Ty.path "revm_primitives::state::Account" ];
                              Ty.path "bool"
                            ]
                        ]
                    ]
                    (Ty.tuple
                      [
                        Ty.apply
                          (Ty.path "ruint::Uint")
                          [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                          [];
                        Ty.path "bool"
                      ])
                ]
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "revm::journaled_state::JournaledState",
                    "load_account",
                    [ DB ]
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm::context::inner_evm_context::InnerEvmContext",
                      "journaled_state"
                    |);
                    M.read (| address |);
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm::context::inner_evm_context::InnerEvmContext",
                      "db"
                    |)
                  ]
                |);
                M.closure
                  (fun γ =>
                    ltac:(M.monadic
                      match γ with
                      | [ α0 ] =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| α0 |),
                            [
                              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 acc := M.copy (| γ0_0 |) in
                                  let is_cold := M.copy (| γ0_1 |) in
                                  Value.Tuple
                                    [
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| acc |),
                                            "revm_primitives::state::Account",
                                            "info"
                                          |),
                                          "revm_primitives::state::AccountInfo",
                                          "balance"
                                        |)
                                      |);
                                      M.read (| is_cold |)
                                    ]))
                            ]
                          |)))
                      | _ => M.impossible "wrong number of arguments"
                      end))
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_balance :
        forall (DB : Ty.t),
        M.IsAssociatedFunction (Self DB) "balance" (balance DB).
      
      (*
          pub fn code(&mut self, address: Address) -> Result<(Bytecode, bool), EVMError<DB::Error>> {
              self.journaled_state
                  .load_code(address, &mut self.db)
                  .map(|(a, is_cold)| (a.info.code.clone().unwrap(), is_cold))
          }
      *)
      Definition code (DB : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self DB in
        match ε, τ, α with
        | [], [], [ self; address ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let address := M.alloc (| address |) in
            M.call_closure (|
              M.get_associated_function (|
                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 ]
                  ],
                "map",
                [
                  Ty.tuple [ Ty.path "revm_primitives::bytecode::Bytecode"; Ty.path "bool" ];
                  Ty.function
                    [
                      Ty.tuple
                        [
                          Ty.tuple
                            [
                              Ty.apply
                                (Ty.path "&mut")
                                []
                                [ Ty.path "revm_primitives::state::Account" ];
                              Ty.path "bool"
                            ]
                        ]
                    ]
                    (Ty.tuple [ Ty.path "revm_primitives::bytecode::Bytecode"; Ty.path "bool" ])
                ]
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "revm::journaled_state::JournaledState",
                    "load_code",
                    [ DB ]
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm::context::inner_evm_context::InnerEvmContext",
                      "journaled_state"
                    |);
                    M.read (| address |);
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm::context::inner_evm_context::InnerEvmContext",
                      "db"
                    |)
                  ]
                |);
                M.closure
                  (fun γ =>
                    ltac:(M.monadic
                      match γ with
                      | [ α0 ] =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| α0 |),
                            [
                              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 a := M.copy (| γ0_0 |) in
                                  let is_cold := M.copy (| γ0_1 |) in
                                  Value.Tuple
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path "core::option::Option")
                                            []
                                            [ Ty.path "revm_primitives::bytecode::Bytecode" ],
                                          "unwrap",
                                          []
                                        |),
                                        [
                                          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 (| a |),
                                                  "revm_primitives::state::Account",
                                                  "info"
                                                |),
                                                "revm_primitives::state::AccountInfo",
                                                "code"
                                              |)
                                            ]
                                          |)
                                        ]
                                      |);
                                      M.read (| is_cold |)
                                    ]))
                            ]
                          |)))
                      | _ => M.impossible "wrong number of arguments"
                      end))
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_code :
        forall (DB : Ty.t),
        M.IsAssociatedFunction (Self DB) "code" (code DB).
      
      (*
          pub fn code_hash(&mut self, address: Address) -> Result<(B256, bool), EVMError<DB::Error>> {
              let (acc, is_cold) = self.journaled_state.load_code(address, &mut self.db)?;
              if acc.is_empty() {
                  return Ok((B256::ZERO, is_cold));
              }
              Ok((acc.info.code_hash, is_cold))
          }
      *)
      Definition code_hash (DB : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self DB in
        match ε, τ, α with
        | [], [], [ self; address ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let address := M.alloc (| address |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  M.match_operator (|
                    M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::try_trait::Try",
                            Ty.apply
                              (Ty.path "core::result::Result")
                              []
                              [
                                Ty.tuple
                                  [
                                    Ty.apply
                                      (Ty.path "&mut")
                                      []
                                      [ Ty.path "revm_primitives::state::Account" ];
                                    Ty.path "bool"
                                  ];
                                Ty.apply
                                  (Ty.path "revm_primitives::result::EVMError")
                                  []
                                  [ Ty.associated ]
                              ],
                            [],
                            "branch",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "revm::journaled_state::JournaledState",
                                "load_code",
                                [ DB ]
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "revm::context::inner_evm_context::InnerEvmContext",
                                  "journaled_state"
                                |);
                                M.read (| address |);
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "revm::context::inner_evm_context::InnerEvmContext",
                                  "db"
                                |)
                              ]
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::control_flow::ControlFlow::Break",
                                0
                              |) in
                            let residual := M.copy (| γ0_0 |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  M.return_ (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::ops::try_trait::FromResidual",
                                        Ty.apply
                                          (Ty.path "core::result::Result")
                                          []
                                          [
                                            Ty.tuple
                                              [
                                                Ty.apply
                                                  (Ty.path
                                                    "alloy_primitives::bits::fixed::FixedBytes")
                                                  [ Value.Integer IntegerKind.Usize 32 ]
                                                  [];
                                                Ty.path "bool"
                                              ];
                                            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 acc := M.copy (| γ0_0 |) in
                          let is_cold := M.copy (| γ0_1 |) in
                          let~ _ :=
                            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_primitives::state::Account",
                                              "is_empty",
                                              []
                                            |),
                                            [ M.read (| acc |) ]
                                          |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    M.alloc (|
                                      M.never_to_any (|
                                        M.read (|
                                          M.return_ (|
                                            Value.StructTuple
                                              "core::result::Result::Ok"
                                              [
                                                Value.Tuple
                                                  [
                                                    M.read (|
                                                      M.get_constant (|
                                                        "alloy_primitives::bits::fixed::ZERO"
                                                      |)
                                                    |);
                                                    M.read (| is_cold |)
                                                  ]
                                              ]
                                          |)
                                        |)
                                      |)
                                    |)));
                                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                              ]
                            |) in
                          M.alloc (|
                            Value.StructTuple
                              "core::result::Result::Ok"
                              [
                                Value.Tuple
                                  [
                                    M.read (|
                                      M.SubPointer.get_struct_record_field (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| acc |),
                                          "revm_primitives::state::Account",
                                          "info"
                                        |),
                                        "revm_primitives::state::AccountInfo",
                                        "code_hash"
                                      |)
                                    |);
                                    M.read (| is_cold |)
                                  ]
                              ]
                          |)))
                    ]
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_code_hash :
        forall (DB : Ty.t),
        M.IsAssociatedFunction (Self DB) "code_hash" (code_hash DB).
      
      (*
          pub fn sload(
              &mut self,
              address: Address,
              index: U256,
          ) -> Result<(U256, bool), EVMError<DB::Error>> {
              // account is always warm. reference on that statement https://eips.ethereum.org/EIPS/eip-2929 see `Note 2:`
              self.journaled_state.sload(address, index, &mut self.db)
          }
      *)
      Definition sload (DB : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self DB in
        match ε, τ, α with
        | [], [], [ self; address; index ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let address := M.alloc (| address |) in
            let index := M.alloc (| index |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "revm::journaled_state::JournaledState",
                "sload",
                [ DB ]
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm::context::inner_evm_context::InnerEvmContext",
                  "journaled_state"
                |);
                M.read (| address |);
                M.read (| index |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm::context::inner_evm_context::InnerEvmContext",
                  "db"
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_sload :
        forall (DB : Ty.t),
        M.IsAssociatedFunction (Self DB) "sload" (sload DB).
      
      (*
          pub fn sstore(
              &mut self,
              address: Address,
              index: U256,
              value: U256,
          ) -> Result<SStoreResult, EVMError<DB::Error>> {
              self.journaled_state
                  .sstore(address, index, value, &mut self.db)
          }
      *)
      Definition sstore (DB : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self DB in
        match ε, τ, α with
        | [], [], [ self; address; index; value ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let address := M.alloc (| address |) in
            let index := M.alloc (| index |) in
            let value := M.alloc (| value |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "revm::journaled_state::JournaledState",
                "sstore",
                [ DB ]
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm::context::inner_evm_context::InnerEvmContext",
                  "journaled_state"
                |);
                M.read (| address |);
                M.read (| index |);
                M.read (| value |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm::context::inner_evm_context::InnerEvmContext",
                  "db"
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_sstore :
        forall (DB : Ty.t),
        M.IsAssociatedFunction (Self DB) "sstore" (sstore DB).
      
      (*
          pub fn tload(&mut self, address: Address, index: U256) -> U256 {
              self.journaled_state.tload(address, index)
          }
      *)
      Definition tload (DB : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self DB in
        match ε, τ, α with
        | [], [], [ self; address; index ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let address := M.alloc (| address |) in
            let index := M.alloc (| index |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "revm::journaled_state::JournaledState",
                "tload",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm::context::inner_evm_context::InnerEvmContext",
                  "journaled_state"
                |);
                M.read (| address |);
                M.read (| index |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_tload :
        forall (DB : Ty.t),
        M.IsAssociatedFunction (Self DB) "tload" (tload DB).
      
      (*
          pub fn tstore(&mut self, address: Address, index: U256, value: U256) {
              self.journaled_state.tstore(address, index, value)
          }
      *)
      Definition tstore (DB : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self DB in
        match ε, τ, α with
        | [], [], [ self; address; index; value ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let address := M.alloc (| address |) in
            let index := M.alloc (| index |) in
            let value := M.alloc (| value |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "revm::journaled_state::JournaledState",
                "tstore",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm::context::inner_evm_context::InnerEvmContext",
                  "journaled_state"
                |);
                M.read (| address |);
                M.read (| index |);
                M.read (| value |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_tstore :
        forall (DB : Ty.t),
        M.IsAssociatedFunction (Self DB) "tstore" (tstore DB).
      
      (*
          pub fn selfdestruct(
              &mut self,
              address: Address,
              target: Address,
          ) -> Result<SelfDestructResult, EVMError<DB::Error>> {
              self.journaled_state
                  .selfdestruct(address, target, &mut self.db)
          }
      *)
      Definition selfdestruct
          (DB : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self DB in
        match ε, τ, α with
        | [], [], [ self; address; target ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let address := M.alloc (| address |) in
            let target := M.alloc (| target |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "revm::journaled_state::JournaledState",
                "selfdestruct",
                [ DB ]
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm::context::inner_evm_context::InnerEvmContext",
                  "journaled_state"
                |);
                M.read (| address |);
                M.read (| target |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm::context::inner_evm_context::InnerEvmContext",
                  "db"
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_selfdestruct :
        forall (DB : Ty.t),
        M.IsAssociatedFunction (Self DB) "selfdestruct" (selfdestruct DB).
      
      (*
          pub fn make_eofcreate_frame(
              &mut self,
              spec_id: SpecId,
              inputs: &EOFCreateInput,
          ) -> Result<FrameOrResult, EVMError<DB::Error>> {
              let return_error = |e| {
                  Ok(FrameOrResult::new_eofcreate_result(
                      InterpreterResult {
                          result: e,
                          gas: Gas::new(inputs.gas_limit),
                          output: Bytes::new(),
                      },
                      inputs.created_address,
                      inputs.return_memory_range.clone(),
                  ))
              };
      
              // Check depth
              if self.journaled_state.depth() > CALL_STACK_LIMIT {
                  return return_error(InstructionResult::CallTooDeep);
              }
      
              // Fetch balance of caller.
              let (caller_balance, _) = self.balance(inputs.caller)?;
      
              // Check if caller has enough balance to send to the created contract.
              if caller_balance < inputs.value {
                  return return_error(InstructionResult::OutOfFunds);
              }
      
              // Increase nonce of caller and check if it overflows
              if self.journaled_state.inc_nonce(inputs.caller).is_none() {
                  // can't happen on mainnet.
                  return return_error(InstructionResult::Return);
              }
      
              // Load account so it needs to be marked as warm for access list.
              self.journaled_state
                  .load_account(inputs.created_address, &mut self.db)?;
      
              // create account, transfer funds and make the journal checkpoint.
              let checkpoint = match self.journaled_state.create_account_checkpoint(
                  inputs.caller,
                  inputs.created_address,
                  inputs.value,
                  spec_id,
              ) {
                  Ok(checkpoint) => checkpoint,
                  Err(e) => {
                      return return_error(e);
                  }
              };
      
              let contract = Contract::new(
                  Bytes::new(),
                  // fine to clone as it is Bytes.
                  Bytecode::Eof(inputs.eof_init_code.clone()),
                  None,
                  inputs.created_address,
                  inputs.caller,
                  inputs.value,
              );
      
              let mut interpreter = Interpreter::new(contract, inputs.gas_limit, false);
              // EOF init will enable RETURNCONTRACT opcode.
              interpreter.set_is_eof_init();
      
              Ok(FrameOrResult::new_eofcreate_frame(
                  inputs.created_address,
                  inputs.return_memory_range.clone(),
                  checkpoint,
                  interpreter,
              ))
          }
      *)
      Definition make_eofcreate_frame
          (DB : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self DB in
        match ε, τ, α with
        | [], [], [ self; spec_id; inputs ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let spec_id := M.alloc (| spec_id |) in
            let inputs := M.alloc (| inputs |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ return_error :=
                    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 e := M.copy (| γ |) in
                                        Value.StructTuple
                                          "core::result::Result::Ok"
                                          [
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.path "revm::frame::FrameOrResult",
                                                "new_eofcreate_result",
                                                []
                                              |),
                                              [
                                                Value.StructRecord
                                                  "revm_interpreter::interpreter::InterpreterResult"
                                                  [
                                                    ("result", M.read (| e |));
                                                    ("gas",
                                                      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::eof_create_inputs::EOFCreateInput",
                                                              "gas_limit"
                                                            |)
                                                          |)
                                                        ]
                                                      |));
                                                    ("output",
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path "alloy_primitives::bytes_::Bytes",
                                                          "new",
                                                          []
                                                        |),
                                                        []
                                                      |))
                                                  ];
                                                M.read (|
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.read (| inputs |),
                                                    "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput",
                                                    "created_address"
                                                  |)
                                                |);
                                                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::eof_create_inputs::EOFCreateInput",
                                                      "return_memory_range"
                                                    |)
                                                  ]
                                                |)
                                              ]
                                            |)
                                          ]))
                                  ]
                                |)))
                            | _ => 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.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_error;
                                        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 "ruint::Uint")
                                      [
                                        Value.Integer IntegerKind.Usize 256;
                                        Value.Integer IntegerKind.Usize 4
                                      ]
                                      [];
                                    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 ],
                                "balance",
                                []
                              |),
                              [
                                M.read (| self |);
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| inputs |),
                                    "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput",
                                    "caller"
                                  |)
                                |)
                              ]
                            |)
                          ]
                        |)
                      |),
                      [
                        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 caller_balance := M.copy (| γ0_0 |) in
                          let~ _ :=
                            M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::cmp::PartialOrd",
                                              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
                                                  ]
                                                  []
                                              ],
                                              "lt",
                                              []
                                            |),
                                            [
                                              caller_balance;
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| inputs |),
                                                "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput",
                                                "value"
                                              |)
                                            ]
                                          |)
                                        |)) 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_error;
                                                Value.Tuple
                                                  [
                                                    Value.StructTuple
                                                      "revm_interpreter::instruction_result::InstructionResult::OutOfFunds"
                                                      []
                                                  ]
                                              ]
                                            |)
                                          |)
                                        |)
                                      |)
                                    |)));
                                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                              ]
                            |) in
                          let~ _ :=
                            M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply
                                                (Ty.path "core::option::Option")
                                                []
                                                [ Ty.path "u64" ],
                                              "is_none",
                                              []
                                            |),
                                            [
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.path "revm::journaled_state::JournaledState",
                                                    "inc_nonce",
                                                    []
                                                  |),
                                                  [
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| self |),
                                                      "revm::context::inner_evm_context::InnerEvmContext",
                                                      "journaled_state"
                                                    |);
                                                    M.read (|
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.read (| inputs |),
                                                        "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput",
                                                        "caller"
                                                      |)
                                                    |)
                                                  ]
                                                |)
                                              |)
                                            ]
                                          |)
                                        |)) 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_error;
                                                Value.Tuple
                                                  [
                                                    Value.StructTuple
                                                      "revm_interpreter::instruction_result::InstructionResult::Return"
                                                      []
                                                  ]
                                              ]
                                            |)
                                          |)
                                        |)
                                      |)
                                    |)));
                                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                              ]
                            |) in
                          let~ _ :=
                            M.match_operator (|
                              M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::try_trait::Try",
                                    Ty.apply
                                      (Ty.path "core::result::Result")
                                      []
                                      [
                                        Ty.tuple
                                          [
                                            Ty.apply
                                              (Ty.path "&mut")
                                              []
                                              [ Ty.path "revm_primitives::state::Account" ];
                                            Ty.path "bool"
                                          ];
                                        Ty.apply
                                          (Ty.path "revm_primitives::result::EVMError")
                                          []
                                          [ Ty.associated ]
                                      ],
                                    [],
                                    "branch",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "revm::journaled_state::JournaledState",
                                        "load_account",
                                        [ DB ]
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "revm::context::inner_evm_context::InnerEvmContext",
                                          "journaled_state"
                                        |);
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| inputs |),
                                            "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput",
                                            "created_address"
                                          |)
                                        |);
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "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~ checkpoint :=
                            M.copy (|
                              M.match_operator (|
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "revm::journaled_state::JournaledState",
                                      "create_account_checkpoint",
                                      []
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| self |),
                                        "revm::context::inner_evm_context::InnerEvmContext",
                                        "journaled_state"
                                      |);
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| inputs |),
                                          "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput",
                                          "caller"
                                        |)
                                      |);
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| inputs |),
                                          "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput",
                                          "created_address"
                                        |)
                                      |);
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| inputs |),
                                          "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput",
                                          "value"
                                        |)
                                      |);
                                      M.read (| spec_id |)
                                    ]
                                  |)
                                |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ0_0 :=
                                        M.SubPointer.get_struct_tuple_field (|
                                          γ,
                                          "core::result::Result::Ok",
                                          0
                                        |) in
                                      let checkpoint := M.copy (| γ0_0 |) in
                                      checkpoint));
                                  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
                                      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_error; Value.Tuple [ M.read (| e |) ] ]
                                              |)
                                            |)
                                          |)
                                        |)
                                      |)))
                                ]
                              |)
                            |) in
                          let~ contract :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "revm_interpreter::interpreter::contract::Contract",
                                  "new",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "alloy_primitives::bytes_::Bytes",
                                      "new",
                                      []
                                    |),
                                    []
                                  |);
                                  Value.StructTuple
                                    "revm_primitives::bytecode::Bytecode::Eof"
                                    [
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::clone::Clone",
                                          Ty.path "revm_primitives::bytecode::eof::Eof",
                                          [],
                                          "clone",
                                          []
                                        |),
                                        [
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| inputs |),
                                            "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput",
                                            "eof_init_code"
                                          |)
                                        ]
                                      |)
                                    ];
                                  Value.StructTuple "core::option::Option::None" [];
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| inputs |),
                                      "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput",
                                      "created_address"
                                    |)
                                  |);
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| inputs |),
                                      "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput",
                                      "caller"
                                    |)
                                  |);
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| inputs |),
                                      "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput",
                                      "value"
                                    |)
                                  |)
                                ]
                              |)
                            |) in
                          let~ interpreter :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "revm_interpreter::interpreter::Interpreter",
                                  "new",
                                  []
                                |),
                                [
                                  M.read (| contract |);
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| inputs |),
                                      "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput",
                                      "gas_limit"
                                    |)
                                  |);
                                  Value.Bool false
                                ]
                              |)
                            |) in
                          let~ _ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "revm_interpreter::interpreter::Interpreter",
                                  "set_is_eof_init",
                                  []
                                |),
                                [ interpreter ]
                              |)
                            |) in
                          M.alloc (|
                            Value.StructTuple
                              "core::result::Result::Ok"
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "revm::frame::FrameOrResult",
                                    "new_eofcreate_frame",
                                    []
                                  |),
                                  [
                                    M.read (|
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| inputs |),
                                        "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput",
                                        "created_address"
                                      |)
                                    |);
                                    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::eof_create_inputs::EOFCreateInput",
                                          "return_memory_range"
                                        |)
                                      ]
                                    |);
                                    M.read (| checkpoint |);
                                    M.read (| interpreter |)
                                  ]
                                |)
                              ]
                          |)))
                    ]
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_make_eofcreate_frame :
        forall (DB : Ty.t),
        M.IsAssociatedFunction (Self DB) "make_eofcreate_frame" (make_eofcreate_frame DB).
      
      (*
          pub fn eofcreate_return<SPEC: Spec>(
              &mut self,
              interpreter_result: &mut InterpreterResult,
              address: Address,
              journal_checkpoint: JournalCheckpoint,
          ) {
              // Note we still execute RETURN opcode and return the bytes.
              // In EOF those opcodes should abort execution.
              //
              // In RETURN gas is still protecting us from ddos and in oog,
              // behaviour will be same as if it failed on return.
              //
              // Bytes of RETURN will drained in `insert_eofcreate_outcome`.
              if interpreter_result.result != InstructionResult::ReturnContract {
                  self.journaled_state.checkpoint_revert(journal_checkpoint);
                  return;
              }
      
              // commit changes reduces depth by -1.
              self.journaled_state.checkpoint_commit();
      
              // decode bytecode has a performance hit, but it has reasonable restrains.
              let bytecode =
                  Eof::decode(interpreter_result.output.clone()).expect("Eof is already verified");
      
              // eof bytecode is going to be hashed.
              self.journaled_state
                  .set_code(address, Bytecode::Eof(bytecode));
          }
      *)
      Definition eofcreate_return
          (DB : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self DB in
        match ε, τ, α with
        | [], [ SPEC ], [ self; interpreter_result; address; journal_checkpoint ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let interpreter_result := M.alloc (| interpreter_result |) in
            let address := M.alloc (| address |) in
            let journal_checkpoint := M.alloc (| journal_checkpoint |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    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_interpreter::instruction_result::InstructionResult",
                                      [
                                        Ty.path
                                          "revm_interpreter::instruction_result::InstructionResult"
                                      ],
                                      "ne",
                                      []
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| interpreter_result |),
                                        "revm_interpreter::interpreter::InterpreterResult",
                                        "result"
                                      |);
                                      M.alloc (|
                                        Value.StructTuple
                                          "revm_interpreter::instruction_result::InstructionResult::ReturnContract"
                                          []
                                      |)
                                    ]
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) 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.read (| self |),
                                            "revm::context::inner_evm_context::InnerEvmContext",
                                            "journaled_state"
                                          |);
                                          M.read (| journal_checkpoint |)
                                        ]
                                      |)
                                    |) in
                                  M.return_ (| Value.Tuple [] |)
                                |)
                              |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) 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.read (| self |),
                            "revm::context::inner_evm_context::InnerEvmContext",
                            "journaled_state"
                          |)
                        ]
                      |)
                    |) in
                  let~ bytecode :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "core::result::Result")
                            []
                            [
                              Ty.path "revm_primitives::bytecode::eof::Eof";
                              Ty.path "revm_primitives::bytecode::eof::EofDecodeError"
                            ],
                          "expect",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "revm_primitives::bytecode::eof::Eof",
                              "decode",
                              []
                            |),
                            [
                              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 (| interpreter_result |),
                                    "revm_interpreter::interpreter::InterpreterResult",
                                    "output"
                                  |)
                                ]
                              |)
                            ]
                          |);
                          M.read (| Value.String "Eof is already verified" |)
                        ]
                      |)
                    |) in
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "revm::journaled_state::JournaledState",
                          "set_code",
                          []
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "revm::context::inner_evm_context::InnerEvmContext",
                            "journaled_state"
                          |);
                          M.read (| address |);
                          Value.StructTuple
                            "revm_primitives::bytecode::Bytecode::Eof"
                            [ M.read (| bytecode |) ]
                        ]
                      |)
                    |) in
                  M.alloc (| Value.Tuple [] |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_eofcreate_return :
        forall (DB : Ty.t),
        M.IsAssociatedFunction (Self DB) "eofcreate_return" (eofcreate_return DB).
      
      (*
          pub fn make_create_frame(
              &mut self,
              spec_id: SpecId,
              inputs: &CreateInputs,
          ) -> Result<FrameOrResult, EVMError<DB::Error>> {
              // Prepare crate.
              let gas = Gas::new(inputs.gas_limit);
      
              let return_error = |e| {
                  Ok(FrameOrResult::new_create_result(
                      InterpreterResult {
                          result: e,
                          gas,
                          output: Bytes::new(),
                      },
                      None,
                  ))
              };
      
              // Check depth
              if self.journaled_state.depth() > CALL_STACK_LIMIT {
                  return return_error(InstructionResult::CallTooDeep);
              }
      
              // Fetch balance of caller.
              let (caller_balance, _) = self.balance(inputs.caller)?;
      
              // Check if caller has enough balance to send to the created contract.
              if caller_balance < inputs.value {
                  return return_error(InstructionResult::OutOfFunds);
              }
      
              // Increase nonce of caller and check if it overflows
              let old_nonce;
              if let Some(nonce) = self.journaled_state.inc_nonce(inputs.caller) {
                  old_nonce = nonce - 1;
              } else {
                  return return_error(InstructionResult::Return);
              }
      
              // Create address
              let mut init_code_hash = B256::ZERO;
              let created_address = match inputs.scheme {
                  CreateScheme::Create => inputs.caller.create(old_nonce),
                  CreateScheme::Create2 { salt } => {
                      init_code_hash = keccak256(&inputs.init_code);
                      inputs.caller.create2(salt.to_be_bytes(), init_code_hash)
                  }
              };
      
              // Load account so it needs to be marked as warm for access list.
              self.journaled_state
                  .load_account(created_address, &mut self.db)?;
      
              // create account, transfer funds and make the journal checkpoint.
              let checkpoint = match self.journaled_state.create_account_checkpoint(
                  inputs.caller,
                  created_address,
                  inputs.value,
                  spec_id,
              ) {
                  Ok(checkpoint) => checkpoint,
                  Err(e) => {
                      return return_error(e);
                  }
              };
      
              let bytecode = Bytecode::new_raw(inputs.init_code.clone());
      
              let contract = Contract::new(
                  Bytes::new(),
                  bytecode,
                  Some(init_code_hash),
                  created_address,
                  inputs.caller,
                  inputs.value,
              );
      
              Ok(FrameOrResult::new_create_frame(
                  created_address,
                  checkpoint,
                  Interpreter::new(contract, gas.limit(), false),
              ))
          }
      *)
      Definition make_create_frame
          (DB : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self DB in
        match ε, τ, α with
        | [], [], [ self; spec_id; inputs ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let spec_id := M.alloc (| spec_id |) 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::create_inputs::CreateInputs",
                              "gas_limit"
                            |)
                          |)
                        ]
                      |)
                    |) in
                  let~ return_error :=
                    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 e := M.copy (| γ |) in
                                        Value.StructTuple
                                          "core::result::Result::Ok"
                                          [
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.path "revm::frame::FrameOrResult",
                                                "new_create_result",
                                                []
                                              |),
                                              [
                                                Value.StructRecord
                                                  "revm_interpreter::interpreter::InterpreterResult"
                                                  [
                                                    ("result", M.read (| e |));
                                                    ("gas", M.read (| gas |));
                                                    ("output",
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path "alloy_primitives::bytes_::Bytes",
                                                          "new",
                                                          []
                                                        |),
                                                        []
                                                      |))
                                                  ];
                                                Value.StructTuple "core::option::Option::None" []
                                              ]
                                            |)
                                          ]))
                                  ]
                                |)))
                            | _ => 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.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_error;
                                        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 "ruint::Uint")
                                      [
                                        Value.Integer IntegerKind.Usize 256;
                                        Value.Integer IntegerKind.Usize 4
                                      ]
                                      [];
                                    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 ],
                                "balance",
                                []
                              |),
                              [
                                M.read (| self |);
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| inputs |),
                                    "revm_interpreter::interpreter_action::create_inputs::CreateInputs",
                                    "caller"
                                  |)
                                |)
                              ]
                            |)
                          ]
                        |)
                      |),
                      [
                        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 caller_balance := M.copy (| γ0_0 |) in
                          let~ _ :=
                            M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::cmp::PartialOrd",
                                              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
                                                  ]
                                                  []
                                              ],
                                              "lt",
                                              []
                                            |),
                                            [
                                              caller_balance;
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| inputs |),
                                                "revm_interpreter::interpreter_action::create_inputs::CreateInputs",
                                                "value"
                                              |)
                                            ]
                                          |)
                                        |)) 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_error;
                                                Value.Tuple
                                                  [
                                                    Value.StructTuple
                                                      "revm_interpreter::instruction_result::InstructionResult::OutOfFunds"
                                                      []
                                                  ]
                                              ]
                                            |)
                                          |)
                                        |)
                                      |)
                                    |)));
                                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                              ]
                            |) in
                          let~ old_nonce := M.copy (| Value.DeclaredButUndefined |) in
                          let~ _ :=
                            M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "revm::journaled_state::JournaledState",
                                            "inc_nonce",
                                            []
                                          |),
                                          [
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| self |),
                                              "revm::context::inner_evm_context::InnerEvmContext",
                                              "journaled_state"
                                            |);
                                            M.read (|
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| inputs |),
                                                "revm_interpreter::interpreter_action::create_inputs::CreateInputs",
                                                "caller"
                                              |)
                                            |)
                                          ]
                                        |)
                                      |) in
                                    let γ0_0 :=
                                      M.SubPointer.get_struct_tuple_field (|
                                        γ,
                                        "core::option::Option::Some",
                                        0
                                      |) in
                                    let nonce := M.copy (| γ0_0 |) in
                                    let~ _ :=
                                      M.write (|
                                        old_nonce,
                                        BinOp.Wrap.sub (|
                                          M.read (| nonce |),
                                          Value.Integer IntegerKind.U64 1
                                        |)
                                      |) in
                                    M.alloc (| Value.Tuple [] |)));
                                fun γ =>
                                  ltac:(M.monadic
                                    (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_error;
                                                Value.Tuple
                                                  [
                                                    Value.StructTuple
                                                      "revm_interpreter::instruction_result::InstructionResult::Return"
                                                      []
                                                  ]
                                              ]
                                            |)
                                          |)
                                        |)
                                      |)
                                    |)))
                              ]
                            |) in
                          let~ init_code_hash :=
                            M.copy (|
                              M.get_constant (| "alloy_primitives::bits::fixed::ZERO" |)
                            |) in
                          let~ created_address :=
                            M.copy (|
                              M.match_operator (|
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| inputs |),
                                  "revm_interpreter::interpreter_action::create_inputs::CreateInputs",
                                  "scheme"
                                |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let _ :=
                                        M.is_struct_tuple (|
                                          γ,
                                          "revm_primitives::env::CreateScheme::Create"
                                        |) in
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "alloy_primitives::bits::address::Address",
                                            "create",
                                            []
                                          |),
                                          [
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| inputs |),
                                              "revm_interpreter::interpreter_action::create_inputs::CreateInputs",
                                              "caller"
                                            |);
                                            M.read (| old_nonce |)
                                          ]
                                        |)
                                      |)));
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ0_0 :=
                                        M.SubPointer.get_struct_record_field (|
                                          γ,
                                          "revm_primitives::env::CreateScheme::Create2",
                                          "salt"
                                        |) in
                                      let salt := M.copy (| γ0_0 |) in
                                      let~ _ :=
                                        M.write (|
                                          init_code_hash,
                                          M.call_closure (|
                                            M.get_function (|
                                              "alloy_primitives::utils::keccak256",
                                              [
                                                Ty.apply
                                                  (Ty.path "&")
                                                  []
                                                  [ Ty.path "alloy_primitives::bytes_::Bytes" ]
                                              ]
                                            |),
                                            [
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| inputs |),
                                                "revm_interpreter::interpreter_action::create_inputs::CreateInputs",
                                                "init_code"
                                              |)
                                            ]
                                          |)
                                        |) in
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "alloy_primitives::bits::address::Address",
                                            "create2",
                                            [
                                              Ty.apply
                                                (Ty.path "array")
                                                [ Value.Integer IntegerKind.Usize 32 ]
                                                [ Ty.path "u8" ];
                                              Ty.apply
                                                (Ty.path
                                                  "alloy_primitives::bits::fixed::FixedBytes")
                                                [ Value.Integer IntegerKind.Usize 32 ]
                                                []
                                            ]
                                          |),
                                          [
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| inputs |),
                                              "revm_interpreter::interpreter_action::create_inputs::CreateInputs",
                                              "caller"
                                            |);
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply
                                                  (Ty.path "ruint::Uint")
                                                  [
                                                    Value.Integer IntegerKind.Usize 256;
                                                    Value.Integer IntegerKind.Usize 4
                                                  ]
                                                  [],
                                                "to_be_bytes",
                                                []
                                              |),
                                              [ salt ]
                                            |);
                                            M.read (| init_code_hash |)
                                          ]
                                        |)
                                      |)))
                                ]
                              |)
                            |) 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.path "revm::journaled_state::JournaledState",
                                        "load_account",
                                        [ DB ]
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "revm::context::inner_evm_context::InnerEvmContext",
                                          "journaled_state"
                                        |);
                                        M.read (| created_address |);
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "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~ checkpoint :=
                            M.copy (|
                              M.match_operator (|
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "revm::journaled_state::JournaledState",
                                      "create_account_checkpoint",
                                      []
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| self |),
                                        "revm::context::inner_evm_context::InnerEvmContext",
                                        "journaled_state"
                                      |);
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| inputs |),
                                          "revm_interpreter::interpreter_action::create_inputs::CreateInputs",
                                          "caller"
                                        |)
                                      |);
                                      M.read (| created_address |);
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| inputs |),
                                          "revm_interpreter::interpreter_action::create_inputs::CreateInputs",
                                          "value"
                                        |)
                                      |);
                                      M.read (| spec_id |)
                                    ]
                                  |)
                                |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ0_0 :=
                                        M.SubPointer.get_struct_tuple_field (|
                                          γ,
                                          "core::result::Result::Ok",
                                          0
                                        |) in
                                      let checkpoint := M.copy (| γ0_0 |) in
                                      checkpoint));
                                  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
                                      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_error; Value.Tuple [ M.read (| e |) ] ]
                                              |)
                                            |)
                                          |)
                                        |)
                                      |)))
                                ]
                              |)
                            |) in
                          let~ bytecode :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "revm_primitives::bytecode::Bytecode",
                                  "new_raw",
                                  []
                                |),
                                [
                                  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::create_inputs::CreateInputs",
                                        "init_code"
                                      |)
                                    ]
                                  |)
                                ]
                              |)
                            |) in
                          let~ contract :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "revm_interpreter::interpreter::contract::Contract",
                                  "new",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "alloy_primitives::bytes_::Bytes",
                                      "new",
                                      []
                                    |),
                                    []
                                  |);
                                  M.read (| bytecode |);
                                  Value.StructTuple
                                    "core::option::Option::Some"
                                    [ M.read (| init_code_hash |) ];
                                  M.read (| created_address |);
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| inputs |),
                                      "revm_interpreter::interpreter_action::create_inputs::CreateInputs",
                                      "caller"
                                    |)
                                  |);
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| inputs |),
                                      "revm_interpreter::interpreter_action::create_inputs::CreateInputs",
                                      "value"
                                    |)
                                  |)
                                ]
                              |)
                            |) in
                          M.alloc (|
                            Value.StructTuple
                              "core::result::Result::Ok"
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "revm::frame::FrameOrResult",
                                    "new_create_frame",
                                    []
                                  |),
                                  [
                                    M.read (| created_address |);
                                    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 ]
                                        |);
                                        Value.Bool false
                                      ]
                                    |)
                                  ]
                                |)
                              ]
                          |)))
                    ]
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_make_create_frame :
        forall (DB : Ty.t),
        M.IsAssociatedFunction (Self DB) "make_create_frame" (make_create_frame DB).
      
      (*
          pub fn call_return(
              &mut self,
              interpreter_result: &InterpreterResult,
              journal_checkpoint: JournalCheckpoint,
          ) {
              // revert changes or not.
              if matches!(interpreter_result.result, return_ok!()) {
                  self.journaled_state.checkpoint_commit();
              } else {
                  self.journaled_state.checkpoint_revert(journal_checkpoint);
              }
          }
      *)
      Definition call_return
          (DB : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self DB in
        match ε, τ, α with
        | [], [], [ self; interpreter_result; journal_checkpoint ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let interpreter_result := M.alloc (| interpreter_result |) in
            let journal_checkpoint := M.alloc (| journal_checkpoint |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.match_operator (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| interpreter_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.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.read (| self |),
                                "revm::context::inner_evm_context::InnerEvmContext",
                                "journaled_state"
                              |);
                              M.read (| journal_checkpoint |)
                            ]
                          |)
                        |) in
                      M.alloc (| Value.Tuple [] |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_call_return :
        forall (DB : Ty.t),
        M.IsAssociatedFunction (Self DB) "call_return" (call_return DB).
      
      (*
          pub fn create_return<SPEC: Spec>(
              &mut self,
              interpreter_result: &mut InterpreterResult,
              address: Address,
              journal_checkpoint: JournalCheckpoint,
          ) {
              // if return is not ok revert and return.
              if !matches!(interpreter_result.result, return_ok!()) {
                  self.journaled_state.checkpoint_revert(journal_checkpoint);
                  return;
              }
              // Host error if present on execution
              // if ok, check contract creation limit and calculate gas deduction on output len.
              //
              // EIP-3541: Reject new contract code starting with the 0xEF byte
              if SPEC::enabled(LONDON)
                  && !interpreter_result.output.is_empty()
                  && interpreter_result.output.first() == Some(&0xEF)
              {
                  self.journaled_state.checkpoint_revert(journal_checkpoint);
                  interpreter_result.result = InstructionResult::CreateContractStartingWithEF;
                  return;
              }
      
              // EIP-170: Contract code size limit
              // By default limit is 0x6000 (~25kb)
              if SPEC::enabled(SPURIOUS_DRAGON)
                  && interpreter_result.output.len()
                      > self
                          .env
                          .cfg
                          .limit_contract_code_size
                          .unwrap_or(MAX_CODE_SIZE)
              {
                  self.journaled_state.checkpoint_revert(journal_checkpoint);
                  interpreter_result.result = InstructionResult::CreateContractSizeLimit;
                  return;
              }
              let gas_for_code = interpreter_result.output.len() as u64 * gas::CODEDEPOSIT;
              if !interpreter_result.gas.record_cost(gas_for_code) {
                  // record code deposit gas cost and check if we are out of gas.
                  // EIP-2 point 3: If contract creation does not have enough gas to pay for the
                  // final gas fee for adding the contract code to the state, the contract
                  //  creation fails (i.e. goes out-of-gas) rather than leaving an empty contract.
                  if SPEC::enabled(HOMESTEAD) {
                      self.journaled_state.checkpoint_revert(journal_checkpoint);
                      interpreter_result.result = InstructionResult::OutOfGas;
                      return;
                  } else {
                      interpreter_result.output = Bytes::new();
                  }
              }
              // if we have enough gas we can commit changes.
              self.journaled_state.checkpoint_commit();
      
              // Do analysis of bytecode straight away.
              let bytecode = match self.env.cfg.perf_analyse_created_bytecodes {
                  AnalysisKind::Raw => Bytecode::new_raw(interpreter_result.output.clone()),
                  AnalysisKind::Analyse => {
                      to_analysed(Bytecode::new_raw(interpreter_result.output.clone()))
                  }
              };
      
              // set code
              self.journaled_state.set_code(address, bytecode);
      
              interpreter_result.result = InstructionResult::Return;
          }
      *)
      Definition create_return
          (DB : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self DB in
        match ε, τ, α with
        | [], [ SPEC ], [ self; interpreter_result; address; journal_checkpoint ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let interpreter_result := M.alloc (| interpreter_result |) in
            let address := M.alloc (| address |) in
            let journal_checkpoint := M.alloc (| journal_checkpoint |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  UnOp.not (|
                                    M.read (|
                                      M.match_operator (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| interpreter_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
                            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.read (| self |),
                                            "revm::context::inner_evm_context::InnerEvmContext",
                                            "journaled_state"
                                          |);
                                          M.read (| journal_checkpoint |)
                                        ]
                                      |)
                                    |) in
                                  M.return_ (| Value.Tuple [] |)
                                |)
                              |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  LogicalOp.and (|
                                    LogicalOp.and (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "revm_primitives::specification::Spec",
                                          SPEC,
                                          [],
                                          "enabled",
                                          []
                                        |),
                                        [
                                          Value.StructTuple
                                            "revm_primitives::specification::SpecId::LONDON"
                                            []
                                        ]
                                      |),
                                      ltac:(M.monadic
                                        (UnOp.not (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "bytes::bytes::Bytes",
                                              "is_empty",
                                              []
                                            |),
                                            [
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::ops::deref::Deref",
                                                  Ty.path "alloy_primitives::bytes_::Bytes",
                                                  [],
                                                  "deref",
                                                  []
                                                |),
                                                [
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.read (| interpreter_result |),
                                                    "revm_interpreter::interpreter::InterpreterResult",
                                                    "output"
                                                  |)
                                                ]
                                              |)
                                            ]
                                          |)
                                        |)))
                                    |),
                                    ltac:(M.monadic
                                      (M.call_closure (|
                                        M.get_trait_method (|
                                          "core::cmp::PartialEq",
                                          Ty.apply
                                            (Ty.path "core::option::Option")
                                            []
                                            [ Ty.apply (Ty.path "&") [] [ Ty.path "u8" ] ],
                                          [
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [ Ty.apply (Ty.path "&") [] [ Ty.path "u8" ] ]
                                          ],
                                          "eq",
                                          []
                                        |),
                                        [
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                                "first",
                                                []
                                              |),
                                              [
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::ops::deref::Deref",
                                                    Ty.path "bytes::bytes::Bytes",
                                                    [],
                                                    "deref",
                                                    []
                                                  |),
                                                  [
                                                    M.call_closure (|
                                                      M.get_trait_method (|
                                                        "core::ops::deref::Deref",
                                                        Ty.path "alloy_primitives::bytes_::Bytes",
                                                        [],
                                                        "deref",
                                                        []
                                                      |),
                                                      [
                                                        M.SubPointer.get_struct_record_field (|
                                                          M.read (| interpreter_result |),
                                                          "revm_interpreter::interpreter::InterpreterResult",
                                                          "output"
                                                        |)
                                                      ]
                                                    |)
                                                  ]
                                                |)
                                              ]
                                            |)
                                          |);
                                          M.alloc (|
                                            Value.StructTuple
                                              "core::option::Option::Some"
                                              [ M.alloc (| Value.Integer IntegerKind.U8 239 |) ]
                                          |)
                                        ]
                                      |)))
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) 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.read (| self |),
                                            "revm::context::inner_evm_context::InnerEvmContext",
                                            "journaled_state"
                                          |);
                                          M.read (| journal_checkpoint |)
                                        ]
                                      |)
                                    |) in
                                  let~ _ :=
                                    M.write (|
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| interpreter_result |),
                                        "revm_interpreter::interpreter::InterpreterResult",
                                        "result"
                                      |),
                                      Value.StructTuple
                                        "revm_interpreter::instruction_result::InstructionResult::CreateContractStartingWithEF"
                                        []
                                    |) in
                                  M.return_ (| Value.Tuple [] |)
                                |)
                              |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  LogicalOp.and (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "revm_primitives::specification::Spec",
                                        SPEC,
                                        [],
                                        "enabled",
                                        []
                                      |),
                                      [
                                        Value.StructTuple
                                          "revm_primitives::specification::SpecId::SPURIOUS_DRAGON"
                                          []
                                      ]
                                    |),
                                    ltac:(M.monadic
                                      (BinOp.gt (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "bytes::bytes::Bytes",
                                            "len",
                                            []
                                          |),
                                          [
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::ops::deref::Deref",
                                                Ty.path "alloy_primitives::bytes_::Bytes",
                                                [],
                                                "deref",
                                                []
                                              |),
                                              [
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| interpreter_result |),
                                                  "revm_interpreter::interpreter::InterpreterResult",
                                                  "output"
                                                |)
                                              ]
                                            |)
                                          ]
                                        |),
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [ Ty.path "usize" ],
                                            "unwrap_or",
                                            []
                                          |),
                                          [
                                            M.read (|
                                              M.SubPointer.get_struct_record_field (|
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (|
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| self |),
                                                      "revm::context::inner_evm_context::InnerEvmContext",
                                                      "env"
                                                    |)
                                                  |),
                                                  "revm_primitives::env::Env",
                                                  "cfg"
                                                |),
                                                "revm_primitives::env::CfgEnv",
                                                "limit_contract_code_size"
                                              |)
                                            |);
                                            M.read (|
                                              M.get_constant (|
                                                "revm_primitives::constants::MAX_CODE_SIZE"
                                              |)
                                            |)
                                          ]
                                        |)
                                      |)))
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) 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.read (| self |),
                                            "revm::context::inner_evm_context::InnerEvmContext",
                                            "journaled_state"
                                          |);
                                          M.read (| journal_checkpoint |)
                                        ]
                                      |)
                                    |) in
                                  let~ _ :=
                                    M.write (|
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| interpreter_result |),
                                        "revm_interpreter::interpreter::InterpreterResult",
                                        "result"
                                      |),
                                      Value.StructTuple
                                        "revm_interpreter::instruction_result::InstructionResult::CreateContractSizeLimit"
                                        []
                                    |) in
                                  M.return_ (| Value.Tuple [] |)
                                |)
                              |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  let~ gas_for_code :=
                    M.alloc (|
                      BinOp.Wrap.mul (|
                        M.rust_cast
                          (M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "bytes::bytes::Bytes",
                              "len",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::ops::deref::Deref",
                                  Ty.path "alloy_primitives::bytes_::Bytes",
                                  [],
                                  "deref",
                                  []
                                |),
                                [
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| interpreter_result |),
                                    "revm_interpreter::interpreter::InterpreterResult",
                                    "output"
                                  |)
                                ]
                              |)
                            ]
                          |)),
                        M.read (|
                          M.get_constant (| "revm_interpreter::gas::constants::CODEDEPOSIT" |)
                        |)
                      |)
                    |) in
                  let~ _ :=
                    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_interpreter::gas::Gas",
                                        "record_cost",
                                        []
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| interpreter_result |),
                                          "revm_interpreter::interpreter::InterpreterResult",
                                          "gas"
                                        |);
                                        M.read (| gas_for_code |)
                                      ]
                                    |)
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "revm_primitives::specification::Spec",
                                              SPEC,
                                              [],
                                              "enabled",
                                              []
                                            |),
                                            [
                                              Value.StructTuple
                                                "revm_primitives::specification::SpecId::HOMESTEAD"
                                                []
                                            ]
                                          |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) 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.read (| self |),
                                                    "revm::context::inner_evm_context::InnerEvmContext",
                                                    "journaled_state"
                                                  |);
                                                  M.read (| journal_checkpoint |)
                                                ]
                                              |)
                                            |) in
                                          let~ _ :=
                                            M.write (|
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| interpreter_result |),
                                                "revm_interpreter::interpreter::InterpreterResult",
                                                "result"
                                              |),
                                              Value.StructTuple
                                                "revm_interpreter::instruction_result::InstructionResult::OutOfGas"
                                                []
                                            |) in
                                          M.return_ (| Value.Tuple [] |)
                                        |)
                                      |)
                                    |)));
                                fun γ =>
                                  ltac:(M.monadic
                                    (let~ _ :=
                                      M.write (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| interpreter_result |),
                                          "revm_interpreter::interpreter::InterpreterResult",
                                          "output"
                                        |),
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "alloy_primitives::bytes_::Bytes",
                                            "new",
                                            []
                                          |),
                                          []
                                        |)
                                      |) in
                                    M.alloc (| Value.Tuple [] |)))
                              ]
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "revm::journaled_state::JournaledState",
                          "checkpoint_commit",
                          []
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "revm::context::inner_evm_context::InnerEvmContext",
                            "journaled_state"
                          |)
                        ]
                      |)
                    |) in
                  let~ bytecode :=
                    M.copy (|
                      M.match_operator (|
                        M.SubPointer.get_struct_record_field (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (|
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "revm::context::inner_evm_context::InnerEvmContext",
                                "env"
                              |)
                            |),
                            "revm_primitives::env::Env",
                            "cfg"
                          |),
                          "revm_primitives::env::CfgEnv",
                          "perf_analyse_created_bytecodes"
                        |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let _ :=
                                M.is_struct_tuple (|
                                  γ,
                                  "revm_primitives::env::AnalysisKind::Raw"
                                |) in
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "revm_primitives::bytecode::Bytecode",
                                    "new_raw",
                                    []
                                  |),
                                  [
                                    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 (| interpreter_result |),
                                          "revm_interpreter::interpreter::InterpreterResult",
                                          "output"
                                        |)
                                      ]
                                    |)
                                  ]
                                |)
                              |)));
                          fun γ =>
                            ltac:(M.monadic
                              (let _ :=
                                M.is_struct_tuple (|
                                  γ,
                                  "revm_primitives::env::AnalysisKind::Analyse"
                                |) in
                              M.alloc (|
                                M.call_closure (|
                                  M.get_function (|
                                    "revm_interpreter::interpreter::analysis::to_analysed",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "revm_primitives::bytecode::Bytecode",
                                        "new_raw",
                                        []
                                      |),
                                      [
                                        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 (| interpreter_result |),
                                              "revm_interpreter::interpreter::InterpreterResult",
                                              "output"
                                            |)
                                          ]
                                        |)
                                      ]
                                    |)
                                  ]
                                |)
                              |)))
                        ]
                      |)
                    |) in
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "revm::journaled_state::JournaledState",
                          "set_code",
                          []
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "revm::context::inner_evm_context::InnerEvmContext",
                            "journaled_state"
                          |);
                          M.read (| address |);
                          M.read (| bytecode |)
                        ]
                      |)
                    |) in
                  let~ _ :=
                    M.write (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| interpreter_result |),
                        "revm_interpreter::interpreter::InterpreterResult",
                        "result"
                      |),
                      Value.StructTuple
                        "revm_interpreter::instruction_result::InstructionResult::Return"
                        []
                    |) in
                  M.alloc (| Value.Tuple [] |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_create_return :
        forall (DB : Ty.t),
        M.IsAssociatedFunction (Self DB) "create_return" (create_return DB).
    End Impl_revm_context_inner_evm_context_InnerEvmContext_DB.
  End inner_evm_context.
End context.
