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

Module instructions.
  Module i256.
    (*
    Enum Sign
    {
      const_params := [];
      ty_params := [];
      variants :=
        [
          {
            name := "Minus";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "Zero";
            item := StructTuple [];
            discriminant := Some 0;
          };
          {
            name := "Plus";
            item := StructTuple [];
            discriminant := Some 1;
          }
        ];
    }
    *)
    
    Module Impl_core_clone_Clone_for_revm_interpreter_instructions_i256_Sign.
      Definition Self : Ty.t := Ty.path "revm_interpreter::instructions::i256::Sign".
      
      (* 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_instructions_i256_Sign.
    
    Module Impl_core_marker_Copy_for_revm_interpreter_instructions_i256_Sign.
      Definition Self : Ty.t := Ty.path "revm_interpreter::instructions::i256::Sign".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::Copy"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Copy_for_revm_interpreter_instructions_i256_Sign.
    
    Module Impl_core_fmt_Debug_for_revm_interpreter_instructions_i256_Sign.
      Definition Self : Ty.t := Ty.path "revm_interpreter::instructions::i256::Sign".
      
      (* 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::instructions::i256::Sign::Minus"
                            |) in
                          M.alloc (| M.read (| Value.String "Minus" |) |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_interpreter::instructions::i256::Sign::Zero"
                            |) in
                          M.alloc (| M.read (| Value.String "Zero" |) |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_interpreter::instructions::i256::Sign::Plus"
                            |) in
                          M.alloc (| M.read (| Value.String "Plus" |) |)))
                    ]
                  |)
                |)
              ]
            |)))
        | _, _, _ => 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_instructions_i256_Sign.
    
    Module Impl_core_marker_StructuralPartialEq_for_revm_interpreter_instructions_i256_Sign.
      Definition Self : Ty.t := Ty.path "revm_interpreter::instructions::i256::Sign".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_revm_interpreter_instructions_i256_Sign.
    
    Module Impl_core_cmp_PartialEq_for_revm_interpreter_instructions_i256_Sign.
      Definition Self : Ty.t := Ty.path "revm_interpreter::instructions::i256::Sign".
      
      (* 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::instructions::i256::Sign" ]
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              let~ __arg1_discr :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::discriminant_value",
                      [ Ty.path "revm_interpreter::instructions::i256::Sign" ]
                    |),
                    [ 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_instructions_i256_Sign.
    
    Module Impl_core_cmp_Eq_for_revm_interpreter_instructions_i256_Sign.
      Definition Self : Ty.t := Ty.path "revm_interpreter::instructions::i256::Sign".
      
      (* 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_instructions_i256_Sign.
    
    Module Impl_core_cmp_PartialOrd_for_revm_interpreter_instructions_i256_Sign.
      Definition Self : Ty.t := Ty.path "revm_interpreter::instructions::i256::Sign".
      
      (* PartialOrd *)
      Definition partial_cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let~ __self_discr :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::discriminant_value",
                      [ Ty.path "revm_interpreter::instructions::i256::Sign" ]
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              let~ __arg1_discr :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::discriminant_value",
                      [ Ty.path "revm_interpreter::instructions::i256::Sign" ]
                    |),
                    [ M.read (| other |) ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::cmp::PartialOrd",
                    Ty.path "i8",
                    [ Ty.path "i8" ],
                    "partial_cmp",
                    []
                  |),
                  [ __self_discr; __arg1_discr ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("partial_cmp", InstanceField.Method partial_cmp) ].
    End Impl_core_cmp_PartialOrd_for_revm_interpreter_instructions_i256_Sign.
    
    Module Impl_core_cmp_Ord_for_revm_interpreter_instructions_i256_Sign.
      Definition Self : Ty.t := Ty.path "revm_interpreter::instructions::i256::Sign".
      
      (* Ord *)
      Definition cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let~ __self_discr :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::discriminant_value",
                      [ Ty.path "revm_interpreter::instructions::i256::Sign" ]
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              let~ __arg1_discr :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::discriminant_value",
                      [ Ty.path "revm_interpreter::instructions::i256::Sign" ]
                    |),
                    [ M.read (| other |) ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (| "core::cmp::Ord", Ty.path "i8", [], "cmp", [] |),
                  [ __self_discr; __arg1_discr ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::Ord"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("cmp", InstanceField.Method cmp) ].
    End Impl_core_cmp_Ord_for_revm_interpreter_instructions_i256_Sign.
    
    Module Impl_core_hash_Hash_for_revm_interpreter_instructions_i256_Sign.
      Definition Self : Ty.t := Ty.path "revm_interpreter::instructions::i256::Sign".
      
      (* 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::instructions::i256::Sign" ]
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (| "core::hash::Hash", Ty.path "i8", [], "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_instructions_i256_Sign.
    
    Definition value_MAX_POSITIVE_VALUE : Value.t :=
      M.run
        ltac:(M.monadic
          (M.alloc (|
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "ruint::Uint")
                  [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                  [],
                "from_limbs",
                []
              |),
              [
                Value.Array
                  [
                    Value.Integer IntegerKind.U64 18446744073709551615;
                    Value.Integer IntegerKind.U64 18446744073709551615;
                    Value.Integer IntegerKind.U64 18446744073709551615;
                    Value.Integer IntegerKind.U64 9223372036854775807
                  ]
              ]
            |)
          |))).
    
    Definition value_MIN_NEGATIVE_VALUE : Value.t :=
      M.run
        ltac:(M.monadic
          (M.alloc (|
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "ruint::Uint")
                  [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                  [],
                "from_limbs",
                []
              |),
              [
                Value.Array
                  [
                    Value.Integer IntegerKind.U64 0;
                    Value.Integer IntegerKind.U64 0;
                    Value.Integer IntegerKind.U64 0;
                    Value.Integer IntegerKind.U64 9223372036854775808
                  ]
              ]
            |)
          |))).
    
    Definition value_FLIPH_BITMASK_U64 : Value.t :=
      M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U64 9223372036854775807 |))).
    
    (*
    pub fn i256_sign(val: &U256) -> Sign {
        if val.bit(U256::BITS - 1) {
            Sign::Minus
        } else {
            // SAFETY: false == 0 == Zero, true == 1 == Plus
            unsafe { core::mem::transmute( *val != U256::ZERO) }
        }
    }
    *)
    Definition i256_sign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ val ] =>
        ltac:(M.monadic
          (let val := M.alloc (| val |) in
          M.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "ruint::Uint")
                                [
                                  Value.Integer IntegerKind.Usize 256;
                                  Value.Integer IntegerKind.Usize 4
                                ]
                                [],
                              "bit",
                              []
                            |),
                            [
                              M.read (| val |);
                              BinOp.Wrap.sub (|
                                M.read (| M.get_constant (| "ruint::BITS'1" |) |),
                                Value.Integer IntegerKind.Usize 1
                              |)
                            ]
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (|
                      Value.StructTuple "revm_interpreter::instructions::i256::Sign::Minus" []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (M.alloc (|
                      M.call_closure (|
                        M.get_function (|
                          "core::intrinsics::transmute",
                          [ Ty.path "bool"; Ty.path "revm_interpreter::instructions::i256::Sign" ]
                        |),
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::cmp::PartialEq",
                              Ty.apply
                                (Ty.path "ruint::Uint")
                                [
                                  Value.Integer IntegerKind.Usize 256;
                                  Value.Integer IntegerKind.Usize 4
                                ]
                                [],
                              [
                                Ty.apply
                                  (Ty.path "ruint::Uint")
                                  [
                                    Value.Integer IntegerKind.Usize 256;
                                    Value.Integer IntegerKind.Usize 4
                                  ]
                                  []
                              ],
                              "ne",
                              []
                            |),
                            [ M.read (| val |); M.get_constant (| "ruint::ZERO" |) ]
                          |)
                        ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_i256_sign :
      M.IsFunction "revm_interpreter::instructions::i256::i256_sign" i256_sign.
    
    (*
    pub fn i256_sign_compl(val: &mut U256) -> Sign {
        let sign = i256_sign(val);
        if sign == Sign::Minus {
            two_compl_mut(val);
        }
        sign
    }
    *)
    Definition i256_sign_compl (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ val ] =>
        ltac:(M.monadic
          (let val := M.alloc (| val |) in
          M.read (|
            let~ sign :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (| "revm_interpreter::instructions::i256::i256_sign", [] |),
                  [ M.read (| val |) ]
                |)
              |) in
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::cmp::PartialEq",
                                Ty.path "revm_interpreter::instructions::i256::Sign",
                                [ Ty.path "revm_interpreter::instructions::i256::Sign" ],
                                "eq",
                                []
                              |),
                              [
                                sign;
                                M.alloc (|
                                  Value.StructTuple
                                    "revm_interpreter::instructions::i256::Sign::Minus"
                                    []
                                |)
                              ]
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      let~ _ :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_function (|
                              "revm_interpreter::instructions::i256::two_compl_mut",
                              []
                            |),
                            [ M.read (| val |) ]
                          |)
                        |) in
                      M.alloc (| Value.Tuple [] |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            sign
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_i256_sign_compl :
      M.IsFunction "revm_interpreter::instructions::i256::i256_sign_compl" i256_sign_compl.
    
    (*
    fn u256_remove_sign(val: &mut U256) {
        // SAFETY: U256 does not have any padding bytes
        unsafe {
            val.as_limbs_mut()[3] &= FLIPH_BITMASK_U64;
        }
    }
    *)
    Definition u256_remove_sign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ val ] =>
        ltac:(M.monadic
          (let val := M.alloc (| val |) in
          M.read (|
            let~ _ :=
              let β :=
                M.SubPointer.get_array_field (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "ruint::Uint")
                        [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                        [],
                      "as_limbs_mut",
                      []
                    |),
                    [ M.read (| val |) ]
                  |),
                  M.alloc (| Value.Integer IntegerKind.Usize 3 |)
                |) in
              M.write (|
                β,
                BinOp.bit_and
                  (M.read (| β |))
                  (M.read (|
                    M.get_constant (| "revm_interpreter::instructions::i256::FLIPH_BITMASK_U64" |)
                  |))
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_u256_remove_sign :
      M.IsFunction "revm_interpreter::instructions::i256::u256_remove_sign" u256_remove_sign.
    
    (*
    pub fn two_compl_mut(op: &mut U256) {
        *op = two_compl( *op);
    }
    *)
    Definition two_compl_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ op ] =>
        ltac:(M.monadic
          (let op := M.alloc (| op |) in
          M.read (|
            let~ _ :=
              M.write (|
                M.read (| op |),
                M.call_closure (|
                  M.get_function (| "revm_interpreter::instructions::i256::two_compl", [] |),
                  [ M.read (| M.read (| op |) |) ]
                |)
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_two_compl_mut :
      M.IsFunction "revm_interpreter::instructions::i256::two_compl_mut" two_compl_mut.
    
    (*
    pub fn two_compl(op: U256) -> U256 {
        op.wrapping_neg()
    }
    *)
    Definition two_compl (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ op ] =>
        ltac:(M.monadic
          (let op := M.alloc (| op |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply
                (Ty.path "ruint::Uint")
                [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                [],
              "wrapping_neg",
              []
            |),
            [ M.read (| op |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_two_compl :
      M.IsFunction "revm_interpreter::instructions::i256::two_compl" two_compl.
    
    (*
    pub fn i256_cmp(first: &U256, second: &U256) -> Ordering {
        let first_sign = i256_sign(first);
        let second_sign = i256_sign(second);
        match first_sign.cmp(&second_sign) {
            // note: adding `if first_sign != Sign::Zero` to short circuit zero comparisons performs
            // slower on average, as of #582
            Ordering::Equal => first.cmp(second),
            o => o,
        }
    }
    *)
    Definition i256_cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ first; second ] =>
        ltac:(M.monadic
          (let first := M.alloc (| first |) in
          let second := M.alloc (| second |) in
          M.read (|
            let~ first_sign :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (| "revm_interpreter::instructions::i256::i256_sign", [] |),
                  [ M.read (| first |) ]
                |)
              |) in
            let~ second_sign :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (| "revm_interpreter::instructions::i256::i256_sign", [] |),
                  [ M.read (| second |) ]
                |)
              |) in
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::cmp::Ord",
                    Ty.path "revm_interpreter::instructions::i256::Sign",
                    [],
                    "cmp",
                    []
                  |),
                  [ first_sign; second_sign ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::cmp::Ordering::Equal" |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::cmp::Ord",
                          Ty.apply
                            (Ty.path "ruint::Uint")
                            [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4
                            ]
                            [],
                          [],
                          "cmp",
                          []
                        |),
                        [ M.read (| first |); M.read (| second |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let o := M.copy (| γ |) in
                    o))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_i256_cmp :
      M.IsFunction "revm_interpreter::instructions::i256::i256_cmp" i256_cmp.
    
    (*
    pub fn i256_div(mut first: U256, mut second: U256) -> U256 {
        let second_sign = i256_sign_compl(&mut second);
        if second_sign == Sign::Zero {
            return U256::ZERO;
        }
    
        let first_sign = i256_sign_compl(&mut first);
        if first == MIN_NEGATIVE_VALUE && second == U256::from(1) {
            return two_compl(MIN_NEGATIVE_VALUE);
        }
    
        // necessary overflow checks are done above, perform the division
        let mut d = first / second;
    
        // set sign bit to zero
        u256_remove_sign(&mut d);
    
        // two's complement only if the signs are different
        // note: this condition has better codegen than an exhaustive match, as of #582
        if (first_sign == Sign::Minus && second_sign != Sign::Minus)
            || (second_sign == Sign::Minus && first_sign != Sign::Minus)
        {
            two_compl(d)
        } else {
            d
        }
    }
    *)
    Definition i256_div (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ first; second ] =>
        ltac:(M.monadic
          (let first := M.alloc (| first |) in
          let second := M.alloc (| second |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ second_sign :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "revm_interpreter::instructions::i256::i256_sign_compl",
                        []
                      |),
                      [ second ]
                    |)
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::cmp::PartialEq",
                                    Ty.path "revm_interpreter::instructions::i256::Sign",
                                    [ Ty.path "revm_interpreter::instructions::i256::Sign" ],
                                    "eq",
                                    []
                                  |),
                                  [
                                    second_sign;
                                    M.alloc (|
                                      Value.StructTuple
                                        "revm_interpreter::instructions::i256::Sign::Zero"
                                        []
                                    |)
                                  ]
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                M.return_ (| M.read (| M.get_constant (| "ruint::ZERO" |) |) |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ first_sign :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "revm_interpreter::instructions::i256::i256_sign_compl",
                        []
                      |),
                      [ first ]
                    |)
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                LogicalOp.and (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::cmp::PartialEq",
                                      Ty.apply
                                        (Ty.path "ruint::Uint")
                                        [
                                          Value.Integer IntegerKind.Usize 256;
                                          Value.Integer IntegerKind.Usize 4
                                        ]
                                        [],
                                      [
                                        Ty.apply
                                          (Ty.path "ruint::Uint")
                                          [
                                            Value.Integer IntegerKind.Usize 256;
                                            Value.Integer IntegerKind.Usize 4
                                          ]
                                          []
                                      ],
                                      "eq",
                                      []
                                    |),
                                    [
                                      first;
                                      M.get_constant (|
                                        "revm_interpreter::instructions::i256::MIN_NEGATIVE_VALUE"
                                      |)
                                    ]
                                  |),
                                  ltac:(M.monadic
                                    (M.call_closure (|
                                      M.get_trait_method (|
                                        "core::cmp::PartialEq",
                                        Ty.apply
                                          (Ty.path "ruint::Uint")
                                          [
                                            Value.Integer IntegerKind.Usize 256;
                                            Value.Integer IntegerKind.Usize 4
                                          ]
                                          [],
                                        [
                                          Ty.apply
                                            (Ty.path "ruint::Uint")
                                            [
                                              Value.Integer IntegerKind.Usize 256;
                                              Value.Integer IntegerKind.Usize 4
                                            ]
                                            []
                                        ],
                                        "eq",
                                        []
                                      |),
                                      [
                                        second;
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply
                                                (Ty.path "ruint::Uint")
                                                [
                                                  Value.Integer IntegerKind.Usize 256;
                                                  Value.Integer IntegerKind.Usize 4
                                                ]
                                                [],
                                              "from",
                                              [ Ty.path "i32" ]
                                            |),
                                            [ Value.Integer IntegerKind.I32 1 ]
                                          |)
                                        |)
                                      ]
                                    |)))
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                M.return_ (|
                                  M.call_closure (|
                                    M.get_function (|
                                      "revm_interpreter::instructions::i256::two_compl",
                                      []
                                    |),
                                    [
                                      M.read (|
                                        M.get_constant (|
                                          "revm_interpreter::instructions::i256::MIN_NEGATIVE_VALUE"
                                        |)
                                      |)
                                    ]
                                  |)
                                |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ d :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::arith::Div",
                        Ty.apply
                          (Ty.path "ruint::Uint")
                          [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                          [],
                        [
                          Ty.apply
                            (Ty.path "ruint::Uint")
                            [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4
                            ]
                            []
                        ],
                        "div",
                        []
                      |),
                      [ M.read (| first |); M.read (| second |) ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "revm_interpreter::instructions::i256::u256_remove_sign",
                        []
                      |),
                      [ d ]
                    |)
                  |) in
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              LogicalOp.or (|
                                LogicalOp.and (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::cmp::PartialEq",
                                      Ty.path "revm_interpreter::instructions::i256::Sign",
                                      [ Ty.path "revm_interpreter::instructions::i256::Sign" ],
                                      "eq",
                                      []
                                    |),
                                    [
                                      first_sign;
                                      M.alloc (|
                                        Value.StructTuple
                                          "revm_interpreter::instructions::i256::Sign::Minus"
                                          []
                                      |)
                                    ]
                                  |),
                                  ltac:(M.monadic
                                    (M.call_closure (|
                                      M.get_trait_method (|
                                        "core::cmp::PartialEq",
                                        Ty.path "revm_interpreter::instructions::i256::Sign",
                                        [ Ty.path "revm_interpreter::instructions::i256::Sign" ],
                                        "ne",
                                        []
                                      |),
                                      [
                                        second_sign;
                                        M.alloc (|
                                          Value.StructTuple
                                            "revm_interpreter::instructions::i256::Sign::Minus"
                                            []
                                        |)
                                      ]
                                    |)))
                                |),
                                ltac:(M.monadic
                                  (LogicalOp.and (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::cmp::PartialEq",
                                        Ty.path "revm_interpreter::instructions::i256::Sign",
                                        [ Ty.path "revm_interpreter::instructions::i256::Sign" ],
                                        "eq",
                                        []
                                      |),
                                      [
                                        second_sign;
                                        M.alloc (|
                                          Value.StructTuple
                                            "revm_interpreter::instructions::i256::Sign::Minus"
                                            []
                                        |)
                                      ]
                                    |),
                                    ltac:(M.monadic
                                      (M.call_closure (|
                                        M.get_trait_method (|
                                          "core::cmp::PartialEq",
                                          Ty.path "revm_interpreter::instructions::i256::Sign",
                                          [ Ty.path "revm_interpreter::instructions::i256::Sign" ],
                                          "ne",
                                          []
                                        |),
                                        [
                                          first_sign;
                                          M.alloc (|
                                            Value.StructTuple
                                              "revm_interpreter::instructions::i256::Sign::Minus"
                                              []
                                          |)
                                        ]
                                      |)))
                                  |)))
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_function (|
                              "revm_interpreter::instructions::i256::two_compl",
                              []
                            |),
                            [ M.read (| d |) ]
                          |)
                        |)));
                    fun γ => ltac:(M.monadic d)
                  ]
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_i256_div :
      M.IsFunction "revm_interpreter::instructions::i256::i256_div" i256_div.
    
    (*
    pub fn i256_mod(mut first: U256, mut second: U256) -> U256 {
        let first_sign = i256_sign_compl(&mut first);
        if first_sign == Sign::Zero {
            return U256::ZERO;
        }
    
        let second_sign = i256_sign_compl(&mut second);
        if second_sign == Sign::Zero {
            return U256::ZERO;
        }
    
        let mut r = first % second;
    
        // set sign bit to zero
        u256_remove_sign(&mut r);
    
        if first_sign == Sign::Minus {
            two_compl(r)
        } else {
            r
        }
    }
    *)
    Definition i256_mod (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ first; second ] =>
        ltac:(M.monadic
          (let first := M.alloc (| first |) in
          let second := M.alloc (| second |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ first_sign :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "revm_interpreter::instructions::i256::i256_sign_compl",
                        []
                      |),
                      [ first ]
                    |)
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::cmp::PartialEq",
                                    Ty.path "revm_interpreter::instructions::i256::Sign",
                                    [ Ty.path "revm_interpreter::instructions::i256::Sign" ],
                                    "eq",
                                    []
                                  |),
                                  [
                                    first_sign;
                                    M.alloc (|
                                      Value.StructTuple
                                        "revm_interpreter::instructions::i256::Sign::Zero"
                                        []
                                    |)
                                  ]
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                M.return_ (| M.read (| M.get_constant (| "ruint::ZERO" |) |) |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ second_sign :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "revm_interpreter::instructions::i256::i256_sign_compl",
                        []
                      |),
                      [ second ]
                    |)
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::cmp::PartialEq",
                                    Ty.path "revm_interpreter::instructions::i256::Sign",
                                    [ Ty.path "revm_interpreter::instructions::i256::Sign" ],
                                    "eq",
                                    []
                                  |),
                                  [
                                    second_sign;
                                    M.alloc (|
                                      Value.StructTuple
                                        "revm_interpreter::instructions::i256::Sign::Zero"
                                        []
                                    |)
                                  ]
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                M.return_ (| M.read (| M.get_constant (| "ruint::ZERO" |) |) |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ r :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::arith::Rem",
                        Ty.apply
                          (Ty.path "ruint::Uint")
                          [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                          [],
                        [
                          Ty.apply
                            (Ty.path "ruint::Uint")
                            [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4
                            ]
                            []
                        ],
                        "rem",
                        []
                      |),
                      [ M.read (| first |); M.read (| second |) ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "revm_interpreter::instructions::i256::u256_remove_sign",
                        []
                      |),
                      [ r ]
                    |)
                  |) in
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::cmp::PartialEq",
                                  Ty.path "revm_interpreter::instructions::i256::Sign",
                                  [ Ty.path "revm_interpreter::instructions::i256::Sign" ],
                                  "eq",
                                  []
                                |),
                                [
                                  first_sign;
                                  M.alloc (|
                                    Value.StructTuple
                                      "revm_interpreter::instructions::i256::Sign::Minus"
                                      []
                                  |)
                                ]
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_function (|
                              "revm_interpreter::instructions::i256::two_compl",
                              []
                            |),
                            [ M.read (| r |) ]
                          |)
                        |)));
                    fun γ => ltac:(M.monadic r)
                  ]
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_i256_mod :
      M.IsFunction "revm_interpreter::instructions::i256::i256_mod" i256_mod.
  End i256.
End instructions.
