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

Module random.
  (* Trait *)
  (* Empty module 'RandomSource' *)
  
  (* Trait *)
  (* Empty module 'Random' *)
  
  Module Impl_core_random_Random_for_bool.
    Definition Self : Ty.t := Ty.path "bool".
    
    (*
        fn random(source: &mut (impl RandomSource + ?Sized)) -> Self {
            u8::random(source) & 1 == 1
        }
    *)
    Definition random (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ impl_RandomSource__plus___Sized ], [ source ] =>
        ltac:(M.monadic
          (let source := M.alloc (| source |) in
          BinOp.eq (|
            BinOp.bit_and
              (M.call_closure (|
                M.get_trait_method (|
                  "core::random::Random",
                  Ty.path "u8",
                  [],
                  "random",
                  [ impl_RandomSource__plus___Sized ]
                |),
                [ M.read (| source |) ]
              |))
              (Value.Integer IntegerKind.U8 1),
            Value.Integer IntegerKind.U8 1
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::random::Random"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("random", InstanceField.Method random) ].
  End Impl_core_random_Random_for_bool.
  
  Module Impl_core_random_Random_for_u8.
    Definition Self : Ty.t := Ty.path "u8".
    
    (*
                fn random(source: &mut (impl RandomSource + ?Sized)) -> Self {
                    let mut bytes = (0 as Self).to_ne_bytes();
                    source.fill_bytes(&mut bytes);
                    Self::from_ne_bytes(bytes)
                }
    *)
    Definition random (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ impl_RandomSource__plus___Sized ], [ source ] =>
        ltac:(M.monadic
          (let source := M.alloc (| source |) in
          M.read (|
            let~ bytes :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "u8", "to_ne_bytes", [] |),
                  [ M.read (| M.use (M.alloc (| Value.Integer IntegerKind.U8 0 |)) |) ]
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::random::RandomSource",
                    impl_RandomSource__plus___Sized,
                    [],
                    "fill_bytes",
                    []
                  |),
                  [ M.read (| source |); bytes ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "u8", "from_ne_bytes", [] |),
                [ M.read (| bytes |) ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::random::Random"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("random", InstanceField.Method random) ].
  End Impl_core_random_Random_for_u8.
  
  Module Impl_core_random_Random_for_i8.
    Definition Self : Ty.t := Ty.path "i8".
    
    (*
                fn random(source: &mut (impl RandomSource + ?Sized)) -> Self {
                    let mut bytes = (0 as Self).to_ne_bytes();
                    source.fill_bytes(&mut bytes);
                    Self::from_ne_bytes(bytes)
                }
    *)
    Definition random (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ impl_RandomSource__plus___Sized ], [ source ] =>
        ltac:(M.monadic
          (let source := M.alloc (| source |) in
          M.read (|
            let~ bytes :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "i8", "to_ne_bytes", [] |),
                  [ M.read (| M.use (M.alloc (| Value.Integer IntegerKind.I8 0 |)) |) ]
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::random::RandomSource",
                    impl_RandomSource__plus___Sized,
                    [],
                    "fill_bytes",
                    []
                  |),
                  [ M.read (| source |); bytes ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "i8", "from_ne_bytes", [] |),
                [ M.read (| bytes |) ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::random::Random"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("random", InstanceField.Method random) ].
  End Impl_core_random_Random_for_i8.
  
  Module Impl_core_random_Random_for_u16.
    Definition Self : Ty.t := Ty.path "u16".
    
    (*
                fn random(source: &mut (impl RandomSource + ?Sized)) -> Self {
                    let mut bytes = (0 as Self).to_ne_bytes();
                    source.fill_bytes(&mut bytes);
                    Self::from_ne_bytes(bytes)
                }
    *)
    Definition random (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ impl_RandomSource__plus___Sized ], [ source ] =>
        ltac:(M.monadic
          (let source := M.alloc (| source |) in
          M.read (|
            let~ bytes :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "u16", "to_ne_bytes", [] |),
                  [ M.read (| M.use (M.alloc (| Value.Integer IntegerKind.U16 0 |)) |) ]
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::random::RandomSource",
                    impl_RandomSource__plus___Sized,
                    [],
                    "fill_bytes",
                    []
                  |),
                  [ M.read (| source |); bytes ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "u16", "from_ne_bytes", [] |),
                [ M.read (| bytes |) ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::random::Random"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("random", InstanceField.Method random) ].
  End Impl_core_random_Random_for_u16.
  
  Module Impl_core_random_Random_for_i16.
    Definition Self : Ty.t := Ty.path "i16".
    
    (*
                fn random(source: &mut (impl RandomSource + ?Sized)) -> Self {
                    let mut bytes = (0 as Self).to_ne_bytes();
                    source.fill_bytes(&mut bytes);
                    Self::from_ne_bytes(bytes)
                }
    *)
    Definition random (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ impl_RandomSource__plus___Sized ], [ source ] =>
        ltac:(M.monadic
          (let source := M.alloc (| source |) in
          M.read (|
            let~ bytes :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "i16", "to_ne_bytes", [] |),
                  [ M.read (| M.use (M.alloc (| Value.Integer IntegerKind.I16 0 |)) |) ]
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::random::RandomSource",
                    impl_RandomSource__plus___Sized,
                    [],
                    "fill_bytes",
                    []
                  |),
                  [ M.read (| source |); bytes ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "i16", "from_ne_bytes", [] |),
                [ M.read (| bytes |) ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::random::Random"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("random", InstanceField.Method random) ].
  End Impl_core_random_Random_for_i16.
  
  Module Impl_core_random_Random_for_u32.
    Definition Self : Ty.t := Ty.path "u32".
    
    (*
                fn random(source: &mut (impl RandomSource + ?Sized)) -> Self {
                    let mut bytes = (0 as Self).to_ne_bytes();
                    source.fill_bytes(&mut bytes);
                    Self::from_ne_bytes(bytes)
                }
    *)
    Definition random (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ impl_RandomSource__plus___Sized ], [ source ] =>
        ltac:(M.monadic
          (let source := M.alloc (| source |) in
          M.read (|
            let~ bytes :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "u32", "to_ne_bytes", [] |),
                  [ M.read (| M.use (M.alloc (| Value.Integer IntegerKind.U32 0 |)) |) ]
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::random::RandomSource",
                    impl_RandomSource__plus___Sized,
                    [],
                    "fill_bytes",
                    []
                  |),
                  [ M.read (| source |); bytes ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "u32", "from_ne_bytes", [] |),
                [ M.read (| bytes |) ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::random::Random"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("random", InstanceField.Method random) ].
  End Impl_core_random_Random_for_u32.
  
  Module Impl_core_random_Random_for_i32.
    Definition Self : Ty.t := Ty.path "i32".
    
    (*
                fn random(source: &mut (impl RandomSource + ?Sized)) -> Self {
                    let mut bytes = (0 as Self).to_ne_bytes();
                    source.fill_bytes(&mut bytes);
                    Self::from_ne_bytes(bytes)
                }
    *)
    Definition random (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ impl_RandomSource__plus___Sized ], [ source ] =>
        ltac:(M.monadic
          (let source := M.alloc (| source |) in
          M.read (|
            let~ bytes :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "i32", "to_ne_bytes", [] |),
                  [ M.read (| M.use (M.alloc (| Value.Integer IntegerKind.I32 0 |)) |) ]
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::random::RandomSource",
                    impl_RandomSource__plus___Sized,
                    [],
                    "fill_bytes",
                    []
                  |),
                  [ M.read (| source |); bytes ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "i32", "from_ne_bytes", [] |),
                [ M.read (| bytes |) ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::random::Random"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("random", InstanceField.Method random) ].
  End Impl_core_random_Random_for_i32.
  
  Module Impl_core_random_Random_for_u64.
    Definition Self : Ty.t := Ty.path "u64".
    
    (*
                fn random(source: &mut (impl RandomSource + ?Sized)) -> Self {
                    let mut bytes = (0 as Self).to_ne_bytes();
                    source.fill_bytes(&mut bytes);
                    Self::from_ne_bytes(bytes)
                }
    *)
    Definition random (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ impl_RandomSource__plus___Sized ], [ source ] =>
        ltac:(M.monadic
          (let source := M.alloc (| source |) in
          M.read (|
            let~ bytes :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "u64", "to_ne_bytes", [] |),
                  [ M.read (| M.use (M.alloc (| Value.Integer IntegerKind.U64 0 |)) |) ]
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::random::RandomSource",
                    impl_RandomSource__plus___Sized,
                    [],
                    "fill_bytes",
                    []
                  |),
                  [ M.read (| source |); bytes ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "u64", "from_ne_bytes", [] |),
                [ M.read (| bytes |) ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::random::Random"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("random", InstanceField.Method random) ].
  End Impl_core_random_Random_for_u64.
  
  Module Impl_core_random_Random_for_i64.
    Definition Self : Ty.t := Ty.path "i64".
    
    (*
                fn random(source: &mut (impl RandomSource + ?Sized)) -> Self {
                    let mut bytes = (0 as Self).to_ne_bytes();
                    source.fill_bytes(&mut bytes);
                    Self::from_ne_bytes(bytes)
                }
    *)
    Definition random (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ impl_RandomSource__plus___Sized ], [ source ] =>
        ltac:(M.monadic
          (let source := M.alloc (| source |) in
          M.read (|
            let~ bytes :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "i64", "to_ne_bytes", [] |),
                  [ M.read (| M.use (M.alloc (| Value.Integer IntegerKind.I64 0 |)) |) ]
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::random::RandomSource",
                    impl_RandomSource__plus___Sized,
                    [],
                    "fill_bytes",
                    []
                  |),
                  [ M.read (| source |); bytes ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "i64", "from_ne_bytes", [] |),
                [ M.read (| bytes |) ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::random::Random"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("random", InstanceField.Method random) ].
  End Impl_core_random_Random_for_i64.
  
  Module Impl_core_random_Random_for_u128.
    Definition Self : Ty.t := Ty.path "u128".
    
    (*
                fn random(source: &mut (impl RandomSource + ?Sized)) -> Self {
                    let mut bytes = (0 as Self).to_ne_bytes();
                    source.fill_bytes(&mut bytes);
                    Self::from_ne_bytes(bytes)
                }
    *)
    Definition random (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ impl_RandomSource__plus___Sized ], [ source ] =>
        ltac:(M.monadic
          (let source := M.alloc (| source |) in
          M.read (|
            let~ bytes :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "u128", "to_ne_bytes", [] |),
                  [ M.read (| M.use (M.alloc (| Value.Integer IntegerKind.U128 0 |)) |) ]
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::random::RandomSource",
                    impl_RandomSource__plus___Sized,
                    [],
                    "fill_bytes",
                    []
                  |),
                  [ M.read (| source |); bytes ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "u128", "from_ne_bytes", [] |),
                [ M.read (| bytes |) ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::random::Random"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("random", InstanceField.Method random) ].
  End Impl_core_random_Random_for_u128.
  
  Module Impl_core_random_Random_for_i128.
    Definition Self : Ty.t := Ty.path "i128".
    
    (*
                fn random(source: &mut (impl RandomSource + ?Sized)) -> Self {
                    let mut bytes = (0 as Self).to_ne_bytes();
                    source.fill_bytes(&mut bytes);
                    Self::from_ne_bytes(bytes)
                }
    *)
    Definition random (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ impl_RandomSource__plus___Sized ], [ source ] =>
        ltac:(M.monadic
          (let source := M.alloc (| source |) in
          M.read (|
            let~ bytes :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "i128", "to_ne_bytes", [] |),
                  [ M.read (| M.use (M.alloc (| Value.Integer IntegerKind.I128 0 |)) |) ]
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::random::RandomSource",
                    impl_RandomSource__plus___Sized,
                    [],
                    "fill_bytes",
                    []
                  |),
                  [ M.read (| source |); bytes ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "i128", "from_ne_bytes", [] |),
                [ M.read (| bytes |) ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::random::Random"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("random", InstanceField.Method random) ].
  End Impl_core_random_Random_for_i128.
  
  Module Impl_core_random_Random_for_usize.
    Definition Self : Ty.t := Ty.path "usize".
    
    (*
                fn random(source: &mut (impl RandomSource + ?Sized)) -> Self {
                    let mut bytes = (0 as Self).to_ne_bytes();
                    source.fill_bytes(&mut bytes);
                    Self::from_ne_bytes(bytes)
                }
    *)
    Definition random (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ impl_RandomSource__plus___Sized ], [ source ] =>
        ltac:(M.monadic
          (let source := M.alloc (| source |) in
          M.read (|
            let~ bytes :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "usize", "to_ne_bytes", [] |),
                  [ M.read (| M.use (M.alloc (| Value.Integer IntegerKind.Usize 0 |)) |) ]
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::random::RandomSource",
                    impl_RandomSource__plus___Sized,
                    [],
                    "fill_bytes",
                    []
                  |),
                  [ M.read (| source |); bytes ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "usize", "from_ne_bytes", [] |),
                [ M.read (| bytes |) ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::random::Random"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("random", InstanceField.Method random) ].
  End Impl_core_random_Random_for_usize.
  
  Module Impl_core_random_Random_for_isize.
    Definition Self : Ty.t := Ty.path "isize".
    
    (*
                fn random(source: &mut (impl RandomSource + ?Sized)) -> Self {
                    let mut bytes = (0 as Self).to_ne_bytes();
                    source.fill_bytes(&mut bytes);
                    Self::from_ne_bytes(bytes)
                }
    *)
    Definition random (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ impl_RandomSource__plus___Sized ], [ source ] =>
        ltac:(M.monadic
          (let source := M.alloc (| source |) in
          M.read (|
            let~ bytes :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "isize", "to_ne_bytes", [] |),
                  [ M.read (| M.use (M.alloc (| Value.Integer IntegerKind.Isize 0 |)) |) ]
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::random::RandomSource",
                    impl_RandomSource__plus___Sized,
                    [],
                    "fill_bytes",
                    []
                  |),
                  [ M.read (| source |); bytes ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "isize", "from_ne_bytes", [] |),
                [ M.read (| bytes |) ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::random::Random"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("random", InstanceField.Method random) ].
  End Impl_core_random_Random_for_isize.
End random.
