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

(* StructTuple
  {
    name := "Choice";
    const_params := [];
    ty_params := [];
    fields := [ Ty.path "u8" ];
  } *)

Module Impl_core_marker_Copy_for_subtle_Choice.
  Definition Self : Ty.t := Ty.path "subtle::Choice".
  
  Axiom Implements :
    M.IsTraitInstance "core::marker::Copy" Self (* Trait polymorphic types *) [] (* Instance *) [].
End Impl_core_marker_Copy_for_subtle_Choice.

Module Impl_core_clone_Clone_for_subtle_Choice.
  Definition Self : Ty.t := Ty.path "subtle::Choice".
  
  (* 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.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_subtle_Choice.

Module Impl_core_fmt_Debug_for_subtle_Choice.
  Definition Self : Ty.t := Ty.path "subtle::Choice".
  
  (* Debug *)
  Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; f ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let f := M.alloc (| f |) in
        M.call_closure (|
          M.get_associated_function (|
            Ty.path "core::fmt::Formatter",
            "debug_tuple_field1_finish",
            []
          |),
          [
            M.read (| f |);
            M.read (| Value.String "Choice" |);
            M.alloc (|
              M.SubPointer.get_struct_tuple_field (| M.read (| self |), "subtle::Choice", 0 |)
            |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::fmt::Debug"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
End Impl_core_fmt_Debug_for_subtle_Choice.

Module Impl_subtle_Choice.
  Definition Self : Ty.t := Ty.path "subtle::Choice".
  
  (*
      pub fn unwrap_u8(&self) -> u8 {
          self.0
      }
  *)
  Definition unwrap_u8 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        M.read (|
          M.SubPointer.get_struct_tuple_field (| M.read (| self |), "subtle::Choice", 0 |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_unwrap_u8 : M.IsAssociatedFunction Self "unwrap_u8" unwrap_u8.
End Impl_subtle_Choice.

Module Impl_core_convert_From_subtle_Choice_for_bool.
  Definition Self : Ty.t := Ty.path "bool".
  
  (*
      fn from(source: Choice) -> bool {
          debug_assert!((source.0 == 0u8) | (source.0 == 1u8));
          source.0 != 0
      }
  *)
  Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ source ] =>
      ltac:(M.monadic
        (let source := M.alloc (| source |) in
        M.read (|
          let~ _ :=
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.use (M.alloc (| Value.Bool true |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    let~ _ :=
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.use
                                  (M.alloc (|
                                    UnOp.not (|
                                      BinOp.bit_or
                                        (BinOp.eq (|
                                          M.read (|
                                            M.SubPointer.get_struct_tuple_field (|
                                              source,
                                              "subtle::Choice",
                                              0
                                            |)
                                          |),
                                          Value.Integer IntegerKind.U8 0
                                        |))
                                        (BinOp.eq (|
                                          M.read (|
                                            M.SubPointer.get_struct_tuple_field (|
                                              source,
                                              "subtle::Choice",
                                              0
                                            |)
                                          |),
                                          Value.Integer IntegerKind.U8 1
                                        |))
                                    |)
                                  |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              M.alloc (|
                                M.never_to_any (|
                                  M.call_closure (|
                                    M.get_function (| "core::panicking::panic", [] |),
                                    [
                                      M.read (|
                                        Value.String
                                          "assertion failed: (source.0 == 0u8) | (source.0 == 1u8)"
                                      |)
                                    ]
                                  |)
                                |)
                              |)));
                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                        ]
                      |) in
                    M.alloc (| Value.Tuple [] |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
              ]
            |) in
          M.alloc (|
            BinOp.ne (|
              M.read (| M.SubPointer.get_struct_tuple_field (| source, "subtle::Choice", 0 |) |),
              Value.Integer IntegerKind.U8 0
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::convert::From"
      Self
      (* Trait polymorphic types *) [ (* T *) Ty.path "subtle::Choice" ]
      (* Instance *) [ ("from", InstanceField.Method from) ].
End Impl_core_convert_From_subtle_Choice_for_bool.

Module Impl_core_ops_bit_BitAnd_for_subtle_Choice.
  Definition Self : Ty.t := Ty.path "subtle::Choice".
  
  (*     type Output = Choice; *)
  Definition _Output : Ty.t := Ty.path "subtle::Choice".
  
  (*
      fn bitand(self, rhs: Choice) -> Choice {
          (self.0 & rhs.0).into()
      }
  *)
  Definition bitand (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; rhs ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let rhs := M.alloc (| rhs |) in
        M.call_closure (|
          M.get_trait_method (|
            "core::convert::Into",
            Ty.path "u8",
            [ Ty.path "subtle::Choice" ],
            "into",
            []
          |),
          [
            BinOp.bit_and
              (M.read (| M.SubPointer.get_struct_tuple_field (| self, "subtle::Choice", 0 |) |))
              (M.read (| M.SubPointer.get_struct_tuple_field (| rhs, "subtle::Choice", 0 |) |))
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::ops::bit::BitAnd"
      Self
      (* Trait polymorphic types *) []
      (* Instance *)
      [ ("Output", InstanceField.Ty _Output); ("bitand", InstanceField.Method bitand) ].
End Impl_core_ops_bit_BitAnd_for_subtle_Choice.

Module Impl_core_ops_bit_BitAndAssign_for_subtle_Choice.
  Definition Self : Ty.t := Ty.path "subtle::Choice".
  
  (*
      fn bitand_assign(&mut self, rhs: Choice) {
          *self = *self & rhs;
      }
  *)
  Definition bitand_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; rhs ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let rhs := M.alloc (| rhs |) in
        M.read (|
          let~ _ :=
            M.write (|
              M.read (| self |),
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::bit::BitAnd",
                  Ty.path "subtle::Choice",
                  [ Ty.path "subtle::Choice" ],
                  "bitand",
                  []
                |),
                [ M.read (| M.read (| self |) |); M.read (| rhs |) ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::ops::bit::BitAndAssign"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("bitand_assign", InstanceField.Method bitand_assign) ].
End Impl_core_ops_bit_BitAndAssign_for_subtle_Choice.

Module Impl_core_ops_bit_BitOr_for_subtle_Choice.
  Definition Self : Ty.t := Ty.path "subtle::Choice".
  
  (*     type Output = Choice; *)
  Definition _Output : Ty.t := Ty.path "subtle::Choice".
  
  (*
      fn bitor(self, rhs: Choice) -> Choice {
          (self.0 | rhs.0).into()
      }
  *)
  Definition bitor (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; rhs ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let rhs := M.alloc (| rhs |) in
        M.call_closure (|
          M.get_trait_method (|
            "core::convert::Into",
            Ty.path "u8",
            [ Ty.path "subtle::Choice" ],
            "into",
            []
          |),
          [
            BinOp.bit_or
              (M.read (| M.SubPointer.get_struct_tuple_field (| self, "subtle::Choice", 0 |) |))
              (M.read (| M.SubPointer.get_struct_tuple_field (| rhs, "subtle::Choice", 0 |) |))
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::ops::bit::BitOr"
      Self
      (* Trait polymorphic types *) []
      (* Instance *)
      [ ("Output", InstanceField.Ty _Output); ("bitor", InstanceField.Method bitor) ].
End Impl_core_ops_bit_BitOr_for_subtle_Choice.

Module Impl_core_ops_bit_BitOrAssign_for_subtle_Choice.
  Definition Self : Ty.t := Ty.path "subtle::Choice".
  
  (*
      fn bitor_assign(&mut self, rhs: Choice) {
          *self = *self | rhs;
      }
  *)
  Definition bitor_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; rhs ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let rhs := M.alloc (| rhs |) in
        M.read (|
          let~ _ :=
            M.write (|
              M.read (| self |),
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::bit::BitOr",
                  Ty.path "subtle::Choice",
                  [ Ty.path "subtle::Choice" ],
                  "bitor",
                  []
                |),
                [ M.read (| M.read (| self |) |); M.read (| rhs |) ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::ops::bit::BitOrAssign"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("bitor_assign", InstanceField.Method bitor_assign) ].
End Impl_core_ops_bit_BitOrAssign_for_subtle_Choice.

Module Impl_core_ops_bit_BitXor_for_subtle_Choice.
  Definition Self : Ty.t := Ty.path "subtle::Choice".
  
  (*     type Output = Choice; *)
  Definition _Output : Ty.t := Ty.path "subtle::Choice".
  
  (*
      fn bitxor(self, rhs: Choice) -> Choice {
          (self.0 ^ rhs.0).into()
      }
  *)
  Definition bitxor (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; rhs ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let rhs := M.alloc (| rhs |) in
        M.call_closure (|
          M.get_trait_method (|
            "core::convert::Into",
            Ty.path "u8",
            [ Ty.path "subtle::Choice" ],
            "into",
            []
          |),
          [
            BinOp.bit_xor
              (M.read (| M.SubPointer.get_struct_tuple_field (| self, "subtle::Choice", 0 |) |))
              (M.read (| M.SubPointer.get_struct_tuple_field (| rhs, "subtle::Choice", 0 |) |))
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::ops::bit::BitXor"
      Self
      (* Trait polymorphic types *) []
      (* Instance *)
      [ ("Output", InstanceField.Ty _Output); ("bitxor", InstanceField.Method bitxor) ].
End Impl_core_ops_bit_BitXor_for_subtle_Choice.

Module Impl_core_ops_bit_BitXorAssign_for_subtle_Choice.
  Definition Self : Ty.t := Ty.path "subtle::Choice".
  
  (*
      fn bitxor_assign(&mut self, rhs: Choice) {
          *self = *self ^ rhs;
      }
  *)
  Definition bitxor_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; rhs ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let rhs := M.alloc (| rhs |) in
        M.read (|
          let~ _ :=
            M.write (|
              M.read (| self |),
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::bit::BitXor",
                  Ty.path "subtle::Choice",
                  [ Ty.path "subtle::Choice" ],
                  "bitxor",
                  []
                |),
                [ M.read (| M.read (| self |) |); M.read (| rhs |) ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::ops::bit::BitXorAssign"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("bitxor_assign", InstanceField.Method bitxor_assign) ].
End Impl_core_ops_bit_BitXorAssign_for_subtle_Choice.

Module Impl_core_ops_bit_Not_for_subtle_Choice.
  Definition Self : Ty.t := Ty.path "subtle::Choice".
  
  (*     type Output = Choice; *)
  Definition _Output : Ty.t := Ty.path "subtle::Choice".
  
  (*
      fn not(self) -> Choice {
          (1u8 & (!self.0)).into()
      }
  *)
  Definition not (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        M.call_closure (|
          M.get_trait_method (|
            "core::convert::Into",
            Ty.path "u8",
            [ Ty.path "subtle::Choice" ],
            "into",
            []
          |),
          [
            BinOp.bit_and
              (Value.Integer IntegerKind.U8 1)
              (UnOp.not (|
                M.read (| M.SubPointer.get_struct_tuple_field (| self, "subtle::Choice", 0 |) |)
              |))
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::ops::bit::Not"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("Output", InstanceField.Ty _Output); ("not", InstanceField.Method not) ].
End Impl_core_ops_bit_Not_for_subtle_Choice.

(*
fn black_box(input: u8) -> u8 {
    debug_assert!((input == 0u8) | (input == 1u8));

    unsafe {
        // Optimization barrier
        //
        // Unsafe is ok, because:
        //   - &input is not NULL;
        //   - size of input is not zero;
        //   - u8 is neither Sync, nor Send;
        //   - u8 is Copy, so input is always live;
        //   - u8 type is always properly aligned.
        core::ptr::read_volatile(&input as *const u8)
    }
}
*)
Definition black_box (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [ input ] =>
    ltac:(M.monadic
      (let input := M.alloc (| input |) in
      M.read (|
        let~ _ :=
          M.match_operator (|
            M.alloc (| Value.Tuple [] |),
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ := M.use (M.alloc (| Value.Bool true |)) in
                  let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  UnOp.not (|
                                    BinOp.bit_or
                                      (BinOp.eq (|
                                        M.read (| input |),
                                        Value.Integer IntegerKind.U8 0
                                      |))
                                      (BinOp.eq (|
                                        M.read (| input |),
                                        Value.Integer IntegerKind.U8 1
                                      |))
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.call_closure (|
                                  M.get_function (| "core::panicking::panic", [] |),
                                  [
                                    M.read (|
                                      Value.String
                                        "assertion failed: (input == 0u8) | (input == 1u8)"
                                    |)
                                  ]
                                |)
                              |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  M.alloc (| Value.Tuple [] |)));
              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
            ]
          |) in
        M.alloc (|
          M.call_closure (|
            M.get_function (| "core::ptr::read_volatile", [ Ty.path "u8" ] |),
            [ M.read (| M.use (M.alloc (| input |)) |) ]
          |)
        |)
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

Axiom Function_black_box : M.IsFunction "subtle::black_box" black_box.

Module Impl_core_convert_From_u8_for_subtle_Choice.
  Definition Self : Ty.t := Ty.path "subtle::Choice".
  
  (*
      fn from(input: u8) -> Choice {
          // Our goal is to prevent the compiler from inferring that the value held inside the
          // resulting `Choice` struct is really an `i1` instead of an `i8`.
          Choice(black_box(input))
      }
  *)
  Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ input ] =>
      ltac:(M.monadic
        (let input := M.alloc (| input |) in
        Value.StructTuple
          "subtle::Choice"
          [
            M.call_closure (|
              M.get_function (| "subtle::black_box", [] |),
              [ M.read (| input |) ]
            |)
          ]))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::convert::From"
      Self
      (* Trait polymorphic types *) [ (* T *) Ty.path "u8" ]
      (* Instance *) [ ("from", InstanceField.Method from) ].
End Impl_core_convert_From_u8_for_subtle_Choice.

(* Trait *)
Module ConstantTimeEq.
  Definition ct_ne (Self : Ty.t) (ε : 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.call_closure (|
          M.get_trait_method (| "core::ops::bit::Not", Ty.path "subtle::Choice", [], "not", [] |),
          [
            M.call_closure (|
              M.get_trait_method (| "subtle::ConstantTimeEq", Self, [], "ct_eq", [] |),
              [ M.read (| self |); M.read (| other |) ]
            |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom ProvidedMethod_ct_ne : M.IsProvidedMethod "subtle::ConstantTimeEq" "ct_ne" ct_ne.
End ConstantTimeEq.

Module Impl_subtle_ConstantTimeEq_where_subtle_ConstantTimeEq_T_for_slice_T.
  Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "slice") [] [ T ].
  
  (*
      fn ct_eq(&self, _rhs: &[T]) -> Choice {
          let len = self.len();
  
          // Short-circuit on the *lengths* of the slices, not their
          // contents.
          if len != _rhs.len() {
              return Choice::from(0);
          }
  
          // This loop shouldn't be shortcircuitable, since the compiler
          // shouldn't be able to reason about the value of the `u8`
          // unwrapped from the `ct_eq` result.
          let mut x = 1u8;
          for (ai, bi) in self.iter().zip(_rhs.iter()) {
              x &= ai.ct_eq(bi).unwrap_u8();
          }
  
          x.into()
      }
  *)
  Definition ct_eq (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    let Self : Ty.t := Self T in
    match ε, τ, α with
    | [], [], [ self; _rhs ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let _rhs := M.alloc (| _rhs |) in
        M.catch_return (|
          ltac:(M.monadic
            (M.read (|
              let~ len :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.apply (Ty.path "slice") [] [ T ], "len", [] |),
                    [ M.read (| self |) ]
                  |)
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.ne (|
                                M.read (| len |),
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "slice") [] [ T ],
                                    "len",
                                    []
                                  |),
                                  [ M.read (| _rhs |) ]
                                |)
                              |)
                            |)) 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_trait_method (|
                                    "core::convert::From",
                                    Ty.path "subtle::Choice",
                                    [ Ty.path "u8" ],
                                    "from",
                                    []
                                  |),
                                  [ Value.Integer IntegerKind.U8 0 ]
                                |)
                              |)
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ x := M.alloc (| Value.Integer IntegerKind.U8 1 |) in
              let~ _ :=
                M.use
                  (M.match_operator (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::iter::traits::collect::IntoIterator",
                          Ty.apply
                            (Ty.path "core::iter::adapters::zip::Zip")
                            []
                            [
                              Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ];
                              Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ]
                            ],
                          [],
                          "into_iter",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::iter::traits::iterator::Iterator",
                              Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ],
                              [],
                              "zip",
                              [ Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ] ]
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "slice") [] [ T ],
                                  "iter",
                                  []
                                |),
                                [ M.read (| self |) ]
                              |);
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "slice") [] [ T ],
                                  "iter",
                                  []
                                |),
                                [ M.read (| _rhs |) ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let iter := M.copy (| γ |) in
                          M.loop (|
                            ltac:(M.monadic
                              (let~ _ :=
                                M.match_operator (|
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::iter::traits::iterator::Iterator",
                                        Ty.apply
                                          (Ty.path "core::iter::adapters::zip::Zip")
                                          []
                                          [
                                            Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ];
                                            Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ]
                                          ],
                                        [],
                                        "next",
                                        []
                                      |),
                                      [ iter ]
                                    |)
                                  |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let _ :=
                                          M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                                        M.alloc (|
                                          M.never_to_any (| M.read (| M.break (||) |) |)
                                        |)));
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ0_0 :=
                                          M.SubPointer.get_struct_tuple_field (|
                                            γ,
                                            "core::option::Option::Some",
                                            0
                                          |) in
                                        let γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                                        let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                                        let ai := M.copy (| γ1_0 |) in
                                        let bi := M.copy (| γ1_1 |) in
                                        let~ _ :=
                                          let β := x in
                                          M.write (|
                                            β,
                                            BinOp.bit_and
                                              (M.read (| β |))
                                              (M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path "subtle::Choice",
                                                  "unwrap_u8",
                                                  []
                                                |),
                                                [
                                                  M.alloc (|
                                                    M.call_closure (|
                                                      M.get_trait_method (|
                                                        "subtle::ConstantTimeEq",
                                                        T,
                                                        [],
                                                        "ct_eq",
                                                        []
                                                      |),
                                                      [ M.read (| ai |); M.read (| bi |) ]
                                                    |)
                                                  |)
                                                ]
                                              |))
                                          |) in
                                        M.alloc (| Value.Tuple [] |)))
                                  ]
                                |) in
                              M.alloc (| Value.Tuple [] |)))
                          |)))
                    ]
                  |)) in
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::convert::Into",
                    Ty.path "u8",
                    [ Ty.path "subtle::Choice" ],
                    "into",
                    []
                  |),
                  [ M.read (| x |) ]
                |)
              |)
            |)))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    forall (T : Ty.t),
    M.IsTraitInstance
      "subtle::ConstantTimeEq"
      (Self T)
      (* Trait polymorphic types *) []
      (* Instance *) [ ("ct_eq", InstanceField.Method (ct_eq T)) ].
