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

Module handler.
  (* StructRecord
    {
      name := "Handler";
      const_params := [];
      ty_params := [ "H"; "EXT"; "DB" ];
      fields :=
        [
          ("cfg", Ty.path "revm_primitives::env::handler_cfg::HandlerCfg");
          ("instruction_table",
            Ty.apply
              (Ty.path "core::option::Option")
              []
              [ Ty.apply (Ty.path "revm_interpreter::opcode::InstructionTables") [] [ H ] ]);
          ("registers",
            Ty.apply
              (Ty.path "alloc::vec::Vec")
              []
              [
                Ty.apply (Ty.path "revm::handler::register::HandleRegisters") [] [ EXT; DB ];
                Ty.path "alloc::alloc::Global"
              ]);
          ("validation",
            Ty.apply
              (Ty.path "revm::handler::handle_types::validation::ValidationHandler")
              []
              [ EXT; DB ]);
          ("pre_execution",
            Ty.apply
              (Ty.path "revm::handler::handle_types::pre_execution::PreExecutionHandler")
              []
              [ EXT; DB ]);
          ("post_execution",
            Ty.apply
              (Ty.path "revm::handler::handle_types::post_execution::PostExecutionHandler")
              []
              [ EXT; DB ]);
          ("execution",
            Ty.apply
              (Ty.path "revm::handler::handle_types::execution::ExecutionHandler")
              []
              [ EXT; DB ])
        ];
    } *)
  
  Module Impl_revm_handler_Handler_revm_evm_Evm_EXT_DB_EXT_DB.
    Definition Self (EXT DB : Ty.t) : Ty.t :=
      Ty.apply
        (Ty.path "revm::handler::Handler")
        []
        [ Ty.apply (Ty.path "revm::evm::Evm") [] [ EXT; DB ]; EXT; DB ].
    
    (*
        pub fn new(cfg: HandlerCfg) -> Self {
            cfg_if::cfg_if! {
                if #[cfg(feature = "optimism")] {
                    if cfg.is_optimism {
                        Handler::optimism_with_spec(cfg.spec_id)
                    } else {
                        Handler::mainnet_with_spec(cfg.spec_id)
                    }
                } else {
                    Handler::mainnet_with_spec(cfg.spec_id)
                }
            }
        }
    *)
    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
      | [], [], [ cfg ] =>
        ltac:(M.monadic
          (let cfg := M.alloc (| cfg |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply
                (Ty.path "revm::handler::Handler")
                []
                [ Ty.apply (Ty.path "revm::evm::Evm") [] [ EXT; DB ]; EXT; DB ],
              "mainnet_with_spec",
              []
            |),
            [
              M.read (|
                M.SubPointer.get_struct_record_field (|
                  cfg,
                  "revm_primitives::env::handler_cfg::HandlerCfg",
                  "spec_id"
                |)
              |)
            ]
          |)))
      | _, _, _ => 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 mainnet<SPEC: Spec>() -> Self {
            Self {
                cfg: HandlerCfg::new(SPEC::SPEC_ID),
                instruction_table: Some(InstructionTables::new_plain::<SPEC>()),
                registers: Vec::new(),
                validation: ValidationHandler::new::<SPEC>(),
                pre_execution: PreExecutionHandler::new::<SPEC>(),
                post_execution: PostExecutionHandler::new::<SPEC>(),
                execution: ExecutionHandler::new::<SPEC>(),
            }
        }
    *)
    Definition mainnet (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::Handler"
            [
              ("cfg",
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "revm_primitives::env::handler_cfg::HandlerCfg",
                    "new",
                    []
                  |),
                  [
                    M.read (|
                      M.get_constant (| "revm_primitives::specification::Spec::SPEC_ID" |)
                    |)
                  ]
                |));
              ("instruction_table",
                Value.StructTuple
                  "core::option::Option::Some"
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "revm_interpreter::opcode::InstructionTables")
                          []
                          [ Ty.apply (Ty.path "revm::evm::Evm") [] [ EXT; DB ] ],
                        "new_plain",
                        [ SPEC ]
                      |),
                      []
                    |)
                  ]);
              ("registers",
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [
                        Ty.apply
                          (Ty.path "revm::handler::register::HandleRegisters")
                          []
                          [ EXT; DB ];
                        Ty.path "alloc::alloc::Global"
                      ],
                    "new",
                    []
                  |),
                  []
                |));
              ("validation",
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "revm::handler::handle_types::validation::ValidationHandler")
                      []
                      [ EXT; DB ],
                    "new",
                    [ SPEC ]
                  |),
                  []
                |));
              ("pre_execution",
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "revm::handler::handle_types::pre_execution::PreExecutionHandler")
                      []
                      [ EXT; DB ],
                    "new",
                    [ SPEC ]
                  |),
                  []
                |));
              ("post_execution",
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "revm::handler::handle_types::post_execution::PostExecutionHandler")
                      []
                      [ EXT; DB ],
                    "new",
                    [ SPEC ]
                  |),
                  []
                |));
              ("execution",
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "revm::handler::handle_types::execution::ExecutionHandler")
                      []
                      [ EXT; DB ],
                    "new",
                    [ SPEC ]
                  |),
                  []
                |))
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_mainnet :
      forall (EXT DB : Ty.t),
      M.IsAssociatedFunction (Self EXT DB) "mainnet" (mainnet EXT DB).
    
    (*
        pub fn is_optimism(&self) -> bool {
            self.cfg.is_optimism()
        }
    *)
    Definition is_optimism
        (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_associated_function (|
              Ty.path "revm_primitives::env::handler_cfg::HandlerCfg",
              "is_optimism",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "revm::handler::Handler",
                "cfg"
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_optimism :
      forall (EXT DB : Ty.t),
      M.IsAssociatedFunction (Self EXT DB) "is_optimism" (is_optimism EXT DB).
    
    (*
        pub fn mainnet_with_spec(spec_id: SpecId) -> Self {
            spec_to_generic!(spec_id, Self::mainnet::<SPEC>())
        }
    *)
    Definition mainnet_with_spec
        (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_id ] =>
        ltac:(M.monadic
          (let spec_id := M.alloc (| spec_id |) in
          M.read (|
            M.match_operator (|
              spec_id,
              [
                fun γ =>
                  ltac:(M.monadic
                    (M.find_or_pattern (|
                      γ,
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_primitives::specification::SpecId::FRONTIER"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_primitives::specification::SpecId::FRONTIER_THAWING"
                              |) in
                            Value.Tuple []))
                      ],
                      M.closure
                        (fun γ =>
                          ltac:(M.monadic
                            match γ with
                            | [] =>
                              ltac:(M.monadic
                                (M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "revm::handler::Handler")
                                        []
                                        [
                                          Ty.apply (Ty.path "revm::evm::Evm") [] [ EXT; DB ];
                                          EXT;
                                          DB
                                        ],
                                      "mainnet",
                                      [ Ty.path "revm_primitives::specification::FrontierSpec" ]
                                    |),
                                    []
                                  |)
                                |)))
                            | _ => M.impossible "wrong number of arguments"
                            end))
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (M.find_or_pattern (|
                      γ,
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_primitives::specification::SpecId::HOMESTEAD"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_primitives::specification::SpecId::DAO_FORK"
                              |) in
                            Value.Tuple []))
                      ],
                      M.closure
                        (fun γ =>
                          ltac:(M.monadic
                            match γ with
                            | [] =>
                              ltac:(M.monadic
                                (M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "revm::handler::Handler")
                                        []
                                        [
                                          Ty.apply (Ty.path "revm::evm::Evm") [] [ EXT; DB ];
                                          EXT;
                                          DB
                                        ],
                                      "mainnet",
                                      [ Ty.path "revm_primitives::specification::HomesteadSpec" ]
                                    |),
                                    []
                                  |)
                                |)))
                            | _ => M.impossible "wrong number of arguments"
                            end))
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::specification::SpecId::TANGERINE"
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "revm::handler::Handler")
                            []
                            [ Ty.apply (Ty.path "revm::evm::Evm") [] [ EXT; DB ]; EXT; DB ],
                          "mainnet",
                          [ Ty.path "revm_primitives::specification::TangerineSpec" ]
                        |),
                        []
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::specification::SpecId::SPURIOUS_DRAGON"
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "revm::handler::Handler")
                            []
                            [ Ty.apply (Ty.path "revm::evm::Evm") [] [ EXT; DB ]; EXT; DB ],
                          "mainnet",
                          [ Ty.path "revm_primitives::specification::SpuriousDragonSpec" ]
                        |),
                        []
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::specification::SpecId::BYZANTIUM"
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "revm::handler::Handler")
                            []
                            [ Ty.apply (Ty.path "revm::evm::Evm") [] [ EXT; DB ]; EXT; DB ],
                          "mainnet",
                          [ Ty.path "revm_primitives::specification::ByzantiumSpec" ]
                        |),
                        []
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (M.find_or_pattern (|
                      γ,
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_primitives::specification::SpecId::PETERSBURG"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_primitives::specification::SpecId::CONSTANTINOPLE"
                              |) in
                            Value.Tuple []))
                      ],
                      M.closure
                        (fun γ =>
                          ltac:(M.monadic
                            match γ with
                            | [] =>
                              ltac:(M.monadic
                                (M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "revm::handler::Handler")
                                        []
                                        [
                                          Ty.apply (Ty.path "revm::evm::Evm") [] [ EXT; DB ];
                                          EXT;
                                          DB
                                        ],
                                      "mainnet",
                                      [ Ty.path "revm_primitives::specification::PetersburgSpec" ]
                                    |),
                                    []
                                  |)
                                |)))
                            | _ => M.impossible "wrong number of arguments"
                            end))
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (M.find_or_pattern (|
                      γ,
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_primitives::specification::SpecId::ISTANBUL"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_primitives::specification::SpecId::MUIR_GLACIER"
                              |) in
                            Value.Tuple []))
                      ],
                      M.closure
                        (fun γ =>
                          ltac:(M.monadic
                            match γ with
                            | [] =>
                              ltac:(M.monadic
                                (M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "revm::handler::Handler")
                                        []
                                        [
                                          Ty.apply (Ty.path "revm::evm::Evm") [] [ EXT; DB ];
                                          EXT;
                                          DB
                                        ],
                                      "mainnet",
                                      [ Ty.path "revm_primitives::specification::IstanbulSpec" ]
                                    |),
                                    []
                                  |)
                                |)))
                            | _ => M.impossible "wrong number of arguments"
                            end))
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (| γ, "revm_primitives::specification::SpecId::BERLIN" |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "revm::handler::Handler")
                            []
                            [ Ty.apply (Ty.path "revm::evm::Evm") [] [ EXT; DB ]; EXT; DB ],
                          "mainnet",
                          [ Ty.path "revm_primitives::specification::BerlinSpec" ]
                        |),
                        []
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (M.find_or_pattern (|
                      γ,
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_primitives::specification::SpecId::LONDON"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_primitives::specification::SpecId::ARROW_GLACIER"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_primitives::specification::SpecId::GRAY_GLACIER"
                              |) in
                            Value.Tuple []))
                      ],
                      M.closure
                        (fun γ =>
                          ltac:(M.monadic
                            match γ with
                            | [] =>
                              ltac:(M.monadic
                                (M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "revm::handler::Handler")
                                        []
                                        [
                                          Ty.apply (Ty.path "revm::evm::Evm") [] [ EXT; DB ];
                                          EXT;
                                          DB
                                        ],
                                      "mainnet",
                                      [ Ty.path "revm_primitives::specification::LondonSpec" ]
                                    |),
                                    []
                                  |)
                                |)))
                            | _ => M.impossible "wrong number of arguments"
                            end))
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (| γ, "revm_primitives::specification::SpecId::MERGE" |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "revm::handler::Handler")
                            []
                            [ Ty.apply (Ty.path "revm::evm::Evm") [] [ EXT; DB ]; EXT; DB ],
                          "mainnet",
                          [ Ty.path "revm_primitives::specification::MergeSpec" ]
                        |),
                        []
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::specification::SpecId::SHANGHAI"
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "revm::handler::Handler")
                            []
                            [ Ty.apply (Ty.path "revm::evm::Evm") [] [ EXT; DB ]; EXT; DB ],
                          "mainnet",
                          [ Ty.path "revm_primitives::specification::ShanghaiSpec" ]
                        |),
                        []
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (| γ, "revm_primitives::specification::SpecId::CANCUN" |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "revm::handler::Handler")
                            []
                            [ Ty.apply (Ty.path "revm::evm::Evm") [] [ EXT; DB ]; EXT; DB ],
                          "mainnet",
                          [ Ty.path "revm_primitives::specification::CancunSpec" ]
                        |),
                        []
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (| γ, "revm_primitives::specification::SpecId::LATEST" |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "revm::handler::Handler")
                            []
                            [ Ty.apply (Ty.path "revm::evm::Evm") [] [ EXT; DB ]; EXT; DB ],
                          "mainnet",
                          [ Ty.path "revm_primitives::specification::LatestSpec" ]
                        |),
                        []
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (| γ, "revm_primitives::specification::SpecId::PRAGUE" |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "revm::handler::Handler")
                            []
                            [ Ty.apply (Ty.path "revm::evm::Evm") [] [ EXT; DB ]; EXT; DB ],
                          "mainnet",
                          [ Ty.path "revm_primitives::specification::PragueSpec" ]
                        |),
                        []
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_mainnet_with_spec :
      forall (EXT DB : Ty.t),
      M.IsAssociatedFunction (Self EXT DB) "mainnet_with_spec" (mainnet_with_spec EXT DB).
    
    (*
        pub fn cfg(&self) -> HandlerCfg {
            self.cfg
        }
    *)
    Definition cfg (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.read (|
            M.SubPointer.get_struct_record_field (|
              M.read (| self |),
              "revm::handler::Handler",
              "cfg"
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_cfg :
      forall (EXT DB : Ty.t),
      M.IsAssociatedFunction (Self EXT DB) "cfg" (cfg EXT DB).
    
    (*
        pub fn take_instruction_table(&mut self) -> Option<InstructionTables<'a, Evm<'a, EXT, DB>>> {
            self.instruction_table.take()
        }
    *)
    Definition take_instruction_table
        (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_associated_function (|
              Ty.apply
                (Ty.path "core::option::Option")
                []
                [
                  Ty.apply
                    (Ty.path "revm_interpreter::opcode::InstructionTables")
                    []
                    [ Ty.apply (Ty.path "revm::evm::Evm") [] [ EXT; DB ] ]
                ],
              "take",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "revm::handler::Handler",
                "instruction_table"
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_take_instruction_table :
      forall (EXT DB : Ty.t),
      M.IsAssociatedFunction (Self EXT DB) "take_instruction_table" (take_instruction_table EXT DB).
    
    (*
        pub fn set_instruction_table(&mut self, table: InstructionTables<'a, Evm<'a, EXT, DB>>) {
            self.instruction_table = Some(table);
        }
    *)
    Definition set_instruction_table
        (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; table ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let table := M.alloc (| table |) in
          M.read (|
            let~ _ :=
              M.write (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm::handler::Handler",
                  "instruction_table"
                |),
                Value.StructTuple "core::option::Option::Some" [ M.read (| table |) ]
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_set_instruction_table :
      forall (EXT DB : Ty.t),
      M.IsAssociatedFunction (Self EXT DB) "set_instruction_table" (set_instruction_table EXT DB).
    
    (*
        pub fn pre_execution(&self) -> &PreExecutionHandler<'a, EXT, DB> {
            &self.pre_execution
        }
    *)
    Definition pre_execution
        (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.SubPointer.get_struct_record_field (|
            M.read (| self |),
            "revm::handler::Handler",
            "pre_execution"
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_pre_execution :
      forall (EXT DB : Ty.t),
      M.IsAssociatedFunction (Self EXT DB) "pre_execution" (pre_execution EXT DB).
    
    (*
        pub fn post_execution(&self) -> &PostExecutionHandler<'a, EXT, DB> {
            &self.post_execution
        }
    *)
    Definition post_execution
        (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.SubPointer.get_struct_record_field (|
            M.read (| self |),
            "revm::handler::Handler",
            "post_execution"
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_post_execution :
      forall (EXT DB : Ty.t),
      M.IsAssociatedFunction (Self EXT DB) "post_execution" (post_execution EXT DB).
    
    (*
        pub fn execution(&self) -> &ExecutionHandler<'a, EXT, DB> {
            &self.execution
        }
    *)
    Definition execution
        (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.SubPointer.get_struct_record_field (|
            M.read (| self |),
            "revm::handler::Handler",
            "execution"
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_execution :
      forall (EXT DB : Ty.t),
      M.IsAssociatedFunction (Self EXT DB) "execution" (execution EXT DB).
    
    (*
        pub fn validation(&self) -> &ValidationHandler<'a, EXT, DB> {
            &self.validation
        }
    *)
    Definition validation
        (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.SubPointer.get_struct_record_field (|
            M.read (| self |),
            "revm::handler::Handler",
            "validation"
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_validation :
      forall (EXT DB : Ty.t),
      M.IsAssociatedFunction (Self EXT DB) "validation" (validation EXT DB).
    
    (*
        pub fn append_handler_register(&mut self, register: HandleRegisters<EXT, DB>) {
            register.register(self);
            self.registers.push(register);
        }
    *)
    Definition append_handler_register
        (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; register ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let register := M.alloc (| register |) in
          M.read (|
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "revm::handler::register::HandleRegisters") [] [ EXT; DB ],
                    "register",
                    []
                  |),
                  [ register; M.read (| self |) ]
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [
                        Ty.apply
                          (Ty.path "revm::handler::register::HandleRegisters")
                          []
                          [ EXT; DB ];
                        Ty.path "alloc::alloc::Global"
                      ],
                    "push",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm::handler::Handler",
                      "registers"
                    |);
                    M.read (| register |)
                  ]
                |)
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_append_handler_register :
      forall (EXT DB : Ty.t),
      M.IsAssociatedFunction
        (Self EXT DB)
        "append_handler_register"
        (append_handler_register EXT DB).
    
    (*
        pub fn append_handler_register_plain(&mut self, register: HandleRegister<EXT, DB>) {
            register(self);
            self.registers.push(HandleRegisters::Plain(register));
        }
    *)
    Definition append_handler_register_plain
        (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; register ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let register := M.alloc (| register |) in
          M.read (|
            let~ _ :=
              M.alloc (| M.call_closure (| M.read (| register |), [ M.read (| self |) ] |) |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [
                        Ty.apply
                          (Ty.path "revm::handler::register::HandleRegisters")
                          []
                          [ EXT; DB ];
                        Ty.path "alloc::alloc::Global"
                      ],
                    "push",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm::handler::Handler",
                      "registers"
                    |);
                    Value.StructTuple
                      "revm::handler::register::HandleRegisters::Plain"
                      [ M.read (| register |) ]
                  ]
                |)
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_append_handler_register_plain :
      forall (EXT DB : Ty.t),
      M.IsAssociatedFunction
        (Self EXT DB)
        "append_handler_register_plain"
        (append_handler_register_plain EXT DB).
    
    (*
        pub fn append_handler_register_box(&mut self, register: HandleRegisterBox<EXT, DB>) {
            register(self);
            self.registers.push(HandleRegisters::Box(register));
        }
    *)
    Definition append_handler_register_box
        (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; register ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let register := M.alloc (| register |) in
          M.read (|
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::function::Fn",
                    Ty.apply
                      (Ty.path "alloc::boxed::Box")
                      []
                      [
                        Ty.dyn
                          [
                            ("existential predicate with variables", []);
                            ("existential predicate with variables", [])
                          ];
                        Ty.path "alloc::alloc::Global"
                      ],
                    [
                      Ty.tuple
                        [
                          Ty.apply
                            (Ty.path "&mut")
                            []
                            [
                              Ty.apply
                                (Ty.path "revm::handler::Handler")
                                []
                                [ Ty.apply (Ty.path "revm::evm::Evm") [] [ EXT; DB ]; EXT; DB ]
                            ]
                        ]
                    ],
                    "call",
                    []
                  |),
                  [ register; Value.Tuple [ M.read (| self |) ] ]
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [
                        Ty.apply
                          (Ty.path "revm::handler::register::HandleRegisters")
                          []
                          [ EXT; DB ];
                        Ty.path "alloc::alloc::Global"
                      ],
                    "push",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm::handler::Handler",
                      "registers"
                    |);
                    Value.StructTuple
                      "revm::handler::register::HandleRegisters::Box"
                      [ M.read (| register |) ]
                  ]
                |)
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_append_handler_register_box :
      forall (EXT DB : Ty.t),
      M.IsAssociatedFunction
        (Self EXT DB)
        "append_handler_register_box"
        (append_handler_register_box EXT DB).
    
    (*
        pub fn pop_handle_register(&mut self) -> Option<HandleRegisters<EXT, DB>> {
            let out = self.registers.pop();
            if out.is_some() {
                let registers = core::mem::take(&mut self.registers);
                let mut base_handler = Handler::mainnet_with_spec(self.cfg.spec_id);
                // apply all registers to default handeler and raw mainnet instruction table.
                for register in registers {
                    base_handler.append_handler_register(register)
                }
                *self = base_handler;
            }
            out
        }
    *)
    Definition pop_handle_register
        (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.read (|
            let~ out :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [
                        Ty.apply
                          (Ty.path "revm::handler::register::HandleRegisters")
                          []
                          [ EXT; DB ];
                        Ty.path "alloc::alloc::Global"
                      ],
                    "pop",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm::handler::Handler",
                      "registers"
                    |)
                  ]
                |)
              |) 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.apply
                                      (Ty.path "revm::handler::register::HandleRegisters")
                                      []
                                      [ EXT; DB ]
                                  ],
                                "is_some",
                                []
                              |),
                              [ out ]
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      let~ registers :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_function (|
                              "core::mem::take",
                              [
                                Ty.apply
                                  (Ty.path "alloc::vec::Vec")
                                  []
                                  [
                                    Ty.apply
                                      (Ty.path "revm::handler::register::HandleRegisters")
                                      []
                                      [ EXT; DB ];
                                    Ty.path "alloc::alloc::Global"
                                  ]
                              ]
                            |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "revm::handler::Handler",
                                "registers"
                              |)
                            ]
                          |)
                        |) in
                      let~ base_handler :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "revm::handler::Handler")
                                []
                                [ Ty.apply (Ty.path "revm::evm::Evm") [] [ EXT; DB ]; EXT; DB ],
                              "mainnet_with_spec",
                              []
                            |),
                            [
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "revm::handler::Handler",
                                    "cfg"
                                  |),
                                  "revm_primitives::env::handler_cfg::HandlerCfg",
                                  "spec_id"
                                |)
                              |)
                            ]
                          |)
                        |) in
                      let~ _ :=
                        M.use
                          (M.match_operator (|
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::iter::traits::collect::IntoIterator",
                                  Ty.apply
                                    (Ty.path "alloc::vec::Vec")
                                    []
                                    [
                                      Ty.apply
                                        (Ty.path "revm::handler::register::HandleRegisters")
                                        []
                                        [ EXT; DB ];
                                      Ty.path "alloc::alloc::Global"
                                    ],
                                  [],
                                  "into_iter",
                                  []
                                |),
                                [ M.read (| registers |) ]
                              |)
                            |),
                            [
                              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 "alloc::vec::into_iter::IntoIter")
                                                  []
                                                  [
                                                    Ty.apply
                                                      (Ty.path
                                                        "revm::handler::register::HandleRegisters")
                                                      []
                                                      [ EXT; DB ];
                                                    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 register := M.copy (| γ0_0 |) in
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.apply
                                                        (Ty.path "revm::handler::Handler")
                                                        []
                                                        [
                                                          Ty.apply
                                                            (Ty.path "revm::evm::Evm")
                                                            []
                                                            [ EXT; DB ];
                                                          EXT;
                                                          DB
                                                        ],
                                                      "append_handler_register",
                                                      []
                                                    |),
                                                    [ base_handler; M.read (| register |) ]
                                                  |)
                                                |)))
                                          ]
                                        |) in
                                      M.alloc (| Value.Tuple [] |)))
                                  |)))
                            ]
                          |)) in
                      let~ _ := M.write (| M.read (| self |), M.read (| base_handler |) |) in
                      M.alloc (| Value.Tuple [] |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            out
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_pop_handle_register :
      forall (EXT DB : Ty.t),
      M.IsAssociatedFunction (Self EXT DB) "pop_handle_register" (pop_handle_register EXT DB).
    
    (*
        pub fn create_handle_generic<SPEC: Spec>(&mut self) -> EvmHandler<'a, EXT, DB> {
            let registers = core::mem::take(&mut self.registers);
            let mut base_handler = Handler::mainnet::<SPEC>();
            // apply all registers to default handeler and raw mainnet instruction table.
            for register in registers {
                base_handler.append_handler_register(register)
            }
            base_handler
        }
    *)
    Definition create_handle_generic
        (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 ], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            let~ registers :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::mem::take",
                    [
                      Ty.apply
                        (Ty.path "alloc::vec::Vec")
                        []
                        [
                          Ty.apply
                            (Ty.path "revm::handler::register::HandleRegisters")
                            []
                            [ EXT; DB ];
                          Ty.path "alloc::alloc::Global"
                        ]
                    ]
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm::handler::Handler",
                      "registers"
                    |)
                  ]
                |)
              |) in
            let~ base_handler :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "revm::handler::Handler")
                      []
                      [ Ty.apply (Ty.path "revm::evm::Evm") [] [ EXT; DB ]; EXT; DB ],
                    "mainnet",
                    [ SPEC ]
                  |),
                  []
                |)
              |) in
            let~ _ :=
              M.use
                (M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::collect::IntoIterator",
                        Ty.apply
                          (Ty.path "alloc::vec::Vec")
                          []
                          [
                            Ty.apply
                              (Ty.path "revm::handler::register::HandleRegisters")
                              []
                              [ EXT; DB ];
                            Ty.path "alloc::alloc::Global"
                          ],
                        [],
                        "into_iter",
                        []
                      |),
                      [ M.read (| registers |) ]
                    |)
                  |),
                  [
                    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 "alloc::vec::into_iter::IntoIter")
                                        []
                                        [
                                          Ty.apply
                                            (Ty.path "revm::handler::register::HandleRegisters")
                                            []
                                            [ EXT; DB ];
                                          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 register := M.copy (| γ0_0 |) in
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "revm::handler::Handler")
                                              []
                                              [
                                                Ty.apply (Ty.path "revm::evm::Evm") [] [ EXT; DB ];
                                                EXT;
                                                DB
                                              ],
                                            "append_handler_register",
                                            []
                                          |),
                                          [ base_handler; M.read (| register |) ]
                                        |)
                                      |)))
                                ]
                              |) in
                            M.alloc (| Value.Tuple [] |)))
                        |)))
                  ]
                |)) in
            base_handler
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_create_handle_generic :
      forall (EXT DB : Ty.t),
      M.IsAssociatedFunction (Self EXT DB) "create_handle_generic" (create_handle_generic EXT DB).
    
    (*
        pub fn modify_spec_id(&mut self, spec_id: SpecId) {
            if self.cfg.spec_id == spec_id {
                return;
            }
    
            let registers = core::mem::take(&mut self.registers);
            // register for optimism is added as a register, so we need to create mainnet handler here.
            let mut handler = Handler::mainnet_with_spec(spec_id);
            // apply all registers to default handler and raw mainnet instruction table.
            for register in registers {
                handler.append_handler_register(register)
            }
            handler.cfg = self.cfg();
            handler.cfg.spec_id = spec_id;
            *self = handler;
        }
    *)
    Definition modify_spec_id
        (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; spec_id ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let spec_id := M.alloc (| spec_id |) 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_primitives::specification::SpecId",
                                    [ Ty.path "revm_primitives::specification::SpecId" ],
                                    "eq",
                                    []
                                  |),
                                  [
                                    M.SubPointer.get_struct_record_field (|
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| self |),
                                        "revm::handler::Handler",
                                        "cfg"
                                      |),
                                      "revm_primitives::env::handler_cfg::HandlerCfg",
                                      "spec_id"
                                    |);
                                    spec_id
                                  ]
                                |)
                              |)) 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.Tuple [] |) |) |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ registers :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::mem::take",
                        [
                          Ty.apply
                            (Ty.path "alloc::vec::Vec")
                            []
                            [
                              Ty.apply
                                (Ty.path "revm::handler::register::HandleRegisters")
                                []
                                [ EXT; DB ];
                              Ty.path "alloc::alloc::Global"
                            ]
                        ]
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::handler::Handler",
                          "registers"
                        |)
                      ]
                    |)
                  |) in
                let~ handler :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "revm::handler::Handler")
                          []
                          [ Ty.apply (Ty.path "revm::evm::Evm") [] [ EXT; DB ]; EXT; DB ],
                        "mainnet_with_spec",
                        []
                      |),
                      [ M.read (| spec_id |) ]
                    |)
                  |) in
                let~ _ :=
                  M.use
                    (M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::collect::IntoIterator",
                            Ty.apply
                              (Ty.path "alloc::vec::Vec")
                              []
                              [
                                Ty.apply
                                  (Ty.path "revm::handler::register::HandleRegisters")
                                  []
                                  [ EXT; DB ];
                                Ty.path "alloc::alloc::Global"
                              ],
                            [],
                            "into_iter",
                            []
                          |),
                          [ M.read (| registers |) ]
                        |)
                      |),
                      [
                        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 "alloc::vec::into_iter::IntoIter")
                                            []
                                            [
                                              Ty.apply
                                                (Ty.path "revm::handler::register::HandleRegisters")
                                                []
                                                [ EXT; DB ];
                                              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 register := M.copy (| γ0_0 |) in
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply
                                                  (Ty.path "revm::handler::Handler")
                                                  []
                                                  [
                                                    Ty.apply
                                                      (Ty.path "revm::evm::Evm")
                                                      []
                                                      [ EXT; DB ];
                                                    EXT;
                                                    DB
                                                  ],
                                                "append_handler_register",
                                                []
                                              |),
                                              [ handler; M.read (| register |) ]
                                            |)
                                          |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) in
                let~ _ :=
                  M.write (|
                    M.SubPointer.get_struct_record_field (|
                      handler,
                      "revm::handler::Handler",
                      "cfg"
                    |),
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "revm::handler::Handler")
                          []
                          [ Ty.apply (Ty.path "revm::evm::Evm") [] [ EXT; DB ]; EXT; DB ],
                        "cfg",
                        []
                      |),
                      [ M.read (| self |) ]
                    |)
                  |) in
                let~ _ :=
                  M.write (|
                    M.SubPointer.get_struct_record_field (|
                      M.SubPointer.get_struct_record_field (|
                        handler,
                        "revm::handler::Handler",
                        "cfg"
                      |),
                      "revm_primitives::env::handler_cfg::HandlerCfg",
                      "spec_id"
                    |),
                    M.read (| spec_id |)
                  |) in
                let~ _ := M.write (| M.read (| self |), M.read (| handler |) |) in
                M.alloc (| Value.Tuple [] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_modify_spec_id :
      forall (EXT DB : Ty.t),
      M.IsAssociatedFunction (Self EXT DB) "modify_spec_id" (modify_spec_id EXT DB).
  End Impl_revm_handler_Handler_revm_evm_Evm_EXT_DB_EXT_DB.
End handler.
