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

Module instruction_result.
  (*
  Enum InstructionResult
  {
    const_params := [];
    ty_params := [];
    variants :=
      [
        {
          name := "Continue";
          item := StructTuple [];
          discriminant := Some 0;
        };
        {
          name := "Stop";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "Return";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "SelfDestruct";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "ReturnContract";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "Revert";
          item := StructTuple [];
          discriminant := Some 16;
        };
        {
          name := "CallTooDeep";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "OutOfFunds";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "CallOrCreate";
          item := StructTuple [];
          discriminant := Some 32;
        };
        {
          name := "OutOfGas";
          item := StructTuple [];
          discriminant := Some 80;
        };
        {
          name := "MemoryOOG";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "MemoryLimitOOG";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "PrecompileOOG";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "InvalidOperandOOG";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "OpcodeNotFound";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "CallNotAllowedInsideStatic";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "StateChangeDuringStaticCall";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "InvalidFEOpcode";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "InvalidJump";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "NotActivated";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "StackUnderflow";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "StackOverflow";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "OutOfOffset";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "CreateCollision";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "OverflowPayment";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "PrecompileError";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "NonceOverflow";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "CreateContractSizeLimit";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "CreateContractStartingWithEF";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "CreateInitCodeSizeLimit";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "FatalExternalError";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "ReturnContractInNotInitEOF";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "EOFOpcodeDisabledInLegacy";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "EOFFunctionStackOverflow";
          item := StructTuple [];
          discriminant := None;
        }
      ];
  }
  *)
  
  Module Impl_core_clone_Clone_for_revm_interpreter_instruction_result_InstructionResult.
    Definition Self : Ty.t := Ty.path "revm_interpreter::instruction_result::InstructionResult".
    
    (* 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_interpreter_instruction_result_InstructionResult.
  
  Module Impl_core_marker_Copy_for_revm_interpreter_instruction_result_InstructionResult.
    Definition Self : Ty.t := Ty.path "revm_interpreter::instruction_result::InstructionResult".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::Copy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_for_revm_interpreter_instruction_result_InstructionResult.
  
  Module Impl_core_fmt_Debug_for_revm_interpreter_instruction_result_InstructionResult.
    Definition Self : Ty.t := Ty.path "revm_interpreter::instruction_result::InstructionResult".
    
    (* 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_interpreter::instruction_result::InstructionResult::Continue"
                          |) in
                        M.alloc (| M.read (| Value.String "Continue" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_interpreter::instruction_result::InstructionResult::Stop"
                          |) in
                        M.alloc (| M.read (| Value.String "Stop" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_interpreter::instruction_result::InstructionResult::Return"
                          |) in
                        M.alloc (| M.read (| Value.String "Return" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_interpreter::instruction_result::InstructionResult::SelfDestruct"
                          |) in
                        M.alloc (| M.read (| Value.String "SelfDestruct" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_interpreter::instruction_result::InstructionResult::ReturnContract"
                          |) in
                        M.alloc (| M.read (| Value.String "ReturnContract" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_interpreter::instruction_result::InstructionResult::Revert"
                          |) in
                        M.alloc (| M.read (| Value.String "Revert" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_interpreter::instruction_result::InstructionResult::CallTooDeep"
                          |) in
                        M.alloc (| M.read (| Value.String "CallTooDeep" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_interpreter::instruction_result::InstructionResult::OutOfFunds"
                          |) in
                        M.alloc (| M.read (| Value.String "OutOfFunds" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_interpreter::instruction_result::InstructionResult::CallOrCreate"
                          |) in
                        M.alloc (| M.read (| Value.String "CallOrCreate" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_interpreter::instruction_result::InstructionResult::OutOfGas"
                          |) in
                        M.alloc (| M.read (| Value.String "OutOfGas" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_interpreter::instruction_result::InstructionResult::MemoryOOG"
                          |) in
                        M.alloc (| M.read (| Value.String "MemoryOOG" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_interpreter::instruction_result::InstructionResult::MemoryLimitOOG"
                          |) in
                        M.alloc (| M.read (| Value.String "MemoryLimitOOG" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_interpreter::instruction_result::InstructionResult::PrecompileOOG"
                          |) in
                        M.alloc (| M.read (| Value.String "PrecompileOOG" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_interpreter::instruction_result::InstructionResult::InvalidOperandOOG"
                          |) in
                        M.alloc (| M.read (| Value.String "InvalidOperandOOG" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_interpreter::instruction_result::InstructionResult::OpcodeNotFound"
                          |) in
                        M.alloc (| M.read (| Value.String "OpcodeNotFound" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_interpreter::instruction_result::InstructionResult::CallNotAllowedInsideStatic"
                          |) in
                        M.alloc (| M.read (| Value.String "CallNotAllowedInsideStatic" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_interpreter::instruction_result::InstructionResult::StateChangeDuringStaticCall"
                          |) in
                        M.alloc (| M.read (| Value.String "StateChangeDuringStaticCall" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_interpreter::instruction_result::InstructionResult::InvalidFEOpcode"
                          |) in
                        M.alloc (| M.read (| Value.String "InvalidFEOpcode" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_interpreter::instruction_result::InstructionResult::InvalidJump"
                          |) in
                        M.alloc (| M.read (| Value.String "InvalidJump" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_interpreter::instruction_result::InstructionResult::NotActivated"
                          |) in
                        M.alloc (| M.read (| Value.String "NotActivated" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_interpreter::instruction_result::InstructionResult::StackUnderflow"
                          |) in
                        M.alloc (| M.read (| Value.String "StackUnderflow" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_interpreter::instruction_result::InstructionResult::StackOverflow"
                          |) in
                        M.alloc (| M.read (| Value.String "StackOverflow" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_interpreter::instruction_result::InstructionResult::OutOfOffset"
                          |) in
                        M.alloc (| M.read (| Value.String "OutOfOffset" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_interpreter::instruction_result::InstructionResult::CreateCollision"
                          |) in
                        M.alloc (| M.read (| Value.String "CreateCollision" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_interpreter::instruction_result::InstructionResult::OverflowPayment"
                          |) in
                        M.alloc (| M.read (| Value.String "OverflowPayment" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_interpreter::instruction_result::InstructionResult::PrecompileError"
                          |) in
                        M.alloc (| M.read (| Value.String "PrecompileError" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_interpreter::instruction_result::InstructionResult::NonceOverflow"
                          |) in
                        M.alloc (| M.read (| Value.String "NonceOverflow" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_interpreter::instruction_result::InstructionResult::CreateContractSizeLimit"
                          |) in
                        M.alloc (| M.read (| Value.String "CreateContractSizeLimit" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_interpreter::instruction_result::InstructionResult::CreateContractStartingWithEF"
                          |) in
                        M.alloc (| M.read (| Value.String "CreateContractStartingWithEF" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_interpreter::instruction_result::InstructionResult::CreateInitCodeSizeLimit"
                          |) in
                        M.alloc (| M.read (| Value.String "CreateInitCodeSizeLimit" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_interpreter::instruction_result::InstructionResult::FatalExternalError"
                          |) in
                        M.alloc (| M.read (| Value.String "FatalExternalError" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_interpreter::instruction_result::InstructionResult::ReturnContractInNotInitEOF"
                          |) in
                        M.alloc (| M.read (| Value.String "ReturnContractInNotInitEOF" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_interpreter::instruction_result::InstructionResult::EOFOpcodeDisabledInLegacy"
                          |) in
                        M.alloc (| M.read (| Value.String "EOFOpcodeDisabledInLegacy" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_interpreter::instruction_result::InstructionResult::EOFFunctionStackOverflow"
                          |) in
                        M.alloc (| M.read (| Value.String "EOFFunctionStackOverflow" |) |)))
                  ]
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::fmt::Debug"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
  End Impl_core_fmt_Debug_for_revm_interpreter_instruction_result_InstructionResult.
  
  Module Impl_core_default_Default_for_revm_interpreter_instruction_result_InstructionResult.
    Definition Self : Ty.t := Ty.path "revm_interpreter::instruction_result::InstructionResult".
    
    (* Default *)
    Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.StructTuple
            "revm_interpreter::instruction_result::InstructionResult::Continue"
            []))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::default::Default"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method default) ].
  End Impl_core_default_Default_for_revm_interpreter_instruction_result_InstructionResult.
  
  Module Impl_core_marker_StructuralPartialEq_for_revm_interpreter_instruction_result_InstructionResult.
    Definition Self : Ty.t := Ty.path "revm_interpreter::instruction_result::InstructionResult".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_revm_interpreter_instruction_result_InstructionResult.
  
  Module Impl_core_cmp_PartialEq_for_revm_interpreter_instruction_result_InstructionResult.
    Definition Self : Ty.t := Ty.path "revm_interpreter::instruction_result::InstructionResult".
    
    (* 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_interpreter::instruction_result::InstructionResult" ]
                  |),
                  [ M.read (| self |) ]
                |)
              |) in
            let~ __arg1_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "revm_interpreter::instruction_result::InstructionResult" ]
                  |),
                  [ 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_interpreter_instruction_result_InstructionResult.
  
  Module Impl_core_cmp_Eq_for_revm_interpreter_instruction_result_InstructionResult.
    Definition Self : Ty.t := Ty.path "revm_interpreter::instruction_result::InstructionResult".
    
    (* 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_interpreter_instruction_result_InstructionResult.
  
  Module Impl_core_hash_Hash_for_revm_interpreter_instruction_result_InstructionResult.
    Definition Self : Ty.t := Ty.path "revm_interpreter::instruction_result::InstructionResult".
    
    (* 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_interpreter::instruction_result::InstructionResult" ]
                  |),
                  [ M.read (| self |) ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (| "core::hash::Hash", Ty.path "u8", [], "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_interpreter_instruction_result_InstructionResult.
  
  Module Impl_core_convert_From_revm_primitives_result_SuccessReason_for_revm_interpreter_instruction_result_InstructionResult.
    Definition Self : Ty.t := Ty.path "revm_interpreter::instruction_result::InstructionResult".
    
    (*
        fn from(value: SuccessReason) -> Self {
            match value {
                SuccessReason::Return => InstructionResult::Return,
                SuccessReason::Stop => InstructionResult::Stop,
                SuccessReason::SelfDestruct => InstructionResult::SelfDestruct,
            }
        }
    *)
    Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ value ] =>
        ltac:(M.monadic
          (let value := M.alloc (| value |) in
          M.read (|
            M.match_operator (|
              value,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (| γ, "revm_primitives::result::SuccessReason::Return" |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::InstructionResult::Return"
                        []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (| γ, "revm_primitives::result::SuccessReason::Stop" |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::InstructionResult::Stop"
                        []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::result::SuccessReason::SelfDestruct"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::InstructionResult::SelfDestruct"
                        []
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::convert::From"
        Self
        (* Trait polymorphic types *) [ (* T *) Ty.path "revm_primitives::result::SuccessReason" ]
        (* Instance *) [ ("from", InstanceField.Method from) ].
  End Impl_core_convert_From_revm_primitives_result_SuccessReason_for_revm_interpreter_instruction_result_InstructionResult.
  
  Module Impl_core_convert_From_revm_primitives_result_HaltReason_for_revm_interpreter_instruction_result_InstructionResult.
    Definition Self : Ty.t := Ty.path "revm_interpreter::instruction_result::InstructionResult".
    
    (*
        fn from(value: HaltReason) -> Self {
            match value {
                HaltReason::OutOfGas(error) => match error {
                    OutOfGasError::Basic => Self::OutOfGas,
                    OutOfGasError::InvalidOperand => Self::InvalidOperandOOG,
                    OutOfGasError::Memory => Self::MemoryOOG,
                    OutOfGasError::MemoryLimit => Self::MemoryLimitOOG,
                    OutOfGasError::Precompile => Self::PrecompileOOG,
                },
                HaltReason::OpcodeNotFound => Self::OpcodeNotFound,
                HaltReason::InvalidFEOpcode => Self::InvalidFEOpcode,
                HaltReason::InvalidJump => Self::InvalidJump,
                HaltReason::NotActivated => Self::NotActivated,
                HaltReason::StackOverflow => Self::StackOverflow,
                HaltReason::StackUnderflow => Self::StackUnderflow,
                HaltReason::OutOfOffset => Self::OutOfOffset,
                HaltReason::CreateCollision => Self::CreateCollision,
                HaltReason::PrecompileError => Self::PrecompileError,
                HaltReason::NonceOverflow => Self::NonceOverflow,
                HaltReason::CreateContractSizeLimit => Self::CreateContractSizeLimit,
                HaltReason::CreateContractStartingWithEF => Self::CreateContractStartingWithEF,
                HaltReason::CreateInitCodeSizeLimit => Self::CreateInitCodeSizeLimit,
                HaltReason::OverflowPayment => Self::OverflowPayment,
                HaltReason::StateChangeDuringStaticCall => Self::StateChangeDuringStaticCall,
                HaltReason::CallNotAllowedInsideStatic => Self::CallNotAllowedInsideStatic,
                HaltReason::OutOfFunds => Self::OutOfFunds,
                HaltReason::CallTooDeep => Self::CallTooDeep,
                #[cfg(feature = "optimism")]
                HaltReason::FailedDeposit => Self::FatalExternalError,
            }
        }
    *)
    Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ value ] =>
        ltac:(M.monadic
          (let value := M.alloc (| value |) in
          M.read (|
            M.match_operator (|
              value,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_primitives::result::HaltReason::OutOfGas",
                        0
                      |) in
                    let error := M.copy (| γ0_0 |) in
                    M.match_operator (|
                      error,
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_primitives::result::OutOfGasError::Basic"
                              |) in
                            M.alloc (|
                              Value.StructTuple
                                "revm_interpreter::instruction_result::InstructionResult::OutOfGas"
                                []
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_primitives::result::OutOfGasError::InvalidOperand"
                              |) in
                            M.alloc (|
                              Value.StructTuple
                                "revm_interpreter::instruction_result::InstructionResult::InvalidOperandOOG"
                                []
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_primitives::result::OutOfGasError::Memory"
                              |) in
                            M.alloc (|
                              Value.StructTuple
                                "revm_interpreter::instruction_result::InstructionResult::MemoryOOG"
                                []
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_primitives::result::OutOfGasError::MemoryLimit"
                              |) in
                            M.alloc (|
                              Value.StructTuple
                                "revm_interpreter::instruction_result::InstructionResult::MemoryLimitOOG"
                                []
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_primitives::result::OutOfGasError::Precompile"
                              |) in
                            M.alloc (|
                              Value.StructTuple
                                "revm_interpreter::instruction_result::InstructionResult::PrecompileOOG"
                                []
                            |)))
                      ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::result::HaltReason::OpcodeNotFound"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::InstructionResult::OpcodeNotFound"
                        []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::result::HaltReason::InvalidFEOpcode"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::InstructionResult::InvalidFEOpcode"
                        []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::result::HaltReason::InvalidJump"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::InstructionResult::InvalidJump"
                        []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::result::HaltReason::NotActivated"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::InstructionResult::NotActivated"
                        []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::result::HaltReason::StackOverflow"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::InstructionResult::StackOverflow"
                        []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::result::HaltReason::StackUnderflow"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::InstructionResult::StackUnderflow"
                        []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::result::HaltReason::OutOfOffset"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::InstructionResult::OutOfOffset"
                        []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::result::HaltReason::CreateCollision"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::InstructionResult::CreateCollision"
                        []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::result::HaltReason::PrecompileError"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::InstructionResult::PrecompileError"
                        []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::result::HaltReason::NonceOverflow"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::InstructionResult::NonceOverflow"
                        []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::result::HaltReason::CreateContractSizeLimit"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::InstructionResult::CreateContractSizeLimit"
                        []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::result::HaltReason::CreateContractStartingWithEF"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::InstructionResult::CreateContractStartingWithEF"
                        []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::result::HaltReason::CreateInitCodeSizeLimit"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::InstructionResult::CreateInitCodeSizeLimit"
                        []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::result::HaltReason::OverflowPayment"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::InstructionResult::OverflowPayment"
                        []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::result::HaltReason::StateChangeDuringStaticCall"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::InstructionResult::StateChangeDuringStaticCall"
                        []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::result::HaltReason::CallNotAllowedInsideStatic"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::InstructionResult::CallNotAllowedInsideStatic"
                        []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::result::HaltReason::OutOfFunds"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::InstructionResult::OutOfFunds"
                        []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::result::HaltReason::CallTooDeep"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::InstructionResult::CallTooDeep"
                        []
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::convert::From"
        Self
        (* Trait polymorphic types *) [ (* T *) Ty.path "revm_primitives::result::HaltReason" ]
        (* Instance *) [ ("from", InstanceField.Method from) ].
  End Impl_core_convert_From_revm_primitives_result_HaltReason_for_revm_interpreter_instruction_result_InstructionResult.
  
  Module Impl_revm_interpreter_instruction_result_InstructionResult.
    Definition Self : Ty.t := Ty.path "revm_interpreter::instruction_result::InstructionResult".
    
    (*
        pub const fn is_ok(self) -> bool {
            matches!(self, crate::return_ok!())
        }
    *)
    Definition is_ok (ε : 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
                    (M.find_or_pattern (|
                      γ,
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_interpreter::instruction_result::InstructionResult::Continue"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_interpreter::instruction_result::InstructionResult::Stop"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_interpreter::instruction_result::InstructionResult::Return"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_interpreter::instruction_result::InstructionResult::SelfDestruct"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_interpreter::instruction_result::InstructionResult::ReturnContract"
                              |) in
                            Value.Tuple []))
                      ],
                      M.closure
                        (fun γ =>
                          ltac:(M.monadic
                            match γ with
                            | [] => ltac:(M.monadic (M.alloc (| Value.Bool true |)))
                            | _ => M.impossible "wrong number of arguments"
                            end))
                    |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_ok : M.IsAssociatedFunction Self "is_ok" is_ok.
    
    (*
        pub const fn is_revert(self) -> bool {
            matches!(self, crate::return_revert!())
        }
    *)
    Definition is_revert (ε : 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
                    (M.find_or_pattern (|
                      γ,
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_interpreter::instruction_result::InstructionResult::Revert"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_interpreter::instruction_result::InstructionResult::CallTooDeep"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_interpreter::instruction_result::InstructionResult::OutOfFunds"
                              |) in
                            Value.Tuple []))
                      ],
                      M.closure
                        (fun γ =>
                          ltac:(M.monadic
                            match γ with
                            | [] => ltac:(M.monadic (M.alloc (| Value.Bool true |)))
                            | _ => M.impossible "wrong number of arguments"
                            end))
                    |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_revert : M.IsAssociatedFunction Self "is_revert" is_revert.
    
    (*
        pub const fn is_error(self) -> bool {
            matches!(self, return_error!())
        }
    *)
    Definition is_error (ε : 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
                    (M.find_or_pattern (|
                      γ,
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_interpreter::instruction_result::InstructionResult::OutOfGas"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_interpreter::instruction_result::InstructionResult::MemoryOOG"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_interpreter::instruction_result::InstructionResult::MemoryLimitOOG"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_interpreter::instruction_result::InstructionResult::PrecompileOOG"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_interpreter::instruction_result::InstructionResult::InvalidOperandOOG"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_interpreter::instruction_result::InstructionResult::OpcodeNotFound"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_interpreter::instruction_result::InstructionResult::CallNotAllowedInsideStatic"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_interpreter::instruction_result::InstructionResult::StateChangeDuringStaticCall"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_interpreter::instruction_result::InstructionResult::InvalidFEOpcode"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_interpreter::instruction_result::InstructionResult::InvalidJump"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_interpreter::instruction_result::InstructionResult::NotActivated"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_interpreter::instruction_result::InstructionResult::StackUnderflow"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_interpreter::instruction_result::InstructionResult::StackOverflow"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_interpreter::instruction_result::InstructionResult::OutOfOffset"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_interpreter::instruction_result::InstructionResult::CreateCollision"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_interpreter::instruction_result::InstructionResult::OverflowPayment"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_interpreter::instruction_result::InstructionResult::PrecompileError"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_interpreter::instruction_result::InstructionResult::NonceOverflow"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_interpreter::instruction_result::InstructionResult::CreateContractSizeLimit"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_interpreter::instruction_result::InstructionResult::CreateContractStartingWithEF"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_interpreter::instruction_result::InstructionResult::CreateInitCodeSizeLimit"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_interpreter::instruction_result::InstructionResult::FatalExternalError"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_interpreter::instruction_result::InstructionResult::ReturnContractInNotInitEOF"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_interpreter::instruction_result::InstructionResult::EOFOpcodeDisabledInLegacy"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_interpreter::instruction_result::InstructionResult::EOFFunctionStackOverflow"
                              |) in
                            Value.Tuple []))
                      ],
                      M.closure
                        (fun γ =>
                          ltac:(M.monadic
                            match γ with
                            | [] => ltac:(M.monadic (M.alloc (| Value.Bool true |)))
                            | _ => M.impossible "wrong number of arguments"
                            end))
                    |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_error : M.IsAssociatedFunction Self "is_error" is_error.
  End Impl_revm_interpreter_instruction_result_InstructionResult.
  
  (*
  Enum SuccessOrHalt
  {
    const_params := [];
    ty_params := [];
    variants :=
      [
        {
          name := "Success";
          item := StructTuple [ Ty.path "revm_primitives::result::SuccessReason" ];
          discriminant := None;
        };
        {
          name := "Revert";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "Halt";
          item := StructTuple [ Ty.path "revm_primitives::result::HaltReason" ];
          discriminant := None;
        };
        {
          name := "FatalExternalError";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "InternalContinue";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "InternalCallOrCreate";
          item := StructTuple [];
          discriminant := None;
        }
      ];
  }
  *)
  
  Module Impl_core_fmt_Debug_for_revm_interpreter_instruction_result_SuccessOrHalt.
    Definition Self : Ty.t := Ty.path "revm_interpreter::instruction_result::SuccessOrHalt".
    
    (* 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_interpreter::instruction_result::SuccessOrHalt::Success",
                        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 "Success" |); __self_0 ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_interpreter::instruction_result::SuccessOrHalt::Revert"
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_str",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "Revert" |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_interpreter::instruction_result::SuccessOrHalt::Halt",
                        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 "Halt" |); __self_0 ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_interpreter::instruction_result::SuccessOrHalt::FatalExternalError"
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_str",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "FatalExternalError" |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_interpreter::instruction_result::SuccessOrHalt::InternalContinue"
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_str",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "InternalContinue" |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_interpreter::instruction_result::SuccessOrHalt::InternalCallOrCreate"
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_str",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "InternalCallOrCreate" |) ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::fmt::Debug"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
  End Impl_core_fmt_Debug_for_revm_interpreter_instruction_result_SuccessOrHalt.
  
  Module Impl_core_marker_Copy_for_revm_interpreter_instruction_result_SuccessOrHalt.
    Definition Self : Ty.t := Ty.path "revm_interpreter::instruction_result::SuccessOrHalt".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::Copy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_for_revm_interpreter_instruction_result_SuccessOrHalt.
  
  Module Impl_core_clone_Clone_for_revm_interpreter_instruction_result_SuccessOrHalt.
    Definition Self : Ty.t := Ty.path "revm_interpreter::instruction_result::SuccessOrHalt".
    
    (* 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 (|
              Value.DeclaredButUndefined,
              [
                fun γ =>
                  ltac:(M.monadic
                    (M.match_operator (|
                      Value.DeclaredButUndefined,
                      [ fun γ => ltac:(M.monadic (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_interpreter_instruction_result_SuccessOrHalt.
  
  Module Impl_core_marker_StructuralPartialEq_for_revm_interpreter_instruction_result_SuccessOrHalt.
    Definition Self : Ty.t := Ty.path "revm_interpreter::instruction_result::SuccessOrHalt".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_revm_interpreter_instruction_result_SuccessOrHalt.
  
  Module Impl_core_cmp_PartialEq_for_revm_interpreter_instruction_result_SuccessOrHalt.
    Definition Self : Ty.t := Ty.path "revm_interpreter::instruction_result::SuccessOrHalt".
    
    (* 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_interpreter::instruction_result::SuccessOrHalt" ]
                  |),
                  [ M.read (| self |) ]
                |)
              |) in
            let~ __arg1_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "revm_interpreter::instruction_result::SuccessOrHalt" ]
                  |),
                  [ 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_interpreter::instruction_result::SuccessOrHalt::Success",
                                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_interpreter::instruction_result::SuccessOrHalt::Success",
                                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::result::SuccessReason" ],
                                  [
                                    Ty.apply
                                      (Ty.path "&")
                                      []
                                      [ Ty.path "revm_primitives::result::SuccessReason" ]
                                  ],
                                  "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_interpreter::instruction_result::SuccessOrHalt::Halt",
                                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_interpreter::instruction_result::SuccessOrHalt::Halt",
                                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::result::HaltReason" ],
                                  [
                                    Ty.apply
                                      (Ty.path "&")
                                      []
                                      [ Ty.path "revm_primitives::result::HaltReason" ]
                                  ],
                                  "eq",
                                  []
                                |),
                                [ __self_0; __arg1_0 ]
                              |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Bool true |)))
                      ]
                    |)
                  |)))
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::PartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("eq", InstanceField.Method eq) ].
  End Impl_core_cmp_PartialEq_for_revm_interpreter_instruction_result_SuccessOrHalt.
  
  Module Impl_core_cmp_Eq_for_revm_interpreter_instruction_result_SuccessOrHalt.
    Definition Self : Ty.t := Ty.path "revm_interpreter::instruction_result::SuccessOrHalt".
    
    (* 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.alloc (| Value.Tuple [] |))) ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::Eq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *)
        [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
  End Impl_core_cmp_Eq_for_revm_interpreter_instruction_result_SuccessOrHalt.
  
  Module Impl_core_hash_Hash_for_revm_interpreter_instruction_result_SuccessOrHalt.
    Definition Self : Ty.t := Ty.path "revm_interpreter::instruction_result::SuccessOrHalt".
    
    (* 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_interpreter::instruction_result::SuccessOrHalt" ]
                  |),
                  [ 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_interpreter::instruction_result::SuccessOrHalt::Success",
                        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::result::SuccessReason",
                          [],
                          "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_interpreter::instruction_result::SuccessOrHalt::Halt",
                        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::result::HaltReason",
                          [],
                          "hash",
                          [ __H ]
                        |),
                        [ M.read (| __self_0 |); M.read (| state |) ]
                      |)
                    |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
              ]
            |)
          |)))
      | _, _, _ => 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_interpreter_instruction_result_SuccessOrHalt.
  
  Module Impl_revm_interpreter_instruction_result_SuccessOrHalt.
    Definition Self : Ty.t := Ty.path "revm_interpreter::instruction_result::SuccessOrHalt".
    
    (*
        pub fn is_success(self) -> bool {
            matches!(self, SuccessOrHalt::Success(_))
        }
    *)
    Definition is_success (ε : 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 γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_interpreter::instruction_result::SuccessOrHalt::Success",
                        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_success : M.IsAssociatedFunction Self "is_success" is_success.
    
    (*
        pub fn to_success(self) -> Option<SuccessReason> {
            match self {
                SuccessOrHalt::Success(reason) => Some(reason),
                _ => None,
            }
        }
    *)
    Definition to_success (ε : 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 γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_interpreter::instruction_result::SuccessOrHalt::Success",
                        0
                      |) in
                    let reason := M.copy (| γ0_0 |) in
                    M.alloc (|
                      Value.StructTuple "core::option::Option::Some" [ M.read (| reason |) ]
                    |)));
                fun γ =>
                  ltac:(M.monadic (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_to_success : M.IsAssociatedFunction Self "to_success" to_success.
    
    (*
        pub fn is_revert(self) -> bool {
            matches!(self, SuccessOrHalt::Revert)
        }
    *)
    Definition is_revert (ε : 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.is_struct_tuple (|
                        γ,
                        "revm_interpreter::instruction_result::SuccessOrHalt::Revert"
                      |) 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_revert : M.IsAssociatedFunction Self "is_revert" is_revert.
    
    (*
        pub fn is_halt(self) -> bool {
            matches!(self, SuccessOrHalt::Halt(_))
        }
    *)
    Definition is_halt (ε : 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 γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_interpreter::instruction_result::SuccessOrHalt::Halt",
                        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_halt : M.IsAssociatedFunction Self "is_halt" is_halt.
    
    (*
        pub fn to_halt(self) -> Option<HaltReason> {
            match self {
                SuccessOrHalt::Halt(reason) => Some(reason),
                _ => None,
            }
        }
    *)
    Definition to_halt (ε : 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 γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_interpreter::instruction_result::SuccessOrHalt::Halt",
                        0
                      |) in
                    let reason := M.copy (| γ0_0 |) in
                    M.alloc (|
                      Value.StructTuple "core::option::Option::Some" [ M.read (| reason |) ]
                    |)));
                fun γ =>
                  ltac:(M.monadic (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_to_halt : M.IsAssociatedFunction Self "to_halt" to_halt.
  End Impl_revm_interpreter_instruction_result_SuccessOrHalt.
  
  Module Impl_core_convert_From_revm_interpreter_instruction_result_InstructionResult_for_revm_interpreter_instruction_result_SuccessOrHalt.
    Definition Self : Ty.t := Ty.path "revm_interpreter::instruction_result::SuccessOrHalt".
    
    (*
        fn from(result: InstructionResult) -> Self {
            match result {
                InstructionResult::Continue => Self::InternalContinue, // used only in interpreter loop
                InstructionResult::Stop => Self::Success(SuccessReason::Stop),
                InstructionResult::Return => Self::Success(SuccessReason::Return),
                InstructionResult::SelfDestruct => Self::Success(SuccessReason::SelfDestruct),
                InstructionResult::Revert => Self::Revert,
                InstructionResult::CallOrCreate => Self::InternalCallOrCreate, // used only in interpreter loop
                InstructionResult::CallTooDeep => Self::Halt(HaltReason::CallTooDeep), // not gonna happen for first call
                InstructionResult::OutOfFunds => Self::Halt(HaltReason::OutOfFunds), // Check for first call is done separately.
                InstructionResult::OutOfGas => Self::Halt(HaltReason::OutOfGas(OutOfGasError::Basic)),
                InstructionResult::MemoryLimitOOG => {
                    Self::Halt(HaltReason::OutOfGas(OutOfGasError::MemoryLimit))
                }
                InstructionResult::MemoryOOG => Self::Halt(HaltReason::OutOfGas(OutOfGasError::Memory)),
                InstructionResult::PrecompileOOG => {
                    Self::Halt(HaltReason::OutOfGas(OutOfGasError::Precompile))
                }
                InstructionResult::InvalidOperandOOG => {
                    Self::Halt(HaltReason::OutOfGas(OutOfGasError::InvalidOperand))
                }
                InstructionResult::OpcodeNotFound | InstructionResult::ReturnContractInNotInitEOF => {
                    Self::Halt(HaltReason::OpcodeNotFound)
                }
                InstructionResult::CallNotAllowedInsideStatic => {
                    Self::Halt(HaltReason::CallNotAllowedInsideStatic)
                } // first call is not static call
                InstructionResult::StateChangeDuringStaticCall => {
                    Self::Halt(HaltReason::StateChangeDuringStaticCall)
                }
                InstructionResult::InvalidFEOpcode => Self::Halt(HaltReason::InvalidFEOpcode),
                InstructionResult::InvalidJump => Self::Halt(HaltReason::InvalidJump),
                InstructionResult::NotActivated => Self::Halt(HaltReason::NotActivated),
                InstructionResult::StackUnderflow => Self::Halt(HaltReason::StackUnderflow),
                InstructionResult::StackOverflow => Self::Halt(HaltReason::StackOverflow),
                InstructionResult::OutOfOffset => Self::Halt(HaltReason::OutOfOffset),
                InstructionResult::CreateCollision => Self::Halt(HaltReason::CreateCollision),
                InstructionResult::OverflowPayment => Self::Halt(HaltReason::OverflowPayment), // Check for first call is done separately.
                InstructionResult::PrecompileError => Self::Halt(HaltReason::PrecompileError),
                InstructionResult::NonceOverflow => Self::Halt(HaltReason::NonceOverflow),
                InstructionResult::CreateContractSizeLimit
                | InstructionResult::CreateContractStartingWithEF => {
                    Self::Halt(HaltReason::CreateContractSizeLimit)
                }
                InstructionResult::CreateInitCodeSizeLimit => {
                    Self::Halt(HaltReason::CreateInitCodeSizeLimit)
                }
                InstructionResult::FatalExternalError => Self::FatalExternalError,
                InstructionResult::EOFOpcodeDisabledInLegacy => Self::Halt(HaltReason::OpcodeNotFound),
                InstructionResult::EOFFunctionStackOverflow => Self::FatalExternalError,
                InstructionResult::ReturnContract => {
                    panic!("Unexpected EOF internal Return Contract")
                }
            }
        }
    *)
    Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ result ] =>
        ltac:(M.monadic
          (let result := M.alloc (| result |) in
          M.read (|
            M.match_operator (|
              result,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_interpreter::instruction_result::InstructionResult::Continue"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::SuccessOrHalt::InternalContinue"
                        []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_interpreter::instruction_result::InstructionResult::Stop"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::SuccessOrHalt::Success"
                        [ Value.StructTuple "revm_primitives::result::SuccessReason::Stop" [] ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_interpreter::instruction_result::InstructionResult::Return"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::SuccessOrHalt::Success"
                        [ Value.StructTuple "revm_primitives::result::SuccessReason::Return" [] ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_interpreter::instruction_result::InstructionResult::SelfDestruct"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::SuccessOrHalt::Success"
                        [
                          Value.StructTuple
                            "revm_primitives::result::SuccessReason::SelfDestruct"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_interpreter::instruction_result::InstructionResult::Revert"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::SuccessOrHalt::Revert"
                        []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_interpreter::instruction_result::InstructionResult::CallOrCreate"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::SuccessOrHalt::InternalCallOrCreate"
                        []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_interpreter::instruction_result::InstructionResult::CallTooDeep"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::SuccessOrHalt::Halt"
                        [ Value.StructTuple "revm_primitives::result::HaltReason::CallTooDeep" [] ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_interpreter::instruction_result::InstructionResult::OutOfFunds"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::SuccessOrHalt::Halt"
                        [ Value.StructTuple "revm_primitives::result::HaltReason::OutOfFunds" [] ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_interpreter::instruction_result::InstructionResult::OutOfGas"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::SuccessOrHalt::Halt"
                        [
                          Value.StructTuple
                            "revm_primitives::result::HaltReason::OutOfGas"
                            [ Value.StructTuple "revm_primitives::result::OutOfGasError::Basic" [] ]
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_interpreter::instruction_result::InstructionResult::MemoryLimitOOG"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::SuccessOrHalt::Halt"
                        [
                          Value.StructTuple
                            "revm_primitives::result::HaltReason::OutOfGas"
                            [
                              Value.StructTuple
                                "revm_primitives::result::OutOfGasError::MemoryLimit"
                                []
                            ]
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_interpreter::instruction_result::InstructionResult::MemoryOOG"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::SuccessOrHalt::Halt"
                        [
                          Value.StructTuple
                            "revm_primitives::result::HaltReason::OutOfGas"
                            [ Value.StructTuple "revm_primitives::result::OutOfGasError::Memory" []
                            ]
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_interpreter::instruction_result::InstructionResult::PrecompileOOG"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::SuccessOrHalt::Halt"
                        [
                          Value.StructTuple
                            "revm_primitives::result::HaltReason::OutOfGas"
                            [
                              Value.StructTuple
                                "revm_primitives::result::OutOfGasError::Precompile"
                                []
                            ]
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_interpreter::instruction_result::InstructionResult::InvalidOperandOOG"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::SuccessOrHalt::Halt"
                        [
                          Value.StructTuple
                            "revm_primitives::result::HaltReason::OutOfGas"
                            [
                              Value.StructTuple
                                "revm_primitives::result::OutOfGasError::InvalidOperand"
                                []
                            ]
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (M.find_or_pattern (|
                      γ,
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_interpreter::instruction_result::InstructionResult::OpcodeNotFound"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_interpreter::instruction_result::InstructionResult::ReturnContractInNotInitEOF"
                              |) in
                            Value.Tuple []))
                      ],
                      M.closure
                        (fun γ =>
                          ltac:(M.monadic
                            match γ with
                            | [] =>
                              ltac:(M.monadic
                                (M.alloc (|
                                  Value.StructTuple
                                    "revm_interpreter::instruction_result::SuccessOrHalt::Halt"
                                    [
                                      Value.StructTuple
                                        "revm_primitives::result::HaltReason::OpcodeNotFound"
                                        []
                                    ]
                                |)))
                            | _ => M.impossible "wrong number of arguments"
                            end))
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_interpreter::instruction_result::InstructionResult::CallNotAllowedInsideStatic"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::SuccessOrHalt::Halt"
                        [
                          Value.StructTuple
                            "revm_primitives::result::HaltReason::CallNotAllowedInsideStatic"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_interpreter::instruction_result::InstructionResult::StateChangeDuringStaticCall"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::SuccessOrHalt::Halt"
                        [
                          Value.StructTuple
                            "revm_primitives::result::HaltReason::StateChangeDuringStaticCall"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_interpreter::instruction_result::InstructionResult::InvalidFEOpcode"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::SuccessOrHalt::Halt"
                        [
                          Value.StructTuple
                            "revm_primitives::result::HaltReason::InvalidFEOpcode"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_interpreter::instruction_result::InstructionResult::InvalidJump"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::SuccessOrHalt::Halt"
                        [ Value.StructTuple "revm_primitives::result::HaltReason::InvalidJump" [] ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_interpreter::instruction_result::InstructionResult::NotActivated"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::SuccessOrHalt::Halt"
                        [ Value.StructTuple "revm_primitives::result::HaltReason::NotActivated" [] ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_interpreter::instruction_result::InstructionResult::StackUnderflow"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::SuccessOrHalt::Halt"
                        [ Value.StructTuple "revm_primitives::result::HaltReason::StackUnderflow" []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_interpreter::instruction_result::InstructionResult::StackOverflow"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::SuccessOrHalt::Halt"
                        [ Value.StructTuple "revm_primitives::result::HaltReason::StackOverflow" []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_interpreter::instruction_result::InstructionResult::OutOfOffset"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::SuccessOrHalt::Halt"
                        [ Value.StructTuple "revm_primitives::result::HaltReason::OutOfOffset" [] ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_interpreter::instruction_result::InstructionResult::CreateCollision"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::SuccessOrHalt::Halt"
                        [
                          Value.StructTuple
                            "revm_primitives::result::HaltReason::CreateCollision"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_interpreter::instruction_result::InstructionResult::OverflowPayment"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::SuccessOrHalt::Halt"
                        [
                          Value.StructTuple
                            "revm_primitives::result::HaltReason::OverflowPayment"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_interpreter::instruction_result::InstructionResult::PrecompileError"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::SuccessOrHalt::Halt"
                        [
                          Value.StructTuple
                            "revm_primitives::result::HaltReason::PrecompileError"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_interpreter::instruction_result::InstructionResult::NonceOverflow"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::SuccessOrHalt::Halt"
                        [ Value.StructTuple "revm_primitives::result::HaltReason::NonceOverflow" []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (M.find_or_pattern (|
                      γ,
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_interpreter::instruction_result::InstructionResult::CreateContractSizeLimit"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm_interpreter::instruction_result::InstructionResult::CreateContractStartingWithEF"
                              |) in
                            Value.Tuple []))
                      ],
                      M.closure
                        (fun γ =>
                          ltac:(M.monadic
                            match γ with
                            | [] =>
                              ltac:(M.monadic
                                (M.alloc (|
                                  Value.StructTuple
                                    "revm_interpreter::instruction_result::SuccessOrHalt::Halt"
                                    [
                                      Value.StructTuple
                                        "revm_primitives::result::HaltReason::CreateContractSizeLimit"
                                        []
                                    ]
                                |)))
                            | _ => M.impossible "wrong number of arguments"
                            end))
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_interpreter::instruction_result::InstructionResult::CreateInitCodeSizeLimit"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::SuccessOrHalt::Halt"
                        [
                          Value.StructTuple
                            "revm_primitives::result::HaltReason::CreateInitCodeSizeLimit"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_interpreter::instruction_result::InstructionResult::FatalExternalError"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::SuccessOrHalt::FatalExternalError"
                        []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_interpreter::instruction_result::InstructionResult::EOFOpcodeDisabledInLegacy"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::SuccessOrHalt::Halt"
                        [ Value.StructTuple "revm_primitives::result::HaltReason::OpcodeNotFound" []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_interpreter::instruction_result::InstructionResult::EOFFunctionStackOverflow"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_interpreter::instruction_result::SuccessOrHalt::FatalExternalError"
                        []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_interpreter::instruction_result::InstructionResult::ReturnContract"
                      |) in
                    M.alloc (|
                      M.never_to_any (|
                        M.call_closure (|
                          M.get_function (| "core::panicking::panic_fmt", [] |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::Arguments",
                                "new_const",
                                []
                              |),
                              [
                                M.alloc (|
                                  Value.Array
                                    [
                                      M.read (|
                                        Value.String "Unexpected EOF internal Return Contract"
                                      |)
                                    ]
                                |)
                              ]
                            |)
                          ]
                        |)
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::convert::From"
        Self
        (* Trait polymorphic types *)
        [ (* T *) Ty.path "revm_interpreter::instruction_result::InstructionResult" ]
        (* Instance *) [ ("from", InstanceField.Method from) ].
  End Impl_core_convert_From_revm_interpreter_instruction_result_InstructionResult_for_revm_interpreter_instruction_result_SuccessOrHalt.
End instruction_result.