End Impl_subtle_ConstantTimeEq_where_subtle_ConstantTimeEq_T_for_slice_T.

Module Impl_subtle_ConstantTimeEq_for_subtle_Choice.
  Definition Self : Ty.t := Ty.path "subtle::Choice".
  
  (*
      fn ct_eq(&self, rhs: &Choice) -> Choice {
          !( *self ^ *rhs)
      }
  *)
  Definition ct_eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; rhs ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let rhs := M.alloc (| rhs |) in
        M.call_closure (|
          M.get_trait_method (| "core::ops::bit::Not", Ty.path "subtle::Choice", [], "not", [] |),
          [
            M.call_closure (|
              M.get_trait_method (|
                "core::ops::bit::BitXor",
                Ty.path "subtle::Choice",
                [ Ty.path "subtle::Choice" ],
                "bitxor",
                []
              |),
              [ M.read (| M.read (| self |) |); M.read (| M.read (| rhs |) |) ]
            |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "subtle::ConstantTimeEq"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("ct_eq", InstanceField.Method ct_eq) ].
End Impl_subtle_ConstantTimeEq_for_subtle_Choice.

Module Impl_subtle_ConstantTimeEq_for_u8.
  Definition Self : Ty.t := Ty.path "u8".
  
  (*
              fn ct_eq(&self, other: &$t_u) -> Choice {
                  // x == 0 if and only if self == other
                  let x: $t_u = self ^ other;
  
                  // If x == 0, then x and -x are both equal to zero;
                  // otherwise, one or both will have its high bit set.
                  let y: $t_u = (x | x.wrapping_neg()) >> ($bit_width - 1);
  
                  // Result is the opposite of the high bit (now shifted to low).
                  ((y ^ (1 as $t_u)) as u8).into()
              }
  *)
  Definition ct_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~ x :=
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::bit::BitXor",
                  Ty.apply (Ty.path "&") [] [ Ty.path "u8" ],
                  [ Ty.apply (Ty.path "&") [] [ Ty.path "u8" ] ],
                  "bitxor",
                  []
                |),
                [ M.read (| self |); M.read (| other |) ]
              |)
            |) in
          let~ y :=
            M.alloc (|
              BinOp.Wrap.shr (|
                BinOp.bit_or
                  (M.read (| x |))
                  (M.call_closure (|
                    M.get_associated_function (| Ty.path "u8", "wrapping_neg", [] |),
                    [ M.read (| x |) ]
                  |)),
                BinOp.Wrap.sub (|
                  Value.Integer IntegerKind.I32 8,
                  Value.Integer IntegerKind.I32 1
                |)
              |)
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_trait_method (|
                "core::convert::Into",
                Ty.path "u8",
                [ Ty.path "subtle::Choice" ],
                "into",
                []
              |),
              [
                M.read (|
                  M.use
                    (M.alloc (|
                      BinOp.bit_xor
                        (M.read (| y |))
                        (M.read (| M.use (M.alloc (| Value.Integer IntegerKind.U8 1 |)) |))
                    |))
                |)
              ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "subtle::ConstantTimeEq"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("ct_eq", InstanceField.Method ct_eq) ].
End Impl_subtle_ConstantTimeEq_for_u8.

Module Impl_subtle_ConstantTimeEq_for_i8.
  Definition Self : Ty.t := Ty.path "i8".
  
  (*
              fn ct_eq(&self, other: &$t_i) -> Choice {
                  // Bitcast to unsigned and call that implementation.
                  ( *self as $t_u).ct_eq(&( *other as $t_u))
              }
  *)
  Definition ct_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.call_closure (|
          M.get_trait_method (| "subtle::ConstantTimeEq", Ty.path "u8", [], "ct_eq", [] |),
          [
            M.alloc (| M.rust_cast (M.read (| M.read (| self |) |)) |);
            M.alloc (| M.rust_cast (M.read (| M.read (| other |) |)) |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "subtle::ConstantTimeEq"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("ct_eq", InstanceField.Method ct_eq) ].
End Impl_subtle_ConstantTimeEq_for_i8.

Module Impl_subtle_ConstantTimeEq_for_u16.
  Definition Self : Ty.t := Ty.path "u16".
  
  (*
              fn ct_eq(&self, other: &$t_u) -> Choice {
                  // x == 0 if and only if self == other
                  let x: $t_u = self ^ other;
  
                  // If x == 0, then x and -x are both equal to zero;
                  // otherwise, one or both will have its high bit set.
                  let y: $t_u = (x | x.wrapping_neg()) >> ($bit_width - 1);
  
                  // Result is the opposite of the high bit (now shifted to low).
                  ((y ^ (1 as $t_u)) as u8).into()
              }
  *)
  Definition ct_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~ x :=
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::bit::BitXor",
                  Ty.apply (Ty.path "&") [] [ Ty.path "u16" ],
                  [ Ty.apply (Ty.path "&") [] [ Ty.path "u16" ] ],
                  "bitxor",
                  []
                |),
                [ M.read (| self |); M.read (| other |) ]
              |)
            |) in
          let~ y :=
            M.alloc (|
              BinOp.Wrap.shr (|
                BinOp.bit_or
                  (M.read (| x |))
                  (M.call_closure (|
                    M.get_associated_function (| Ty.path "u16", "wrapping_neg", [] |),
                    [ M.read (| x |) ]
                  |)),
                BinOp.Wrap.sub (|
                  Value.Integer IntegerKind.I32 16,
                  Value.Integer IntegerKind.I32 1
                |)
              |)
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_trait_method (|
                "core::convert::Into",
                Ty.path "u8",
                [ Ty.path "subtle::Choice" ],
                "into",
                []
              |),
              [
                M.rust_cast
                  (BinOp.bit_xor
                    (M.read (| y |))
                    (M.read (| M.use (M.alloc (| Value.Integer IntegerKind.U16 1 |)) |)))
              ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "subtle::ConstantTimeEq"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("ct_eq", InstanceField.Method ct_eq) ].
End Impl_subtle_ConstantTimeEq_for_u16.

Module Impl_subtle_ConstantTimeEq_for_i16.
  Definition Self : Ty.t := Ty.path "i16".
  
  (*
              fn ct_eq(&self, other: &$t_i) -> Choice {
                  // Bitcast to unsigned and call that implementation.
                  ( *self as $t_u).ct_eq(&( *other as $t_u))
              }
  *)
  Definition ct_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.call_closure (|
          M.get_trait_method (| "subtle::ConstantTimeEq", Ty.path "u16", [], "ct_eq", [] |),
          [
            M.alloc (| M.rust_cast (M.read (| M.read (| self |) |)) |);
            M.alloc (| M.rust_cast (M.read (| M.read (| other |) |)) |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "subtle::ConstantTimeEq"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("ct_eq", InstanceField.Method ct_eq) ].
End Impl_subtle_ConstantTimeEq_for_i16.

Module Impl_subtle_ConstantTimeEq_for_u32.
  Definition Self : Ty.t := Ty.path "u32".
  
  (*
              fn ct_eq(&self, other: &$t_u) -> Choice {
                  // x == 0 if and only if self == other
                  let x: $t_u = self ^ other;
  
                  // If x == 0, then x and -x are both equal to zero;
                  // otherwise, one or both will have its high bit set.
                  let y: $t_u = (x | x.wrapping_neg()) >> ($bit_width - 1);
  
                  // Result is the opposite of the high bit (now shifted to low).
                  ((y ^ (1 as $t_u)) as u8).into()
              }
  *)
  Definition ct_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~ x :=
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::bit::BitXor",
                  Ty.apply (Ty.path "&") [] [ Ty.path "u32" ],
                  [ Ty.apply (Ty.path "&") [] [ Ty.path "u32" ] ],
                  "bitxor",
                  []
                |),
                [ M.read (| self |); M.read (| other |) ]
              |)
            |) in
          let~ y :=
            M.alloc (|
              BinOp.Wrap.shr (|
                BinOp.bit_or
                  (M.read (| x |))
                  (M.call_closure (|
                    M.get_associated_function (| Ty.path "u32", "wrapping_neg", [] |),
                    [ M.read (| x |) ]
                  |)),
                BinOp.Wrap.sub (|
                  Value.Integer IntegerKind.I32 32,
                  Value.Integer IntegerKind.I32 1
                |)
              |)
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_trait_method (|
                "core::convert::Into",
                Ty.path "u8",
                [ Ty.path "subtle::Choice" ],
                "into",
                []
              |),
              [
                M.rust_cast
                  (BinOp.bit_xor
                    (M.read (| y |))
                    (M.read (| M.use (M.alloc (| Value.Integer IntegerKind.U32 1 |)) |)))
              ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "subtle::ConstantTimeEq"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("ct_eq", InstanceField.Method ct_eq) ].
End Impl_subtle_ConstantTimeEq_for_u32.

Module Impl_subtle_ConstantTimeEq_for_i32.
  Definition Self : Ty.t := Ty.path "i32".
  
  (*
              fn ct_eq(&self, other: &$t_i) -> Choice {
                  // Bitcast to unsigned and call that implementation.
                  ( *self as $t_u).ct_eq(&( *other as $t_u))
              }
  *)
  Definition ct_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.call_closure (|
          M.get_trait_method (| "subtle::ConstantTimeEq", Ty.path "u32", [], "ct_eq", [] |),
          [
            M.alloc (| M.rust_cast (M.read (| M.read (| self |) |)) |);
            M.alloc (| M.rust_cast (M.read (| M.read (| other |) |)) |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "subtle::ConstantTimeEq"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("ct_eq", InstanceField.Method ct_eq) ].
End Impl_subtle_ConstantTimeEq_for_i32.

Module Impl_subtle_ConstantTimeEq_for_u64.
  Definition Self : Ty.t := Ty.path "u64".
  
  (*
              fn ct_eq(&self, other: &$t_u) -> Choice {
                  // x == 0 if and only if self == other
                  let x: $t_u = self ^ other;
  
                  // If x == 0, then x and -x are both equal to zero;
                  // otherwise, one or both will have its high bit set.
                  let y: $t_u = (x | x.wrapping_neg()) >> ($bit_width - 1);
  
                  // Result is the opposite of the high bit (now shifted to low).
                  ((y ^ (1 as $t_u)) as u8).into()
              }
  *)
  Definition ct_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~ x :=
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::bit::BitXor",
                  Ty.apply (Ty.path "&") [] [ Ty.path "u64" ],
                  [ Ty.apply (Ty.path "&") [] [ Ty.path "u64" ] ],
                  "bitxor",
                  []
                |),
                [ M.read (| self |); M.read (| other |) ]
              |)
            |) in
          let~ y :=
            M.alloc (|
              BinOp.Wrap.shr (|
                BinOp.bit_or
                  (M.read (| x |))
                  (M.call_closure (|
                    M.get_associated_function (| Ty.path "u64", "wrapping_neg", [] |),
                    [ M.read (| x |) ]
                  |)),
                BinOp.Wrap.sub (|
                  Value.Integer IntegerKind.I32 64,
                  Value.Integer IntegerKind.I32 1
                |)
              |)
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_trait_method (|
                "core::convert::Into",
                Ty.path "u8",
                [ Ty.path "subtle::Choice" ],
                "into",
                []
              |),
              [
                M.rust_cast
                  (BinOp.bit_xor
                    (M.read (| y |))
                    (M.read (| M.use (M.alloc (| Value.Integer IntegerKind.U64 1 |)) |)))
              ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "subtle::ConstantTimeEq"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("ct_eq", InstanceField.Method ct_eq) ].
End Impl_subtle_ConstantTimeEq_for_u64.

Module Impl_subtle_ConstantTimeEq_for_i64.
  Definition Self : Ty.t := Ty.path "i64".
  
  (*
              fn ct_eq(&self, other: &$t_i) -> Choice {
                  // Bitcast to unsigned and call that implementation.
                  ( *self as $t_u).ct_eq(&( *other as $t_u))
              }
  *)
  Definition ct_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.call_closure (|
          M.get_trait_method (| "subtle::ConstantTimeEq", Ty.path "u64", [], "ct_eq", [] |),
          [
            M.alloc (| M.rust_cast (M.read (| M.read (| self |) |)) |);
            M.alloc (| M.rust_cast (M.read (| M.read (| other |) |)) |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "subtle::ConstantTimeEq"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("ct_eq", InstanceField.Method ct_eq) ].
End Impl_subtle_ConstantTimeEq_for_i64.

Module Impl_subtle_ConstantTimeEq_for_usize.
  Definition Self : Ty.t := Ty.path "usize".
  
  (*
              fn ct_eq(&self, other: &$t_u) -> Choice {
                  // x == 0 if and only if self == other
                  let x: $t_u = self ^ other;
  
                  // If x == 0, then x and -x are both equal to zero;
                  // otherwise, one or both will have its high bit set.
                  let y: $t_u = (x | x.wrapping_neg()) >> ($bit_width - 1);
  
                  // Result is the opposite of the high bit (now shifted to low).
                  ((y ^ (1 as $t_u)) as u8).into()
              }
  *)
  Definition ct_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~ x :=
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::bit::BitXor",
                  Ty.apply (Ty.path "&") [] [ Ty.path "usize" ],
                  [ Ty.apply (Ty.path "&") [] [ Ty.path "usize" ] ],
                  "bitxor",
                  []
                |),
                [ M.read (| self |); M.read (| other |) ]
              |)
            |) in
          let~ y :=
            M.alloc (|
              BinOp.Wrap.shr (|
                BinOp.bit_or
                  (M.read (| x |))
                  (M.call_closure (|
                    M.get_associated_function (| Ty.path "usize", "wrapping_neg", [] |),
                    [ M.read (| x |) ]
                  |)),
                BinOp.Wrap.sub (|
                  BinOp.Wrap.mul (|
                    M.call_closure (|
                      M.get_function (| "core::mem::size_of", [ Ty.path "usize" ] |),
                      []
                    |),
                    Value.Integer IntegerKind.Usize 8
                  |),
                  Value.Integer IntegerKind.Usize 1
                |)
              |)
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_trait_method (|
                "core::convert::Into",
                Ty.path "u8",
                [ Ty.path "subtle::Choice" ],
                "into",
                []
              |),
              [
                M.rust_cast
                  (BinOp.bit_xor
                    (M.read (| y |))
                    (M.read (| M.use (M.alloc (| Value.Integer IntegerKind.Usize 1 |)) |)))
              ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "subtle::ConstantTimeEq"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("ct_eq", InstanceField.Method ct_eq) ].
End Impl_subtle_ConstantTimeEq_for_usize.

Module Impl_subtle_ConstantTimeEq_for_isize.
  Definition Self : Ty.t := Ty.path "isize".
  
  (*
              fn ct_eq(&self, other: &$t_i) -> Choice {
                  // Bitcast to unsigned and call that implementation.
                  ( *self as $t_u).ct_eq(&( *other as $t_u))
              }
  *)
  Definition ct_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.call_closure (|
          M.get_trait_method (| "subtle::ConstantTimeEq", Ty.path "usize", [], "ct_eq", [] |),
          [
            M.alloc (| M.rust_cast (M.read (| M.read (| self |) |)) |);
            M.alloc (| M.rust_cast (M.read (| M.read (| other |) |)) |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "subtle::ConstantTimeEq"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("ct_eq", InstanceField.Method ct_eq) ].
End Impl_subtle_ConstantTimeEq_for_isize.

(* Trait *)
Module ConditionallySelectable.
  Definition conditional_assign
      (Self : Ty.t)
      (ε : list Value.t)
      (τ : list Ty.t)
      (α : list Value.t)
      : M :=
    match ε, τ, α with
    | [], [], [ self; other; choice ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let other := M.alloc (| other |) in
        let choice := M.alloc (| choice |) in
        M.read (|
          let~ _ :=
            M.write (|
              M.read (| self |),
              M.call_closure (|
                M.get_trait_method (|
                  "subtle::ConditionallySelectable",
                  Self,
                  [],
                  "conditional_select",
                  []
                |),
                [ M.read (| self |); M.read (| other |); M.read (| choice |) ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom ProvidedMethod_conditional_assign :
    M.IsProvidedMethod "subtle::ConditionallySelectable" "conditional_assign" conditional_assign.
  Definition conditional_swap
      (Self : Ty.t)
      (ε : list Value.t)
      (τ : list Ty.t)
      (α : list Value.t)
      : M :=
    match ε, τ, α with
    | [], [], [ a; b; choice ] =>
      ltac:(M.monadic
        (let a := M.alloc (| a |) in
        let b := M.alloc (| b |) in
        let choice := M.alloc (| choice |) in
        M.read (|
          let~ t := M.copy (| M.read (| a |) |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "subtle::ConditionallySelectable",
                  Self,
                  [],
                  "conditional_assign",
                  []
                |),
                [ M.read (| a |); M.read (| b |); M.read (| choice |) ]
              |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "subtle::ConditionallySelectable",
                  Self,
                  [],
                  "conditional_assign",
                  []
                |),
                [ M.read (| b |); t; M.read (| choice |) ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom ProvidedMethod_conditional_swap :
    M.IsProvidedMethod "subtle::ConditionallySelectable" "conditional_swap" conditional_swap.
End ConditionallySelectable.

Module Impl_subtle_ConditionallySelectable_for_u8.
  Definition Self : Ty.t := Ty.path "u8".
  
  (*
              fn conditional_select(a: &Self, b: &Self, choice: Choice) -> Self {
                  // if choice = 0, mask = (-0) = 0000...0000
                  // if choice = 1, mask = (-1) = 1111...1111
                  let mask = -(choice.unwrap_u8() as to_signed_int!($t)) as $t;
                  a ^ (mask & (a ^ b))
              }
  *)
  Definition conditional_select (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ a; b; choice ] =>
      ltac:(M.monadic
        (let a := M.alloc (| a |) in
        let b := M.alloc (| b |) in
        let choice := M.alloc (| choice |) in
        M.read (|
          let~ mask :=
            M.alloc (|
              M.rust_cast
                (UnOp.neg (|
                  M.rust_cast
                    (M.call_closure (|
                      M.get_associated_function (| Ty.path "subtle::Choice", "unwrap_u8", [] |),
                      [ choice ]
                    |))
                |))
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_trait_method (|
                "core::ops::bit::BitXor",
                Ty.apply (Ty.path "&") [] [ Ty.path "u8" ],
                [ Ty.path "u8" ],
                "bitxor",
                []
              |),
              [
                M.read (| a |);
                BinOp.bit_and
                  (M.read (| mask |))
                  (M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::bit::BitXor",
                      Ty.apply (Ty.path "&") [] [ Ty.path "u8" ],
                      [ Ty.apply (Ty.path "&") [] [ Ty.path "u8" ] ],
                      "bitxor",
                      []
                    |),
                    [ M.read (| a |); M.read (| b |) ]
                  |))
              ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  (*
              fn conditional_assign(&mut self, other: &Self, choice: Choice) {
                  // if choice = 0, mask = (-0) = 0000...0000
                  // if choice = 1, mask = (-1) = 1111...1111
                  let mask = -(choice.unwrap_u8() as to_signed_int!($t)) as $t;
                  *self ^= mask & ( *self ^ *other);
              }
  *)
  Definition conditional_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; other; choice ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let other := M.alloc (| other |) in
        let choice := M.alloc (| choice |) in
        M.read (|
          let~ mask :=
            M.alloc (|
              M.rust_cast
                (UnOp.neg (|
                  M.rust_cast
                    (M.call_closure (|
                      M.get_associated_function (| Ty.path "subtle::Choice", "unwrap_u8", [] |),
                      [ choice ]
                    |))
                |))
            |) in
          let~ _ :=
            let β := M.read (| self |) in
            M.write (|
              β,
              BinOp.bit_xor
                (M.read (| β |))
                (BinOp.bit_and
                  (M.read (| mask |))
                  (BinOp.bit_xor
                    (M.read (| M.read (| self |) |))
                    (M.read (| M.read (| other |) |))))
            |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  (*
              fn conditional_swap(a: &mut Self, b: &mut Self, choice: Choice) {
                  // if choice = 0, mask = (-0) = 0000...0000
                  // if choice = 1, mask = (-1) = 1111...1111
                  let mask = -(choice.unwrap_u8() as to_signed_int!($t)) as $t;
                  let t = mask & ( *a ^ *b);
                  *a ^= t;
                  *b ^= t;
              }
  *)
  Definition conditional_swap (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ a; b; choice ] =>
      ltac:(M.monadic
        (let a := M.alloc (| a |) in
        let b := M.alloc (| b |) in
        let choice := M.alloc (| choice |) in
        M.read (|
          let~ mask :=
            M.alloc (|
              M.rust_cast
                (UnOp.neg (|
                  M.rust_cast
                    (M.call_closure (|
                      M.get_associated_function (| Ty.path "subtle::Choice", "unwrap_u8", [] |),
                      [ choice ]
                    |))
                |))
            |) in
          let~ t :=
            M.alloc (|
              BinOp.bit_and
                (M.read (| mask |))
                (BinOp.bit_xor (M.read (| M.read (| a |) |)) (M.read (| M.read (| b |) |)))
            |) in
          let~ _ :=
            let β := M.read (| a |) in
            M.write (| β, BinOp.bit_xor (M.read (| β |)) (M.read (| t |)) |) in
          let~ _ :=
            let β := M.read (| b |) in
            M.write (| β, BinOp.bit_xor (M.read (| β |)) (M.read (| t |)) |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "subtle::ConditionallySelectable"
      Self
      (* Trait polymorphic types *) []
      (* Instance *)
      [
        ("conditional_select", InstanceField.Method conditional_select);
        ("conditional_assign", InstanceField.Method conditional_assign);
        ("conditional_swap", InstanceField.Method conditional_swap)
      ].
End Impl_subtle_ConditionallySelectable_for_u8.

Module Impl_subtle_ConditionallySelectable_for_i8.
  Definition Self : Ty.t := Ty.path "i8".
  
  (*
              fn conditional_select(a: &Self, b: &Self, choice: Choice) -> Self {
                  // if choice = 0, mask = (-0) = 0000...0000
                  // if choice = 1, mask = (-1) = 1111...1111
                  let mask = -(choice.unwrap_u8() as to_signed_int!($t)) as $t;
                  a ^ (mask & (a ^ b))
              }
  *)
  Definition conditional_select (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ a; b; choice ] =>
      ltac:(M.monadic
        (let a := M.alloc (| a |) in
        let b := M.alloc (| b |) in
        let choice := M.alloc (| choice |) in
        M.read (|
          let~ mask :=
            M.copy (|
              M.use
                (M.alloc (|
                  UnOp.neg (|
                    M.rust_cast
                      (M.call_closure (|
                        M.get_associated_function (| Ty.path "subtle::Choice", "unwrap_u8", [] |),
                        [ choice ]
                      |))
                  |)
                |))
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_trait_method (|
                "core::ops::bit::BitXor",
                Ty.apply (Ty.path "&") [] [ Ty.path "i8" ],
                [ Ty.path "i8" ],
                "bitxor",
                []
              |),
              [
                M.read (| a |);
                BinOp.bit_and
                  (M.read (| mask |))
                  (M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::bit::BitXor",
                      Ty.apply (Ty.path "&") [] [ Ty.path "i8" ],
                      [ Ty.apply (Ty.path "&") [] [ Ty.path "i8" ] ],
                      "bitxor",
                      []
                    |),
                    [ M.read (| a |); M.read (| b |) ]
                  |))
              ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  (*
              fn conditional_assign(&mut self, other: &Self, choice: Choice) {
                  // if choice = 0, mask = (-0) = 0000...0000
                  // if choice = 1, mask = (-1) = 1111...1111
                  let mask = -(choice.unwrap_u8() as to_signed_int!($t)) as $t;
                  *self ^= mask & ( *self ^ *other);
              }
  *)
  Definition conditional_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; other; choice ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let other := M.alloc (| other |) in
        let choice := M.alloc (| choice |) in
        M.read (|
          let~ mask :=
            M.copy (|
              M.use
                (M.alloc (|
                  UnOp.neg (|
                    M.rust_cast
                      (M.call_closure (|
                        M.get_associated_function (| Ty.path "subtle::Choice", "unwrap_u8", [] |),
                        [ choice ]
                      |))
                  |)
                |))
            |) in
          let~ _ :=
            let β := M.read (| self |) in
            M.write (|
              β,
              BinOp.bit_xor
                (M.read (| β |))
                (BinOp.bit_and
                  (M.read (| mask |))
                  (BinOp.bit_xor
                    (M.read (| M.read (| self |) |))
                    (M.read (| M.read (| other |) |))))
            |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  (*
              fn conditional_swap(a: &mut Self, b: &mut Self, choice: Choice) {
                  // if choice = 0, mask = (-0) = 0000...0000
                  // if choice = 1, mask = (-1) = 1111...1111
                  let mask = -(choice.unwrap_u8() as to_signed_int!($t)) as $t;
                  let t = mask & ( *a ^ *b);
                  *a ^= t;
                  *b ^= t;
              }
  *)
  Definition conditional_swap (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ a; b; choice ] =>
      ltac:(M.monadic
        (let a := M.alloc (| a |) in
        let b := M.alloc (| b |) in
        let choice := M.alloc (| choice |) in
        M.read (|
          let~ mask :=
            M.copy (|
              M.use
                (M.alloc (|
                  UnOp.neg (|
                    M.rust_cast
                      (M.call_closure (|
                        M.get_associated_function (| Ty.path "subtle::Choice", "unwrap_u8", [] |),
                        [ choice ]
                      |))
                  |)
                |))
            |) in
          let~ t :=
            M.alloc (|
              BinOp.bit_and
                (M.read (| mask |))
                (BinOp.bit_xor (M.read (| M.read (| a |) |)) (M.read (| M.read (| b |) |)))
            |) in
          let~ _ :=
            let β := M.read (| a |) in
            M.write (| β, BinOp.bit_xor (M.read (| β |)) (M.read (| t |)) |) in
          let~ _ :=
            let β := M.read (| b |) in
            M.write (| β, BinOp.bit_xor (M.read (| β |)) (M.read (| t |)) |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "subtle::ConditionallySelectable"
      Self
      (* Trait polymorphic types *) []
      (* Instance *)
      [
        ("conditional_select", InstanceField.Method conditional_select);
        ("conditional_assign", InstanceField.Method conditional_assign);
        ("conditional_swap", InstanceField.Method conditional_swap)
      ].
End Impl_subtle_ConditionallySelectable_for_i8.

Module Impl_subtle_ConditionallySelectable_for_u16.
  Definition Self : Ty.t := Ty.path "u16".
  
  (*
              fn conditional_select(a: &Self, b: &Self, choice: Choice) -> Self {
                  // if choice = 0, mask = (-0) = 0000...0000
                  // if choice = 1, mask = (-1) = 1111...1111
                  let mask = -(choice.unwrap_u8() as to_signed_int!($t)) as $t;
                  a ^ (mask & (a ^ b))
              }
  *)
  Definition conditional_select (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ a; b; choice ] =>
      ltac:(M.monadic
        (let a := M.alloc (| a |) in
        let b := M.alloc (| b |) in
        let choice := M.alloc (| choice |) in
        M.read (|
          let~ mask :=
            M.alloc (|
              M.rust_cast
                (UnOp.neg (|
                  M.rust_cast
                    (M.call_closure (|
                      M.get_associated_function (| Ty.path "subtle::Choice", "unwrap_u8", [] |),
                      [ choice ]
                    |))
                |))
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_trait_method (|
                "core::ops::bit::BitXor",
                Ty.apply (Ty.path "&") [] [ Ty.path "u16" ],
                [ Ty.path "u16" ],
                "bitxor",
                []
              |),
              [
                M.read (| a |);
                BinOp.bit_and
                  (M.read (| mask |))
                  (M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::bit::BitXor",
                      Ty.apply (Ty.path "&") [] [ Ty.path "u16" ],
                      [ Ty.apply (Ty.path "&") [] [ Ty.path "u16" ] ],
                      "bitxor",
                      []
                    |),
                    [ M.read (| a |); M.read (| b |) ]
                  |))
              ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  (*
              fn conditional_assign(&mut self, other: &Self, choice: Choice) {
                  // if choice = 0, mask = (-0) = 0000...0000
                  // if choice = 1, mask = (-1) = 1111...1111
                  let mask = -(choice.unwrap_u8() as to_signed_int!($t)) as $t;
                  *self ^= mask & ( *self ^ *other);
              }
  *)
  Definition conditional_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; other; choice ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let other := M.alloc (| other |) in
        let choice := M.alloc (| choice |) in
        M.read (|
          let~ mask :=
            M.alloc (|
              M.rust_cast
                (UnOp.neg (|
                  M.rust_cast
                    (M.call_closure (|
                      M.get_associated_function (| Ty.path "subtle::Choice", "unwrap_u8", [] |),
                      [ choice ]
                    |))
                |))
            |) in
          let~ _ :=
            let β := M.read (| self |) in
            M.write (|
              β,
              BinOp.bit_xor
                (M.read (| β |))
                (BinOp.bit_and
                  (M.read (| mask |))
                  (BinOp.bit_xor
                    (M.read (| M.read (| self |) |))
                    (M.read (| M.read (| other |) |))))
            |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  (*
              fn conditional_swap(a: &mut Self, b: &mut Self, choice: Choice) {
                  // if choice = 0, mask = (-0) = 0000...0000
                  // if choice = 1, mask = (-1) = 1111...1111
                  let mask = -(choice.unwrap_u8() as to_signed_int!($t)) as $t;
                  let t = mask & ( *a ^ *b);
                  *a ^= t;
                  *b ^= t;
              }
  *)
  Definition conditional_swap (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ a; b; choice ] =>
      ltac:(M.monadic
        (let a := M.alloc (| a |) in
        let b := M.alloc (| b |) in
        let choice := M.alloc (| choice |) in
        M.read (|
          let~ mask :=
            M.alloc (|
              M.rust_cast
                (UnOp.neg (|
                  M.rust_cast
                    (M.call_closure (|
                      M.get_associated_function (| Ty.path "subtle::Choice", "unwrap_u8", [] |),
                      [ choice ]
                    |))
                |))
            |) in
          let~ t :=
            M.alloc (|
              BinOp.bit_and
                (M.read (| mask |))
                (BinOp.bit_xor (M.read (| M.read (| a |) |)) (M.read (| M.read (| b |) |)))
            |) in
          let~ _ :=
            let β := M.read (| a |) in
            M.write (| β, BinOp.bit_xor (M.read (| β |)) (M.read (| t |)) |) in
          let~ _ :=
            let β := M.read (| b |) in
            M.write (| β, BinOp.bit_xor (M.read (| β |)) (M.read (| t |)) |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "subtle::ConditionallySelectable"
      Self
      (* Trait polymorphic types *) []
      (* Instance *)
      [
        ("conditional_select", InstanceField.Method conditional_select);
        ("conditional_assign", InstanceField.Method conditional_assign);
        ("conditional_swap", InstanceField.Method conditional_swap)
      ].
End Impl_subtle_ConditionallySelectable_for_u16.

Module Impl_subtle_ConditionallySelectable_for_i16.
  Definition Self : Ty.t := Ty.path "i16".
  
  (*
              fn conditional_select(a: &Self, b: &Self, choice: Choice) -> Self {
                  // if choice = 0, mask = (-0) = 0000...0000
                  // if choice = 1, mask = (-1) = 1111...1111
                  let mask = -(choice.unwrap_u8() as to_signed_int!($t)) as $t;
                  a ^ (mask & (a ^ b))
              }
  *)
  Definition conditional_select (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ a; b; choice ] =>
      ltac:(M.monadic
        (let a := M.alloc (| a |) in
        let b := M.alloc (| b |) in
        let choice := M.alloc (| choice |) in
        M.read (|
          let~ mask :=
            M.copy (|
              M.use
                (M.alloc (|
                  UnOp.neg (|
                    M.rust_cast
                      (M.call_closure (|
                        M.get_associated_function (| Ty.path "subtle::Choice", "unwrap_u8", [] |),
                        [ choice ]
                      |))
                  |)
                |))
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_trait_method (|
                "core::ops::bit::BitXor",
                Ty.apply (Ty.path "&") [] [ Ty.path "i16" ],
                [ Ty.path "i16" ],
                "bitxor",
                []
              |),
              [
                M.read (| a |);
                BinOp.bit_and
                  (M.read (| mask |))
                  (M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::bit::BitXor",
                      Ty.apply (Ty.path "&") [] [ Ty.path "i16" ],
                      [ Ty.apply (Ty.path "&") [] [ Ty.path "i16" ] ],
                      "bitxor",
                      []
                    |),
                    [ M.read (| a |); M.read (| b |) ]
                  |))
              ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  (*
              fn conditional_assign(&mut self, other: &Self, choice: Choice) {
                  // if choice = 0, mask = (-0) = 0000...0000
                  // if choice = 1, mask = (-1) = 1111...1111
                  let mask = -(choice.unwrap_u8() as to_signed_int!($t)) as $t;
                  *self ^= mask & ( *self ^ *other);
              }
  *)
  Definition conditional_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; other; choice ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let other := M.alloc (| other |) in
        let choice := M.alloc (| choice |) in
        M.read (|
          let~ mask :=
            M.copy (|
              M.use
                (M.alloc (|
                  UnOp.neg (|
                    M.rust_cast
                      (M.call_closure (|
                        M.get_associated_function (| Ty.path "subtle::Choice", "unwrap_u8", [] |),
                        [ choice ]
                      |))
                  |)
                |))
            |) in
          let~ _ :=
            let β := M.read (| self |) in
            M.write (|
              β,
              BinOp.bit_xor
                (M.read (| β |))
                (BinOp.bit_and
                  (M.read (| mask |))
                  (BinOp.bit_xor
                    (M.read (| M.read (| self |) |))
                    (M.read (| M.read (| other |) |))))
            |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  (*
              fn conditional_swap(a: &mut Self, b: &mut Self, choice: Choice) {
                  // if choice = 0, mask = (-0) = 0000...0000
                  // if choice = 1, mask = (-1) = 1111...1111
                  let mask = -(choice.unwrap_u8() as to_signed_int!($t)) as $t;
                  let t = mask & ( *a ^ *b);
                  *a ^= t;
                  *b ^= t;
              }
  *)
  Definition conditional_swap (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ a; b; choice ] =>
      ltac:(M.monadic
        (let a := M.alloc (| a |) in
        let b := M.alloc (| b |) in
        let choice := M.alloc (| choice |) in
        M.read (|
          let~ mask :=
            M.copy (|
              M.use
                (M.alloc (|
                  UnOp.neg (|
                    M.rust_cast
                      (M.call_closure (|
                        M.get_associated_function (| Ty.path "subtle::Choice", "unwrap_u8", [] |),
                        [ choice ]
                      |))
                  |)
                |))
            |) in
          let~ t :=
            M.alloc (|
              BinOp.bit_and
                (M.read (| mask |))
                (BinOp.bit_xor (M.read (| M.read (| a |) |)) (M.read (| M.read (| b |) |)))
            |) in
          let~ _ :=
            let β := M.read (| a |) in
            M.write (| β, BinOp.bit_xor (M.read (| β |)) (M.read (| t |)) |) in
          let~ _ :=
            let β := M.read (| b |) in
            M.write (| β, BinOp.bit_xor (M.read (| β |)) (M.read (| t |)) |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "subtle::ConditionallySelectable"
      Self
      (* Trait polymorphic types *) []
      (* Instance *)
      [
        ("conditional_select", InstanceField.Method conditional_select);
        ("conditional_assign", InstanceField.Method conditional_assign);
        ("conditional_swap", InstanceField.Method conditional_swap)
      ].
End Impl_subtle_ConditionallySelectable_for_i16.

Module Impl_subtle_ConditionallySelectable_for_u32.
  Definition Self : Ty.t := Ty.path "u32".
  
  (*
              fn conditional_select(a: &Self, b: &Self, choice: Choice) -> Self {
                  // if choice = 0, mask = (-0) = 0000...0000
                  // if choice = 1, mask = (-1) = 1111...1111
                  let mask = -(choice.unwrap_u8() as to_signed_int!($t)) as $t;
                  a ^ (mask & (a ^ b))
              }
  *)
  Definition conditional_select (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ a; b; choice ] =>
      ltac:(M.monadic
        (let a := M.alloc (| a |) in
        let b := M.alloc (| b |) in
        let choice := M.alloc (| choice |) in
        M.read (|
          let~ mask :=
            M.alloc (|
              M.rust_cast
                (UnOp.neg (|
                  M.rust_cast
                    (M.call_closure (|
                      M.get_associated_function (| Ty.path "subtle::Choice", "unwrap_u8", [] |),
                      [ choice ]
                    |))
                |))
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_trait_method (|
                "core::ops::bit::BitXor",
                Ty.apply (Ty.path "&") [] [ Ty.path "u32" ],
                [ Ty.path "u32" ],
                "bitxor",
                []
              |),
              [
                M.read (| a |);
                BinOp.bit_and
                  (M.read (| mask |))
                  (M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::bit::BitXor",
                      Ty.apply (Ty.path "&") [] [ Ty.path "u32" ],
                      [ Ty.apply (Ty.path "&") [] [ Ty.path "u32" ] ],
                      "bitxor",
                      []
                    |),
                    [ M.read (| a |); M.read (| b |) ]
                  |))
              ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  (*
              fn conditional_assign(&mut self, other: &Self, choice: Choice) {
                  // if choice = 0, mask = (-0) = 0000...0000
                  // if choice = 1, mask = (-1) = 1111...1111
                  let mask = -(choice.unwrap_u8() as to_signed_int!($t)) as $t;
                  *self ^= mask & ( *self ^ *other);
              }
  *)
  Definition conditional_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; other; choice ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let other := M.alloc (| other |) in
        let choice := M.alloc (| choice |) in
        M.read (|
          let~ mask :=
            M.alloc (|
              M.rust_cast
                (UnOp.neg (|
                  M.rust_cast
                    (M.call_closure (|
                      M.get_associated_function (| Ty.path "subtle::Choice", "unwrap_u8", [] |),
                      [ choice ]
                    |))
                |))
            |) in
          let~ _ :=
            let β := M.read (| self |) in
            M.write (|
              β,
              BinOp.bit_xor
                (M.read (| β |))
                (BinOp.bit_and
                  (M.read (| mask |))
                  (BinOp.bit_xor
                    (M.read (| M.read (| self |) |))
                    (M.read (| M.read (| other |) |))))
            |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  (*
              fn conditional_swap(a: &mut Self, b: &mut Self, choice: Choice) {
                  // if choice = 0, mask = (-0) = 0000...0000
                  // if choice = 1, mask = (-1) = 1111...1111
                  let mask = -(choice.unwrap_u8() as to_signed_int!($t)) as $t;
                  let t = mask & ( *a ^ *b);
                  *a ^= t;
                  *b ^= t;
              }
  *)
  Definition conditional_swap (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ a; b; choice ] =>
      ltac:(M.monadic
        (let a := M.alloc (| a |) in
        let b := M.alloc (| b |) in
        let choice := M.alloc (| choice |) in
        M.read (|
          let~ mask :=
            M.alloc (|
              M.rust_cast
                (UnOp.neg (|
                  M.rust_cast
                    (M.call_closure (|
                      M.get_associated_function (| Ty.path "subtle::Choice", "unwrap_u8", [] |),
                      [ choice ]
                    |))
                |))
            |) in
          let~ t :=
            M.alloc (|
              BinOp.bit_and
                (M.read (| mask |))
                (BinOp.bit_xor (M.read (| M.read (| a |) |)) (M.read (| M.read (| b |) |)))
            |) in
          let~ _ :=
            let β := M.read (| a |) in
            M.write (| β, BinOp.bit_xor (M.read (| β |)) (M.read (| t |)) |) in
          let~ _ :=
            let β := M.read (| b |) in
            M.write (| β, BinOp.bit_xor (M.read (| β |)) (M.read (| t |)) |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "subtle::ConditionallySelectable"
      Self
      (* Trait polymorphic types *) []
      (* Instance *)
      [
        ("conditional_select", InstanceField.Method conditional_select);
        ("conditional_assign", InstanceField.Method conditional_assign);
        ("conditional_swap", InstanceField.Method conditional_swap)
      ].
End Impl_subtle_ConditionallySelectable_for_u32.

Module Impl_subtle_ConditionallySelectable_for_i32.
  Definition Self : Ty.t := Ty.path "i32".
  
  (*
              fn conditional_select(a: &Self, b: &Self, choice: Choice) -> Self {
                  // if choice = 0, mask = (-0) = 0000...0000
                  // if choice = 1, mask = (-1) = 1111...1111
                  let mask = -(choice.unwrap_u8() as to_signed_int!($t)) as $t;
                  a ^ (mask & (a ^ b))
              }
  *)
  Definition conditional_select (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ a; b; choice ] =>
      ltac:(M.monadic
        (let a := M.alloc (| a |) in
        let b := M.alloc (| b |) in
        let choice := M.alloc (| choice |) in
        M.read (|
          let~ mask :=
            M.copy (|
              M.use
                (M.alloc (|
                  UnOp.neg (|
                    M.rust_cast
                      (M.call_closure (|
                        M.get_associated_function (| Ty.path "subtle::Choice", "unwrap_u8", [] |),
                        [ choice ]
                      |))
                  |)
                |))
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_trait_method (|
                "core::ops::bit::BitXor",
                Ty.apply (Ty.path "&") [] [ Ty.path "i32" ],
                [ Ty.path "i32" ],
                "bitxor",
                []
              |),
              [
                M.read (| a |);
                BinOp.bit_and
                  (M.read (| mask |))
                  (M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::bit::BitXor",
                      Ty.apply (Ty.path "&") [] [ Ty.path "i32" ],
                      [ Ty.apply (Ty.path "&") [] [ Ty.path "i32" ] ],
                      "bitxor",
                      []
                    |),
                    [ M.read (| a |); M.read (| b |) ]
                  |))
              ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  (*
              fn conditional_assign(&mut self, other: &Self, choice: Choice) {
                  // if choice = 0, mask = (-0) = 0000...0000
                  // if choice = 1, mask = (-1) = 1111...1111
                  let mask = -(choice.unwrap_u8() as to_signed_int!($t)) as $t;
                  *self ^= mask & ( *self ^ *other);
              }
  *)
  Definition conditional_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; other; choice ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let other := M.alloc (| other |) in
        let choice := M.alloc (| choice |) in
        M.read (|
          let~ mask :=
            M.copy (|
              M.use
                (M.alloc (|
                  UnOp.neg (|
                    M.rust_cast
                      (M.call_closure (|
                        M.get_associated_function (| Ty.path "subtle::Choice", "unwrap_u8", [] |),
                        [ choice ]
                      |))
                  |)
                |))
            |) in
          let~ _ :=
            let β := M.read (| self |) in
            M.write (|
              β,
              BinOp.bit_xor
                (M.read (| β |))
                (BinOp.bit_and
                  (M.read (| mask |))
                  (BinOp.bit_xor
                    (M.read (| M.read (| self |) |))
                    (M.read (| M.read (| other |) |))))
            |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  (*
              fn conditional_swap(a: &mut Self, b: &mut Self, choice: Choice) {
                  // if choice = 0, mask = (-0) = 0000...0000
                  // if choice = 1, mask = (-1) = 1111...1111
                  let mask = -(choice.unwrap_u8() as to_signed_int!($t)) as $t;
                  let t = mask & ( *a ^ *b);
                  *a ^= t;
                  *b ^= t;
              }
  *)
  Definition conditional_swap (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ a; b; choice ] =>
      ltac:(M.monadic
        (let a := M.alloc (| a |) in
        let b := M.alloc (| b |) in
        let choice := M.alloc (| choice |) in
        M.read (|
          let~ mask :=
            M.copy (|
              M.use
                (M.alloc (|
                  UnOp.neg (|
                    M.rust_cast
                      (M.call_closure (|
                        M.get_associated_function (| Ty.path "subtle::Choice", "unwrap_u8", [] |),
                        [ choice ]
                      |))
                  |)
                |))
            |) in
          let~ t :=
            M.alloc (|
              BinOp.bit_and
                (M.read (| mask |))
                (BinOp.bit_xor (M.read (| M.read (| a |) |)) (M.read (| M.read (| b |) |)))
            |) in
          let~ _ :=
            let β := M.read (| a |) in
            M.write (| β, BinOp.bit_xor (M.read (| β |)) (M.read (| t |)) |) in
          let~ _ :=
            let β := M.read (| b |) in
            M.write (| β, BinOp.bit_xor (M.read (| β |)) (M.read (| t |)) |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "subtle::ConditionallySelectable"
      Self
      (* Trait polymorphic types *) []
      (* Instance *)
      [
        ("conditional_select", InstanceField.Method conditional_select);
        ("conditional_assign", InstanceField.Method conditional_assign);
        ("conditional_swap", InstanceField.Method conditional_swap)
      ].
End Impl_subtle_ConditionallySelectable_for_i32.

Module Impl_subtle_ConditionallySelectable_for_u64.
  Definition Self : Ty.t := Ty.path "u64".
  
  (*
              fn conditional_select(a: &Self, b: &Self, choice: Choice) -> Self {
                  // if choice = 0, mask = (-0) = 0000...0000
                  // if choice = 1, mask = (-1) = 1111...1111
                  let mask = -(choice.unwrap_u8() as to_signed_int!($t)) as $t;
                  a ^ (mask & (a ^ b))
              }
  *)
  Definition conditional_select (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ a; b; choice ] =>
      ltac:(M.monadic
        (let a := M.alloc (| a |) in
        let b := M.alloc (| b |) in
        let choice := M.alloc (| choice |) in
        M.read (|
          let~ mask :=
            M.alloc (|
              M.rust_cast
                (UnOp.neg (|
                  M.rust_cast
                    (M.call_closure (|
                      M.get_associated_function (| Ty.path "subtle::Choice", "unwrap_u8", [] |),
                      [ choice ]
                    |))
                |))
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_trait_method (|
                "core::ops::bit::BitXor",
                Ty.apply (Ty.path "&") [] [ Ty.path "u64" ],
                [ Ty.path "u64" ],
                "bitxor",
                []
              |),
              [
                M.read (| a |);
                BinOp.bit_and
                  (M.read (| mask |))
                  (M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::bit::BitXor",
                      Ty.apply (Ty.path "&") [] [ Ty.path "u64" ],
                      [ Ty.apply (Ty.path "&") [] [ Ty.path "u64" ] ],
                      "bitxor",
                      []
                    |),
                    [ M.read (| a |); M.read (| b |) ]
                  |))
              ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  (*
              fn conditional_assign(&mut self, other: &Self, choice: Choice) {
                  // if choice = 0, mask = (-0) = 0000...0000
                  // if choice = 1, mask = (-1) = 1111...1111
                  let mask = -(choice.unwrap_u8() as to_signed_int!($t)) as $t;
                  *self ^= mask & ( *self ^ *other);
              }
  *)
  Definition conditional_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; other; choice ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let other := M.alloc (| other |) in
        let choice := M.alloc (| choice |) in
        M.read (|
          let~ mask :=
            M.alloc (|
              M.rust_cast
                (UnOp.neg (|
                  M.rust_cast
                    (M.call_closure (|
                      M.get_associated_function (| Ty.path "subtle::Choice", "unwrap_u8", [] |),
                      [ choice ]
                    |))
                |))
            |) in
          let~ _ :=
            let β := M.read (| self |) in
            M.write (|
              β,
              BinOp.bit_xor
                (M.read (| β |))
                (BinOp.bit_and
                  (M.read (| mask |))
                  (BinOp.bit_xor
                    (M.read (| M.read (| self |) |))
                    (M.read (| M.read (| other |) |))))
            |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  (*
              fn conditional_swap(a: &mut Self, b: &mut Self, choice: Choice) {
                  // if choice = 0, mask = (-0) = 0000...0000
                  // if choice = 1, mask = (-1) = 1111...1111
                  let mask = -(choice.unwrap_u8() as to_signed_int!($t)) as $t;
                  let t = mask & ( *a ^ *b);
                  *a ^= t;
                  *b ^= t;
              }
  *)
  Definition conditional_swap (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ a; b; choice ] =>
      ltac:(M.monadic
        (let a := M.alloc (| a |) in
        let b := M.alloc (| b |) in
        let choice := M.alloc (| choice |) in
        M.read (|
          let~ mask :=
            M.alloc (|
              M.rust_cast
                (UnOp.neg (|
                  M.rust_cast
                    (M.call_closure (|
                      M.get_associated_function (| Ty.path "subtle::Choice", "unwrap_u8", [] |),
                      [ choice ]
                    |))
                |))
            |) in
          let~ t :=
            M.alloc (|
              BinOp.bit_and
                (M.read (| mask |))
                (BinOp.bit_xor (M.read (| M.read (| a |) |)) (M.read (| M.read (| b |) |)))
            |) in
          let~ _ :=
            let β := M.read (| a |) in
            M.write (| β, BinOp.bit_xor (M.read (| β |)) (M.read (| t |)) |) in
          let~ _ :=
            let β := M.read (| b |) in
            M.write (| β, BinOp.bit_xor (M.read (| β |)) (M.read (| t |)) |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "subtle::ConditionallySelectable"
      Self
      (* Trait polymorphic types *) []
      (* Instance *)
      [
        ("conditional_select", InstanceField.Method conditional_select);
        ("conditional_assign", InstanceField.Method conditional_assign);
        ("conditional_swap", InstanceField.Method conditional_swap)
      ].
End Impl_subtle_ConditionallySelectable_for_u64.

Module Impl_subtle_ConditionallySelectable_for_i64.
  Definition Self : Ty.t := Ty.path "i64".
  
  (*
              fn conditional_select(a: &Self, b: &Self, choice: Choice) -> Self {
                  // if choice = 0, mask = (-0) = 0000...0000
                  // if choice = 1, mask = (-1) = 1111...1111
                  let mask = -(choice.unwrap_u8() as to_signed_int!($t)) as $t;
                  a ^ (mask & (a ^ b))
              }
  *)
  Definition conditional_select (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ a; b; choice ] =>
      ltac:(M.monadic
        (let a := M.alloc (| a |) in
        let b := M.alloc (| b |) in
        let choice := M.alloc (| choice |) in
        M.read (|
          let~ mask :=
            M.copy (|
              M.use
                (M.alloc (|
                  UnOp.neg (|
                    M.rust_cast
                      (M.call_closure (|
                        M.get_associated_function (| Ty.path "subtle::Choice", "unwrap_u8", [] |),
                        [ choice ]
                      |))
                  |)
                |))
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_trait_method (|
                "core::ops::bit::BitXor",
                Ty.apply (Ty.path "&") [] [ Ty.path "i64" ],
                [ Ty.path "i64" ],
                "bitxor",
                []
              |),
              [
                M.read (| a |);
                BinOp.bit_and
                  (M.read (| mask |))
                  (M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::bit::BitXor",
                      Ty.apply (Ty.path "&") [] [ Ty.path "i64" ],
                      [ Ty.apply (Ty.path "&") [] [ Ty.path "i64" ] ],
                      "bitxor",
                      []
                    |),
                    [ M.read (| a |); M.read (| b |) ]
                  |))
              ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  (*
              fn conditional_assign(&mut self, other: &Self, choice: Choice) {
                  // if choice = 0, mask = (-0) = 0000...0000
                  // if choice = 1, mask = (-1) = 1111...1111
                  let mask = -(choice.unwrap_u8() as to_signed_int!($t)) as $t;
                  *self ^= mask & ( *self ^ *other);
              }
  *)
  Definition conditional_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; other; choice ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let other := M.alloc (| other |) in
        let choice := M.alloc (| choice |) in
        M.read (|
          let~ mask :=
            M.copy (|
              M.use
                (M.alloc (|
                  UnOp.neg (|
                    M.rust_cast
                      (M.call_closure (|
                        M.get_associated_function (| Ty.path "subtle::Choice", "unwrap_u8", [] |),
                        [ choice ]
                      |))
                  |)
                |))
            |) in
          let~ _ :=
            let β := M.read (| self |) in
            M.write (|
              β,
              BinOp.bit_xor
                (M.read (| β |))
                (BinOp.bit_and
                  (M.read (| mask |))
                  (BinOp.bit_xor
                    (M.read (| M.read (| self |) |))
                    (M.read (| M.read (| other |) |))))
            |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  (*
              fn conditional_swap(a: &mut Self, b: &mut Self, choice: Choice) {
                  // if choice = 0, mask = (-0) = 0000...0000
                  // if choice = 1, mask = (-1) = 1111...1111
                  let mask = -(choice.unwrap_u8() as to_signed_int!($t)) as $t;
                  let t = mask & ( *a ^ *b);
                  *a ^= t;
                  *b ^= t;
              }
  *)
  Definition conditional_swap (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ a; b; choice ] =>
      ltac:(M.monadic
        (let a := M.alloc (| a |) in
        let b := M.alloc (| b |) in
        let choice := M.alloc (| choice |) in
        M.read (|
          let~ mask :=
            M.copy (|
              M.use
                (M.alloc (|
                  UnOp.neg (|
                    M.rust_cast
                      (M.call_closure (|
                        M.get_associated_function (| Ty.path "subtle::Choice", "unwrap_u8", [] |),
                        [ choice ]
                      |))
                  |)
                |))
            |) in
          let~ t :=
            M.alloc (|
              BinOp.bit_and
                (M.read (| mask |))
                (BinOp.bit_xor (M.read (| M.read (| a |) |)) (M.read (| M.read (| b |) |)))
            |) in
          let~ _ :=
            let β := M.read (| a |) in
            M.write (| β, BinOp.bit_xor (M.read (| β |)) (M.read (| t |)) |) in
          let~ _ :=
            let β := M.read (| b |) in
            M.write (| β, BinOp.bit_xor (M.read (| β |)) (M.read (| t |)) |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "subtle::ConditionallySelectable"
      Self
      (* Trait polymorphic types *) []
      (* Instance *)
      [
        ("conditional_select", InstanceField.Method conditional_select);
        ("conditional_assign", InstanceField.Method conditional_assign);
        ("conditional_swap", InstanceField.Method conditional_swap)
      ].
End Impl_subtle_ConditionallySelectable_for_i64.

Module Impl_subtle_ConditionallySelectable_for_subtle_Choice.
  Definition Self : Ty.t := Ty.path "subtle::Choice".
  
  (*
      fn conditional_select(a: &Self, b: &Self, choice: Choice) -> Self {
          Choice(u8::conditional_select(&a.0, &b.0, choice))
      }
  *)
  Definition conditional_select (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ a; b; choice ] =>
      ltac:(M.monadic
        (let a := M.alloc (| a |) in
        let b := M.alloc (| b |) in
        let choice := M.alloc (| choice |) in
        Value.StructTuple
          "subtle::Choice"
          [
            M.call_closure (|
              M.get_trait_method (|
                "subtle::ConditionallySelectable",
                Ty.path "u8",
                [],
                "conditional_select",
                []
              |),
              [
                M.SubPointer.get_struct_tuple_field (| M.read (| a |), "subtle::Choice", 0 |);
                M.SubPointer.get_struct_tuple_field (| M.read (| b |), "subtle::Choice", 0 |);
                M.read (| choice |)
              ]
            |)
          ]))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "subtle::ConditionallySelectable"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("conditional_select", InstanceField.Method conditional_select) ].
End Impl_subtle_ConditionallySelectable_for_subtle_Choice.

(* Trait *)
(* Empty module 'ConditionallyNegatable' *)

Module Impl_subtle_ConditionallyNegatable_where_subtle_ConditionallySelectable_T_where_core_ops_arith_Neg_ref__T_for_T.
  Definition Self (T : Ty.t) : Ty.t := T.
  
  (*
      fn conditional_negate(&mut self, choice: Choice) {
          // Need to cast to eliminate mutability
          let self_neg: T = -(self as &T);
          self.conditional_assign(&self_neg, choice);
      }
  *)
  Definition conditional_negate
      (T : Ty.t)
      (ε : list Value.t)
      (τ : list Ty.t)
      (α : list Value.t)
      : M :=
    let Self : Ty.t := Self T in
    match ε, τ, α with
    | [], [], [ self; choice ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let choice := M.alloc (| choice |) in
        M.read (|
          let~ self_neg :=
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::arith::Neg",
                  Ty.apply (Ty.path "&") [] [ T ],
                  [],
                  "neg",
                  []
                |),
                [ M.read (| M.use (M.alloc (| M.read (| self |) |)) |) ]
              |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "subtle::ConditionallySelectable",
                  T,
                  [],
                  "conditional_assign",
                  []
                |),
                [ M.read (| self |); self_neg; M.read (| choice |) ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    forall (T : Ty.t),
    M.IsTraitInstance
      "subtle::ConditionallyNegatable"
      (Self T)
      (* Trait polymorphic types *) []
      (* Instance *) [ ("conditional_negate", InstanceField.Method (conditional_negate T)) ].
End Impl_subtle_ConditionallyNegatable_where_subtle_ConditionallySelectable_T_where_core_ops_arith_Neg_ref__T_for_T.

(* StructRecord
  {
    name := "CtOption";
    const_params := [];
    ty_params := [ "T" ];
    fields := [ ("value", T); ("is_some", Ty.path "subtle::Choice") ];
  } *)

Module Impl_core_clone_Clone_where_core_clone_Clone_T_for_subtle_CtOption_T.
  Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "subtle::CtOption") [] [ T ].
  
  (* Clone *)
  Definition clone (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    let Self : Ty.t := Self T in
    match ε, τ, α with
    | [], [], [ self ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        Value.StructRecord
          "subtle::CtOption"
          [
            ("value",
              M.call_closure (|
                M.get_trait_method (| "core::clone::Clone", T, [], "clone", [] |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "subtle::CtOption",
                    "value"
                  |)
                ]
              |));
            ("is_some",
              M.call_closure (|
                M.get_trait_method (|
                  "core::clone::Clone",
                  Ty.path "subtle::Choice",
                  [],
                  "clone",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "subtle::CtOption",
                    "is_some"
                  |)
                ]
              |))
          ]))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    forall (T : Ty.t),
    M.IsTraitInstance
      "core::clone::Clone"
      (Self T)
      (* Trait polymorphic types *) []
      (* Instance *) [ ("clone", InstanceField.Method (clone T)) ].
End Impl_core_clone_Clone_where_core_clone_Clone_T_for_subtle_CtOption_T.

Module Impl_core_marker_Copy_where_core_marker_Copy_T_for_subtle_CtOption_T.
  Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "subtle::CtOption") [] [ T ].
  
  Axiom Implements :
    forall (T : Ty.t),
    M.IsTraitInstance
      "core::marker::Copy"
      (Self T)
      (* Trait polymorphic types *) []
      (* Instance *) [].
End Impl_core_marker_Copy_where_core_marker_Copy_T_for_subtle_CtOption_T.

Module Impl_core_fmt_Debug_where_core_fmt_Debug_T_for_subtle_CtOption_T.
  Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "subtle::CtOption") [] [ T ].
  
  (* Debug *)
  Definition fmt (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    let Self : Ty.t := Self T in
    match ε, τ, α with
    | [], [], [ self; f ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let f := M.alloc (| f |) in
        M.call_closure (|
          M.get_associated_function (|
            Ty.path "core::fmt::Formatter",
            "debug_struct_field2_finish",
            []
          |),
          [
            M.read (| f |);
            M.read (| Value.String "CtOption" |);
            M.read (| Value.String "value" |);
            M.SubPointer.get_struct_record_field (|
              M.read (| self |),
              "subtle::CtOption",
              "value"
            |);
            M.read (| Value.String "is_some" |);
            M.alloc (|
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "subtle::CtOption",
                "is_some"
              |)
            |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    forall (T : Ty.t),
    M.IsTraitInstance
      "core::fmt::Debug"
      (Self T)
      (* Trait polymorphic types *) []
      (* Instance *) [ ("fmt", InstanceField.Method (fmt T)) ].
End Impl_core_fmt_Debug_where_core_fmt_Debug_T_for_subtle_CtOption_T.

Module Impl_core_convert_From_subtle_CtOption_T_for_core_option_Option_T.
  Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::Option") [] [ T ].
  
  (*
      fn from(source: CtOption<T>) -> Option<T> {
          if source.is_some().unwrap_u8() == 1u8 {
              Option::Some(source.value)
          } else {
              None
          }
      }
  *)
  Definition from (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    let Self : Ty.t := Self T in
    match ε, τ, α with
    | [], [], [ source ] =>
      ltac:(M.monadic
        (let source := M.alloc (| source |) in
        M.read (|
          M.match_operator (|
            M.alloc (| Value.Tuple [] |),
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ :=
                    M.use
                      (M.alloc (|
                        BinOp.eq (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "subtle::Choice",
                              "unwrap_u8",
                              []
                            |),
                            [
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "subtle::CtOption") [] [ T ],
                                    "is_some",
                                    []
                                  |),
                                  [ source ]
                                |)
                              |)
                            ]
                          |),
                          Value.Integer IntegerKind.U8 1
                        |)
                      |)) in
                  let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                  M.alloc (|
                    Value.StructTuple
                      "core::option::Option::Some"
                      [
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            source,
                            "subtle::CtOption",
                            "value"
                          |)
                        |)
                      ]
                  |)));
              fun γ =>
                ltac:(M.monadic (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
            ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    forall (T : Ty.t),
    M.IsTraitInstance
      "core::convert::From"
      (Self T)
      (* Trait polymorphic types *) [ (* T *) Ty.apply (Ty.path "subtle::CtOption") [] [ T ] ]
      (* Instance *) [ ("from", InstanceField.Method (from T)) ].
End Impl_core_convert_From_subtle_CtOption_T_for_core_option_Option_T.

Module Impl_subtle_CtOption_T.
  Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "subtle::CtOption") [] [ T ].
  
  (*
      pub fn new(value: T, is_some: Choice) -> CtOption<T> {
          CtOption {
              value: value,
              is_some: is_some,
          }
      }
  *)
  Definition new (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    let Self : Ty.t := Self T in
    match ε, τ, α with
    | [], [], [ value; is_some ] =>
      ltac:(M.monadic
        (let value := M.alloc (| value |) in
        let is_some := M.alloc (| is_some |) in
        Value.StructRecord
          "subtle::CtOption"
          [ ("value", M.read (| value |)); ("is_some", M.read (| is_some |)) ]))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_new : forall (T : Ty.t), M.IsAssociatedFunction (Self T) "new" (new T).
  
  (*
      pub fn expect(self, msg: &str) -> T {
          assert_eq!(self.is_some.unwrap_u8(), 1, "{}", msg);
  
          self.value
      }
  *)
  Definition expect (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    let Self : Ty.t := Self T in
    match ε, τ, α with
    | [], [], [ self; msg ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let msg := M.alloc (| msg |) in
        M.read (|
          let~ _ :=
            M.match_operator (|
              M.alloc (|
                Value.Tuple
                  [
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (| Ty.path "subtle::Choice", "unwrap_u8", [] |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            self,
                            "subtle::CtOption",
                            "is_some"
                          |)
                        ]
                      |)
                    |);
                    M.alloc (| Value.Integer IntegerKind.U8 1 |)
                  ]
              |),
              [
                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 left_val := M.copy (| γ0_0 |) in
                    let right_val := M.copy (| γ0_1 |) in
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  UnOp.not (|
                                    BinOp.eq (|
                                      M.read (| M.read (| left_val |) |),
                                      M.read (| M.read (| right_val |) |)
                                    |)
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  let~ kind :=
                                    M.alloc (|
                                      Value.StructTuple "core::panicking::AssertKind::Eq" []
                                    |) in
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_function (|
                                        "core::panicking::assert_failed",
                                        [ Ty.path "u8"; Ty.path "u8" ]
                                      |),
                                      [
                                        M.read (| kind |);
                                        M.read (| left_val |);
                                        M.read (| right_val |);
                                        Value.StructTuple
                                          "core::option::Option::Some"
                                          [
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.path "core::fmt::Arguments",
                                                "new_v1",
                                                []
                                              |),
                                              [
                                                M.alloc (|
                                                  Value.Array [ M.read (| Value.String "" |) ]
                                                |);
                                                M.alloc (|
                                                  Value.Array
                                                    [
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path "core::fmt::rt::Argument",
                                                          "new_display",
                                                          [
                                                            Ty.apply
                                                              (Ty.path "&")
                                                              []
                                                              [ Ty.path "str" ]
                                                          ]
                                                        |),
                                                        [ msg ]
                                                      |)
                                                    ]
                                                |)
                                              ]
                                            |)
                                          ]
                                      ]
                                    |)
                                  |)
                                |)
                              |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |)))
              ]
            |) in
          M.SubPointer.get_struct_record_field (| self, "subtle::CtOption", "value" |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_expect :
    forall (T : Ty.t),
    M.IsAssociatedFunction (Self T) "expect" (expect T).
  
  (*
      pub fn unwrap(self) -> T {
          assert_eq!(self.is_some.unwrap_u8(), 1);
  
          self.value
      }
  *)
  Definition unwrap (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    let Self : Ty.t := Self T in
    match ε, τ, α with
    | [], [], [ self ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        M.read (|
          let~ _ :=
            M.match_operator (|
              M.alloc (|
                Value.Tuple
                  [
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (| Ty.path "subtle::Choice", "unwrap_u8", [] |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            self,
                            "subtle::CtOption",
                            "is_some"
                          |)
                        ]
                      |)
                    |);
                    M.alloc (| Value.Integer IntegerKind.U8 1 |)
                  ]
              |),
              [
                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 left_val := M.copy (| γ0_0 |) in
                    let right_val := M.copy (| γ0_1 |) in
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  UnOp.not (|
                                    BinOp.eq (|
                                      M.read (| M.read (| left_val |) |),
                                      M.read (| M.read (| right_val |) |)
                                    |)
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  let~ kind :=
                                    M.alloc (|
                                      Value.StructTuple "core::panicking::AssertKind::Eq" []
                                    |) in
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_function (|
                                        "core::panicking::assert_failed",
                                        [ Ty.path "u8"; Ty.path "u8" ]
                                      |),
                                      [
                                        M.read (| kind |);
                                        M.read (| left_val |);
                                        M.read (| right_val |);
                                        Value.StructTuple "core::option::Option::None" []
                                      ]
                                    |)
                                  |)
                                |)
                              |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |)))
              ]
            |) in
          M.SubPointer.get_struct_record_field (| self, "subtle::CtOption", "value" |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_unwrap :
    forall (T : Ty.t),
    M.IsAssociatedFunction (Self T) "unwrap" (unwrap T).
  
  (*
      pub fn unwrap_or(self, def: T) -> T
      where
          T: ConditionallySelectable,
      {
          T::conditional_select(&def, &self.value, self.is_some)
      }
  *)
  Definition unwrap_or (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    let Self : Ty.t := Self T in
    match ε, τ, α with
    | [], [], [ self; def ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let def := M.alloc (| def |) in
        M.call_closure (|
          M.get_trait_method (|
            "subtle::ConditionallySelectable",
            T,
            [],
            "conditional_select",
            []
          |),
          [
            def;
            M.SubPointer.get_struct_record_field (| self, "subtle::CtOption", "value" |);
            M.read (|
              M.SubPointer.get_struct_record_field (| self, "subtle::CtOption", "is_some" |)
            |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_unwrap_or :
    forall (T : Ty.t),
    M.IsAssociatedFunction (Self T) "unwrap_or" (unwrap_or T).
  
  (*
      pub fn unwrap_or_else<F>(self, f: F) -> T
      where
          T: ConditionallySelectable,
          F: FnOnce() -> T,
      {
          T::conditional_select(&f(), &self.value, self.is_some)
      }
  *)
  Definition unwrap_or_else (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    let Self : Ty.t := Self T in
    match ε, τ, α with
    | [], [ F ], [ self; f ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let f := M.alloc (| f |) in
        M.call_closure (|
          M.get_trait_method (|
            "subtle::ConditionallySelectable",
            T,
            [],
            "conditional_select",
            []
          |),
          [
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::function::FnOnce",
                  F,
                  [ Ty.tuple [] ],
                  "call_once",
                  []
                |),
                [ M.read (| f |); Value.Tuple [] ]
              |)
            |);
            M.SubPointer.get_struct_record_field (| self, "subtle::CtOption", "value" |);
            M.read (|
              M.SubPointer.get_struct_record_field (| self, "subtle::CtOption", "is_some" |)
            |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_unwrap_or_else :
    forall (T : Ty.t),
    M.IsAssociatedFunction (Self T) "unwrap_or_else" (unwrap_or_else T).
  
  (*
      pub fn is_some(&self) -> Choice {
          self.is_some
      }
  *)
  Definition is_some (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    let Self : Ty.t := Self T in
    match ε, τ, α with
    | [], [], [ self ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        M.read (|
          M.SubPointer.get_struct_record_field (|
            M.read (| self |),
            "subtle::CtOption",
            "is_some"
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_is_some :
    forall (T : Ty.t),
    M.IsAssociatedFunction (Self T) "is_some" (is_some T).
  
  (*
      pub fn is_none(&self) -> Choice {
          !self.is_some
      }
  *)
  Definition is_none (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    let Self : Ty.t := Self T in
    match ε, τ, α with
    | [], [], [ self ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        M.call_closure (|
          M.get_trait_method (| "core::ops::bit::Not", Ty.path "subtle::Choice", [], "not", [] |),
          [
            M.read (|
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "subtle::CtOption",
                "is_some"
              |)
            |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_is_none :
    forall (T : Ty.t),
    M.IsAssociatedFunction (Self T) "is_none" (is_none T).
  
  (*
      pub fn map<U, F>(self, f: F) -> CtOption<U>
      where
          T: Default + ConditionallySelectable,
          F: FnOnce(T) -> U,
      {
          CtOption::new(
              f(T::conditional_select(
                  &T::default(),
                  &self.value,
                  self.is_some,
              )),
              self.is_some,
          )
      }
  *)
  Definition map (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    let Self : Ty.t := Self T in
    match ε, τ, α with
    | [], [ U; F ], [ 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.apply (Ty.path "subtle::CtOption") [] [ U ], "new", [] |),
          [
            M.call_closure (|
              M.get_trait_method (|
                "core::ops::function::FnOnce",
                F,
                [ Ty.tuple [ T ] ],
                "call_once",
                []
              |),
              [
                M.read (| f |);
                Value.Tuple
                  [
                    M.call_closure (|
                      M.get_trait_method (|
                        "subtle::ConditionallySelectable",
                        T,
                        [],
                        "conditional_select",
                        []
                      |),
                      [
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                            []
                          |)
                        |);
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "subtle::CtOption",
                          "value"
                        |);
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            self,
                            "subtle::CtOption",
                            "is_some"
                          |)
                        |)
                      ]
                    |)
                  ]
              ]
            |);
            M.read (|
              M.SubPointer.get_struct_record_field (| self, "subtle::CtOption", "is_some" |)
            |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_map : forall (T : Ty.t), M.IsAssociatedFunction (Self T) "map" (map T).
  
  (*
      pub fn and_then<U, F>(self, f: F) -> CtOption<U>
      where
          T: Default + ConditionallySelectable,
          F: FnOnce(T) -> CtOption<U>,
      {
          let mut tmp = f(T::conditional_select(
              &T::default(),
              &self.value,
              self.is_some,
          ));
          tmp.is_some &= self.is_some;
  
          tmp
      }
  *)
  Definition and_then (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    let Self : Ty.t := Self T in
    match ε, τ, α with
    | [], [ U; F ], [ self; f ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let f := M.alloc (| f |) in
        M.read (|
          let~ tmp :=
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::function::FnOnce",
                  F,
                  [ Ty.tuple [ T ] ],
                  "call_once",
                  []
                |),
                [
                  M.read (| f |);
                  Value.Tuple
                    [
                      M.call_closure (|
                        M.get_trait_method (|
                          "subtle::ConditionallySelectable",
                          T,
                          [],
                          "conditional_select",
                          []
                        |),
                        [
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::default::Default",
                                T,
                                [],
                                "default",
                                []
                              |),
                              []
                            |)
                          |);
                          M.SubPointer.get_struct_record_field (|
                            self,
                            "subtle::CtOption",
                            "value"
                          |);
                          M.read (|
                            M.SubPointer.get_struct_record_field (|
                              self,
                              "subtle::CtOption",
                              "is_some"
                            |)
                          |)
                        ]
                      |)
                    ]
                ]
              |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::bit::BitAndAssign",
                  Ty.path "subtle::Choice",
                  [ Ty.path "subtle::Choice" ],
                  "bitand_assign",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (| tmp, "subtle::CtOption", "is_some" |);
                  M.read (|
                    M.SubPointer.get_struct_record_field (| self, "subtle::CtOption", "is_some" |)
                  |)
                ]
              |)
            |) in
          tmp
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_and_then :
    forall (T : Ty.t),
    M.IsAssociatedFunction (Self T) "and_then" (and_then T).
  
  (*
      pub fn or_else<F>(self, f: F) -> CtOption<T>
      where
          T: ConditionallySelectable,
          F: FnOnce() -> CtOption<T>,
      {
          let is_none = self.is_none();
          let f = f();
  
          Self::conditional_select(&self, &f, is_none)
      }
  *)
  Definition or_else (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    let Self : Ty.t := Self T in
    match ε, τ, α with
    | [], [ F ], [ self; f ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let f := M.alloc (| f |) in
        M.read (|
          let~ is_none :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "subtle::CtOption") [] [ T ],
                  "is_none",
                  []
                |),
                [ self ]
              |)
            |) in
          let~ f :=
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::function::FnOnce",
                  F,
                  [ Ty.tuple [] ],
                  "call_once",
                  []
                |),
                [ M.read (| f |); Value.Tuple [] ]
              |)
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_trait_method (|
                "subtle::ConditionallySelectable",
                Ty.apply (Ty.path "subtle::CtOption") [] [ T ],
                [],
                "conditional_select",
                []
              |),
              [ self; f; M.read (| is_none |) ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_or_else :
    forall (T : Ty.t),
    M.IsAssociatedFunction (Self T) "or_else" (or_else T).
End Impl_subtle_CtOption_T.

Module Impl_subtle_ConditionallySelectable_where_subtle_ConditionallySelectable_T_for_subtle_CtOption_T.
  Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "subtle::CtOption") [] [ T ].
  
  (*
      fn conditional_select(a: &Self, b: &Self, choice: Choice) -> Self {
          CtOption::new(
              T::conditional_select(&a.value, &b.value, choice),
              Choice::conditional_select(&a.is_some, &b.is_some, choice),
          )
      }
  *)
  Definition conditional_select
      (T : Ty.t)
      (ε : list Value.t)
      (τ : list Ty.t)
      (α : list Value.t)
      : M :=
    let Self : Ty.t := Self T in
    match ε, τ, α with
    | [], [], [ a; b; choice ] =>
      ltac:(M.monadic
        (let a := M.alloc (| a |) in
        let b := M.alloc (| b |) in
        let choice := M.alloc (| choice |) in
        M.call_closure (|
          M.get_associated_function (| Ty.apply (Ty.path "subtle::CtOption") [] [ T ], "new", [] |),
          [
            M.call_closure (|
              M.get_trait_method (|
                "subtle::ConditionallySelectable",
                T,
                [],
                "conditional_select",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| a |),
                  "subtle::CtOption",
                  "value"
                |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| b |),
                  "subtle::CtOption",
                  "value"
                |);
                M.read (| choice |)
              ]
            |);
            M.call_closure (|
              M.get_trait_method (|
                "subtle::ConditionallySelectable",
                Ty.path "subtle::Choice",
                [],
                "conditional_select",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| a |),
                  "subtle::CtOption",
                  "is_some"
                |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| b |),
                  "subtle::CtOption",
                  "is_some"
                |);
                M.read (| choice |)
              ]
            |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    forall (T : Ty.t),
    M.IsTraitInstance
      "subtle::ConditionallySelectable"
      (Self T)
      (* Trait polymorphic types *) []
      (* Instance *) [ ("conditional_select", InstanceField.Method (conditional_select T)) ].
End Impl_subtle_ConditionallySelectable_where_subtle_ConditionallySelectable_T_for_subtle_CtOption_T.

Module Impl_subtle_ConstantTimeEq_where_subtle_ConstantTimeEq_T_for_subtle_CtOption_T.
  Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "subtle::CtOption") [] [ T ].
  
  (*
      fn ct_eq(&self, rhs: &CtOption<T>) -> Choice {
          let a = self.is_some();
          let b = rhs.is_some();
  
          (a & b & self.value.ct_eq(&rhs.value)) | (!a & !b)
      }
  *)
  Definition ct_eq (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    let Self : Ty.t := Self T in
    match ε, τ, α with
    | [], [], [ self; rhs ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let rhs := M.alloc (| rhs |) in
        M.read (|
          let~ a :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "subtle::CtOption") [] [ T ],
                  "is_some",
                  []
                |),
                [ M.read (| self |) ]
              |)
            |) in
          let~ b :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "subtle::CtOption") [] [ T ],
                  "is_some",
                  []
                |),
                [ M.read (| rhs |) ]
              |)
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_trait_method (|
                "core::ops::bit::BitOr",
                Ty.path "subtle::Choice",
                [ Ty.path "subtle::Choice" ],
                "bitor",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::bit::BitAnd",
                    Ty.path "subtle::Choice",
                    [ Ty.path "subtle::Choice" ],
                    "bitand",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::bit::BitAnd",
                        Ty.path "subtle::Choice",
                        [ Ty.path "subtle::Choice" ],
                        "bitand",
                        []
                      |),
                      [ M.read (| a |); M.read (| b |) ]
                    |);
                    M.call_closure (|
                      M.get_trait_method (| "subtle::ConstantTimeEq", T, [], "ct_eq", [] |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "subtle::CtOption",
                          "value"
                        |);
                        M.SubPointer.get_struct_record_field (|
                          M.read (| rhs |),
                          "subtle::CtOption",
                          "value"
                        |)
                      ]
                    |)
                  ]
                |);
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::bit::BitAnd",
                    Ty.path "subtle::Choice",
                    [ Ty.path "subtle::Choice" ],
                    "bitand",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::bit::Not",
                        Ty.path "subtle::Choice",
                        [],
                        "not",
                        []
                      |),
                      [ M.read (| a |) ]
                    |);
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::bit::Not",
                        Ty.path "subtle::Choice",
                        [],
                        "not",
                        []
                      |),
                      [ M.read (| b |) ]
                    |)
                  ]
                |)
              ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    forall (T : Ty.t),
    M.IsTraitInstance
      "subtle::ConstantTimeEq"
      (Self T)
      (* Trait polymorphic types *) []
      (* Instance *) [ ("ct_eq", InstanceField.Method (ct_eq T)) ].
End Impl_subtle_ConstantTimeEq_where_subtle_ConstantTimeEq_T_for_subtle_CtOption_T.

(* Trait *)
(* Empty module 'ConstantTimeGreater' *)

Module Impl_subtle_ConstantTimeGreater_for_u8.
  Definition Self : Ty.t := Ty.path "u8".
  
  (*
              fn ct_gt(&self, other: &$t_u) -> Choice {
                  let gtb = self & !other; // All the bits in self that are greater than their corresponding bits in other.
                  let mut ltb = !self & other; // All the bits in self that are less than their corresponding bits in other.
                  let mut pow = 1;
  
                  // Less-than operator is okay here because it's dependent on the bit-width.
                  while pow < $bit_width {
                      ltb |= ltb >> pow; // Bit-smear the highest set bit to the right.
                      pow += pow;
                  }
                  let mut bit = gtb & !ltb; // Select the highest set bit.
                  let mut pow = 1;
  
                  while pow < $bit_width {
                      bit |= bit >> pow; // Shift it to the right until we end up with either 0 or 1.
                      pow += pow;
                  }
                  // XXX We should possibly do the above flattening to 0 or 1 in the
                  //     Choice constructor rather than making it a debug error?
                  Choice::from((bit & 1) as u8)
              }
  *)
  Definition ct_gt (ε : 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~ gtb :=
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::bit::BitAnd",
                  Ty.apply (Ty.path "&") [] [ Ty.path "u8" ],
                  [ Ty.path "u8" ],
                  "bitand",
                  []
                |),
                [
                  M.read (| self |);
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::bit::Not",
                      Ty.apply (Ty.path "&") [] [ Ty.path "u8" ],
                      [],
                      "not",
                      []
                    |),
                    [ M.read (| other |) ]
                  |)
                ]
              |)
            |) in
          let~ ltb :=
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::bit::BitAnd",
                  Ty.path "u8",
                  [ Ty.apply (Ty.path "&") [] [ Ty.path "u8" ] ],
                  "bitand",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::bit::Not",
                      Ty.apply (Ty.path "&") [] [ Ty.path "u8" ],
                      [],
                      "not",
                      []
                    |),
                    [ M.read (| self |) ]
                  |);
                  M.read (| other |)
                ]
              |)
            |) in
          let~ pow := M.alloc (| Value.Integer IntegerKind.I32 1 |) in
          let~ _ :=
            M.loop (|
              ltac:(M.monadic
                (M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.lt (| M.read (| pow |), Value.Integer IntegerKind.I32 8 |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ _ :=
                          let β := ltb in
                          M.write (|
                            β,
                            BinOp.bit_or
                              (M.read (| β |))
                              (BinOp.Wrap.shr (| M.read (| ltb |), M.read (| pow |) |))
                          |) in
                        let~ _ :=
                          let β := pow in
                          M.write (| β, BinOp.Wrap.add (| M.read (| β |), M.read (| pow |) |) |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              let~ _ :=
                                M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |) in
                              M.alloc (| Value.Tuple [] |)
                            |)
                          |)
                        |)))
                  ]
                |)))
            |) in
          let~ bit :=
            M.alloc (| BinOp.bit_and (M.read (| gtb |)) (UnOp.not (| M.read (| ltb |) |)) |) in
          let~ pow := M.alloc (| Value.Integer IntegerKind.I32 1 |) in
          let~ _ :=
            M.loop (|
              ltac:(M.monadic
                (M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.lt (| M.read (| pow |), Value.Integer IntegerKind.I32 8 |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ _ :=
                          let β := bit in
                          M.write (|
                            β,
                            BinOp.bit_or
                              (M.read (| β |))
                              (BinOp.Wrap.shr (| M.read (| bit |), M.read (| pow |) |))
                          |) in
                        let~ _ :=
                          let β := pow in
                          M.write (| β, BinOp.Wrap.add (| M.read (| β |), M.read (| pow |) |) |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              let~ _ :=
                                M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |) in
                              M.alloc (| Value.Tuple [] |)
                            |)
                          |)
                        |)))
                  ]
                |)))
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_trait_method (|
                "core::convert::From",
                Ty.path "subtle::Choice",
                [ Ty.path "u8" ],
                "from",
                []
              |),
              [
                M.read (|
                  M.use
                    (M.alloc (|
                      BinOp.bit_and (M.read (| bit |)) (Value.Integer IntegerKind.U8 1)
                    |))
                |)
              ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "subtle::ConstantTimeGreater"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("ct_gt", InstanceField.Method ct_gt) ].
End Impl_subtle_ConstantTimeGreater_for_u8.

Module Impl_subtle_ConstantTimeGreater_for_u16.
  Definition Self : Ty.t := Ty.path "u16".
  
  (*
              fn ct_gt(&self, other: &$t_u) -> Choice {
                  let gtb = self & !other; // All the bits in self that are greater than their corresponding bits in other.
                  let mut ltb = !self & other; // All the bits in self that are less than their corresponding bits in other.
                  let mut pow = 1;
  
                  // Less-than operator is okay here because it's dependent on the bit-width.
                  while pow < $bit_width {
                      ltb |= ltb >> pow; // Bit-smear the highest set bit to the right.
                      pow += pow;
                  }
                  let mut bit = gtb & !ltb; // Select the highest set bit.
                  let mut pow = 1;
  
                  while pow < $bit_width {
                      bit |= bit >> pow; // Shift it to the right until we end up with either 0 or 1.
                      pow += pow;
                  }
                  // XXX We should possibly do the above flattening to 0 or 1 in the
                  //     Choice constructor rather than making it a debug error?
                  Choice::from((bit & 1) as u8)
              }
  *)
  Definition ct_gt (ε : 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~ gtb :=
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::bit::BitAnd",
                  Ty.apply (Ty.path "&") [] [ Ty.path "u16" ],
                  [ Ty.path "u16" ],
                  "bitand",
                  []
                |),
                [
                  M.read (| self |);
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::bit::Not",
                      Ty.apply (Ty.path "&") [] [ Ty.path "u16" ],
                      [],
                      "not",
                      []
                    |),
                    [ M.read (| other |) ]
                  |)
                ]
              |)
            |) in
          let~ ltb :=
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::bit::BitAnd",
                  Ty.path "u16",
                  [ Ty.apply (Ty.path "&") [] [ Ty.path "u16" ] ],
                  "bitand",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::bit::Not",
                      Ty.apply (Ty.path "&") [] [ Ty.path "u16" ],
                      [],
                      "not",
                      []
                    |),
                    [ M.read (| self |) ]
                  |);
                  M.read (| other |)
                ]
              |)
            |) in
          let~ pow := M.alloc (| Value.Integer IntegerKind.I32 1 |) in
          let~ _ :=
            M.loop (|
              ltac:(M.monadic
                (M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.lt (| M.read (| pow |), Value.Integer IntegerKind.I32 16 |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ _ :=
                          let β := ltb in
                          M.write (|
                            β,
                            BinOp.bit_or
                              (M.read (| β |))
                              (BinOp.Wrap.shr (| M.read (| ltb |), M.read (| pow |) |))
                          |) in
                        let~ _ :=
                          let β := pow in
                          M.write (| β, BinOp.Wrap.add (| M.read (| β |), M.read (| pow |) |) |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              let~ _ :=
                                M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |) in
                              M.alloc (| Value.Tuple [] |)
                            |)
                          |)
                        |)))
                  ]
                |)))
            |) in
          let~ bit :=
            M.alloc (| BinOp.bit_and (M.read (| gtb |)) (UnOp.not (| M.read (| ltb |) |)) |) in
          let~ pow := M.alloc (| Value.Integer IntegerKind.I32 1 |) in
          let~ _ :=
            M.loop (|
              ltac:(M.monadic
                (M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.lt (| M.read (| pow |), Value.Integer IntegerKind.I32 16 |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ _ :=
                          let β := bit in
                          M.write (|
                            β,
                            BinOp.bit_or
                              (M.read (| β |))
                              (BinOp.Wrap.shr (| M.read (| bit |), M.read (| pow |) |))
                          |) in
                        let~ _ :=
                          let β := pow in
                          M.write (| β, BinOp.Wrap.add (| M.read (| β |), M.read (| pow |) |) |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              let~ _ :=
                                M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |) in
                              M.alloc (| Value.Tuple [] |)
                            |)
                          |)
                        |)))
                  ]
                |)))
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_trait_method (|
                "core::convert::From",
                Ty.path "subtle::Choice",
                [ Ty.path "u8" ],
                "from",
                []
              |),
              [ M.rust_cast (BinOp.bit_and (M.read (| bit |)) (Value.Integer IntegerKind.U16 1)) ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "subtle::ConstantTimeGreater"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("ct_gt", InstanceField.Method ct_gt) ].
End Impl_subtle_ConstantTimeGreater_for_u16.

Module Impl_subtle_ConstantTimeGreater_for_u32.
  Definition Self : Ty.t := Ty.path "u32".
  
  (*
              fn ct_gt(&self, other: &$t_u) -> Choice {
                  let gtb = self & !other; // All the bits in self that are greater than their corresponding bits in other.
                  let mut ltb = !self & other; // All the bits in self that are less than their corresponding bits in other.
                  let mut pow = 1;
  
                  // Less-than operator is okay here because it's dependent on the bit-width.
                  while pow < $bit_width {
                      ltb |= ltb >> pow; // Bit-smear the highest set bit to the right.
                      pow += pow;
                  }
                  let mut bit = gtb & !ltb; // Select the highest set bit.
                  let mut pow = 1;
  
                  while pow < $bit_width {
                      bit |= bit >> pow; // Shift it to the right until we end up with either 0 or 1.
                      pow += pow;
                  }
                  // XXX We should possibly do the above flattening to 0 or 1 in the
                  //     Choice constructor rather than making it a debug error?
                  Choice::from((bit & 1) as u8)
              }
  *)
  Definition ct_gt (ε : 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~ gtb :=
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::bit::BitAnd",
                  Ty.apply (Ty.path "&") [] [ Ty.path "u32" ],
                  [ Ty.path "u32" ],
                  "bitand",
                  []
                |),
                [
                  M.read (| self |);
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::bit::Not",
                      Ty.apply (Ty.path "&") [] [ Ty.path "u32" ],
                      [],
                      "not",
                      []
                    |),
                    [ M.read (| other |) ]
                  |)
                ]
              |)
            |) in
          let~ ltb :=
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::bit::BitAnd",
                  Ty.path "u32",
                  [ Ty.apply (Ty.path "&") [] [ Ty.path "u32" ] ],
                  "bitand",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::bit::Not",
                      Ty.apply (Ty.path "&") [] [ Ty.path "u32" ],
                      [],
                      "not",
                      []
                    |),
                    [ M.read (| self |) ]
                  |);
                  M.read (| other |)
                ]
              |)
            |) in
          let~ pow := M.alloc (| Value.Integer IntegerKind.I32 1 |) in
          let~ _ :=
            M.loop (|
              ltac:(M.monadic
                (M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.lt (| M.read (| pow |), Value.Integer IntegerKind.I32 32 |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ _ :=
                          let β := ltb in
                          M.write (|
                            β,
                            BinOp.bit_or
                              (M.read (| β |))
                              (BinOp.Wrap.shr (| M.read (| ltb |), M.read (| pow |) |))
                          |) in
                        let~ _ :=
                          let β := pow in
                          M.write (| β, BinOp.Wrap.add (| M.read (| β |), M.read (| pow |) |) |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              let~ _ :=
                                M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |) in
                              M.alloc (| Value.Tuple [] |)
                            |)
                          |)
                        |)))
                  ]
                |)))
            |) in
          let~ bit :=
            M.alloc (| BinOp.bit_and (M.read (| gtb |)) (UnOp.not (| M.read (| ltb |) |)) |) in
          let~ pow := M.alloc (| Value.Integer IntegerKind.I32 1 |) in
          let~ _ :=
            M.loop (|
              ltac:(M.monadic
                (M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.lt (| M.read (| pow |), Value.Integer IntegerKind.I32 32 |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ _ :=
                          let β := bit in
                          M.write (|
                            β,
                            BinOp.bit_or
                              (M.read (| β |))
                              (BinOp.Wrap.shr (| M.read (| bit |), M.read (| pow |) |))
                          |) in
                        let~ _ :=
                          let β := pow in
                          M.write (| β, BinOp.Wrap.add (| M.read (| β |), M.read (| pow |) |) |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              let~ _ :=
                                M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |) in
                              M.alloc (| Value.Tuple [] |)
                            |)
                          |)
                        |)))
                  ]
                |)))
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_trait_method (|
                "core::convert::From",
                Ty.path "subtle::Choice",
                [ Ty.path "u8" ],
                "from",
                []
              |),
              [ M.rust_cast (BinOp.bit_and (M.read (| bit |)) (Value.Integer IntegerKind.U32 1)) ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "subtle::ConstantTimeGreater"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("ct_gt", InstanceField.Method ct_gt) ].
