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

Module interpreter_action.
  Module eof_create_inputs.
    (* StructRecord
      {
        name := "EOFCreateInput";
        const_params := [];
        ty_params := [];
        fields :=
          [
            ("caller", Ty.path "alloy_primitives::bits::address::Address");
            ("created_address", Ty.path "alloy_primitives::bits::address::Address");
            ("value",
              Ty.apply
                (Ty.path "ruint::Uint")
                [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                []);
            ("eof_init_code", Ty.path "revm_primitives::bytecode::eof::Eof");
            ("gas_limit", Ty.path "u64");
            ("return_memory_range",
              Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ])
          ];
      } *)
    
    Module Impl_core_fmt_Debug_for_revm_interpreter_interpreter_action_eof_create_inputs_EOFCreateInput.
      Definition Self : Ty.t :=
        Ty.path "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput".
      
      (* Debug *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.read (|
              let~ names :=
                M.alloc (|
                  M.alloc (|
                    Value.Array
                      [
                        M.read (| Value.String "caller" |);
                        M.read (| Value.String "created_address" |);
                        M.read (| Value.String "value" |);
                        M.read (| Value.String "eof_init_code" |);
                        M.read (| Value.String "gas_limit" |);
                        M.read (| Value.String "return_memory_range" |)
                      ]
                  |)
                |) in
              let~ values :=
                M.alloc (|
                  M.alloc (|
                    Value.Array
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput",
                          "caller"
                        |);
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput",
                          "created_address"
                        |);
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput",
                          "value"
                        |);
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput",
                          "eof_init_code"
                        |);
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput",
                          "gas_limit"
                        |);
                        M.alloc (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput",
                            "return_memory_range"
                          |)
                        |)
                      ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "core::fmt::Formatter",
                    "debug_struct_fields_finish",
                    []
                  |),
                  [
                    M.read (| f |);
                    M.read (| Value.String "EOFCreateInput" |);
                    M.read (| names |);
                    M.read (| values |)
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::fmt::Debug"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
    End Impl_core_fmt_Debug_for_revm_interpreter_interpreter_action_eof_create_inputs_EOFCreateInput.
    
    Module Impl_core_default_Default_for_revm_interpreter_interpreter_action_eof_create_inputs_EOFCreateInput.
      Definition Self : Ty.t :=
        Ty.path "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput".
      
      (* Default *)
      Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [] =>
          ltac:(M.monadic
            (Value.StructRecord
              "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput"
              [
                ("caller",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::default::Default",
                      Ty.path "alloy_primitives::bits::address::Address",
                      [],
                      "default",
                      []
                    |),
                    []
                  |));
                ("created_address",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::default::Default",
                      Ty.path "alloy_primitives::bits::address::Address",
                      [],
                      "default",
                      []
                    |),
                    []
                  |));
                ("value",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::default::Default",
                      Ty.apply
                        (Ty.path "ruint::Uint")
                        [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                        [],
                      [],
                      "default",
                      []
                    |),
                    []
                  |));
                ("eof_init_code",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::default::Default",
                      Ty.path "revm_primitives::bytecode::eof::Eof",
                      [],
                      "default",
                      []
                    |),
                    []
                  |));
                ("gas_limit",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::default::Default",
                      Ty.path "u64",
                      [],
                      "default",
                      []
                    |),
                    []
                  |));
                ("return_memory_range",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::default::Default",
                      Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                      [],
                      "default",
                      []
                    |),
                    []
                  |))
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::default::Default"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("default", InstanceField.Method default) ].
    End Impl_core_default_Default_for_revm_interpreter_interpreter_action_eof_create_inputs_EOFCreateInput.
    
    Module Impl_core_clone_Clone_for_revm_interpreter_interpreter_action_eof_create_inputs_EOFCreateInput.
      Definition Self : Ty.t :=
        Ty.path "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput".
      
      (* Clone *)
      Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            Value.StructRecord
              "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput"
              [
                ("caller",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::clone::Clone",
                      Ty.path "alloy_primitives::bits::address::Address",
                      [],
                      "clone",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput",
                        "caller"
                      |)
                    ]
                  |));
                ("created_address",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::clone::Clone",
                      Ty.path "alloy_primitives::bits::address::Address",
                      [],
                      "clone",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput",
                        "created_address"
                      |)
                    ]
                  |));
                ("value",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::clone::Clone",
                      Ty.apply
                        (Ty.path "ruint::Uint")
                        [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                        [],
                      [],
                      "clone",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput",
                        "value"
                      |)
                    ]
                  |));
                ("eof_init_code",
                  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 (| self |),
                        "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput",
                        "eof_init_code"
                      |)
                    ]
                  |));
                ("gas_limit",
                  M.call_closure (|
                    M.get_trait_method (| "core::clone::Clone", Ty.path "u64", [], "clone", [] |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput",
                        "gas_limit"
                      |)
                    ]
                  |));
                ("return_memory_range",
                  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 (| self |),
                        "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput",
                        "return_memory_range"
                      |)
                    ]
                  |))
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::clone::Clone"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("clone", InstanceField.Method clone) ].
    End Impl_core_clone_Clone_for_revm_interpreter_interpreter_action_eof_create_inputs_EOFCreateInput.
    
    Module Impl_core_marker_StructuralPartialEq_for_revm_interpreter_interpreter_action_eof_create_inputs_EOFCreateInput.
      Definition Self : Ty.t :=
        Ty.path "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_revm_interpreter_interpreter_action_eof_create_inputs_EOFCreateInput.
    
    Module Impl_core_cmp_PartialEq_for_revm_interpreter_interpreter_action_eof_create_inputs_EOFCreateInput.
      Definition Self : Ty.t :=
        Ty.path "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput".
      
      (* PartialEq *)
      Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            LogicalOp.and (|
              LogicalOp.and (|
                LogicalOp.and (|
                  LogicalOp.and (|
                    LogicalOp.and (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::cmp::PartialEq",
                          Ty.path "alloy_primitives::bits::address::Address",
                          [ Ty.path "alloy_primitives::bits::address::Address" ],
                          "eq",
                          []
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput",
                            "caller"
                          |);
                          M.SubPointer.get_struct_record_field (|
                            M.read (| other |),
                            "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput",
                            "caller"
                          |)
                        ]
                      |),
                      ltac:(M.monadic
                        (M.call_closure (|
                          M.get_trait_method (|
                            "core::cmp::PartialEq",
                            Ty.path "alloy_primitives::bits::address::Address",
                            [ Ty.path "alloy_primitives::bits::address::Address" ],
                            "eq",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput",
                              "created_address"
                            |);
                            M.SubPointer.get_struct_record_field (|
                              M.read (| other |),
                              "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput",
                              "created_address"
                            |)
                          ]
                        |)))
                    |),
                    ltac:(M.monadic
                      (M.call_closure (|
                        M.get_trait_method (|
                          "core::cmp::PartialEq",
                          Ty.apply
                            (Ty.path "ruint::Uint")
                            [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4
                            ]
                            [],
                          [
                            Ty.apply
                              (Ty.path "ruint::Uint")
                              [
                                Value.Integer IntegerKind.Usize 256;
                                Value.Integer IntegerKind.Usize 4
                              ]
                              []
                          ],
                          "eq",
                          []
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput",
                            "value"
                          |);
                          M.SubPointer.get_struct_record_field (|
                            M.read (| other |),
                            "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput",
                            "value"
                          |)
                        ]
                      |)))
                  |),
                  ltac:(M.monadic
                    (M.call_closure (|
                      M.get_trait_method (|
                        "core::cmp::PartialEq",
                        Ty.path "revm_primitives::bytecode::eof::Eof",
                        [ Ty.path "revm_primitives::bytecode::eof::Eof" ],
                        "eq",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput",
                          "eof_init_code"
                        |);
                        M.SubPointer.get_struct_record_field (|
                          M.read (| other |),
                          "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput",
                          "eof_init_code"
                        |)
                      ]
                    |)))
                |),
                ltac:(M.monadic
                  (BinOp.eq (|
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput",
                        "gas_limit"
                      |)
                    |),
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| other |),
                        "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput",
                        "gas_limit"
                      |)
                    |)
                  |)))
              |),
              ltac:(M.monadic
                (M.call_closure (|
                  M.get_trait_method (|
                    "core::cmp::PartialEq",
                    Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                    [ Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ] ],
                    "eq",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput",
                      "return_memory_range"
                    |);
                    M.SubPointer.get_struct_record_field (|
                      M.read (| other |),
                      "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput",
                      "return_memory_range"
                    |)
                  ]
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq) ].
    End Impl_core_cmp_PartialEq_for_revm_interpreter_interpreter_action_eof_create_inputs_EOFCreateInput.
    
    Module Impl_core_cmp_Eq_for_revm_interpreter_interpreter_action_eof_create_inputs_EOFCreateInput.
      Definition Self : Ty.t :=
        Ty.path "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput".
      
      (* Eq *)
      Definition assert_receiver_is_total_eq
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                Value.DeclaredButUndefined,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (M.match_operator (|
                        Value.DeclaredButUndefined,
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (M.match_operator (|
                                Value.DeclaredButUndefined,
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (M.match_operator (|
                                        Value.DeclaredButUndefined,
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (M.match_operator (|
                                                Value.DeclaredButUndefined,
                                                [
                                                  fun γ =>
                                                    ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                                ]
                                              |)))
                                        ]
                                      |)))
                                ]
                              |)))
                        ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::Eq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
    End Impl_core_cmp_Eq_for_revm_interpreter_interpreter_action_eof_create_inputs_EOFCreateInput.
    
    Module Impl_revm_interpreter_interpreter_action_eof_create_inputs_EOFCreateInput.
      Definition Self : Ty.t :=
        Ty.path "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput".
      
      (*
          pub fn new(
              caller: Address,
              created_address: Address,
              value: U256,
              eof_init_code: Eof,
              gas_limit: u64,
              return_memory_range: Range<usize>,
          ) -> EOFCreateInput {
              EOFCreateInput {
                  caller,
                  created_address,
                  value,
                  eof_init_code,
                  gas_limit,
                  return_memory_range,
              }
          }
      *)
      Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [],
            [],
            [ caller; created_address; value; eof_init_code; gas_limit; return_memory_range ] =>
          ltac:(M.monadic
            (let caller := M.alloc (| caller |) in
            let created_address := M.alloc (| created_address |) in
            let value := M.alloc (| value |) in
            let eof_init_code := M.alloc (| eof_init_code |) in
            let gas_limit := M.alloc (| gas_limit |) in
            let return_memory_range := M.alloc (| return_memory_range |) in
            Value.StructRecord
              "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput"
              [
                ("caller", M.read (| caller |));
                ("created_address", M.read (| created_address |));
                ("value", M.read (| value |));
                ("eof_init_code", M.read (| eof_init_code |));
                ("gas_limit", M.read (| gas_limit |));
                ("return_memory_range", M.read (| return_memory_range |))
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
    End Impl_revm_interpreter_interpreter_action_eof_create_inputs_EOFCreateInput.
  End eof_create_inputs.
End interpreter_action.
