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

Module bytecode.
  Module eof.
    (* StructRecord
      {
        name := "Eof";
        const_params := [];
        ty_params := [];
        fields :=
          [
            ("header", Ty.path "revm_primitives::bytecode::eof::header::EofHeader");
            ("body", Ty.path "revm_primitives::bytecode::eof::body::EofBody");
            ("raw", Ty.path "alloy_primitives::bytes_::Bytes")
          ];
      } *)
    
    Module Impl_core_clone_Clone_for_revm_primitives_bytecode_eof_Eof.
      Definition Self : Ty.t := Ty.path "revm_primitives::bytecode::eof::Eof".
      
      (* 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_primitives::bytecode::eof::Eof"
              [
                ("header",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::clone::Clone",
                      Ty.path "revm_primitives::bytecode::eof::header::EofHeader",
                      [],
                      "clone",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_primitives::bytecode::eof::Eof",
                        "header"
                      |)
                    ]
                  |));
                ("body",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::clone::Clone",
                      Ty.path "revm_primitives::bytecode::eof::body::EofBody",
                      [],
                      "clone",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_primitives::bytecode::eof::Eof",
                        "body"
                      |)
                    ]
                  |));
                ("raw",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::clone::Clone",
                      Ty.path "alloy_primitives::bytes_::Bytes",
                      [],
                      "clone",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_primitives::bytecode::eof::Eof",
                        "raw"
                      |)
                    ]
                  |))
              ]))
        | _, _, _ => 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_primitives_bytecode_eof_Eof.
    
    Module Impl_core_fmt_Debug_for_revm_primitives_bytecode_eof_Eof.
      Definition Self : Ty.t := Ty.path "revm_primitives::bytecode::eof::Eof".
      
      (* 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.call_closure (|
              M.get_associated_function (|
                Ty.path "core::fmt::Formatter",
                "debug_struct_field3_finish",
                []
              |),
              [
                M.read (| f |);
                M.read (| Value.String "Eof" |);
                M.read (| Value.String "header" |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm_primitives::bytecode::eof::Eof",
                  "header"
                |);
                M.read (| Value.String "body" |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm_primitives::bytecode::eof::Eof",
                  "body"
                |);
                M.read (| Value.String "raw" |);
                M.alloc (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_primitives::bytecode::eof::Eof",
                    "raw"
                  |)
                |)
              ]
            |)))
        | _, _, _ => 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_primitives_bytecode_eof_Eof.
    
    Module Impl_core_marker_StructuralPartialEq_for_revm_primitives_bytecode_eof_Eof.
      Definition Self : Ty.t := Ty.path "revm_primitives::bytecode::eof::Eof".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_revm_primitives_bytecode_eof_Eof.
    
    Module Impl_core_cmp_PartialEq_for_revm_primitives_bytecode_eof_Eof.
      Definition Self : Ty.t := Ty.path "revm_primitives::bytecode::eof::Eof".
      
      (* 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 (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::cmp::PartialEq",
                    Ty.path "revm_primitives::bytecode::eof::header::EofHeader",
                    [ Ty.path "revm_primitives::bytecode::eof::header::EofHeader" ],
                    "eq",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::bytecode::eof::Eof",
                      "header"
                    |);
                    M.SubPointer.get_struct_record_field (|
                      M.read (| other |),
                      "revm_primitives::bytecode::eof::Eof",
                      "header"
                    |)
                  ]
                |),
                ltac:(M.monadic
                  (M.call_closure (|
                    M.get_trait_method (|
                      "core::cmp::PartialEq",
                      Ty.path "revm_primitives::bytecode::eof::body::EofBody",
                      [ Ty.path "revm_primitives::bytecode::eof::body::EofBody" ],
                      "eq",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_primitives::bytecode::eof::Eof",
                        "body"
                      |);
                      M.SubPointer.get_struct_record_field (|
                        M.read (| other |),
                        "revm_primitives::bytecode::eof::Eof",
                        "body"
                      |)
                    ]
                  |)))
              |),
              ltac:(M.monadic
                (M.call_closure (|
                  M.get_trait_method (|
                    "core::cmp::PartialEq",
                    Ty.path "alloy_primitives::bytes_::Bytes",
                    [ Ty.path "alloy_primitives::bytes_::Bytes" ],
                    "eq",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::bytecode::eof::Eof",
                      "raw"
                    |);
                    M.SubPointer.get_struct_record_field (|
                      M.read (| other |),
                      "revm_primitives::bytecode::eof::Eof",
                      "raw"
                    |)
                  ]
                |)))
            |)))
        | _, _, _ => 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_primitives_bytecode_eof_Eof.
    
    Module Impl_core_cmp_Eq_for_revm_primitives_bytecode_eof_Eof.
      Definition Self : Ty.t := Ty.path "revm_primitives::bytecode::eof::Eof".
      
      (* 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.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_primitives_bytecode_eof_Eof.
    
    Module Impl_core_hash_Hash_for_revm_primitives_bytecode_eof_Eof.
      Definition Self : Ty.t := Ty.path "revm_primitives::bytecode::eof::Eof".
      
      (* Hash *)
      Definition hash (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ __H ], [ self; state ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let state := M.alloc (| state |) in
            M.read (|
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::hash::Hash",
                      Ty.path "revm_primitives::bytecode::eof::header::EofHeader",
                      [],
                      "hash",
                      [ __H ]
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_primitives::bytecode::eof::Eof",
                        "header"
                      |);
                      M.read (| state |)
                    ]
                  |)
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::hash::Hash",
                      Ty.path "revm_primitives::bytecode::eof::body::EofBody",
                      [],
                      "hash",
                      [ __H ]
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_primitives::bytecode::eof::Eof",
                        "body"
                      |);
                      M.read (| state |)
                    ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::hash::Hash",
                    Ty.path "alloy_primitives::bytes_::Bytes",
                    [],
                    "hash",
                    [ __H ]
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::bytecode::eof::Eof",
                      "raw"
                    |);
                    M.read (| state |)
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::hash::Hash"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("hash", InstanceField.Method hash) ].
    End Impl_core_hash_Hash_for_revm_primitives_bytecode_eof_Eof.
    
    Module Impl_core_default_Default_for_revm_primitives_bytecode_eof_Eof.
      Definition Self : Ty.t := Ty.path "revm_primitives::bytecode::eof::Eof".
      
      (*
          fn default() -> Self {
              let body = EofBody {
                  // types section with zero inputs, zero outputs and zero max stack size.
                  types_section: vec![TypesSection::default()],
                  // One code section with a STOP byte.
                  code_section: vec![[0x00].into()],
                  container_section: vec![],
                  data_section: Bytes::new(),
                  is_data_filled: true,
              };
              body.into_eof()
          }
      *)
      Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [] =>
          ltac:(M.monadic
            (M.read (|
              let~ body :=
                M.alloc (|
                  Value.StructRecord
                    "revm_primitives::bytecode::eof::body::EofBody"
                    [
                      ("types_section",
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "slice")
                              []
                              [
                                Ty.path
                                  "revm_primitives::bytecode::eof::types_section::TypesSection"
                              ],
                            "into_vec",
                            [ Ty.path "alloc::alloc::Global" ]
                          |),
                          [
                            M.read (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "alloc::boxed::Box")
                                    []
                                    [
                                      Ty.apply
                                        (Ty.path "array")
                                        [ Value.Integer IntegerKind.Usize 1 ]
                                        [
                                          Ty.path
                                            "revm_primitives::bytecode::eof::types_section::TypesSection"
                                        ];
                                      Ty.path "alloc::alloc::Global"
                                    ],
                                  "new",
                                  []
                                |),
                                [
                                  M.alloc (|
                                    Value.Array
                                      [
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::default::Default",
                                            Ty.path
                                              "revm_primitives::bytecode::eof::types_section::TypesSection",
                                            [],
                                            "default",
                                            []
                                          |),
                                          []
                                        |)
                                      ]
                                  |)
                                ]
                              |)
                            |)
                          ]
                        |));
                      ("code_section",
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "slice")
                              []
                              [ Ty.path "alloy_primitives::bytes_::Bytes" ],
                            "into_vec",
                            [ Ty.path "alloc::alloc::Global" ]
                          |),
                          [
                            M.read (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "alloc::boxed::Box")
                                    []
                                    [
                                      Ty.apply
                                        (Ty.path "array")
                                        [ Value.Integer IntegerKind.Usize 1 ]
                                        [ Ty.path "alloy_primitives::bytes_::Bytes" ];
                                      Ty.path "alloc::alloc::Global"
                                    ],
                                  "new",
                                  []
                                |),
                                [
                                  M.alloc (|
                                    Value.Array
                                      [
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::convert::Into",
                                            Ty.apply
                                              (Ty.path "array")
                                              [ Value.Integer IntegerKind.Usize 1 ]
                                              [ Ty.path "u8" ],
                                            [ Ty.path "alloy_primitives::bytes_::Bytes" ],
                                            "into",
                                            []
                                          |),
                                          [ Value.Array [ Value.Integer IntegerKind.U8 0 ] ]
                                        |)
                                      ]
                                  |)
                                ]
                              |)
                            |)
                          ]
                        |));
                      ("container_section",
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "alloc::vec::Vec")
                              []
                              [
                                Ty.path "alloy_primitives::bytes_::Bytes";
                                Ty.path "alloc::alloc::Global"
                              ],
                            "new",
                            []
                          |),
                          []
                        |));
                      ("data_section",
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "alloy_primitives::bytes_::Bytes",
                            "new",
                            []
                          |),
                          []
                        |));
                      ("is_data_filled", Value.Bool true)
                    ]
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "revm_primitives::bytecode::eof::body::EofBody",
                    "into_eof",
                    []
                  |),
                  [ M.read (| body |) ]
                |)
              |)
            |)))
        | _, _, _ => 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_primitives_bytecode_eof_Eof.
    
    Module Impl_revm_primitives_bytecode_eof_Eof.
      Definition Self : Ty.t := Ty.path "revm_primitives::bytecode::eof::Eof".
      
      (*
          pub fn size(&self) -> usize {
              self.header.size() + self.header.body_size()
          }
      *)
      Definition size (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            BinOp.Wrap.add (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "revm_primitives::bytecode::eof::header::EofHeader",
                  "size",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_primitives::bytecode::eof::Eof",
                    "header"
                  |)
                ]
              |),
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "revm_primitives::bytecode::eof::header::EofHeader",
                  "body_size",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_primitives::bytecode::eof::Eof",
                    "header"
                  |)
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_size : M.IsAssociatedFunction Self "size" size.
      
      (*
          pub fn raw(&self) -> &Bytes {
              &self.raw
          }
      *)
      Definition raw (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.SubPointer.get_struct_record_field (|
              M.read (| self |),
              "revm_primitives::bytecode::eof::Eof",
              "raw"
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_raw : M.IsAssociatedFunction Self "raw" raw.
      
      (*
          pub fn data_slice(&self, offset: usize, len: usize) -> &[u8] {
              self.body
                  .data_section
                  .get(offset..)
                  .and_then(|bytes| bytes.get(..min(len, bytes.len())))
                  .unwrap_or(&[])
          }
      *)
      Definition data_slice (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; offset; len ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let offset := M.alloc (| offset |) in
            let len := M.alloc (| len |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "core::option::Option")
                  []
                  [ Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ] ],
                "unwrap_or",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [ Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ]
                      ],
                    "and_then",
                    [
                      Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ];
                      Ty.function
                        [
                          Ty.tuple
                            [
                              Ty.apply
                                (Ty.path "&")
                                []
                                [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ]
                            ]
                        ]
                        (Ty.apply
                          (Ty.path "core::option::Option")
                          []
                          [
                            Ty.apply
                              (Ty.path "&")
                              []
                              [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ]
                          ])
                    ]
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                        "get",
                        [ Ty.apply (Ty.path "core::ops::range::RangeFrom") [] [ Ty.path "usize" ] ]
                      |),
                      [
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::deref::Deref",
                            Ty.path "bytes::bytes::Bytes",
                            [],
                            "deref",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::deref::Deref",
                                Ty.path "alloy_primitives::bytes_::Bytes",
                                [],
                                "deref",
                                []
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "revm_primitives::bytecode::eof::Eof",
                                    "body"
                                  |),
                                  "revm_primitives::bytecode::eof::body::EofBody",
                                  "data_section"
                                |)
                              ]
                            |)
                          ]
                        |);
                        Value.StructRecord
                          "core::ops::range::RangeFrom"
                          [ ("start", M.read (| offset |)) ]
                      ]
                    |);
                    M.closure
                      (fun γ =>
                        ltac:(M.monadic
                          match γ with
                          | [ α0 ] =>
                            ltac:(M.monadic
                              (M.match_operator (|
                                M.alloc (| α0 |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let bytes := M.copy (| γ |) in
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                          "get",
                                          [
                                            Ty.apply
                                              (Ty.path "core::ops::range::RangeTo")
                                              []
                                              [ Ty.path "usize" ]
                                          ]
                                        |),
                                        [
                                          M.read (| bytes |);
                                          Value.StructRecord
                                            "core::ops::range::RangeTo"
                                            [
                                              ("end_",
                                                M.call_closure (|
                                                  M.get_function (|
                                                    "core::cmp::min",
                                                    [ Ty.path "usize" ]
                                                  |),
                                                  [
                                                    M.read (| len |);
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.apply
                                                          (Ty.path "slice")
                                                          []
                                                          [ Ty.path "u8" ],
                                                        "len",
                                                        []
                                                      |),
                                                      [ M.read (| bytes |) ]
                                                    |)
                                                  ]
                                                |))
                                            ]
                                        ]
                                      |)))
                                ]
                              |)))
                          | _ => M.impossible "wrong number of arguments"
                          end))
                  ]
                |);
                M.alloc (| Value.Array [] |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_data_slice : M.IsAssociatedFunction Self "data_slice" data_slice.
      
      (*
          pub fn data(&self) -> &[u8] {
              &self.body.data_section
          }
      *)
      Definition data (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::ops::deref::Deref",
                Ty.path "bytes::bytes::Bytes",
                [],
                "deref",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::deref::Deref",
                    Ty.path "alloy_primitives::bytes_::Bytes",
                    [],
                    "deref",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_primitives::bytecode::eof::Eof",
                        "body"
                      |),
                      "revm_primitives::bytecode::eof::body::EofBody",
                      "data_section"
                    |)
                  ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_data : M.IsAssociatedFunction Self "data" data.
      
      (*
          pub fn encode_slow(&self) -> Bytes {
              let mut buffer: Vec<u8> = Vec::with_capacity(self.size());
              self.header.encode(&mut buffer);
              self.body.encode(&mut buffer);
              buffer.into()
          }
      *)
      Definition encode_slow (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              let~ buffer :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "alloc::vec::Vec")
                        []
                        [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ],
                      "with_capacity",
                      []
                    |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "revm_primitives::bytecode::eof::Eof",
                          "size",
                          []
                        |),
                        [ M.read (| self |) ]
                      |)
                    ]
                  |)
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "revm_primitives::bytecode::eof::header::EofHeader",
                      "encode",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_primitives::bytecode::eof::Eof",
                        "header"
                      |);
                      buffer
                    ]
                  |)
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "revm_primitives::bytecode::eof::body::EofBody",
                      "encode",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_primitives::bytecode::eof::Eof",
                        "body"
                      |);
                      buffer
                    ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::convert::Into",
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ],
                    [ Ty.path "alloy_primitives::bytes_::Bytes" ],
                    "into",
                    []
                  |),
                  [ M.read (| buffer |) ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_encode_slow : M.IsAssociatedFunction Self "encode_slow" encode_slow.
      
      (*
          pub fn decode(raw: Bytes) -> Result<Self, EofDecodeError> {
              let (header, _) = EofHeader::decode(&raw)?;
              let body = EofBody::decode(&raw, &header)?;
              Ok(Self { header, body, raw })
          }
      *)
      Definition decode (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ raw ] =>
          ltac:(M.monadic
            (let raw := M.alloc (| raw |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  M.match_operator (|
                    M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::try_trait::Try",
                            Ty.apply
                              (Ty.path "core::result::Result")
                              []
                              [
                                Ty.tuple
                                  [
                                    Ty.path "revm_primitives::bytecode::eof::header::EofHeader";
                                    Ty.apply
                                      (Ty.path "&")
                                      []
                                      [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ]
                                  ];
                                Ty.path "revm_primitives::bytecode::eof::EofDecodeError"
                              ],
                            [],
                            "branch",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "revm_primitives::bytecode::eof::header::EofHeader",
                                "decode",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::deref::Deref",
                                    Ty.path "bytes::bytes::Bytes",
                                    [],
                                    "deref",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::ops::deref::Deref",
                                        Ty.path "alloy_primitives::bytes_::Bytes",
                                        [],
                                        "deref",
                                        []
                                      |),
                                      [ raw ]
                                    |)
                                  ]
                                |)
                              ]
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::control_flow::ControlFlow::Break",
                                0
                              |) in
                            let residual := M.copy (| γ0_0 |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  M.return_ (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::ops::try_trait::FromResidual",
                                        Ty.apply
                                          (Ty.path "core::result::Result")
                                          []
                                          [
                                            Ty.path "revm_primitives::bytecode::eof::Eof";
                                            Ty.path "revm_primitives::bytecode::eof::EofDecodeError"
                                          ],
                                        [
                                          Ty.apply
                                            (Ty.path "core::result::Result")
                                            []
                                            [
                                              Ty.path "core::convert::Infallible";
                                              Ty.path
                                                "revm_primitives::bytecode::eof::EofDecodeError"
                                            ]
                                        ],
                                        "from_residual",
                                        []
                                      |),
                                      [ M.read (| residual |) ]
                                    |)
                                  |)
                                |)
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::control_flow::ControlFlow::Continue",
                                0
                              |) in
                            let val := M.copy (| γ0_0 |) in
                            val))
                      ]
                    |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                          let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                          let header := M.copy (| γ0_0 |) in
                          let~ body :=
                            M.copy (|
                              M.match_operator (|
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::ops::try_trait::Try",
                                      Ty.apply
                                        (Ty.path "core::result::Result")
                                        []
                                        [
                                          Ty.path "revm_primitives::bytecode::eof::body::EofBody";
                                          Ty.path "revm_primitives::bytecode::eof::EofDecodeError"
                                        ],
                                      [],
                                      "branch",
                                      []
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "revm_primitives::bytecode::eof::body::EofBody",
                                          "decode",
                                          []
                                        |),
                                        [ raw; header ]
                                      |)
                                    ]
                                  |)
                                |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ0_0 :=
                                        M.SubPointer.get_struct_tuple_field (|
                                          γ,
                                          "core::ops::control_flow::ControlFlow::Break",
                                          0
                                        |) in
                                      let residual := M.copy (| γ0_0 |) in
                                      M.alloc (|
                                        M.never_to_any (|
                                          M.read (|
                                            M.return_ (|
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::ops::try_trait::FromResidual",
                                                  Ty.apply
                                                    (Ty.path "core::result::Result")
                                                    []
                                                    [
                                                      Ty.path "revm_primitives::bytecode::eof::Eof";
                                                      Ty.path
                                                        "revm_primitives::bytecode::eof::EofDecodeError"
                                                    ],
                                                  [
                                                    Ty.apply
                                                      (Ty.path "core::result::Result")
                                                      []
                                                      [
                                                        Ty.path "core::convert::Infallible";
                                                        Ty.path
                                                          "revm_primitives::bytecode::eof::EofDecodeError"
                                                      ]
                                                  ],
                                                  "from_residual",
                                                  []
                                                |),
                                                [ M.read (| residual |) ]
                                              |)
                                            |)
                                          |)
                                        |)
                                      |)));
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ0_0 :=
                                        M.SubPointer.get_struct_tuple_field (|
                                          γ,
                                          "core::ops::control_flow::ControlFlow::Continue",
                                          0
                                        |) in
                                      let val := M.copy (| γ0_0 |) in
                                      val))
                                ]
                              |)
                            |) in
                          M.alloc (|
                            Value.StructTuple
                              "core::result::Result::Ok"
                              [
                                Value.StructRecord
                                  "revm_primitives::bytecode::eof::Eof"
                                  [
                                    ("header", M.read (| header |));
                                    ("body", M.read (| body |));
                                    ("raw", M.read (| raw |))
                                  ]
                              ]
                          |)))
                    ]
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_decode : M.IsAssociatedFunction Self "decode" decode.
    End Impl_revm_primitives_bytecode_eof_Eof.
    
    (*
    Enum EofDecodeError
    {
      const_params := [];
      ty_params := [];
      variants :=
        [
          {
            name := "MissingInput";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "MissingBodyWithoutData";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "DanglingData";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "InvalidTypesSection";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "InvalidTypesSectionSize";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "InvalidEOFMagicNumber";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "InvalidEOFVersion";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "InvalidTypesKind";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "InvalidCodeKind";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "InvalidTerminalByte";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "InvalidDataKind";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "InvalidKindAfterCode";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "MismatchCodeAndTypesSize";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "NonSizes";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "ShortInputForSizes";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "ZeroSize";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "TooManyCodeSections";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "ZeroCodeSections";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "TooManyContainerSections";
            item := StructTuple [];
            discriminant := None;
          }
        ];
    }
    *)
    
    Module Impl_core_fmt_Debug_for_revm_primitives_bytecode_eof_EofDecodeError.
      Definition Self : Ty.t := Ty.path "revm_primitives::bytecode::eof::EofDecodeError".
      
      (* 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.call_closure (|
              M.get_associated_function (| Ty.path "core::fmt::Formatter", "write_str", [] |),
              [
                M.read (| f |);
                M.read (|
                  M.match_operator (|
                    self,
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::bytecode::eof::EofDecodeError::MissingInput"
                            |) in
                          M.alloc (| M.read (| Value.String "MissingInput" |) |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::bytecode::eof::EofDecodeError::MissingBodyWithoutData"
                            |) in
                          M.alloc (| M.read (| Value.String "MissingBodyWithoutData" |) |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::bytecode::eof::EofDecodeError::DanglingData"
                            |) in
                          M.alloc (| M.read (| Value.String "DanglingData" |) |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::bytecode::eof::EofDecodeError::InvalidTypesSection"
                            |) in
                          M.alloc (| M.read (| Value.String "InvalidTypesSection" |) |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::bytecode::eof::EofDecodeError::InvalidTypesSectionSize"
                            |) in
                          M.alloc (| M.read (| Value.String "InvalidTypesSectionSize" |) |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::bytecode::eof::EofDecodeError::InvalidEOFMagicNumber"
                            |) in
                          M.alloc (| M.read (| Value.String "InvalidEOFMagicNumber" |) |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::bytecode::eof::EofDecodeError::InvalidEOFVersion"
                            |) in
                          M.alloc (| M.read (| Value.String "InvalidEOFVersion" |) |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::bytecode::eof::EofDecodeError::InvalidTypesKind"
                            |) in
                          M.alloc (| M.read (| Value.String "InvalidTypesKind" |) |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::bytecode::eof::EofDecodeError::InvalidCodeKind"
                            |) in
                          M.alloc (| M.read (| Value.String "InvalidCodeKind" |) |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::bytecode::eof::EofDecodeError::InvalidTerminalByte"
                            |) in
                          M.alloc (| M.read (| Value.String "InvalidTerminalByte" |) |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::bytecode::eof::EofDecodeError::InvalidDataKind"
                            |) in
                          M.alloc (| M.read (| Value.String "InvalidDataKind" |) |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::bytecode::eof::EofDecodeError::InvalidKindAfterCode"
                            |) in
                          M.alloc (| M.read (| Value.String "InvalidKindAfterCode" |) |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::bytecode::eof::EofDecodeError::MismatchCodeAndTypesSize"
                            |) in
                          M.alloc (| M.read (| Value.String "MismatchCodeAndTypesSize" |) |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::bytecode::eof::EofDecodeError::NonSizes"
                            |) in
                          M.alloc (| M.read (| Value.String "NonSizes" |) |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::bytecode::eof::EofDecodeError::ShortInputForSizes"
                            |) in
                          M.alloc (| M.read (| Value.String "ShortInputForSizes" |) |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::bytecode::eof::EofDecodeError::ZeroSize"
                            |) in
                          M.alloc (| M.read (| Value.String "ZeroSize" |) |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::bytecode::eof::EofDecodeError::TooManyCodeSections"
                            |) in
                          M.alloc (| M.read (| Value.String "TooManyCodeSections" |) |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::bytecode::eof::EofDecodeError::ZeroCodeSections"
                            |) in
                          M.alloc (| M.read (| Value.String "ZeroCodeSections" |) |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::bytecode::eof::EofDecodeError::TooManyContainerSections"
                            |) in
                          M.alloc (| M.read (| Value.String "TooManyContainerSections" |) |)))
                    ]
                  |)
                |)
              ]
            |)))
        | _, _, _ => 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_primitives_bytecode_eof_EofDecodeError.
    
    Module Impl_core_hash_Hash_for_revm_primitives_bytecode_eof_EofDecodeError.
      Definition Self : Ty.t := Ty.path "revm_primitives::bytecode::eof::EofDecodeError".
      
      (* Hash *)
      Definition hash (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ __H ], [ self; state ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let state := M.alloc (| state |) in
            M.read (|
              let~ __self_discr :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::discriminant_value",
                      [ Ty.path "revm_primitives::bytecode::eof::EofDecodeError" ]
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (| "core::hash::Hash", Ty.path "isize", [], "hash", [ __H ] |),
                  [ __self_discr; M.read (| state |) ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::hash::Hash"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("hash", InstanceField.Method hash) ].
    End Impl_core_hash_Hash_for_revm_primitives_bytecode_eof_EofDecodeError.
    
    Module Impl_core_marker_StructuralPartialEq_for_revm_primitives_bytecode_eof_EofDecodeError.
      Definition Self : Ty.t := Ty.path "revm_primitives::bytecode::eof::EofDecodeError".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_revm_primitives_bytecode_eof_EofDecodeError.
    
    Module Impl_core_cmp_PartialEq_for_revm_primitives_bytecode_eof_EofDecodeError.
      Definition Self : Ty.t := Ty.path "revm_primitives::bytecode::eof::EofDecodeError".
      
      (* 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
            M.read (|
              let~ __self_discr :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::discriminant_value",
                      [ Ty.path "revm_primitives::bytecode::eof::EofDecodeError" ]
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              let~ __arg1_discr :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::discriminant_value",
                      [ Ty.path "revm_primitives::bytecode::eof::EofDecodeError" ]
                    |),
                    [ M.read (| other |) ]
                  |)
                |) in
              M.alloc (| BinOp.eq (| M.read (| __self_discr |), M.read (| __arg1_discr |) |) |)
            |)))
        | _, _, _ => 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_primitives_bytecode_eof_EofDecodeError.
    
    Module Impl_core_cmp_Eq_for_revm_primitives_bytecode_eof_EofDecodeError.
      Definition Self : Ty.t := Ty.path "revm_primitives::bytecode::eof::EofDecodeError".
      
      (* 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
            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_primitives_bytecode_eof_EofDecodeError.
    
    Module Impl_core_cmp_PartialOrd_for_revm_primitives_bytecode_eof_EofDecodeError.
      Definition Self : Ty.t := Ty.path "revm_primitives::bytecode::eof::EofDecodeError".
      
      (* PartialOrd *)
      Definition partial_cmp (ε : 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
            M.read (|
              let~ __self_discr :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::discriminant_value",
                      [ Ty.path "revm_primitives::bytecode::eof::EofDecodeError" ]
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              let~ __arg1_discr :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::discriminant_value",
                      [ Ty.path "revm_primitives::bytecode::eof::EofDecodeError" ]
                    |),
                    [ M.read (| other |) ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::cmp::PartialOrd",
                    Ty.path "isize",
                    [ Ty.path "isize" ],
                    "partial_cmp",
                    []
                  |),
                  [ __self_discr; __arg1_discr ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("partial_cmp", InstanceField.Method partial_cmp) ].
    End Impl_core_cmp_PartialOrd_for_revm_primitives_bytecode_eof_EofDecodeError.
    
    Module Impl_core_cmp_Ord_for_revm_primitives_bytecode_eof_EofDecodeError.
      Definition Self : Ty.t := Ty.path "revm_primitives::bytecode::eof::EofDecodeError".
      
      (* Ord *)
      Definition cmp (ε : 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
            M.read (|
              let~ __self_discr :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::discriminant_value",
                      [ Ty.path "revm_primitives::bytecode::eof::EofDecodeError" ]
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              let~ __arg1_discr :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::discriminant_value",
                      [ Ty.path "revm_primitives::bytecode::eof::EofDecodeError" ]
                    |),
                    [ M.read (| other |) ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (| "core::cmp::Ord", Ty.path "isize", [], "cmp", [] |),
                  [ __self_discr; __arg1_discr ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::Ord"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("cmp", InstanceField.Method cmp) ].
    End Impl_core_cmp_Ord_for_revm_primitives_bytecode_eof_EofDecodeError.
    
    Module Impl_core_clone_Clone_for_revm_primitives_bytecode_eof_EofDecodeError.
      Definition Self : Ty.t := Ty.path "revm_primitives::bytecode::eof::EofDecodeError".
      
      (* 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
            M.read (| M.read (| self |) |)))
        | _, _, _ => 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_primitives_bytecode_eof_EofDecodeError.
    
    Module Impl_core_marker_Copy_for_revm_primitives_bytecode_eof_EofDecodeError.
      Definition Self : Ty.t := Ty.path "revm_primitives::bytecode::eof::EofDecodeError".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::Copy"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Copy_for_revm_primitives_bytecode_eof_EofDecodeError.
  End eof.
End bytecode.