End Impl_subtle_ConstantTimeGreater_for_u32.

Module Impl_subtle_ConstantTimeGreater_for_u64.
  Definition Self : Ty.t := Ty.path "u64".
  
  (*
              fn ct_gt(&self, other: &$t_u) -> Choice {
                  let gtb = self & !other; // All the bits in self that are greater than their corresponding bits in other.
                  let mut ltb = !self & other; // All the bits in self that are less than their corresponding bits in other.
                  let mut pow = 1;
  
                  // Less-than operator is okay here because it's dependent on the bit-width.
                  while pow < $bit_width {
                      ltb |= ltb >> pow; // Bit-smear the highest set bit to the right.
                      pow += pow;
                  }
                  let mut bit = gtb & !ltb; // Select the highest set bit.
                  let mut pow = 1;
  
                  while pow < $bit_width {
                      bit |= bit >> pow; // Shift it to the right until we end up with either 0 or 1.
                      pow += pow;
                  }
                  // XXX We should possibly do the above flattening to 0 or 1 in the
                  //     Choice constructor rather than making it a debug error?
                  Choice::from((bit & 1) as u8)
              }
  *)
  Definition ct_gt (ε : 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~ gtb :=
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::bit::BitAnd",
                  Ty.apply (Ty.path "&") [] [ Ty.path "u64" ],
                  [ Ty.path "u64" ],
                  "bitand",
                  []
                |),
                [
                  M.read (| self |);
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::bit::Not",
                      Ty.apply (Ty.path "&") [] [ Ty.path "u64" ],
                      [],
                      "not",
                      []
                    |),
                    [ M.read (| other |) ]
                  |)
                ]
              |)
            |) in
          let~ ltb :=
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::bit::BitAnd",
                  Ty.path "u64",
                  [ Ty.apply (Ty.path "&") [] [ Ty.path "u64" ] ],
                  "bitand",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::bit::Not",
                      Ty.apply (Ty.path "&") [] [ Ty.path "u64" ],
                      [],
                      "not",
                      []
                    |),
                    [ M.read (| self |) ]
                  |);
                  M.read (| other |)
                ]
              |)
            |) in
          let~ pow := M.alloc (| Value.Integer IntegerKind.I32 1 |) in
          let~ _ :=
            M.loop (|
              ltac:(M.monadic
                (M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.lt (| M.read (| pow |), Value.Integer IntegerKind.I32 64 |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ _ :=
                          let β := ltb in
                          M.write (|
                            β,
                            BinOp.bit_or
                              (M.read (| β |))
                              (BinOp.Wrap.shr (| M.read (| ltb |), M.read (| pow |) |))
                          |) in
                        let~ _ :=
                          let β := pow in
                          M.write (| β, BinOp.Wrap.add (| M.read (| β |), M.read (| pow |) |) |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              let~ _ :=
                                M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |) in
                              M.alloc (| Value.Tuple [] |)
                            |)
                          |)
                        |)))
                  ]
                |)))
            |) in
          let~ bit :=
            M.alloc (| BinOp.bit_and (M.read (| gtb |)) (UnOp.not (| M.read (| ltb |) |)) |) in
          let~ pow := M.alloc (| Value.Integer IntegerKind.I32 1 |) in
          let~ _ :=
            M.loop (|
              ltac:(M.monadic
                (M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.lt (| M.read (| pow |), Value.Integer IntegerKind.I32 64 |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ _ :=
                          let β := bit in
                          M.write (|
                            β,
                            BinOp.bit_or
                              (M.read (| β |))
                              (BinOp.Wrap.shr (| M.read (| bit |), M.read (| pow |) |))
                          |) in
                        let~ _ :=
                          let β := pow in
                          M.write (| β, BinOp.Wrap.add (| M.read (| β |), M.read (| pow |) |) |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              let~ _ :=
                                M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |) in
                              M.alloc (| Value.Tuple [] |)
                            |)
                          |)
                        |)))
                  ]
                |)))
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_trait_method (|
                "core::convert::From",
                Ty.path "subtle::Choice",
                [ Ty.path "u8" ],
                "from",
                []
              |),
              [ M.rust_cast (BinOp.bit_and (M.read (| bit |)) (Value.Integer IntegerKind.U64 1)) ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "subtle::ConstantTimeGreater"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("ct_gt", InstanceField.Method ct_gt) ].
