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

Module bytecode.
  (*
  Enum Bytecode
  {
    const_params := [];
    ty_params := [];
    variants :=
      [
        {
          name := "LegacyRaw";
          item := StructTuple [ Ty.path "alloy_primitives::bytes_::Bytes" ];
          discriminant := None;
        };
        {
          name := "LegacyAnalyzed";
          item :=
            StructTuple [ Ty.path "revm_primitives::bytecode::legacy::LegacyAnalyzedBytecode" ];
          discriminant := None;
        };
        {
          name := "Eof";
          item := StructTuple [ Ty.path "revm_primitives::bytecode::eof::Eof" ];
          discriminant := None;
        }
      ];
  }
  *)
  
  Module Impl_core_clone_Clone_for_revm_primitives_bytecode_Bytecode.
    Definition Self : Ty.t := Ty.path "revm_primitives::bytecode::Bytecode".
    
    (* 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.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_primitives::bytecode::Bytecode::LegacyRaw",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_primitives::bytecode::Bytecode::LegacyRaw"
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::clone::Clone",
                              Ty.path "alloy_primitives::bytes_::Bytes",
                              [],
                              "clone",
                              []
                            |),
                            [ M.read (| __self_0 |) ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_primitives::bytecode::Bytecode::LegacyAnalyzed",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_primitives::bytecode::Bytecode::LegacyAnalyzed"
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::clone::Clone",
                              Ty.path "revm_primitives::bytecode::legacy::LegacyAnalyzedBytecode",
                              [],
                              "clone",
                              []
                            |),
                            [ M.read (| __self_0 |) ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_primitives::bytecode::Bytecode::Eof",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_primitives::bytecode::Bytecode::Eof"
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::clone::Clone",
                              Ty.path "revm_primitives::bytecode::eof::Eof",
                              [],
                              "clone",
                              []
                            |),
                            [ M.read (| __self_0 |) ]
                          |)
                        ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => 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_Bytecode.
  
  Module Impl_core_fmt_Debug_for_revm_primitives_bytecode_Bytecode.
    Definition Self : Ty.t := Ty.path "revm_primitives::bytecode::Bytecode".
    
    (* 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 (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_primitives::bytecode::Bytecode::LegacyRaw",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "debug_tuple_field1_finish",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "LegacyRaw" |); __self_0 ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_primitives::bytecode::Bytecode::LegacyAnalyzed",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "debug_tuple_field1_finish",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "LegacyAnalyzed" |); __self_0 ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_primitives::bytecode::Bytecode::Eof",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "debug_tuple_field1_finish",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "Eof" |); __self_0 ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => 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_Bytecode.
  
  Module Impl_core_marker_StructuralPartialEq_for_revm_primitives_bytecode_Bytecode.
    Definition Self : Ty.t := Ty.path "revm_primitives::bytecode::Bytecode".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_revm_primitives_bytecode_Bytecode.
  
  Module Impl_core_cmp_PartialEq_for_revm_primitives_bytecode_Bytecode.
    Definition Self : Ty.t := Ty.path "revm_primitives::bytecode::Bytecode".
    
    (* 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::Bytecode" ]
                  |),
                  [ M.read (| self |) ]
                |)
              |) in
            let~ __arg1_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "revm_primitives::bytecode::Bytecode" ]
                  |),
                  [ M.read (| other |) ]
                |)
              |) in
            M.alloc (|
              LogicalOp.and (|
                BinOp.eq (| M.read (| __self_discr |), M.read (| __arg1_discr |) |),
                ltac:(M.monadic
                  (M.read (|
                    M.match_operator (|
                      M.alloc (| Value.Tuple [ M.read (| self |); M.read (| other |) ] |),
                      [
                        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 γ0_0 := M.read (| γ0_0 |) in
                            let γ2_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ0_0,
                                "revm_primitives::bytecode::Bytecode::LegacyRaw",
                                0
                              |) in
                            let __self_0 := M.alloc (| γ2_0 |) in
                            let γ0_1 := M.read (| γ0_1 |) in
                            let γ2_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ0_1,
                                "revm_primitives::bytecode::Bytecode::LegacyRaw",
                                0
                              |) in
                            let __arg1_0 := M.alloc (| γ2_0 |) in
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::cmp::PartialEq",
                                  Ty.apply
                                    (Ty.path "&")
                                    []
                                    [ Ty.path "alloy_primitives::bytes_::Bytes" ],
                                  [
                                    Ty.apply
                                      (Ty.path "&")
                                      []
                                      [ Ty.path "alloy_primitives::bytes_::Bytes" ]
                                  ],
                                  "eq",
                                  []
                                |),
                                [ __self_0; __arg1_0 ]
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                            let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                            let γ0_0 := M.read (| γ0_0 |) in
                            let γ2_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ0_0,
                                "revm_primitives::bytecode::Bytecode::LegacyAnalyzed",
                                0
                              |) in
                            let __self_0 := M.alloc (| γ2_0 |) in
                            let γ0_1 := M.read (| γ0_1 |) in
                            let γ2_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ0_1,
                                "revm_primitives::bytecode::Bytecode::LegacyAnalyzed",
                                0
                              |) in
                            let __arg1_0 := M.alloc (| γ2_0 |) in
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::cmp::PartialEq",
                                  Ty.apply
                                    (Ty.path "&")
                                    []
                                    [
                                      Ty.path
                                        "revm_primitives::bytecode::legacy::LegacyAnalyzedBytecode"
                                    ],
                                  [
                                    Ty.apply
                                      (Ty.path "&")
                                      []
                                      [
                                        Ty.path
                                          "revm_primitives::bytecode::legacy::LegacyAnalyzedBytecode"
                                      ]
                                  ],
                                  "eq",
                                  []
                                |),
                                [ __self_0; __arg1_0 ]
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                            let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                            let γ0_0 := M.read (| γ0_0 |) in
                            let γ2_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ0_0,
                                "revm_primitives::bytecode::Bytecode::Eof",
                                0
                              |) in
                            let __self_0 := M.alloc (| γ2_0 |) in
                            let γ0_1 := M.read (| γ0_1 |) in
                            let γ2_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ0_1,
                                "revm_primitives::bytecode::Bytecode::Eof",
                                0
                              |) in
                            let __arg1_0 := M.alloc (| γ2_0 |) in
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::cmp::PartialEq",
                                  Ty.apply
                                    (Ty.path "&")
                                    []
                                    [ Ty.path "revm_primitives::bytecode::eof::Eof" ],
                                  [
                                    Ty.apply
                                      (Ty.path "&")
                                      []
                                      [ Ty.path "revm_primitives::bytecode::eof::Eof" ]
                                  ],
                                  "eq",
                                  []
                                |),
                                [ __self_0; __arg1_0 ]
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (M.alloc (|
                              M.never_to_any (|
                                M.call_closure (|
                                  M.get_function (| "core::intrinsics::unreachable", [] |),
                                  []
                                |)
                              |)
                            |)))
                      ]
                    |)
                  |)))
              |)
            |)
          |)))
      | _, _, _ => 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_Bytecode.
  
  Module Impl_core_cmp_Eq_for_revm_primitives_bytecode_Bytecode.
    Definition Self : Ty.t := Ty.path "revm_primitives::bytecode::Bytecode".
    
    (* 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_Bytecode.
  
  Module Impl_core_hash_Hash_for_revm_primitives_bytecode_Bytecode.
    Definition Self : Ty.t := Ty.path "revm_primitives::bytecode::Bytecode".
    
    (* 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::Bytecode" ]
                  |),
                  [ M.read (| self |) ]
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (| "core::hash::Hash", Ty.path "isize", [], "hash", [ __H ] |),
                  [ __self_discr; M.read (| state |) ]
                |)
              |) in
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_primitives::bytecode::Bytecode::LegacyRaw",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::hash::Hash",
                          Ty.path "alloy_primitives::bytes_::Bytes",
                          [],
                          "hash",
                          [ __H ]
                        |),
                        [ M.read (| __self_0 |); M.read (| state |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_primitives::bytecode::Bytecode::LegacyAnalyzed",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::hash::Hash",
                          Ty.path "revm_primitives::bytecode::legacy::LegacyAnalyzedBytecode",
                          [],
                          "hash",
                          [ __H ]
                        |),
                        [ M.read (| __self_0 |); M.read (| state |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_primitives::bytecode::Bytecode::Eof",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::hash::Hash",
                          Ty.path "revm_primitives::bytecode::eof::Eof",
                          [],
                          "hash",
                          [ __H ]
                        |),
                        [ M.read (| __self_0 |); 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_Bytecode.
  
  Module Impl_core_default_Default_for_revm_primitives_bytecode_Bytecode.
    Definition Self : Ty.t := Ty.path "revm_primitives::bytecode::Bytecode".
    
    (*
        fn default() -> Self {
            // Creates a new legacy analyzed [`Bytecode`] with exactly one STOP opcode.
            Self::new()
        }
    *)
    Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (M.call_closure (|
            M.get_associated_function (|
              Ty.path "revm_primitives::bytecode::Bytecode",
              "new",
              []
            |),
            []
          |)))
      | _, _, _ => 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_Bytecode.
  
  Module Impl_revm_primitives_bytecode_Bytecode.
    Definition Self : Ty.t := Ty.path "revm_primitives::bytecode::Bytecode".
    
    (*
        pub fn new() -> Self {
            Self::LegacyAnalyzed(LegacyAnalyzedBytecode::default())
        }
    *)
    Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.StructTuple
            "revm_primitives::bytecode::Bytecode::LegacyAnalyzed"
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.path "revm_primitives::bytecode::legacy::LegacyAnalyzedBytecode",
                  [],
                  "default",
                  []
                |),
                []
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
    
    (*
        pub fn legacy_jump_table(&self) -> Option<&JumpTable> {
            match &self {
                Self::LegacyAnalyzed(analyzed) => Some(analyzed.jump_table()),
                _ => None,
            }
        }
    *)
    Definition legacy_jump_table (ε : 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 (|
              M.alloc (| self |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ := M.read (| γ |) in
                    let γ2_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_primitives::bytecode::Bytecode::LegacyAnalyzed",
                        0
                      |) in
                    let analyzed := M.alloc (| γ2_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::option::Option::Some"
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "revm_primitives::bytecode::legacy::LegacyAnalyzedBytecode",
                              "jump_table",
                              []
                            |),
                            [ M.read (| analyzed |) ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_legacy_jump_table :
      M.IsAssociatedFunction Self "legacy_jump_table" legacy_jump_table.
    
    (*
        pub fn hash_slow(&self) -> B256 {
            if self.is_empty() {
                KECCAK_EMPTY
            } else {
                keccak256(self.original_byte_slice())
            }
        }
    *)
    Definition hash_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 (|
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "revm_primitives::bytecode::Bytecode",
                              "is_empty",
                              []
                            |),
                            [ M.read (| self |) ]
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.get_constant (| "revm_primitives::utilities::KECCAK_EMPTY" |)));
                fun γ =>
                  ltac:(M.monadic
                    (M.alloc (|
                      M.call_closure (|
                        M.get_function (|
                          "alloy_primitives::utils::keccak256",
                          [
                            Ty.apply
                              (Ty.path "&")
                              []
                              [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ]
                          ]
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "revm_primitives::bytecode::Bytecode",
                              "original_byte_slice",
                              []
                            |),
                            [ M.read (| self |) ]
                          |)
                        ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_hash_slow : M.IsAssociatedFunction Self "hash_slow" hash_slow.
    
    (*
        pub const fn eof(&self) -> Option<&Eof> {
            match self {
                Self::Eof(eof) => Some(eof),
                _ => None,
            }
        }
    *)
    Definition eof (ε : 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 (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_primitives::bytecode::Bytecode::Eof",
                        0
                      |) in
                    let eof := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      Value.StructTuple "core::option::Option::Some" [ M.read (| eof |) ]
                    |)));
                fun γ =>
                  ltac:(M.monadic (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_eof : M.IsAssociatedFunction Self "eof" eof.
    
    (*
        pub const fn is_eof(&self) -> bool {
            matches!(self, Self::Eof(_))
        }
    *)
    Definition is_eof (ε : 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 (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_primitives::bytecode::Bytecode::Eof",
                        0
                      |) in
                    M.alloc (| Value.Bool true |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_eof : M.IsAssociatedFunction Self "is_eof" is_eof.
    
    (*
        pub fn new_raw(bytecode: Bytes) -> Self {
            Self::LegacyRaw(bytecode)
        }
    *)
    Definition new_raw (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ bytecode ] =>
        ltac:(M.monadic
          (let bytecode := M.alloc (| bytecode |) in
          Value.StructTuple
            "revm_primitives::bytecode::Bytecode::LegacyRaw"
            [ M.read (| bytecode |) ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_new_raw : M.IsAssociatedFunction Self "new_raw" new_raw.
    
    (*
        pub unsafe fn new_analyzed(
            bytecode: Bytes,
            original_len: usize,
            jump_table: JumpTable,
        ) -> Self {
            Self::LegacyAnalyzed(LegacyAnalyzedBytecode::new(
                bytecode,
                original_len,
                jump_table,
            ))
        }
    *)
    Definition new_analyzed (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ bytecode; original_len; jump_table ] =>
        ltac:(M.monadic
          (let bytecode := M.alloc (| bytecode |) in
          let original_len := M.alloc (| original_len |) in
          let jump_table := M.alloc (| jump_table |) in
          Value.StructTuple
            "revm_primitives::bytecode::Bytecode::LegacyAnalyzed"
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "revm_primitives::bytecode::legacy::LegacyAnalyzedBytecode",
                  "new",
                  []
                |),
                [ M.read (| bytecode |); M.read (| original_len |); M.read (| jump_table |) ]
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_new_analyzed : M.IsAssociatedFunction Self "new_analyzed" new_analyzed.
    
    (*
        pub fn bytecode(&self) -> &Bytes {
            match self {
                Self::LegacyRaw(bytes) => bytes,
                Self::LegacyAnalyzed(analyzed) => analyzed.bytecode(),
                Self::Eof(eof) => eof
                    .body
                    .code(0)
                    .expect("Valid EOF has at least one code section"),
            }
        }
    *)
    Definition bytecode (ε : 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 (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_primitives::bytecode::Bytecode::LegacyRaw",
                        0
                      |) in
                    let bytes := M.alloc (| γ1_0 |) in
                    M.alloc (| M.read (| bytes |) |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_primitives::bytecode::Bytecode::LegacyAnalyzed",
                        0
                      |) in
                    let analyzed := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "revm_primitives::bytecode::legacy::LegacyAnalyzedBytecode",
                          "bytecode",
                          []
                        |),
                        [ M.read (| analyzed |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_primitives::bytecode::Bytecode::Eof",
                        0
                      |) in
                    let eof := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "core::option::Option")
                            []
                            [
                              Ty.apply
                                (Ty.path "&")
                                []
                                [ Ty.path "alloy_primitives::bytes_::Bytes" ]
                            ],
                          "expect",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "revm_primitives::bytecode::eof::body::EofBody",
                              "code",
                              []
                            |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| eof |),
                                "revm_primitives::bytecode::eof::Eof",
                                "body"
                              |);
                              Value.Integer IntegerKind.Usize 0
                            ]
                          |);
                          M.read (| Value.String "Valid EOF has at least one code section" |)
                        ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_bytecode : M.IsAssociatedFunction Self "bytecode" bytecode.
    
    (*
        pub fn is_execution_ready(&self) -> bool {
            !matches!(self, Self::LegacyRaw(_))
        }
    *)
    Definition is_execution_ready (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          UnOp.not (|
            M.read (|
              M.match_operator (|
                self,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let γ1_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "revm_primitives::bytecode::Bytecode::LegacyRaw",
                          0
                        |) in
                      M.alloc (| Value.Bool true |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
                ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_execution_ready :
      M.IsAssociatedFunction Self "is_execution_ready" is_execution_ready.
    
    (*
        pub fn original_bytes(&self) -> Bytes {
            match self {
                Self::LegacyRaw(bytes) => bytes.clone(),
                Self::LegacyAnalyzed(analyzed) => analyzed.original_bytes(),
                Self::Eof(eof) => eof.raw().clone(),
            }
        }
    *)
    Definition original_bytes (ε : 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 (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_primitives::bytecode::Bytecode::LegacyRaw",
                        0
                      |) in
                    let bytes := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::clone::Clone",
                          Ty.path "alloy_primitives::bytes_::Bytes",
                          [],
                          "clone",
                          []
                        |),
                        [ M.read (| bytes |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_primitives::bytecode::Bytecode::LegacyAnalyzed",
                        0
                      |) in
                    let analyzed := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "revm_primitives::bytecode::legacy::LegacyAnalyzedBytecode",
                          "original_bytes",
                          []
                        |),
                        [ M.read (| analyzed |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_primitives::bytecode::Bytecode::Eof",
                        0
                      |) in
                    let eof := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::clone::Clone",
                          Ty.path "alloy_primitives::bytes_::Bytes",
                          [],
                          "clone",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "revm_primitives::bytecode::eof::Eof",
                              "raw",
                              []
                            |),
                            [ M.read (| eof |) ]
                          |)
                        ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_original_bytes :
      M.IsAssociatedFunction Self "original_bytes" original_bytes.
    
    (*
        pub fn original_byte_slice(&self) -> &[u8] {
            match self {
                Self::LegacyRaw(bytes) => bytes,
                Self::LegacyAnalyzed(analyzed) => analyzed.original_byte_slice(),
                Self::Eof(eof) => eof.raw(),
            }
        }
    *)
    Definition original_byte_slice (ε : 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 (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_primitives::bytecode::Bytecode::LegacyRaw",
                        0
                      |) in
                    let bytes := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      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.read (| bytes |) ]
                          |)
                        ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_primitives::bytecode::Bytecode::LegacyAnalyzed",
                        0
                      |) in
                    let analyzed := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "revm_primitives::bytecode::legacy::LegacyAnalyzedBytecode",
                          "original_byte_slice",
                          []
                        |),
                        [ M.read (| analyzed |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_primitives::bytecode::Bytecode::Eof",
                        0
                      |) in
                    let eof := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      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.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "revm_primitives::bytecode::eof::Eof",
                                  "raw",
                                  []
                                |),
                                [ M.read (| eof |) ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_original_byte_slice :
      M.IsAssociatedFunction Self "original_byte_slice" original_byte_slice.
    
    (*
        pub fn len(&self) -> usize {
            match self {
                Self::LegacyRaw(bytes) => bytes.len(),
                Self::LegacyAnalyzed(analyzed) => analyzed.original_len(),
                Self::Eof(eof) => eof.size(),
            }
        }
    *)
    Definition len (ε : 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 (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_primitives::bytecode::Bytecode::LegacyRaw",
                        0
                      |) in
                    let bytes := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (| Ty.path "bytes::bytes::Bytes", "len", [] |),
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::deref::Deref",
                              Ty.path "alloy_primitives::bytes_::Bytes",
                              [],
                              "deref",
                              []
                            |),
                            [ M.read (| bytes |) ]
                          |)
                        ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_primitives::bytecode::Bytecode::LegacyAnalyzed",
                        0
                      |) in
                    let analyzed := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "revm_primitives::bytecode::legacy::LegacyAnalyzedBytecode",
                          "original_len",
                          []
                        |),
                        [ M.read (| analyzed |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_primitives::bytecode::Bytecode::Eof",
                        0
                      |) in
                    let eof := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "revm_primitives::bytecode::eof::Eof",
                          "size",
                          []
                        |),
                        [ M.read (| eof |) ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_len : M.IsAssociatedFunction Self "len" len.
    
    (*
        pub fn is_empty(&self) -> bool {
            self.len() == 0
        }
    *)
    Definition is_empty (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          BinOp.eq (|
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "revm_primitives::bytecode::Bytecode",
                "len",
                []
              |),
              [ M.read (| self |) ]
            |),
            Value.Integer IntegerKind.Usize 0
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_empty : M.IsAssociatedFunction Self "is_empty" is_empty.
  End Impl_revm_primitives_bytecode_Bytecode.
End bytecode.
