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

Module handler.
  Module handle_types.
    Module pre_execution.
      Axiom LoadPrecompilesHandle :
        forall (DB : Ty.t),
        (Ty.apply
            (Ty.path "revm::handler::handle_types::pre_execution::LoadPrecompilesHandle")
            []
            [ DB ]) =
          (Ty.apply
            (Ty.path "alloc::sync::Arc")
            []
            [ Ty.dyn [ ("core::ops::function::Fn::Trait", []) ]; Ty.path "alloc::alloc::Global" ]).
      
      Axiom LoadAccountsHandle :
        forall (EXT DB : Ty.t),
        (Ty.apply
            (Ty.path "revm::handler::handle_types::pre_execution::LoadAccountsHandle")
            []
            [ EXT; DB ]) =
          (Ty.apply
            (Ty.path "alloc::sync::Arc")
            []
            [
              Ty.dyn
                [
                  ("existential predicate with variables", []);
                  ("existential predicate with variables", [])
                ];
              Ty.path "alloc::alloc::Global"
            ]).
      
      Axiom DeductCallerHandle :
        forall (EXT DB : Ty.t),
        (Ty.apply
            (Ty.path "revm::handler::handle_types::pre_execution::DeductCallerHandle")
            []
            [ EXT; DB ]) =
          (Ty.apply
            (Ty.path "alloc::sync::Arc")
            []
            [
              Ty.dyn
                [
                  ("existential predicate with variables", []);
                  ("existential predicate with variables", [])
                ];
              Ty.path "alloc::alloc::Global"
            ]).
      
      (* StructRecord
        {
          name := "PreExecutionHandler";
          const_params := [];
          ty_params := [ "EXT"; "DB" ];
          fields :=
            [
              ("load_precompiles",
                Ty.apply
                  (Ty.path "alloc::sync::Arc")
                  []
                  [
                    Ty.dyn [ ("core::ops::function::Fn::Trait", []) ];
                    Ty.path "alloc::alloc::Global"
                  ]);
              ("load_accounts",
                Ty.apply
                  (Ty.path "alloc::sync::Arc")
                  []
                  [
                    Ty.dyn
                      [
                        ("existential predicate with variables", []);
                        ("existential predicate with variables", [])
                      ];
                    Ty.path "alloc::alloc::Global"
                  ]);
              ("deduct_caller",
                Ty.apply
                  (Ty.path "alloc::sync::Arc")
                  []
                  [
                    Ty.dyn
                      [
                        ("existential predicate with variables", []);
                        ("existential predicate with variables", [])
                      ];
                    Ty.path "alloc::alloc::Global"
                  ])
            ];
        } *)
      
      Module Impl_revm_handler_handle_types_pre_execution_PreExecutionHandler_EXT_DB.
        Definition Self (EXT DB : Ty.t) : Ty.t :=
          Ty.apply
            (Ty.path "revm::handler::handle_types::pre_execution::PreExecutionHandler")
            []
            [ EXT; DB ].
        
        (*
            pub fn new<SPEC: Spec + 'a>() -> Self {
                Self {
                    load_precompiles: Arc::new(mainnet::load_precompiles::<SPEC, DB>),
                    load_accounts: Arc::new(mainnet::load_accounts::<SPEC, EXT, DB>),
                    deduct_caller: Arc::new(mainnet::deduct_caller::<SPEC, EXT, DB>),
                }
            }
        *)
        Definition new (EXT DB : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self EXT DB in
          match ε, τ, α with
          | [], [ SPEC ], [] =>
            ltac:(M.monadic
              (Value.StructRecord
                "revm::handler::handle_types::pre_execution::PreExecutionHandler"
                [
                  ("load_precompiles",
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::sync::Arc")
                          []
                          [
                            Ty.function
                              []
                              (Ty.apply
                                (Ty.path "revm::context::context_precompiles::ContextPrecompiles")
                                []
                                [ DB ]);
                            Ty.path "alloc::alloc::Global"
                          ],
                        "new",
                        []
                      |),
                      [
                        M.get_function (|
                          "revm::handler::mainnet::pre_execution::load_precompiles",
                          [ SPEC; DB ]
                        |)
                      ]
                    |));
                  ("load_accounts",
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::sync::Arc")
                          []
                          [
                            Ty.function
                              [
                                Ty.apply
                                  (Ty.path "&mut")
                                  []
                                  [ Ty.apply (Ty.path "revm::context::Context") [] [ EXT; DB ] ]
                              ]
                              (Ty.apply
                                (Ty.path "core::result::Result")
                                []
                                [
                                  Ty.tuple [];
                                  Ty.apply
                                    (Ty.path "revm_primitives::result::EVMError")
                                    []
                                    [ Ty.associated ]
                                ]);
                            Ty.path "alloc::alloc::Global"
                          ],
                        "new",
                        []
                      |),
                      [
                        M.get_function (|
                          "revm::handler::mainnet::pre_execution::load_accounts",
                          [ SPEC; EXT; DB ]
                        |)
                      ]
                    |));
                  ("deduct_caller",
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::sync::Arc")
                          []
                          [
                            Ty.function
                              [
                                Ty.apply
                                  (Ty.path "&mut")
                                  []
                                  [ Ty.apply (Ty.path "revm::context::Context") [] [ EXT; DB ] ]
                              ]
                              (Ty.apply
                                (Ty.path "core::result::Result")
                                []
                                [
                                  Ty.tuple [];
                                  Ty.apply
                                    (Ty.path "revm_primitives::result::EVMError")
                                    []
                                    [ Ty.associated ]
                                ]);
                            Ty.path "alloc::alloc::Global"
                          ],
                        "new",
                        []
                      |),
                      [
                        M.get_function (|
                          "revm::handler::mainnet::pre_execution::deduct_caller",
                          [ SPEC; EXT; DB ]
                        |)
                      ]
                    |))
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_new :
          forall (EXT DB : Ty.t),
          M.IsAssociatedFunction (Self EXT DB) "new" (new EXT DB).
        (*
            pub fn deduct_caller(&self, context: &mut Context<EXT, DB>) -> Result<(), EVMError<DB::Error>> {
                (self.deduct_caller)(context)
            }
        *)
        Definition deduct_caller
            (EXT DB : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self EXT DB in
          match ε, τ, α with
          | [], [], [ self; context ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let context := M.alloc (| context |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::function::Fn",
                  Ty.dyn
                    [
                      ("existential predicate with variables", []);
                      ("existential predicate with variables", [])
                    ],
                  [
                    Ty.tuple
                      [
                        Ty.apply
                          (Ty.path "&mut")
                          []
                          [ Ty.apply (Ty.path "revm::context::Context") [] [ EXT; DB ] ]
                      ]
                  ],
                  "call",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::deref::Deref",
                      Ty.apply
                        (Ty.path "alloc::sync::Arc")
                        []
                        [
                          Ty.dyn
                            [
                              ("existential predicate with variables", []);
                              ("existential predicate with variables", [])
                            ];
                          Ty.path "alloc::alloc::Global"
                        ],
                      [],
                      "deref",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm::handler::handle_types::pre_execution::PreExecutionHandler",
                        "deduct_caller"
                      |)
                    ]
                  |);
                  Value.Tuple [ M.read (| context |) ]
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_deduct_caller :
          forall (EXT DB : Ty.t),
          M.IsAssociatedFunction (Self EXT DB) "deduct_caller" (deduct_caller EXT DB).
        
        (*
            pub fn load_accounts(&self, context: &mut Context<EXT, DB>) -> Result<(), EVMError<DB::Error>> {
                (self.load_accounts)(context)
            }
        *)
        Definition load_accounts
            (EXT DB : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self EXT DB in
          match ε, τ, α with
          | [], [], [ self; context ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let context := M.alloc (| context |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::function::Fn",
                  Ty.dyn
                    [
                      ("existential predicate with variables", []);
                      ("existential predicate with variables", [])
                    ],
                  [
                    Ty.tuple
                      [
                        Ty.apply
                          (Ty.path "&mut")
                          []
                          [ Ty.apply (Ty.path "revm::context::Context") [] [ EXT; DB ] ]
                      ]
                  ],
                  "call",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::deref::Deref",
                      Ty.apply
                        (Ty.path "alloc::sync::Arc")
                        []
                        [
                          Ty.dyn
                            [
                              ("existential predicate with variables", []);
                              ("existential predicate with variables", [])
                            ];
                          Ty.path "alloc::alloc::Global"
                        ],
                      [],
                      "deref",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm::handler::handle_types::pre_execution::PreExecutionHandler",
                        "load_accounts"
                      |)
                    ]
                  |);
                  Value.Tuple [ M.read (| context |) ]
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_load_accounts :
          forall (EXT DB : Ty.t),
          M.IsAssociatedFunction (Self EXT DB) "load_accounts" (load_accounts EXT DB).
        
        (*
            pub fn load_precompiles(&self) -> ContextPrecompiles<DB> {
                (self.load_precompiles)()
            }
        *)
        Definition load_precompiles
            (EXT DB : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self EXT DB in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::function::Fn",
                  Ty.dyn [ ("core::ops::function::Fn::Trait", []) ],
                  [ Ty.tuple [] ],
                  "call",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::deref::Deref",
                      Ty.apply
                        (Ty.path "alloc::sync::Arc")
                        []
                        [
                          Ty.dyn [ ("core::ops::function::Fn::Trait", []) ];
                          Ty.path "alloc::alloc::Global"
                        ],
                      [],
                      "deref",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm::handler::handle_types::pre_execution::PreExecutionHandler",
                        "load_precompiles"
                      |)
                    ]
                  |);
                  Value.Tuple []
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_load_precompiles :
          forall (EXT DB : Ty.t),
          M.IsAssociatedFunction (Self EXT DB) "load_precompiles" (load_precompiles EXT DB).
      End Impl_revm_handler_handle_types_pre_execution_PreExecutionHandler_EXT_DB.
      
    End pre_execution.
  End handle_types.
End handler.
