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

Module bytecode.
  Module legacy.
    (* StructRecord
      {
        name := "LegacyAnalyzedBytecode";
        const_params := [];
        ty_params := [];
        fields :=
          [
            ("bytecode", Ty.path "alloy_primitives::bytes_::Bytes");
            ("original_len", Ty.path "usize");
            ("jump_table", Ty.path "revm_primitives::bytecode::legacy::jump_map::JumpTable")
          ];
      } *)
    
    Module Impl_core_clone_Clone_for_revm_primitives_bytecode_legacy_LegacyAnalyzedBytecode.
      Definition Self : Ty.t := Ty.path "revm_primitives::bytecode::legacy::LegacyAnalyzedBytecode".
      
      (* 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::legacy::LegacyAnalyzedBytecode"
              [
                ("bytecode",
                  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::legacy::LegacyAnalyzedBytecode",
                        "bytecode"
                      |)
                    ]
                  |));
                ("original_len",
                  M.call_closure (|
                    M.get_trait_method (| "core::clone::Clone", Ty.path "usize", [], "clone", [] |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_primitives::bytecode::legacy::LegacyAnalyzedBytecode",
                        "original_len"
                      |)
                    ]
                  |));
                ("jump_table",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::clone::Clone",
                      Ty.path "revm_primitives::bytecode::legacy::jump_map::JumpTable",
                      [],
                      "clone",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_primitives::bytecode::legacy::LegacyAnalyzedBytecode",
                        "jump_table"
                      |)
                    ]
                  |))
              ]))
        | _, _, _ => 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_legacy_LegacyAnalyzedBytecode.
    
    Module Impl_core_fmt_Debug_for_revm_primitives_bytecode_legacy_LegacyAnalyzedBytecode.
      Definition Self : Ty.t := Ty.path "revm_primitives::bytecode::legacy::LegacyAnalyzedBytecode".
      
      (* 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 "LegacyAnalyzedBytecode" |);
                M.read (| Value.String "bytecode" |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm_primitives::bytecode::legacy::LegacyAnalyzedBytecode",
                  "bytecode"
                |);
                M.read (| Value.String "original_len" |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm_primitives::bytecode::legacy::LegacyAnalyzedBytecode",
                  "original_len"
                |);
                M.read (| Value.String "jump_table" |);
                M.alloc (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_primitives::bytecode::legacy::LegacyAnalyzedBytecode",
                    "jump_table"
                  |)
                |)
              ]
            |)))
        | _, _, _ => 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_legacy_LegacyAnalyzedBytecode.
    
    Module Impl_core_marker_StructuralPartialEq_for_revm_primitives_bytecode_legacy_LegacyAnalyzedBytecode.
      Definition Self : Ty.t := Ty.path "revm_primitives::bytecode::legacy::LegacyAnalyzedBytecode".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_revm_primitives_bytecode_legacy_LegacyAnalyzedBytecode.
    
    Module Impl_core_cmp_PartialEq_for_revm_primitives_bytecode_legacy_LegacyAnalyzedBytecode.
      Definition Self : Ty.t := Ty.path "revm_primitives::bytecode::legacy::LegacyAnalyzedBytecode".
      
      (* 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 "alloy_primitives::bytes_::Bytes",
                    [ Ty.path "alloy_primitives::bytes_::Bytes" ],
                    "eq",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::bytecode::legacy::LegacyAnalyzedBytecode",
                      "bytecode"
                    |);
                    M.SubPointer.get_struct_record_field (|
                      M.read (| other |),
                      "revm_primitives::bytecode::legacy::LegacyAnalyzedBytecode",
                      "bytecode"
                    |)
                  ]
                |),
                ltac:(M.monadic
                  (BinOp.eq (|
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_primitives::bytecode::legacy::LegacyAnalyzedBytecode",
                        "original_len"
                      |)
                    |),
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| other |),
                        "revm_primitives::bytecode::legacy::LegacyAnalyzedBytecode",
                        "original_len"
                      |)
                    |)
                  |)))
              |),
              ltac:(M.monadic
                (M.call_closure (|
                  M.get_trait_method (|
                    "core::cmp::PartialEq",
                    Ty.path "revm_primitives::bytecode::legacy::jump_map::JumpTable",
                    [ Ty.path "revm_primitives::bytecode::legacy::jump_map::JumpTable" ],
                    "eq",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::bytecode::legacy::LegacyAnalyzedBytecode",
                      "jump_table"
                    |);
                    M.SubPointer.get_struct_record_field (|
                      M.read (| other |),
                      "revm_primitives::bytecode::legacy::LegacyAnalyzedBytecode",
                      "jump_table"
                    |)
                  ]
                |)))
            |)))
        | _, _, _ => 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_legacy_LegacyAnalyzedBytecode.
    
    Module Impl_core_cmp_Eq_for_revm_primitives_bytecode_legacy_LegacyAnalyzedBytecode.
      Definition Self : Ty.t := Ty.path "revm_primitives::bytecode::legacy::LegacyAnalyzedBytecode".
      
      (* 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_legacy_LegacyAnalyzedBytecode.
    
    Module Impl_core_hash_Hash_for_revm_primitives_bytecode_legacy_LegacyAnalyzedBytecode.
      Definition Self : Ty.t := Ty.path "revm_primitives::bytecode::legacy::LegacyAnalyzedBytecode".
      
      (* 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 "alloy_primitives::bytes_::Bytes",
                      [],
                      "hash",
                      [ __H ]
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_primitives::bytecode::legacy::LegacyAnalyzedBytecode",
                        "bytecode"
                      |);
                      M.read (| state |)
                    ]
                  |)
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::hash::Hash",
                      Ty.path "usize",
                      [],
                      "hash",
                      [ __H ]
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_primitives::bytecode::legacy::LegacyAnalyzedBytecode",
                        "original_len"
                      |);
                      M.read (| state |)
                    ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::hash::Hash",
                    Ty.path "revm_primitives::bytecode::legacy::jump_map::JumpTable",
                    [],
                    "hash",
                    [ __H ]
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::bytecode::legacy::LegacyAnalyzedBytecode",
                      "jump_table"
                    |);
                    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_legacy_LegacyAnalyzedBytecode.
    
    Module Impl_core_default_Default_for_revm_primitives_bytecode_legacy_LegacyAnalyzedBytecode.
      Definition Self : Ty.t := Ty.path "revm_primitives::bytecode::legacy::LegacyAnalyzedBytecode".
      
      (*
          fn default() -> Self {
              Self {
                  bytecode: Bytes::from_static(&[0]),
                  original_len: 0,
                  jump_table: JumpTable(Arc::new(bitvec![u8, Lsb0; 0])),
              }
          }
      *)
      Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [] =>
          ltac:(M.monadic
            (Value.StructRecord
              "revm_primitives::bytecode::legacy::LegacyAnalyzedBytecode"
              [
                ("bytecode",
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "alloy_primitives::bytes_::Bytes",
                      "from_static",
                      []
                    |),
                    [ M.alloc (| Value.Array [ Value.Integer IntegerKind.U8 0 ] |) ]
                  |));
                ("original_len", Value.Integer IntegerKind.Usize 0);
                ("jump_table",
                  Value.StructTuple
                    "revm_primitives::bytecode::legacy::jump_map::JumpTable"
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "alloc::sync::Arc")
                            []
                            [
                              Ty.apply
                                (Ty.path "bitvec::vec::BitVec")
                                []
                                [ Ty.path "u8"; Ty.path "bitvec::order::Lsb0" ];
                              Ty.path "alloc::alloc::Global"
                            ],
                          "new",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "bitvec::vec::BitVec")
                                []
                                [ Ty.path "u8"; Ty.path "bitvec::order::Lsb0" ],
                              "from_bitslice",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::ops::index::Index",
                                  Ty.apply
                                    (Ty.path "bitvec::array::BitArray")
                                    []
                                    [
                                      Ty.apply
                                        (Ty.path "array")
                                        [ Value.Integer IntegerKind.Usize 1 ]
                                        [ Ty.path "u8" ];
                                      Ty.path "bitvec::order::Lsb0"
                                    ],
                                  [
                                    Ty.apply
                                      (Ty.path "core::ops::range::RangeTo")
                                      []
                                      [ Ty.path "usize" ]
                                  ],
                                  "index",
                                  []
                                |),
                                [
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "bitvec::array::BitArray")
                                          []
                                          [
                                            Ty.apply
                                              (Ty.path "array")
                                              [ Value.Integer IntegerKind.Usize 1 ]
                                              [ Ty.path "u8" ];
                                            Ty.path "bitvec::order::Lsb0"
                                          ],
                                        "new",
                                        []
                                      |),
                                      [
                                        Value.Array
                                          [
                                            M.read (|
                                              M.SubPointer.get_struct_record_field (|
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.apply
                                                        (Ty.path "bitvec::mem::BitElement")
                                                        []
                                                        [ Ty.path "u8" ],
                                                      "new",
                                                      []
                                                    |),
                                                    [
                                                      M.read (|
                                                        M.get_constant (|
                                                          "revm_primitives::bytecode::legacy::default::ELEM"
                                                        |)
                                                      |)
                                                    ]
                                                  |)
                                                |),
                                                "bitvec::mem::BitElement",
                                                "elem"
                                              |)
                                            |)
                                          ]
                                      ]
                                    |)
                                  |);
                                  Value.StructRecord
                                    "core::ops::range::RangeTo"
                                    [
                                      ("end_",
                                        M.read (|
                                          M.get_constant (|
                                            "revm_primitives::bytecode::legacy::default::BITS"
                                          |)
                                        |))
                                    ]
                                ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    ])
              ]))
        | _, _, _ => 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_legacy_LegacyAnalyzedBytecode.
    
    Module Impl_revm_primitives_bytecode_legacy_LegacyAnalyzedBytecode.
      Definition Self : Ty.t := Ty.path "revm_primitives::bytecode::legacy::LegacyAnalyzedBytecode".
      
      (*
          pub fn new(bytecode: Bytes, original_len: usize, jump_table: JumpTable) -> Self {
              Self {
                  bytecode,
                  original_len,
                  jump_table,
              }
          }
      *)
      Definition new (ε : 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.StructRecord
              "revm_primitives::bytecode::legacy::LegacyAnalyzedBytecode"
              [
                ("bytecode", M.read (| bytecode |));
                ("original_len", M.read (| original_len |));
                ("jump_table", M.read (| jump_table |))
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
      
      (*
          pub fn bytecode(&self) -> &Bytes {
              &self.bytecode
          }
      *)
      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.SubPointer.get_struct_record_field (|
              M.read (| self |),
              "revm_primitives::bytecode::legacy::LegacyAnalyzedBytecode",
              "bytecode"
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_bytecode : M.IsAssociatedFunction Self "bytecode" bytecode.
      
      (*
          pub fn original_len(&self) -> usize {
              self.original_len
          }
      *)
      Definition original_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.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "revm_primitives::bytecode::legacy::LegacyAnalyzedBytecode",
                "original_len"
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_original_len :
        M.IsAssociatedFunction Self "original_len" original_len.
      
      (*
          pub fn original_bytes(&self) -> Bytes {
              self.bytecode.slice(..self.original_len)
          }
      *)
      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.call_closure (|
              M.get_associated_function (|
                Ty.path "alloy_primitives::bytes_::Bytes",
                "slice",
                [ Ty.apply (Ty.path "core::ops::range::RangeTo") [] [ Ty.path "usize" ] ]
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm_primitives::bytecode::legacy::LegacyAnalyzedBytecode",
                  "bytecode"
                |);
                Value.StructRecord
                  "core::ops::range::RangeTo"
                  [
                    ("end_",
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm_primitives::bytecode::legacy::LegacyAnalyzedBytecode",
                          "original_len"
                        |)
                      |))
                  ]
              ]
            |)))
        | _, _, _ => 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] {
              &self.bytecode[..self.original_len]
          }
      *)
      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.call_closure (|
              M.get_trait_method (|
                "core::ops::index::Index",
                Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                [ Ty.apply (Ty.path "core::ops::range::RangeTo") [] [ Ty.path "usize" ] ],
                "index",
                []
              |),
              [
                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.read (| self |),
                          "revm_primitives::bytecode::legacy::LegacyAnalyzedBytecode",
                          "bytecode"
                        |)
                      ]
                    |)
                  ]
                |);
                Value.StructRecord
                  "core::ops::range::RangeTo"
                  [
                    ("end_",
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm_primitives::bytecode::legacy::LegacyAnalyzedBytecode",
                          "original_len"
                        |)
                      |))
                  ]
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_original_byte_slice :
        M.IsAssociatedFunction Self "original_byte_slice" original_byte_slice.
      
      (*
          pub fn jump_table(&self) -> &JumpTable {
              &self.jump_table
          }
      *)
      Definition 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.SubPointer.get_struct_record_field (|
              M.read (| self |),
              "revm_primitives::bytecode::legacy::LegacyAnalyzedBytecode",
              "jump_table"
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_jump_table : M.IsAssociatedFunction Self "jump_table" jump_table.
    End Impl_revm_primitives_bytecode_legacy_LegacyAnalyzedBytecode.
  End legacy.
End bytecode.