End Impl_subtle_ConstantTimeGreater_for_u64.

(* Trait *)
Module ConstantTimeLess.
  Definition ct_lt (Self : Ty.t) (ε : 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.call_closure (|
          M.get_trait_method (|
            "core::ops::bit::BitAnd",
            Ty.path "subtle::Choice",
            [ Ty.path "subtle::Choice" ],
            "bitand",
            []
          |),
          [
            M.call_closure (|
              M.get_trait_method (|
                "core::ops::bit::Not",
                Ty.path "subtle::Choice",
                [],
                "not",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (| "subtle::ConstantTimeGreater", Self, [], "ct_gt", [] |),
                  [ M.read (| self |); M.read (| other |) ]
                |)
              ]
            |);
            M.call_closure (|
              M.get_trait_method (|
                "core::ops::bit::Not",
                Ty.path "subtle::Choice",
                [],
                "not",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (| "subtle::ConstantTimeEq", Self, [], "ct_eq", [] |),
                  [ M.read (| self |); M.read (| other |) ]
                |)
              ]
            |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom ProvidedMethod_ct_lt : M.IsProvidedMethod "subtle::ConstantTimeLess" "ct_lt" ct_lt.
End ConstantTimeLess.

Module Impl_subtle_ConstantTimeLess_for_u8.
  Definition Self : Ty.t := Ty.path "u8".
  
  Axiom Implements :
    M.IsTraitInstance
      "subtle::ConstantTimeLess"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [].
End Impl_subtle_ConstantTimeLess_for_u8.

Module Impl_subtle_ConstantTimeLess_for_u16.
  Definition Self : Ty.t := Ty.path "u16".
  
  Axiom Implements :
    M.IsTraitInstance
      "subtle::ConstantTimeLess"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [].
End Impl_subtle_ConstantTimeLess_for_u16.

Module Impl_subtle_ConstantTimeLess_for_u32.
  Definition Self : Ty.t := Ty.path "u32".
  
  Axiom Implements :
    M.IsTraitInstance
      "subtle::ConstantTimeLess"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [].
End Impl_subtle_ConstantTimeLess_for_u32.

Module Impl_subtle_ConstantTimeLess_for_u64.
  Definition Self : Ty.t := Ty.path "u64".
  
  Axiom Implements :
    M.IsTraitInstance
      "subtle::ConstantTimeLess"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [].
End Impl_subtle_ConstantTimeLess_for_u64.
