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

Module ffi.
  Module c_str.
    (* StructRecord
      {
        name := "CStr";
        const_params := [];
        ty_params := [];
        fields := [ ("inner", Ty.apply (Ty.path "slice") [] [ Ty.path "i8" ]) ];
      } *)
    
    Module Impl_core_marker_StructuralPartialEq_for_core_ffi_c_str_CStr.
      Definition Self : Ty.t := Ty.path "core::ffi::c_str::CStr".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_core_ffi_c_str_CStr.
    
    Module Impl_core_cmp_PartialEq_for_core_ffi_c_str_CStr.
      Definition Self : Ty.t := Ty.path "core::ffi::c_str::CStr".
      
      (* PartialEq *)
      Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.apply (Ty.path "slice") [] [ Ty.path "i8" ],
                [ Ty.apply (Ty.path "slice") [] [ Ty.path "i8" ] ],
                "eq",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::ffi::c_str::CStr",
                  "inner"
                |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| other |),
                  "core::ffi::c_str::CStr",
                  "inner"
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq) ].
    End Impl_core_cmp_PartialEq_for_core_ffi_c_str_CStr.
    
    Module Impl_core_cmp_Eq_for_core_ffi_c_str_CStr.
      Definition Self : Ty.t := Ty.path "core::ffi::c_str::CStr".
      
      (* Eq *)
      Definition assert_receiver_is_total_eq
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                Value.DeclaredButUndefined,
                [ fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::Eq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
    End Impl_core_cmp_Eq_for_core_ffi_c_str_CStr.
    
    Module Impl_core_hash_Hash_for_core_ffi_c_str_CStr.
      Definition Self : Ty.t := Ty.path "core::ffi::c_str::CStr".
      
      (* Hash *)
      Definition hash (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ __H ], [ self; state ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let state := M.alloc (| state |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::hash::Hash",
                Ty.apply (Ty.path "slice") [] [ Ty.path "i8" ],
                [],
                "hash",
                [ __H ]
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::ffi::c_str::CStr",
                  "inner"
                |);
                M.read (| state |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::hash::Hash"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("hash", InstanceField.Method hash) ].
    End Impl_core_hash_Hash_for_core_ffi_c_str_CStr.
    
    (* StructRecord
      {
        name := "FromBytesWithNulError";
        const_params := [];
        ty_params := [];
        fields := [ ("kind", Ty.path "core::ffi::c_str::FromBytesWithNulErrorKind") ];
      } *)
    
    Module Impl_core_clone_Clone_for_core_ffi_c_str_FromBytesWithNulError.
      Definition Self : Ty.t := Ty.path "core::ffi::c_str::FromBytesWithNulError".
      
      (* Clone *)
      Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            Value.StructRecord
              "core::ffi::c_str::FromBytesWithNulError"
              [
                ("kind",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::clone::Clone",
                      Ty.path "core::ffi::c_str::FromBytesWithNulErrorKind",
                      [],
                      "clone",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::ffi::c_str::FromBytesWithNulError",
                        "kind"
                      |)
                    ]
                  |))
              ]))
        | _, _, _ => 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_core_ffi_c_str_FromBytesWithNulError.
    
    Module Impl_core_marker_StructuralPartialEq_for_core_ffi_c_str_FromBytesWithNulError.
      Definition Self : Ty.t := Ty.path "core::ffi::c_str::FromBytesWithNulError".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_core_ffi_c_str_FromBytesWithNulError.
    
    Module Impl_core_cmp_PartialEq_for_core_ffi_c_str_FromBytesWithNulError.
      Definition Self : Ty.t := Ty.path "core::ffi::c_str::FromBytesWithNulError".
      
      (* PartialEq *)
      Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.path "core::ffi::c_str::FromBytesWithNulErrorKind",
                [ Ty.path "core::ffi::c_str::FromBytesWithNulErrorKind" ],
                "eq",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::ffi::c_str::FromBytesWithNulError",
                  "kind"
                |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| other |),
                  "core::ffi::c_str::FromBytesWithNulError",
                  "kind"
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq) ].
    End Impl_core_cmp_PartialEq_for_core_ffi_c_str_FromBytesWithNulError.
    
    Module Impl_core_cmp_Eq_for_core_ffi_c_str_FromBytesWithNulError.
      Definition Self : Ty.t := Ty.path "core::ffi::c_str::FromBytesWithNulError".
      
      (* Eq *)
      Definition assert_receiver_is_total_eq
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                Value.DeclaredButUndefined,
                [ fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::Eq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
    End Impl_core_cmp_Eq_for_core_ffi_c_str_FromBytesWithNulError.
    
    Module Impl_core_fmt_Debug_for_core_ffi_c_str_FromBytesWithNulError.
      Definition Self : Ty.t := Ty.path "core::ffi::c_str::FromBytesWithNulError".
      
      (* Debug *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "core::fmt::Formatter",
                "debug_struct_field1_finish",
                []
              |),
              [
                M.read (| f |);
                M.read (| Value.String "FromBytesWithNulError" |);
                M.read (| Value.String "kind" |);
                M.alloc (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::ffi::c_str::FromBytesWithNulError",
                    "kind"
                  |)
                |)
              ]
            |)))
        | _, _, _ => 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_core_ffi_c_str_FromBytesWithNulError.
    
    (*
    Enum FromBytesWithNulErrorKind
    {
      const_params := [];
      ty_params := [];
      variants :=
        [
          {
            name := "InteriorNul";
            item := StructTuple [ Ty.path "usize" ];
            discriminant := None;
          };
          {
            name := "NotNulTerminated";
            item := StructTuple [];
            discriminant := None;
          }
        ];
    }
    *)
    
    Module Impl_core_clone_Clone_for_core_ffi_c_str_FromBytesWithNulErrorKind.
      Definition Self : Ty.t := Ty.path "core::ffi::c_str::FromBytesWithNulErrorKind".
      
      (* 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 (|
                self,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let γ1_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::ffi::c_str::FromBytesWithNulErrorKind::InteriorNul",
                          0
                        |) in
                      let __self_0 := M.alloc (| γ1_0 |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::ffi::c_str::FromBytesWithNulErrorKind::InteriorNul"
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::clone::Clone",
                                Ty.path "usize",
                                [],
                                "clone",
                                []
                              |),
                              [ M.read (| __self_0 |) ]
                            |)
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "core::ffi::c_str::FromBytesWithNulErrorKind::NotNulTerminated"
                        |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::ffi::c_str::FromBytesWithNulErrorKind::NotNulTerminated"
                          []
                      |)))
                ]
              |)
            |)))
        | _, _, _ => 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_core_ffi_c_str_FromBytesWithNulErrorKind.
    
    Module Impl_core_marker_StructuralPartialEq_for_core_ffi_c_str_FromBytesWithNulErrorKind.
      Definition Self : Ty.t := Ty.path "core::ffi::c_str::FromBytesWithNulErrorKind".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_core_ffi_c_str_FromBytesWithNulErrorKind.
    
    Module Impl_core_cmp_PartialEq_for_core_ffi_c_str_FromBytesWithNulErrorKind.
      Definition Self : Ty.t := Ty.path "core::ffi::c_str::FromBytesWithNulErrorKind".
      
      (* PartialEq *)
      Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let~ __self_discr :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::discriminant_value",
                      [ Ty.path "core::ffi::c_str::FromBytesWithNulErrorKind" ]
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              let~ __arg1_discr :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::discriminant_value",
                      [ Ty.path "core::ffi::c_str::FromBytesWithNulErrorKind" ]
                    |),
                    [ M.read (| other |) ]
                  |)
                |) in
              M.alloc (|
                LogicalOp.and (|
                  BinOp.eq (| M.read (| __self_discr |), M.read (| __arg1_discr |) |),
                  ltac:(M.monadic
                    (M.read (|
                      M.match_operator (|
                        M.alloc (| Value.Tuple [ M.read (| self |); M.read (| other |) ] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                              let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                              let γ0_0 := M.read (| γ0_0 |) in
                              let γ2_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ0_0,
                                  "core::ffi::c_str::FromBytesWithNulErrorKind::InteriorNul",
                                  0
                                |) in
                              let __self_0 := M.alloc (| γ2_0 |) in
                              let γ0_1 := M.read (| γ0_1 |) in
                              let γ2_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ0_1,
                                  "core::ffi::c_str::FromBytesWithNulErrorKind::InteriorNul",
                                  0
                                |) in
                              let __arg1_0 := M.alloc (| γ2_0 |) in
                              M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::cmp::PartialEq",
                                    Ty.apply (Ty.path "&") [] [ Ty.path "usize" ],
                                    [ Ty.apply (Ty.path "&") [] [ Ty.path "usize" ] ],
                                    "eq",
                                    []
                                  |),
                                  [ __self_0; __arg1_0 ]
                                |)
                              |)));
                          fun γ => ltac:(M.monadic (M.alloc (| Value.Bool true |)))
                        ]
                      |)
                    |)))
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq) ].
    End Impl_core_cmp_PartialEq_for_core_ffi_c_str_FromBytesWithNulErrorKind.
    
    Module Impl_core_cmp_Eq_for_core_ffi_c_str_FromBytesWithNulErrorKind.
      Definition Self : Ty.t := Ty.path "core::ffi::c_str::FromBytesWithNulErrorKind".
      
      (* Eq *)
      Definition assert_receiver_is_total_eq
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                Value.DeclaredButUndefined,
                [ fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::Eq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
    End Impl_core_cmp_Eq_for_core_ffi_c_str_FromBytesWithNulErrorKind.
    
    Module Impl_core_fmt_Debug_for_core_ffi_c_str_FromBytesWithNulErrorKind.
      Definition Self : Ty.t := Ty.path "core::ffi::c_str::FromBytesWithNulErrorKind".
      
      (* Debug *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.read (|
              M.match_operator (|
                self,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let γ1_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::ffi::c_str::FromBytesWithNulErrorKind::InteriorNul",
                          0
                        |) in
                      let __self_0 := M.alloc (| γ1_0 |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::fmt::Formatter",
                            "debug_tuple_field1_finish",
                            []
                          |),
                          [ M.read (| f |); M.read (| Value.String "InteriorNul" |); __self_0 ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "core::ffi::c_str::FromBytesWithNulErrorKind::NotNulTerminated"
                        |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::fmt::Formatter",
                            "write_str",
                            []
                          |),
                          [ M.read (| f |); M.read (| Value.String "NotNulTerminated" |) ]
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => 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_core_ffi_c_str_FromBytesWithNulErrorKind.
    
    Module Impl_core_ffi_c_str_FromBytesWithNulError.
      Definition Self : Ty.t := Ty.path "core::ffi::c_str::FromBytesWithNulError".
      
      (*
          const fn interior_nul(pos: usize) -> FromBytesWithNulError {
              FromBytesWithNulError { kind: FromBytesWithNulErrorKind::InteriorNul(pos) }
          }
      *)
      Definition interior_nul (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ pos ] =>
          ltac:(M.monadic
            (let pos := M.alloc (| pos |) in
            Value.StructRecord
              "core::ffi::c_str::FromBytesWithNulError"
              [
                ("kind",
                  Value.StructTuple
                    "core::ffi::c_str::FromBytesWithNulErrorKind::InteriorNul"
                    [ M.read (| pos |) ])
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_interior_nul :
        M.IsAssociatedFunction Self "interior_nul" interior_nul.
      
      (*
          const fn not_nul_terminated() -> FromBytesWithNulError {
              FromBytesWithNulError { kind: FromBytesWithNulErrorKind::NotNulTerminated }
          }
      *)
      Definition not_nul_terminated (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [] =>
          ltac:(M.monadic
            (Value.StructRecord
              "core::ffi::c_str::FromBytesWithNulError"
              [
                ("kind",
                  Value.StructTuple
                    "core::ffi::c_str::FromBytesWithNulErrorKind::NotNulTerminated"
                    [])
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_not_nul_terminated :
        M.IsAssociatedFunction Self "not_nul_terminated" not_nul_terminated.
    End Impl_core_ffi_c_str_FromBytesWithNulError.
    
    Module Impl_core_error_Error_for_core_ffi_c_str_FromBytesWithNulError.
      Definition Self : Ty.t := Ty.path "core::ffi::c_str::FromBytesWithNulError".
      
      (*
          fn description(&self) -> &str {
              match self.kind {
                  FromBytesWithNulErrorKind::InteriorNul(..) => {
                      "data provided contains an interior nul byte"
                  }
                  FromBytesWithNulErrorKind::NotNulTerminated => "data provided is not nul terminated",
              }
          }
      *)
      Definition description (ε : 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 (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::ffi::c_str::FromBytesWithNulError",
                  "kind"
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "core::ffi::c_str::FromBytesWithNulErrorKind::InteriorNul"
                        |) in
                      M.alloc (|
                        M.read (| Value.String "data provided contains an interior nul byte" |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "core::ffi::c_str::FromBytesWithNulErrorKind::NotNulTerminated"
                        |) in
                      M.alloc (|
                        M.read (| Value.String "data provided is not nul terminated" |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::error::Error"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("description", InstanceField.Method description) ].
    End Impl_core_error_Error_for_core_ffi_c_str_FromBytesWithNulError.
    
    (* StructTuple
      {
        name := "FromBytesUntilNulError";
        const_params := [];
        ty_params := [];
        fields := [ Ty.tuple [] ];
      } *)
    
    Module Impl_core_clone_Clone_for_core_ffi_c_str_FromBytesUntilNulError.
      Definition Self : Ty.t := Ty.path "core::ffi::c_str::FromBytesUntilNulError".
      
      (* Clone *)
      Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            Value.StructTuple
              "core::ffi::c_str::FromBytesUntilNulError"
              [
                M.call_closure (|
                  M.get_trait_method (| "core::clone::Clone", Ty.tuple [], [], "clone", [] |),
                  [
                    M.SubPointer.get_struct_tuple_field (|
                      M.read (| self |),
                      "core::ffi::c_str::FromBytesUntilNulError",
                      0
                    |)
                  ]
                |)
              ]))
        | _, _, _ => 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_core_ffi_c_str_FromBytesUntilNulError.
    
    Module Impl_core_marker_StructuralPartialEq_for_core_ffi_c_str_FromBytesUntilNulError.
      Definition Self : Ty.t := Ty.path "core::ffi::c_str::FromBytesUntilNulError".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_core_ffi_c_str_FromBytesUntilNulError.
    
    Module Impl_core_cmp_PartialEq_for_core_ffi_c_str_FromBytesUntilNulError.
      Definition Self : Ty.t := Ty.path "core::ffi::c_str::FromBytesUntilNulError".
      
      (* PartialEq *)
      Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.tuple [],
                [ Ty.tuple [] ],
                "eq",
                []
              |),
              [
                M.SubPointer.get_struct_tuple_field (|
                  M.read (| self |),
                  "core::ffi::c_str::FromBytesUntilNulError",
                  0
                |);
                M.SubPointer.get_struct_tuple_field (|
                  M.read (| other |),
                  "core::ffi::c_str::FromBytesUntilNulError",
                  0
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq) ].
    End Impl_core_cmp_PartialEq_for_core_ffi_c_str_FromBytesUntilNulError.
    
    Module Impl_core_cmp_Eq_for_core_ffi_c_str_FromBytesUntilNulError.
      Definition Self : Ty.t := Ty.path "core::ffi::c_str::FromBytesUntilNulError".
      
      (* Eq *)
      Definition assert_receiver_is_total_eq
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                Value.DeclaredButUndefined,
                [ fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::Eq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
    End Impl_core_cmp_Eq_for_core_ffi_c_str_FromBytesUntilNulError.
    
    Module Impl_core_fmt_Debug_for_core_ffi_c_str_FromBytesUntilNulError.
      Definition Self : Ty.t := Ty.path "core::ffi::c_str::FromBytesUntilNulError".
      
      (* 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 "FromBytesUntilNulError" |);
                M.alloc (|
                  M.SubPointer.get_struct_tuple_field (|
                    M.read (| self |),
                    "core::ffi::c_str::FromBytesUntilNulError",
                    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_core_ffi_c_str_FromBytesUntilNulError.
    
    Module Impl_core_fmt_Display_for_core_ffi_c_str_FromBytesUntilNulError.
      Definition Self : Ty.t := Ty.path "core::ffi::c_str::FromBytesUntilNulError".
      
      (*
          fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
              write!(f, "data provided does not contain a nul")
          }
      *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.call_closure (|
              M.get_associated_function (| Ty.path "core::fmt::Formatter", "write_fmt", [] |),
              [
                M.read (| f |);
                M.call_closure (|
                  M.get_associated_function (| Ty.path "core::fmt::Arguments", "new_const", [] |),
                  [
                    M.alloc (|
                      Value.Array
                        [ M.read (| Value.String "data provided does not contain a nul" |) ]
                    |)
                  ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::fmt::Display"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
    End Impl_core_fmt_Display_for_core_ffi_c_str_FromBytesUntilNulError.
    
    Module Impl_core_fmt_Debug_for_core_ffi_c_str_CStr.
      Definition Self : Ty.t := Ty.path "core::ffi::c_str::CStr".
      
      (*
          fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
              write!(f, "\"{}\"", self.to_bytes().escape_ascii())
          }
      *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.call_closure (|
              M.get_associated_function (| Ty.path "core::fmt::Formatter", "write_fmt", [] |),
              [
                M.read (| f |);
                M.call_closure (|
                  M.get_associated_function (| Ty.path "core::fmt::Arguments", "new_v1", [] |),
                  [
                    M.alloc (|
                      Value.Array [ M.read (| Value.String """" |); M.read (| Value.String """" |) ]
                    |);
                    M.alloc (|
                      Value.Array
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::rt::Argument",
                              "new_display",
                              [ Ty.path "core::slice::ascii::EscapeAscii" ]
                            |),
                            [
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                    "escape_ascii",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "core::ffi::c_str::CStr",
                                        "to_bytes",
                                        []
                                      |),
                                      [ M.read (| self |) ]
                                    |)
                                  ]
                                |)
                              |)
                            ]
                          |)
                        ]
                    |)
                  ]
                |)
              ]
            |)))
        | _, _, _ => 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_core_ffi_c_str_CStr.
    
    Module Impl_core_default_Default_for_ref__core_ffi_c_str_CStr.
      Definition Self : Ty.t := Ty.apply (Ty.path "&") [] [ Ty.path "core::ffi::c_str::CStr" ].
      
      (*
          fn default() -> Self {
              const SLICE: &[c_char] = &[0];
              // SAFETY: `SLICE` is indeed pointing to a valid nul-terminated string.
              unsafe { CStr::from_ptr(SLICE.as_ptr()) }
          }
      *)
      Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [] =>
          ltac:(M.monadic
            (M.call_closure (|
              M.get_associated_function (| Ty.path "core::ffi::c_str::CStr", "from_ptr", [] |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "slice") [] [ Ty.path "i8" ],
                    "as_ptr",
                    []
                  |),
                  [ M.read (| M.get_constant (| "core::ffi::c_str::default::SLICE" |) |) ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::default::Default"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("default", InstanceField.Method default) ].
    End Impl_core_default_Default_for_ref__core_ffi_c_str_CStr.
    
    Module Impl_core_fmt_Display_for_core_ffi_c_str_FromBytesWithNulError.
      Definition Self : Ty.t := Ty.path "core::ffi::c_str::FromBytesWithNulError".
      
      (*
          fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
              f.write_str(self.description())?;
              if let FromBytesWithNulErrorKind::InteriorNul(pos) = self.kind {
                  write!(f, " at byte pos {pos}")?;
              }
              Ok(())
          }
      *)
      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.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::try_trait::Try",
                            Ty.apply
                              (Ty.path "core::result::Result")
                              []
                              [ Ty.tuple []; Ty.path "core::fmt::Error" ],
                            [],
                            "branch",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::Formatter",
                                "write_str",
                                []
                              |),
                              [
                                M.read (| f |);
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::error::Error",
                                    Ty.path "core::ffi::c_str::FromBytesWithNulError",
                                    [],
                                    "description",
                                    []
                                  |),
                                  [ M.read (| self |) ]
                                |)
                              ]
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::control_flow::ControlFlow::Break",
                                0
                              |) in
                            let residual := M.copy (| γ0_0 |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  M.return_ (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::ops::try_trait::FromResidual",
                                        Ty.apply
                                          (Ty.path "core::result::Result")
                                          []
                                          [ Ty.tuple []; Ty.path "core::fmt::Error" ],
                                        [
                                          Ty.apply
                                            (Ty.path "core::result::Result")
                                            []
                                            [
                                              Ty.path "core::convert::Infallible";
                                              Ty.path "core::fmt::Error"
                                            ]
                                        ],
                                        "from_residual",
                                        []
                                      |),
                                      [ M.read (| residual |) ]
                                    |)
                                  |)
                                |)
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::control_flow::ControlFlow::Continue",
                                0
                              |) in
                            let val := M.copy (| γ0_0 |) in
                            val))
                      ]
                    |) in
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::ffi::c_str::FromBytesWithNulError",
                                "kind"
                              |) in
                            let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ffi::c_str::FromBytesWithNulErrorKind::InteriorNul",
                                0
                              |) in
                            let pos := M.copy (| γ0_0 |) in
                            let~ _ :=
                              M.match_operator (|
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::ops::try_trait::Try",
                                      Ty.apply
                                        (Ty.path "core::result::Result")
                                        []
                                        [ Ty.tuple []; Ty.path "core::fmt::Error" ],
                                      [],
                                      "branch",
                                      []
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "core::fmt::Formatter",
                                          "write_fmt",
                                          []
                                        |),
                                        [
                                          M.read (| f |);
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "core::fmt::Arguments",
                                              "new_v1",
                                              []
                                            |),
                                            [
                                              M.alloc (|
                                                Value.Array
                                                  [ M.read (| Value.String " at byte pos " |) ]
                                              |);
                                              M.alloc (|
                                                Value.Array
                                                  [
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.path "core::fmt::rt::Argument",
                                                        "new_display",
                                                        [ Ty.path "usize" ]
                                                      |),
                                                      [ pos ]
                                                    |)
                                                  ]
                                              |)
                                            ]
                                          |)
                                        ]
                                      |)
                                    ]
                                  |)
                                |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ0_0 :=
                                        M.SubPointer.get_struct_tuple_field (|
                                          γ,
                                          "core::ops::control_flow::ControlFlow::Break",
                                          0
                                        |) in
                                      let residual := M.copy (| γ0_0 |) in
                                      M.alloc (|
                                        M.never_to_any (|
                                          M.read (|
                                            M.return_ (|
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::ops::try_trait::FromResidual",
                                                  Ty.apply
                                                    (Ty.path "core::result::Result")
                                                    []
                                                    [ Ty.tuple []; Ty.path "core::fmt::Error" ],
                                                  [
                                                    Ty.apply
                                                      (Ty.path "core::result::Result")
                                                      []
                                                      [
                                                        Ty.path "core::convert::Infallible";
                                                        Ty.path "core::fmt::Error"
                                                      ]
                                                  ],
                                                  "from_residual",
                                                  []
                                                |),
                                                [ M.read (| residual |) ]
                                              |)
                                            |)
                                          |)
                                        |)
                                      |)));
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ0_0 :=
                                        M.SubPointer.get_struct_tuple_field (|
                                          γ,
                                          "core::ops::control_flow::ControlFlow::Continue",
                                          0
                                        |) in
                                      let val := M.copy (| γ0_0 |) in
                                      val))
                                ]
                              |) in
                            M.alloc (| Value.Tuple [] |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::fmt::Display"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
    End Impl_core_fmt_Display_for_core_ffi_c_str_FromBytesWithNulError.
    
    Module Impl_core_ffi_c_str_CStr.
      Definition Self : Ty.t := Ty.path "core::ffi::c_str::CStr".
      
      (*
          pub const unsafe fn from_ptr<'a>(ptr: *const c_char) -> &'a CStr {
              // SAFETY: The caller has provided a pointer that points to a valid C
              // string with a NUL terminator less than `isize::MAX` from `ptr`.
              let len = unsafe { strlen(ptr) };
      
              // SAFETY: The caller has provided a valid pointer with length less than
              // `isize::MAX`, so `from_raw_parts` is safe. The content remains valid
              // and doesn't change for the lifetime of the returned `CStr`. This
              // means the call to `from_bytes_with_nul_unchecked` is correct.
              //
              // The cast from c_char to u8 is ok because a c_char is always one byte.
              unsafe { Self::from_bytes_with_nul_unchecked(slice::from_raw_parts(ptr.cast(), len + 1)) }
          }
      *)
      Definition from_ptr (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ ptr ] =>
          ltac:(M.monadic
            (let ptr := M.alloc (| ptr |) in
            M.read (|
              let~ len :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "core::ffi::c_str::strlen", [] |),
                    [ M.read (| ptr |) ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "core::ffi::c_str::CStr",
                    "from_bytes_with_nul_unchecked",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_function (| "core::slice::raw::from_raw_parts", [ Ty.path "u8" ] |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "*const") [] [ Ty.path "i8" ],
                            "cast",
                            [ Ty.path "u8" ]
                          |),
                          [ M.read (| ptr |) ]
                        |);
                        BinOp.Wrap.add (| M.read (| len |), Value.Integer IntegerKind.Usize 1 |)
                      ]
                    |)
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_from_ptr : M.IsAssociatedFunction Self "from_ptr" from_ptr.
      
      (*
          pub const fn from_bytes_until_nul(bytes: &[u8]) -> Result<&CStr, FromBytesUntilNulError> {
              let nul_pos = memchr::memchr(0, bytes);
              match nul_pos {
                  Some(nul_pos) => {
                      // FIXME(const-hack) replace with range index
                      // SAFETY: nul_pos + 1 <= bytes.len()
                      let subslice = unsafe { crate::slice::from_raw_parts(bytes.as_ptr(), nul_pos + 1) };
                      // SAFETY: We know there is a nul byte at nul_pos, so this slice
                      // (ending at the nul byte) is a well-formed C string.
                      Ok(unsafe { CStr::from_bytes_with_nul_unchecked(subslice) })
                  }
                  None => Err(FromBytesUntilNulError(())),
              }
          }
      *)
      Definition from_bytes_until_nul (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ bytes ] =>
          ltac:(M.monadic
            (let bytes := M.alloc (| bytes |) in
            M.read (|
              let~ nul_pos :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "core::slice::memchr::memchr", [] |),
                    [ Value.Integer IntegerKind.U8 0; M.read (| bytes |) ]
                  |)
                |) in
              M.match_operator (|
                nul_pos,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::option::Option::Some",
                          0
                        |) in
                      let nul_pos := M.copy (| γ0_0 |) in
                      let~ subslice :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_function (|
                              "core::slice::raw::from_raw_parts",
                              [ Ty.path "u8" ]
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                  "as_ptr",
                                  []
                                |),
                                [ M.read (| bytes |) ]
                              |);
                              BinOp.Wrap.add (|
                                M.read (| nul_pos |),
                                Value.Integer IntegerKind.Usize 1
                              |)
                            ]
                          |)
                        |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::result::Result::Ok"
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::ffi::c_str::CStr",
                                "from_bytes_with_nul_unchecked",
                                []
                              |),
                              [ M.read (| subslice |) ]
                            |)
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::result::Result::Err"
                          [
                            Value.StructTuple
                              "core::ffi::c_str::FromBytesUntilNulError"
                              [ Value.Tuple [] ]
                          ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_from_bytes_until_nul :
        M.IsAssociatedFunction Self "from_bytes_until_nul" from_bytes_until_nul.
      
      (*
          pub const fn from_bytes_with_nul(bytes: &[u8]) -> Result<&Self, FromBytesWithNulError> {
              let nul_pos = memchr::memchr(0, bytes);
              match nul_pos {
                  Some(nul_pos) if nul_pos + 1 == bytes.len() => {
                      // SAFETY: We know there is only one nul byte, at the end
                      // of the byte slice.
                      Ok(unsafe { Self::from_bytes_with_nul_unchecked(bytes) })
                  }
                  Some(nul_pos) => Err(FromBytesWithNulError::interior_nul(nul_pos)),
                  None => Err(FromBytesWithNulError::not_nul_terminated()),
              }
          }
      *)
      Definition from_bytes_with_nul (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ bytes ] =>
          ltac:(M.monadic
            (let bytes := M.alloc (| bytes |) in
            M.read (|
              let~ nul_pos :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "core::slice::memchr::memchr", [] |),
                    [ Value.Integer IntegerKind.U8 0; M.read (| bytes |) ]
                  |)
                |) in
              M.match_operator (|
                nul_pos,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::option::Option::Some",
                          0
                        |) in
                      let nul_pos := M.copy (| γ0_0 |) in
                      let γ :=
                        M.alloc (|
                          BinOp.eq (|
                            BinOp.Wrap.add (|
                              M.read (| nul_pos |),
                              Value.Integer IntegerKind.Usize 1
                            |),
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                "len",
                                []
                              |),
                              [ M.read (| bytes |) ]
                            |)
                          |)
                        |) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::result::Result::Ok"
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::ffi::c_str::CStr",
                                "from_bytes_with_nul_unchecked",
                                []
                              |),
                              [ M.read (| bytes |) ]
                            |)
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::option::Option::Some",
                          0
                        |) in
                      let nul_pos := M.copy (| γ0_0 |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::result::Result::Err"
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::ffi::c_str::FromBytesWithNulError",
                                "interior_nul",
                                []
                              |),
                              [ M.read (| nul_pos |) ]
                            |)
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::result::Result::Err"
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::ffi::c_str::FromBytesWithNulError",
                                "not_nul_terminated",
                                []
                              |),
                              []
                            |)
                          ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_from_bytes_with_nul :
        M.IsAssociatedFunction Self "from_bytes_with_nul" from_bytes_with_nul.
      
      (*
          pub const unsafe fn from_bytes_with_nul_unchecked(bytes: &[u8]) -> &CStr {
              #[inline]
              fn rt_impl(bytes: &[u8]) -> &CStr {
                  // Chance at catching some UB at runtime with debug builds.
                  debug_assert!(!bytes.is_empty() && bytes[bytes.len() - 1] == 0);
      
                  // SAFETY: Casting to CStr is safe because its internal representation
                  // is a [u8] too (safe only inside std).
                  // Dereferencing the obtained pointer is safe because it comes from a
                  // reference. Making a reference is then safe because its lifetime
                  // is bound by the lifetime of the given `bytes`.
                  unsafe { &*(bytes as *const [u8] as *const CStr) }
              }
      
              const fn const_impl(bytes: &[u8]) -> &CStr {
                  // Saturating so that an empty slice panics in the assert with a good
                  // message, not here due to underflow.
                  let mut i = bytes.len().saturating_sub(1);
                  assert!(!bytes.is_empty() && bytes[i] == 0, "input was not nul-terminated");
      
                  // Ending nul byte exists, skip to the rest.
                  while i != 0 {
                      i -= 1;
                      let byte = bytes[i];
                      assert!(byte != 0, "input contained interior nul");
                  }
      
                  // SAFETY: See `rt_impl` cast.
                  unsafe { &*(bytes as *const [u8] as *const CStr) }
              }
      
              intrinsics::const_eval_select((bytes,), const_impl, rt_impl)
          }
      *)
      Definition from_bytes_with_nul_unchecked
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        match ε, τ, α with
        | [], [], [ bytes ] =>
          ltac:(M.monadic
            (let bytes := M.alloc (| bytes |) in
            M.call_closure (|
              M.get_function (|
                "core::intrinsics::const_eval_select",
                [
                  Ty.tuple
                    [ Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ]
                    ];
                  Ty.function
                    [ Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ] ]
                    (Ty.apply (Ty.path "&") [] [ Ty.path "core::ffi::c_str::CStr" ]);
                  Ty.function
                    [ Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ] ]
                    (Ty.apply (Ty.path "&") [] [ Ty.path "core::ffi::c_str::CStr" ]);
                  Ty.apply (Ty.path "&") [] [ Ty.path "core::ffi::c_str::CStr" ]
                ]
              |),
              [
                Value.Tuple [ M.read (| bytes |) ];
                M.get_associated_function (|
                  Self,
                  "const_impl.from_bytes_with_nul_unchecked",
                  []
                |);
                M.get_associated_function (| Self, "rt_impl.from_bytes_with_nul_unchecked", [] |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_from_bytes_with_nul_unchecked :
        M.IsAssociatedFunction Self "from_bytes_with_nul_unchecked" from_bytes_with_nul_unchecked.
      
      (*
          pub const fn as_ptr(&self) -> *const c_char {
              self.inner.as_ptr()
          }
      *)
      Definition as_ptr (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "slice") [] [ Ty.path "i8" ],
                "as_ptr",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::ffi::c_str::CStr",
                  "inner"
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_as_ptr : M.IsAssociatedFunction Self "as_ptr" as_ptr.
      
      (*
          const fn as_non_null_ptr(&self) -> NonNull<c_char> {
              // FIXME(effects) replace with `NonNull::from`
              // SAFETY: a reference is never null
              unsafe { NonNull::new_unchecked(&self.inner as *const [c_char] as *mut [c_char]) }
                  .as_non_null_ptr()
          }
      *)
      Definition as_non_null_ptr (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "core::ptr::non_null::NonNull")
                  []
                  [ Ty.apply (Ty.path "slice") [] [ Ty.path "i8" ] ],
                "as_non_null_ptr",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "core::ptr::non_null::NonNull")
                      []
                      [ Ty.apply (Ty.path "slice") [] [ Ty.path "i8" ] ],
                    "new_unchecked",
                    []
                  |),
                  [
                    M.rust_cast
                      (M.read (|
                        M.use
                          (M.alloc (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "core::ffi::c_str::CStr",
                              "inner"
                            |)
                          |))
                      |))
                  ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_as_non_null_ptr :
        M.IsAssociatedFunction Self "as_non_null_ptr" as_non_null_ptr.
      
      (*
          pub const fn count_bytes(&self) -> usize {
              self.inner.len() - 1
          }
      *)
      Definition count_bytes (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            BinOp.Wrap.sub (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "slice") [] [ Ty.path "i8" ],
                  "len",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::ffi::c_str::CStr",
                    "inner"
                  |)
                ]
              |),
              Value.Integer IntegerKind.Usize 1
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_count_bytes : M.IsAssociatedFunction Self "count_bytes" count_bytes.
      
      (*
          pub const fn is_empty(&self) -> bool {
              // SAFETY: We know there is at least one byte; for empty strings it
              // is the NUL terminator.
              // FIXME(const-hack): use get_unchecked
              unsafe { *self.inner.as_ptr() == 0 }
          }
      *)
      Definition is_empty (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            BinOp.eq (|
              M.read (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "slice") [] [ Ty.path "i8" ],
                    "as_ptr",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::ffi::c_str::CStr",
                      "inner"
                    |)
                  ]
                |)
              |),
              Value.Integer IntegerKind.I8 0
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_is_empty : M.IsAssociatedFunction Self "is_empty" is_empty.
      
      (*
          pub const fn to_bytes(&self) -> &[u8] {
              let bytes = self.to_bytes_with_nul();
              // FIXME(const-hack) replace with range index
              // SAFETY: to_bytes_with_nul returns slice with length at least 1
              unsafe { slice::from_raw_parts(bytes.as_ptr(), bytes.len() - 1) }
          }
      *)
      Definition to_bytes (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              let~ bytes :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "core::ffi::c_str::CStr",
                      "to_bytes_with_nul",
                      []
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_function (| "core::slice::raw::from_raw_parts", [ Ty.path "u8" ] |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                        "as_ptr",
                        []
                      |),
                      [ M.read (| bytes |) ]
                    |);
                    BinOp.Wrap.sub (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                          "len",
                          []
                        |),
                        [ M.read (| bytes |) ]
                      |),
                      Value.Integer IntegerKind.Usize 1
                    |)
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_to_bytes : M.IsAssociatedFunction Self "to_bytes" to_bytes.
      
      (*
          pub const fn to_bytes_with_nul(&self) -> &[u8] {
              // SAFETY: Transmuting a slice of `c_char`s to a slice of `u8`s
              // is safe on all supported targets.
              unsafe { &*((&raw const self.inner) as *const [u8]) }
          }
      *)
      Definition to_bytes_with_nul (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.rust_cast
              (M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::ffi::c_str::CStr",
                "inner"
              |))))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_to_bytes_with_nul :
        M.IsAssociatedFunction Self "to_bytes_with_nul" to_bytes_with_nul.
      
      (*
          pub fn bytes(&self) -> Bytes<'_> {
              Bytes::new(self)
          }
      *)
      Definition bytes (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_associated_function (| Ty.path "core::ffi::c_str::Bytes", "new", [] |),
              [ M.read (| self |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_bytes : M.IsAssociatedFunction Self "bytes" bytes.
      
      (*
          pub const fn to_str(&self) -> Result<&str, str::Utf8Error> {
              // N.B., when `CStr` is changed to perform the length check in `.to_bytes()`
              // instead of in `from_ptr()`, it may be worth considering if this should
              // be rewritten to do the UTF-8 check inline with the length calculation
              // instead of doing it afterwards.
              str::from_utf8(self.to_bytes())
          }
      *)
      Definition to_str (ε : 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_function (| "core::str::converts::from_utf8", [] |),
              [
                M.call_closure (|
                  M.get_associated_function (| Ty.path "core::ffi::c_str::CStr", "to_bytes", [] |),
                  [ M.read (| self |) ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_to_str : M.IsAssociatedFunction Self "to_str" to_str.
    End Impl_core_ffi_c_str_CStr.
    
    Module Impl_core_cmp_PartialOrd_for_core_ffi_c_str_CStr.
      Definition Self : Ty.t := Ty.path "core::ffi::c_str::CStr".
      
      (*
          fn partial_cmp(&self, other: &CStr) -> Option<Ordering> {
              self.to_bytes().partial_cmp(&other.to_bytes())
          }
      *)
      Definition partial_cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialOrd",
                Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ],
                "partial_cmp",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (| Ty.path "core::ffi::c_str::CStr", "to_bytes", [] |),
                  [ M.read (| self |) ]
                |);
                M.call_closure (|
                  M.get_associated_function (| Ty.path "core::ffi::c_str::CStr", "to_bytes", [] |),
                  [ M.read (| other |) ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("partial_cmp", InstanceField.Method partial_cmp) ].
    End Impl_core_cmp_PartialOrd_for_core_ffi_c_str_CStr.
    
    Module Impl_core_cmp_Ord_for_core_ffi_c_str_CStr.
      Definition Self : Ty.t := Ty.path "core::ffi::c_str::CStr".
      
      (*
          fn cmp(&self, other: &CStr) -> Ordering {
              self.to_bytes().cmp(&other.to_bytes())
          }
      *)
      Definition cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::cmp::Ord",
                Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                [],
                "cmp",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (| Ty.path "core::ffi::c_str::CStr", "to_bytes", [] |),
                  [ M.read (| self |) ]
                |);
                M.call_closure (|
                  M.get_associated_function (| Ty.path "core::ffi::c_str::CStr", "to_bytes", [] |),
                  [ M.read (| other |) ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::Ord"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("cmp", InstanceField.Method cmp) ].
    End Impl_core_cmp_Ord_for_core_ffi_c_str_CStr.
    
    Module Impl_core_ops_index_Index_core_ops_range_RangeFrom_usize_for_core_ffi_c_str_CStr.
      Definition Self : Ty.t := Ty.path "core::ffi::c_str::CStr".
      
      (*     type Output = CStr; *)
      Definition _Output : Ty.t := Ty.path "core::ffi::c_str::CStr".
      
      (*
          fn index(&self, index: ops::RangeFrom<usize>) -> &CStr {
              let bytes = self.to_bytes_with_nul();
              // we need to manually check the starting index to account for the null
              // byte, since otherwise we could get an empty string that doesn't end
              // in a null.
              if index.start < bytes.len() {
                  // SAFETY: Non-empty tail of a valid `CStr` is still a valid `CStr`.
                  unsafe { CStr::from_bytes_with_nul_unchecked(&bytes[index.start..]) }
              } else {
                  panic!(
                      "index out of bounds: the len is {} but the index is {}",
                      bytes.len(),
                      index.start
                  );
              }
          }
      *)
      Definition index (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; index ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let index := M.alloc (| index |) in
            M.read (|
              let~ bytes :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "core::ffi::c_str::CStr",
                      "to_bytes_with_nul",
                      []
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            BinOp.lt (|
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  index,
                                  "core::ops::range::RangeFrom",
                                  "start"
                                |)
                              |),
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                  "len",
                                  []
                                |),
                                [ M.read (| bytes |) ]
                              |)
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::ffi::c_str::CStr",
                            "from_bytes_with_nul_unchecked",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::index::Index",
                                Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                [
                                  Ty.apply
                                    (Ty.path "core::ops::range::RangeFrom")
                                    []
                                    [ Ty.path "usize" ]
                                ],
                                "index",
                                []
                              |),
                              [
                                M.read (| bytes |);
                                Value.StructRecord
                                  "core::ops::range::RangeFrom"
                                  [
                                    ("start",
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          index,
                                          "core::ops::range::RangeFrom",
                                          "start"
                                        |)
                                      |))
                                  ]
                              ]
                            |)
                          ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        M.never_to_any (|
                          M.call_closure (|
                            M.get_function (| "core::panicking::panic_fmt", [] |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::Arguments",
                                  "new_v1",
                                  []
                                |),
                                [
                                  M.alloc (|
                                    Value.Array
                                      [
                                        M.read (|
                                          Value.String "index out of bounds: the len is "
                                        |);
                                        M.read (| Value.String " but the index is " |)
                                      ]
                                  |);
                                  M.alloc (|
                                    Value.Array
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "core::fmt::rt::Argument",
                                            "new_display",
                                            [ Ty.path "usize" ]
                                          |),
                                          [
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                                  "len",
                                                  []
                                                |),
                                                [ M.read (| bytes |) ]
                                              |)
                                            |)
                                          ]
                                        |);
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "core::fmt::rt::Argument",
                                            "new_display",
                                            [ Ty.path "usize" ]
                                          |),
                                          [
                                            M.SubPointer.get_struct_record_field (|
                                              index,
                                              "core::ops::range::RangeFrom",
                                              "start"
                                            |)
                                          ]
                                        |)
                                      ]
                                  |)
                                ]
                              |)
                            ]
                          |)
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::index::Index"
          Self
          (* Trait polymorphic types *)
          [ (* Idx *) Ty.apply (Ty.path "core::ops::range::RangeFrom") [] [ Ty.path "usize" ] ]
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("index", InstanceField.Method index) ].
    End Impl_core_ops_index_Index_core_ops_range_RangeFrom_usize_for_core_ffi_c_str_CStr.
    
    Module Impl_core_convert_AsRef_core_ffi_c_str_CStr_for_core_ffi_c_str_CStr.
      Definition Self : Ty.t := Ty.path "core::ffi::c_str::CStr".
      
      (*
          fn as_ref(&self) -> &CStr {
              self
          }
      *)
      Definition as_ref (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (| self |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::convert::AsRef"
          Self
          (* Trait polymorphic types *) [ (* T *) Ty.path "core::ffi::c_str::CStr" ]
          (* Instance *) [ ("as_ref", InstanceField.Method as_ref) ].
    End Impl_core_convert_AsRef_core_ffi_c_str_CStr_for_core_ffi_c_str_CStr.
    
    (*
    const unsafe fn strlen(ptr: *const c_char) -> usize {
        const fn strlen_ct(s: *const c_char) -> usize {
            let mut len = 0;
    
            // SAFETY: Outer caller has provided a pointer to a valid C string.
            while unsafe { *s.add(len) } != 0 {
                len += 1;
            }
    
            len
        }
    
        #[inline]
        fn strlen_rt(s: *const c_char) -> usize {
            extern "C" {
                /// Provided by libc or compiler_builtins.
                fn strlen(s: *const c_char) -> usize;
            }
    
            // SAFETY: Outer caller has provided a pointer to a valid C string.
            unsafe { strlen(s) }
        }
    
        intrinsics::const_eval_select((ptr,), strlen_ct, strlen_rt)
    }
    *)
    Definition strlen (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ ptr ] =>
        ltac:(M.monadic
          (let ptr := M.alloc (| ptr |) in
          M.call_closure (|
            M.get_function (|
              "core::intrinsics::const_eval_select",
              [
                Ty.tuple [ Ty.apply (Ty.path "*const") [] [ Ty.path "i8" ] ];
                Ty.function [ Ty.apply (Ty.path "*const") [] [ Ty.path "i8" ] ] (Ty.path "usize");
                Ty.function [ Ty.apply (Ty.path "*const") [] [ Ty.path "i8" ] ] (Ty.path "usize");
                Ty.path "usize"
              ]
            |),
            [
              Value.Tuple [ M.read (| ptr |) ];
              M.get_function (| "core::ffi::c_str::strlen.strlen_ct", [] |);
              M.get_function (| "core::ffi::c_str::strlen.strlen_rt", [] |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_strlen : M.IsFunction "core::ffi::c_str::strlen" strlen.
    
    Module strlen.
      (*
          const fn strlen_ct(s: *const c_char) -> usize {
              let mut len = 0;
      
              // SAFETY: Outer caller has provided a pointer to a valid C string.
              while unsafe { *s.add(len) } != 0 {
                  len += 1;
              }
      
              len
          }
      *)
      Definition strlen_ct (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ s ] =>
          ltac:(M.monadic
            (let s := M.alloc (| s |) in
            M.read (|
              let~ len := M.alloc (| Value.Integer IntegerKind.Usize 0 |) in
              let~ _ :=
                M.loop (|
                  ltac:(M.monadic
                    (M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  BinOp.ne (|
                                    M.read (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply (Ty.path "*const") [] [ Ty.path "i8" ],
                                          "add",
                                          []
                                        |),
                                        [ M.read (| s |); M.read (| len |) ]
                                      |)
                                    |),
                                    Value.Integer IntegerKind.I8 0
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            let~ _ :=
                              let β := len in
                              M.write (|
                                β,
                                BinOp.Wrap.add (|
                                  M.read (| β |),
                                  Value.Integer IntegerKind.Usize 1
                                |)
                              |) 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
              len
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_strlen_ct : M.IsFunction "core::ffi::c_str::strlen::strlen_ct" strlen_ct.
      
      (*
          fn strlen_rt(s: *const c_char) -> usize {
              extern "C" {
                  /// Provided by libc or compiler_builtins.
                  fn strlen(s: *const c_char) -> usize;
              }
      
              // SAFETY: Outer caller has provided a pointer to a valid C string.
              unsafe { strlen(s) }
          }
      *)
      Definition strlen_rt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ s ] =>
          ltac:(M.monadic
            (let s := M.alloc (| s |) in
            M.call_closure (|
              M.get_function (| "core::ffi::c_str::strlen::strlen_rt::strlen", [] |),
              [ M.read (| s |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_strlen_rt : M.IsFunction "core::ffi::c_str::strlen::strlen_rt" strlen_rt.
      
      Module strlen_rt.
        Parameter strlen : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
        
        Axiom Function_strlen : M.IsFunction "core::ffi::c_str::strlen::strlen_rt::strlen" strlen.
      End strlen_rt.
    End strlen.
    
    (* StructRecord
      {
        name := "Bytes";
        const_params := [];
        ty_params := [];
        fields :=
          [
            ("ptr", Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ Ty.path "u8" ]);
            ("phantom",
              Ty.apply
                (Ty.path "core::marker::PhantomData")
                []
                [ Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "i8" ] ] ])
          ];
      } *)
    
    Module Impl_core_clone_Clone_for_core_ffi_c_str_Bytes.
      Definition Self : Ty.t := Ty.path "core::ffi::c_str::Bytes".
      
      (* Clone *)
      Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            Value.StructRecord
              "core::ffi::c_str::Bytes"
              [
                ("ptr",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::clone::Clone",
                      Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ Ty.path "u8" ],
                      [],
                      "clone",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::ffi::c_str::Bytes",
                        "ptr"
                      |)
                    ]
                  |));
                ("phantom",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::clone::Clone",
                      Ty.apply
                        (Ty.path "core::marker::PhantomData")
                        []
                        [
                          Ty.apply
                            (Ty.path "&")
                            []
                            [ Ty.apply (Ty.path "slice") [] [ Ty.path "i8" ] ]
                        ],
                      [],
                      "clone",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::ffi::c_str::Bytes",
                        "phantom"
                      |)
                    ]
                  |))
              ]))
        | _, _, _ => 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_core_ffi_c_str_Bytes.
    
    Module Impl_core_fmt_Debug_for_core_ffi_c_str_Bytes.
      Definition Self : Ty.t := Ty.path "core::ffi::c_str::Bytes".
      
      (* Debug *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "core::fmt::Formatter",
                "debug_struct_field2_finish",
                []
              |),
              [
                M.read (| f |);
                M.read (| Value.String "Bytes" |);
                M.read (| Value.String "ptr" |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::ffi::c_str::Bytes",
                  "ptr"
                |);
                M.read (| Value.String "phantom" |);
                M.alloc (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::ffi::c_str::Bytes",
                    "phantom"
                  |)
                |)
              ]
            |)))
        | _, _, _ => 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_core_ffi_c_str_Bytes.
    
    Module Impl_core_marker_Send_for_core_ffi_c_str_Bytes.
      Definition Self : Ty.t := Ty.path "core::ffi::c_str::Bytes".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::Send"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Send_for_core_ffi_c_str_Bytes.
    
    Module Impl_core_marker_Sync_for_core_ffi_c_str_Bytes.
      Definition Self : Ty.t := Ty.path "core::ffi::c_str::Bytes".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::Sync"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Sync_for_core_ffi_c_str_Bytes.
    
    Module Impl_core_ffi_c_str_Bytes.
      Definition Self : Ty.t := Ty.path "core::ffi::c_str::Bytes".
      
      (*
          fn new(s: &'a CStr) -> Self {
              Self { ptr: s.as_non_null_ptr().cast(), phantom: PhantomData }
          }
      *)
      Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ s ] =>
          ltac:(M.monadic
            (let s := M.alloc (| s |) in
            Value.StructRecord
              "core::ffi::c_str::Bytes"
              [
                ("ptr",
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ Ty.path "i8" ],
                      "cast",
                      [ Ty.path "u8" ]
                    |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::ffi::c_str::CStr",
                          "as_non_null_ptr",
                          []
                        |),
                        [ M.read (| s |) ]
                      |)
                    ]
                  |));
                ("phantom", Value.StructTuple "core::marker::PhantomData" [])
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
      
      (*
          fn is_empty(&self) -> bool {
              // SAFETY: We uphold that the pointer is always valid to dereference
              // by starting with a valid C string and then never incrementing beyond
              // the nul terminator.
              unsafe { self.ptr.read() == 0 }
          }
      *)
      Definition is_empty (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            BinOp.eq (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ Ty.path "u8" ],
                  "read",
                  []
                |),
                [
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::ffi::c_str::Bytes",
                      "ptr"
                    |)
                  |)
                ]
              |),
              Value.Integer IntegerKind.U8 0
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_is_empty : M.IsAssociatedFunction Self "is_empty" is_empty.
    End Impl_core_ffi_c_str_Bytes.
    
    Module Impl_core_iter_traits_iterator_Iterator_for_core_ffi_c_str_Bytes.
      Definition Self : Ty.t := Ty.path "core::ffi::c_str::Bytes".
      
      (*     type Item = u8; *)
      Definition _Item : Ty.t := Ty.path "u8".
      
      (*
          fn next(&mut self) -> Option<u8> {
              // SAFETY: We only choose a pointer from a valid C string, which must
              // be non-null and contain at least one value. Since we always stop at
              // the nul terminator, which is guaranteed to exist, we can assume that
              // the pointer is non-null and valid. This lets us safely dereference
              // it and assume that adding 1 will create a new, non-null, valid
              // pointer.
              unsafe {
                  let ret = self.ptr.read();
                  if ret == 0 {
                      None
                  } else {
                      self.ptr = self.ptr.add(1);
                      Some(ret)
                  }
              }
          }
      *)
      Definition next (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              let~ ret :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ Ty.path "u8" ],
                      "read",
                      []
                    |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::ffi::c_str::Bytes",
                          "ptr"
                        |)
                      |)
                    ]
                  |)
                |) in
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            BinOp.eq (| M.read (| ret |), Value.Integer IntegerKind.U8 0 |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (| Value.StructTuple "core::option::Option::None" [] |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let~ _ :=
                        M.write (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "core::ffi::c_str::Bytes",
                            "ptr"
                          |),
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ Ty.path "u8" ],
                              "add",
                              []
                            |),
                            [
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "core::ffi::c_str::Bytes",
                                  "ptr"
                                |)
                              |);
                              Value.Integer IntegerKind.Usize 1
                            ]
                          |)
                        |) in
                      M.alloc (|
                        Value.StructTuple "core::option::Option::Some" [ M.read (| ret |) ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn size_hint(&self) -> (usize, Option<usize>) {
              if self.is_empty() { (0, Some(0)) } else { (1, None) }
          }
      *)
      Definition size_hint (ε : 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 (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::ffi::c_str::Bytes",
                                "is_empty",
                                []
                              |),
                              [ M.read (| self |) ]
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        Value.Tuple
                          [
                            Value.Integer IntegerKind.Usize 0;
                            Value.StructTuple
                              "core::option::Option::Some"
                              [ Value.Integer IntegerKind.Usize 0 ]
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        Value.Tuple
                          [
                            Value.Integer IntegerKind.Usize 1;
                            Value.StructTuple "core::option::Option::None" []
                          ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn count(self) -> usize {
              // SAFETY: We always hold a valid pointer to a C string
              unsafe { strlen(self.ptr.as_ptr().cast()) }
          }
      *)
      Definition count (ε : 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_function (| "core::ffi::c_str::strlen", [] |),
              [
                (* MutToConstPointer *)
                M.pointer_coercion
                  (M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "*mut") [] [ Ty.path "u8" ],
                      "cast",
                      [ Ty.path "i8" ]
                    |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ Ty.path "u8" ],
                          "as_ptr",
                          []
                        |),
                        [
                          M.read (|
                            M.SubPointer.get_struct_record_field (|
                              self,
                              "core::ffi::c_str::Bytes",
                              "ptr"
                            |)
                          |)
                        ]
                      |)
                    ]
                  |))
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::iter::traits::iterator::Iterator"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("Item", InstanceField.Ty _Item);
            ("next", InstanceField.Method next);
            ("size_hint", InstanceField.Method size_hint);
            ("count", InstanceField.Method count)
          ].
    End Impl_core_iter_traits_iterator_Iterator_for_core_ffi_c_str_Bytes.
    
    Module Impl_core_iter_traits_marker_FusedIterator_for_core_ffi_c_str_Bytes.
      Definition Self : Ty.t := Ty.path "core::ffi::c_str::Bytes".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::iter::traits::marker::FusedIterator"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_iter_traits_marker_FusedIterator_for_core_ffi_c_str_Bytes.
  End c_str.
End ffi.
