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

Module io.
  Module borrowed_buf.
    (* StructRecord
      {
        name := "BorrowedBuf";
        const_params := [];
        ty_params := [];
        fields :=
          [
            ("buf",
              Ty.apply
                (Ty.path "&mut")
                []
                [
                  Ty.apply
                    (Ty.path "slice")
                    []
                    [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ Ty.path "u8" ]
                    ]
                ]);
            ("filled", Ty.path "usize");
            ("init", Ty.path "usize")
          ];
      } *)
    
    Module Impl_core_fmt_Debug_for_core_io_borrowed_buf_BorrowedBuf.
      Definition Self : Ty.t := Ty.path "core::io::borrowed_buf::BorrowedBuf".
      
      (*
          fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result {
              f.debug_struct("BorrowedBuf")
                  .field("init", &self.init)
                  .field("filled", &self.filled)
                  .field("capacity", &self.capacity())
                  .finish()
          }
      *)
      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::builders::DebugStruct",
                "finish",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "core::fmt::builders::DebugStruct",
                    "field",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "core::fmt::builders::DebugStruct",
                        "field",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::fmt::builders::DebugStruct",
                            "field",
                            []
                          |),
                          [
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::Formatter",
                                  "debug_struct",
                                  []
                                |),
                                [ M.read (| f |); M.read (| Value.String "BorrowedBuf" |) ]
                              |)
                            |);
                            M.read (| Value.String "init" |);
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "core::io::borrowed_buf::BorrowedBuf",
                              "init"
                            |)
                          ]
                        |);
                        M.read (| Value.String "filled" |);
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::io::borrowed_buf::BorrowedBuf",
                          "filled"
                        |)
                      ]
                    |);
                    M.read (| Value.String "capacity" |);
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::io::borrowed_buf::BorrowedBuf",
                          "capacity",
                          []
                        |),
                        [ 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_io_borrowed_buf_BorrowedBuf.
    
    Module Impl_core_convert_From_ref_mut_slice_u8_for_core_io_borrowed_buf_BorrowedBuf.
      Definition Self : Ty.t := Ty.path "core::io::borrowed_buf::BorrowedBuf".
      
      (*
          fn from(slice: &'data mut [u8]) -> BorrowedBuf<'data> {
              let len = slice.len();
      
              BorrowedBuf {
                  // SAFETY: initialized data never becoming uninitialized is an invariant of BorrowedBuf
                  buf: unsafe { (slice as *mut [u8]).as_uninit_slice_mut().unwrap() },
                  filled: 0,
                  init: len,
              }
          }
      *)
      Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ slice ] =>
          ltac:(M.monadic
            (let slice := M.alloc (| slice |) in
            M.read (|
              let~ len :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                      "len",
                      []
                    |),
                    [ M.read (| slice |) ]
                  |)
                |) in
              M.alloc (|
                Value.StructRecord
                  "core::io::borrowed_buf::BorrowedBuf"
                  [
                    ("buf",
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "core::option::Option")
                            []
                            [
                              Ty.apply
                                (Ty.path "&mut")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "slice")
                                    []
                                    [
                                      Ty.apply
                                        (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                        []
                                        [ Ty.path "u8" ]
                                    ]
                                ]
                            ],
                          "unwrap",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "*mut")
                                []
                                [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ],
                              "as_uninit_slice_mut",
                              []
                            |),
                            [ M.read (| M.use (M.alloc (| M.read (| slice |) |)) |) ]
                          |)
                        ]
                      |));
                    ("filled", Value.Integer IntegerKind.Usize 0);
                    ("init", M.read (| len |))
                  ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::convert::From"
          Self
          (* Trait polymorphic types *)
          [ (* T *) Ty.apply (Ty.path "&mut") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ]
          ]
          (* Instance *) [ ("from", InstanceField.Method from) ].
    End Impl_core_convert_From_ref_mut_slice_u8_for_core_io_borrowed_buf_BorrowedBuf.
    
    Module Impl_core_convert_From_ref_mut_slice_core_mem_maybe_uninit_MaybeUninit_u8_for_core_io_borrowed_buf_BorrowedBuf.
      Definition Self : Ty.t := Ty.path "core::io::borrowed_buf::BorrowedBuf".
      
      (*
          fn from(buf: &'data mut [MaybeUninit<u8>]) -> BorrowedBuf<'data> {
              BorrowedBuf { buf, filled: 0, init: 0 }
          }
      *)
      Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ buf ] =>
          ltac:(M.monadic
            (let buf := M.alloc (| buf |) in
            Value.StructRecord
              "core::io::borrowed_buf::BorrowedBuf"
              [
                ("buf", M.read (| buf |));
                ("filled", Value.Integer IntegerKind.Usize 0);
                ("init", Value.Integer IntegerKind.Usize 0)
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::convert::From"
          Self
          (* Trait polymorphic types *)
          [
            (* T *)
            Ty.apply
              (Ty.path "&mut")
              []
              [
                Ty.apply
                  (Ty.path "slice")
                  []
                  [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ Ty.path "u8" ] ]
              ]
          ]
          (* Instance *) [ ("from", InstanceField.Method from) ].
    End Impl_core_convert_From_ref_mut_slice_core_mem_maybe_uninit_MaybeUninit_u8_for_core_io_borrowed_buf_BorrowedBuf.
    
    Module Impl_core_io_borrowed_buf_BorrowedBuf.
      Definition Self : Ty.t := Ty.path "core::io::borrowed_buf::BorrowedBuf".
      
      (*
          pub fn capacity(&self) -> usize {
              self.buf.len()
          }
      *)
      Definition capacity (ε : 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.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ Ty.path "u8" ] ],
                "len",
                []
              |),
              [
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::io::borrowed_buf::BorrowedBuf",
                    "buf"
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_capacity : M.IsAssociatedFunction Self "capacity" capacity.
      
      (*
          pub fn len(&self) -> usize {
              self.filled
          }
      *)
      Definition len (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::io::borrowed_buf::BorrowedBuf",
                "filled"
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_len : M.IsAssociatedFunction Self "len" len.
      
      (*
          pub fn init_len(&self) -> usize {
              self.init
          }
      *)
      Definition init_len (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::io::borrowed_buf::BorrowedBuf",
                "init"
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_init_len : M.IsAssociatedFunction Self "init_len" init_len.
      
      (*
          pub fn filled(&self) -> &[u8] {
              // SAFETY: We only slice the filled part of the buffer, which is always valid
              unsafe {
                  let buf = self.buf.get_unchecked(..self.filled);
                  MaybeUninit::slice_assume_init_ref(buf)
              }
          }
      *)
      Definition filled (ε : 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~ buf :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "slice")
                        []
                        [
                          Ty.apply
                            (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                            []
                            [ Ty.path "u8" ]
                        ],
                      "get_unchecked",
                      [ Ty.apply (Ty.path "core::ops::range::RangeTo") [] [ Ty.path "usize" ] ]
                    |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::io::borrowed_buf::BorrowedBuf",
                          "buf"
                        |)
                      |);
                      Value.StructRecord
                        "core::ops::range::RangeTo"
                        [
                          ("end_",
                            M.read (|
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::io::borrowed_buf::BorrowedBuf",
                                "filled"
                              |)
                            |))
                        ]
                    ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ Ty.path "u8" ],
                    "slice_assume_init_ref",
                    []
                  |),
                  [ M.read (| buf |) ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_filled : M.IsAssociatedFunction Self "filled" filled.
      
      (*
          pub fn filled_mut(&mut self) -> &mut [u8] {
              // SAFETY: We only slice the filled part of the buffer, which is always valid
              unsafe {
                  let buf = self.buf.get_unchecked_mut(..self.filled);
                  MaybeUninit::slice_assume_init_mut(buf)
              }
          }
      *)
      Definition filled_mut (ε : 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~ buf :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "slice")
                        []
                        [
                          Ty.apply
                            (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                            []
                            [ Ty.path "u8" ]
                        ],
                      "get_unchecked_mut",
                      [ Ty.apply (Ty.path "core::ops::range::RangeTo") [] [ Ty.path "usize" ] ]
                    |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::io::borrowed_buf::BorrowedBuf",
                          "buf"
                        |)
                      |);
                      Value.StructRecord
                        "core::ops::range::RangeTo"
                        [
                          ("end_",
                            M.read (|
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::io::borrowed_buf::BorrowedBuf",
                                "filled"
                              |)
                            |))
                        ]
                    ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ Ty.path "u8" ],
                    "slice_assume_init_mut",
                    []
                  |),
                  [ M.read (| buf |) ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_filled_mut : M.IsAssociatedFunction Self "filled_mut" filled_mut.
      
      (*
          pub fn unfilled<'this>(&'this mut self) -> BorrowedCursor<'this> {
              BorrowedCursor {
                  start: self.filled,
                  // SAFETY: we never assign into `BorrowedCursor::buf`, so treating its
                  // lifetime covariantly is safe.
                  buf: unsafe {
                      mem::transmute::<&'this mut BorrowedBuf<'data>, &'this mut BorrowedBuf<'this>>(self)
                  },
              }
          }
      *)
      Definition unfilled (ε : 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::io::borrowed_buf::BorrowedCursor"
              [
                ("start",
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::io::borrowed_buf::BorrowedBuf",
                      "filled"
                    |)
                  |));
                ("buf",
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::transmute",
                      [
                        Ty.apply
                          (Ty.path "&mut")
                          []
                          [ Ty.path "core::io::borrowed_buf::BorrowedBuf" ];
                        Ty.apply
                          (Ty.path "&mut")
                          []
                          [ Ty.path "core::io::borrowed_buf::BorrowedBuf" ]
                      ]
                    |),
                    [ M.read (| self |) ]
                  |))
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_unfilled : M.IsAssociatedFunction Self "unfilled" unfilled.
      
      (*
          pub fn clear(&mut self) -> &mut Self {
              self.filled = 0;
              self
          }
      *)
      Definition clear (ε : 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~ _ :=
                M.write (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::io::borrowed_buf::BorrowedBuf",
                    "filled"
                  |),
                  Value.Integer IntegerKind.Usize 0
                |) in
              M.alloc (| M.read (| self |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_clear : M.IsAssociatedFunction Self "clear" clear.
      
      (*
          pub unsafe fn set_init(&mut self, n: usize) -> &mut Self {
              self.init = cmp::max(self.init, n);
              self
          }
      *)
      Definition set_init (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; n ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let n := M.alloc (| n |) in
            M.read (|
              let~ _ :=
                M.write (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::io::borrowed_buf::BorrowedBuf",
                    "init"
                  |),
                  M.call_closure (|
                    M.get_function (| "core::cmp::max", [ Ty.path "usize" ] |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::io::borrowed_buf::BorrowedBuf",
                          "init"
                        |)
                      |);
                      M.read (| n |)
                    ]
                  |)
                |) in
              M.alloc (| M.read (| self |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_set_init : M.IsAssociatedFunction Self "set_init" set_init.
    End Impl_core_io_borrowed_buf_BorrowedBuf.
    
    (* StructRecord
      {
        name := "BorrowedCursor";
        const_params := [];
        ty_params := [];
        fields :=
          [
            ("buf", Ty.apply (Ty.path "&mut") [] [ Ty.path "core::io::borrowed_buf::BorrowedBuf" ]);
            ("start", Ty.path "usize")
          ];
      } *)
    
    Module Impl_core_fmt_Debug_for_core_io_borrowed_buf_BorrowedCursor.
      Definition Self : Ty.t := Ty.path "core::io::borrowed_buf::BorrowedCursor".
      
      (* 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 "BorrowedCursor" |);
                M.read (| Value.String "buf" |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::io::borrowed_buf::BorrowedCursor",
                  "buf"
                |);
                M.read (| Value.String "start" |);
                M.alloc (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::io::borrowed_buf::BorrowedCursor",
                    "start"
                  |)
                |)
              ]
            |)))
        | _, _, _ => 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_io_borrowed_buf_BorrowedCursor.
    
    Module Impl_core_io_borrowed_buf_BorrowedCursor.
      Definition Self : Ty.t := Ty.path "core::io::borrowed_buf::BorrowedCursor".
      
      (*
          pub fn reborrow<'this>(&'this mut self) -> BorrowedCursor<'this> {
              BorrowedCursor {
                  // SAFETY: we never assign into `BorrowedCursor::buf`, so treating its
                  // lifetime covariantly is safe.
                  buf: unsafe {
                      mem::transmute::<&'this mut BorrowedBuf<'a>, &'this mut BorrowedBuf<'this>>(
                          self.buf,
                      )
                  },
                  start: self.start,
              }
          }
      *)
      Definition reborrow (ε : 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::io::borrowed_buf::BorrowedCursor"
              [
                ("buf",
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::transmute",
                      [
                        Ty.apply
                          (Ty.path "&mut")
                          []
                          [ Ty.path "core::io::borrowed_buf::BorrowedBuf" ];
                        Ty.apply
                          (Ty.path "&mut")
                          []
                          [ Ty.path "core::io::borrowed_buf::BorrowedBuf" ]
                      ]
                    |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::io::borrowed_buf::BorrowedCursor",
                          "buf"
                        |)
                      |)
                    ]
                  |));
                ("start",
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::io::borrowed_buf::BorrowedCursor",
                      "start"
                    |)
                  |))
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_reborrow : M.IsAssociatedFunction Self "reborrow" reborrow.
      
      (*
          pub fn capacity(&self) -> usize {
              self.buf.capacity() - self.buf.filled
          }
      *)
      Definition capacity (ε : 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.path "core::io::borrowed_buf::BorrowedBuf",
                  "capacity",
                  []
                |),
                [
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::io::borrowed_buf::BorrowedCursor",
                      "buf"
                    |)
                  |)
                ]
              |),
              M.read (|
                M.SubPointer.get_struct_record_field (|
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::io::borrowed_buf::BorrowedCursor",
                      "buf"
                    |)
                  |),
                  "core::io::borrowed_buf::BorrowedBuf",
                  "filled"
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_capacity : M.IsAssociatedFunction Self "capacity" capacity.
      
      (*
          pub fn written(&self) -> usize {
              self.buf.filled - self.start
          }
      *)
      Definition written (ε : 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.read (|
                M.SubPointer.get_struct_record_field (|
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::io::borrowed_buf::BorrowedCursor",
                      "buf"
                    |)
                  |),
                  "core::io::borrowed_buf::BorrowedBuf",
                  "filled"
                |)
              |),
              M.read (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::io::borrowed_buf::BorrowedCursor",
                  "start"
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_written : M.IsAssociatedFunction Self "written" written.
      
      (*
          pub fn init_ref(&self) -> &[u8] {
              // SAFETY: We only slice the initialized part of the buffer, which is always valid
              unsafe {
                  let buf = self.buf.buf.get_unchecked(self.buf.filled..self.buf.init);
                  MaybeUninit::slice_assume_init_ref(buf)
              }
          }
      *)
      Definition init_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 (|
              let~ buf :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "slice")
                        []
                        [
                          Ty.apply
                            (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                            []
                            [ Ty.path "u8" ]
                        ],
                      "get_unchecked",
                      [ Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ] ]
                    |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "core::io::borrowed_buf::BorrowedCursor",
                              "buf"
                            |)
                          |),
                          "core::io::borrowed_buf::BorrowedBuf",
                          "buf"
                        |)
                      |);
                      Value.StructRecord
                        "core::ops::range::Range"
                        [
                          ("start",
                            M.read (|
                              M.SubPointer.get_struct_record_field (|
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "core::io::borrowed_buf::BorrowedCursor",
                                    "buf"
                                  |)
                                |),
                                "core::io::borrowed_buf::BorrowedBuf",
                                "filled"
                              |)
                            |));
                          ("end_",
                            M.read (|
                              M.SubPointer.get_struct_record_field (|
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "core::io::borrowed_buf::BorrowedCursor",
                                    "buf"
                                  |)
                                |),
                                "core::io::borrowed_buf::BorrowedBuf",
                                "init"
                              |)
                            |))
                        ]
                    ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ Ty.path "u8" ],
                    "slice_assume_init_ref",
                    []
                  |),
                  [ M.read (| buf |) ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_init_ref : M.IsAssociatedFunction Self "init_ref" init_ref.
      
      (*
          pub fn init_mut(&mut self) -> &mut [u8] {
              // SAFETY: We only slice the initialized part of the buffer, which is always valid
              unsafe {
                  let buf = self.buf.buf.get_unchecked_mut(self.buf.filled..self.buf.init);
                  MaybeUninit::slice_assume_init_mut(buf)
              }
          }
      *)
      Definition init_mut (ε : 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~ buf :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "slice")
                        []
                        [
                          Ty.apply
                            (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                            []
                            [ Ty.path "u8" ]
                        ],
                      "get_unchecked_mut",
                      [ Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ] ]
                    |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "core::io::borrowed_buf::BorrowedCursor",
                              "buf"
                            |)
                          |),
                          "core::io::borrowed_buf::BorrowedBuf",
                          "buf"
                        |)
                      |);
                      Value.StructRecord
                        "core::ops::range::Range"
                        [
                          ("start",
                            M.read (|
                              M.SubPointer.get_struct_record_field (|
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "core::io::borrowed_buf::BorrowedCursor",
                                    "buf"
                                  |)
                                |),
                                "core::io::borrowed_buf::BorrowedBuf",
                                "filled"
                              |)
                            |));
                          ("end_",
                            M.read (|
                              M.SubPointer.get_struct_record_field (|
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "core::io::borrowed_buf::BorrowedCursor",
                                    "buf"
                                  |)
                                |),
                                "core::io::borrowed_buf::BorrowedBuf",
                                "init"
                              |)
                            |))
                        ]
                    ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ Ty.path "u8" ],
                    "slice_assume_init_mut",
                    []
                  |),
                  [ M.read (| buf |) ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_init_mut : M.IsAssociatedFunction Self "init_mut" init_mut.
      
      (*
          pub fn uninit_mut(&mut self) -> &mut [MaybeUninit<u8>] {
              // SAFETY: always in bounds
              unsafe { self.buf.buf.get_unchecked_mut(self.buf.init..) }
          }
      *)
      Definition uninit_mut (ε : 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.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ Ty.path "u8" ] ],
                "get_unchecked_mut",
                [ Ty.apply (Ty.path "core::ops::range::RangeFrom") [] [ Ty.path "usize" ] ]
              |),
              [
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::io::borrowed_buf::BorrowedCursor",
                        "buf"
                      |)
                    |),
                    "core::io::borrowed_buf::BorrowedBuf",
                    "buf"
                  |)
                |);
                Value.StructRecord
                  "core::ops::range::RangeFrom"
                  [
                    ("start",
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "core::io::borrowed_buf::BorrowedCursor",
                              "buf"
                            |)
                          |),
                          "core::io::borrowed_buf::BorrowedBuf",
                          "init"
                        |)
                      |))
                  ]
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_uninit_mut : M.IsAssociatedFunction Self "uninit_mut" uninit_mut.
      
      (*
          pub unsafe fn as_mut(&mut self) -> &mut [MaybeUninit<u8>] {
              // SAFETY: always in bounds
              unsafe { self.buf.buf.get_unchecked_mut(self.buf.filled..) }
          }
      *)
      Definition as_mut (ε : 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.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ Ty.path "u8" ] ],
                "get_unchecked_mut",
                [ Ty.apply (Ty.path "core::ops::range::RangeFrom") [] [ Ty.path "usize" ] ]
              |),
              [
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::io::borrowed_buf::BorrowedCursor",
                        "buf"
                      |)
                    |),
                    "core::io::borrowed_buf::BorrowedBuf",
                    "buf"
                  |)
                |);
                Value.StructRecord
                  "core::ops::range::RangeFrom"
                  [
                    ("start",
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "core::io::borrowed_buf::BorrowedCursor",
                              "buf"
                            |)
                          |),
                          "core::io::borrowed_buf::BorrowedBuf",
                          "filled"
                        |)
                      |))
                  ]
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_as_mut : M.IsAssociatedFunction Self "as_mut" as_mut.
      
      (*
          pub fn advance(&mut self, n: usize) -> &mut Self {
              let filled = self.buf.filled.strict_add(n);
              assert!(filled <= self.buf.init);
      
              self.buf.filled = filled;
              self
          }
      *)
      Definition advance (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; n ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let n := M.alloc (| n |) in
            M.read (|
              let~ filled :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "usize", "strict_add", [] |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "core::io::borrowed_buf::BorrowedCursor",
                              "buf"
                            |)
                          |),
                          "core::io::borrowed_buf::BorrowedBuf",
                          "filled"
                        |)
                      |);
                      M.read (| n |)
                    ]
                  |)
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              UnOp.not (|
                                BinOp.le (|
                                  M.read (| filled |),
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "core::io::borrowed_buf::BorrowedCursor",
                                          "buf"
                                        |)
                                      |),
                                      "core::io::borrowed_buf::BorrowedBuf",
                                      "init"
                                    |)
                                  |)
                                |)
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.call_closure (|
                              M.get_function (| "core::panicking::panic", [] |),
                              [
                                M.read (|
                                  Value.String "assertion failed: filled <= self.buf.init"
                                |)
                              ]
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ _ :=
                M.write (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::io::borrowed_buf::BorrowedCursor",
                        "buf"
                      |)
                    |),
                    "core::io::borrowed_buf::BorrowedBuf",
                    "filled"
                  |),
                  M.read (| filled |)
                |) in
              M.alloc (| M.read (| self |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_advance : M.IsAssociatedFunction Self "advance" advance.
      
      (*
          pub unsafe fn advance_unchecked(&mut self, n: usize) -> &mut Self {
              self.buf.filled += n;
              self.buf.init = cmp::max(self.buf.init, self.buf.filled);
              self
          }
      *)
      Definition advance_unchecked (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; n ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let n := M.alloc (| n |) in
            M.read (|
              let~ _ :=
                let β :=
                  M.SubPointer.get_struct_record_field (|
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::io::borrowed_buf::BorrowedCursor",
                        "buf"
                      |)
                    |),
                    "core::io::borrowed_buf::BorrowedBuf",
                    "filled"
                  |) in
                M.write (| β, BinOp.Wrap.add (| M.read (| β |), M.read (| n |) |) |) in
              let~ _ :=
                M.write (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::io::borrowed_buf::BorrowedCursor",
                        "buf"
                      |)
                    |),
                    "core::io::borrowed_buf::BorrowedBuf",
                    "init"
                  |),
                  M.call_closure (|
                    M.get_function (| "core::cmp::max", [ Ty.path "usize" ] |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "core::io::borrowed_buf::BorrowedCursor",
                              "buf"
                            |)
                          |),
                          "core::io::borrowed_buf::BorrowedBuf",
                          "init"
                        |)
                      |);
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "core::io::borrowed_buf::BorrowedCursor",
                              "buf"
                            |)
                          |),
                          "core::io::borrowed_buf::BorrowedBuf",
                          "filled"
                        |)
                      |)
                    ]
                  |)
                |) in
              M.alloc (| M.read (| self |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_advance_unchecked :
        M.IsAssociatedFunction Self "advance_unchecked" advance_unchecked.
      
      (*
          pub fn ensure_init(&mut self) -> &mut Self {
              let uninit = self.uninit_mut();
              // SAFETY: 0 is a valid value for MaybeUninit<u8> and the length matches the allocation
              // since it is comes from a slice reference.
              unsafe {
                  ptr::write_bytes(uninit.as_mut_ptr(), 0, uninit.len());
              }
              self.buf.init = self.buf.capacity();
      
              self
          }
      *)
      Definition ensure_init (ε : 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~ uninit :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "core::io::borrowed_buf::BorrowedCursor",
                      "uninit_mut",
                      []
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              let~ _ :=
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::intrinsics::write_bytes",
                        [
                          Ty.apply
                            (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                            []
                            [ Ty.path "u8" ]
                        ]
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "slice")
                              []
                              [
                                Ty.apply
                                  (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                  []
                                  [ Ty.path "u8" ]
                              ],
                            "as_mut_ptr",
                            []
                          |),
                          [ M.read (| uninit |) ]
                        |);
                        Value.Integer IntegerKind.U8 0;
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "slice")
                              []
                              [
                                Ty.apply
                                  (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                  []
                                  [ Ty.path "u8" ]
                              ],
                            "len",
                            []
                          |),
                          [ M.read (| uninit |) ]
                        |)
                      ]
                    |)
                  |) in
                M.alloc (| Value.Tuple [] |) in
              let~ _ :=
                M.write (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::io::borrowed_buf::BorrowedCursor",
                        "buf"
                      |)
                    |),
                    "core::io::borrowed_buf::BorrowedBuf",
                    "init"
                  |),
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "core::io::borrowed_buf::BorrowedBuf",
                      "capacity",
                      []
                    |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::io::borrowed_buf::BorrowedCursor",
                          "buf"
                        |)
                      |)
                    ]
                  |)
                |) in
              M.alloc (| M.read (| self |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_ensure_init : M.IsAssociatedFunction Self "ensure_init" ensure_init.
      
      (*
          pub unsafe fn set_init(&mut self, n: usize) -> &mut Self {
              self.buf.init = cmp::max(self.buf.init, self.buf.filled + n);
              self
          }
      *)
      Definition set_init (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; n ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let n := M.alloc (| n |) in
            M.read (|
              let~ _ :=
                M.write (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::io::borrowed_buf::BorrowedCursor",
                        "buf"
                      |)
                    |),
                    "core::io::borrowed_buf::BorrowedBuf",
                    "init"
                  |),
                  M.call_closure (|
                    M.get_function (| "core::cmp::max", [ Ty.path "usize" ] |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "core::io::borrowed_buf::BorrowedCursor",
                              "buf"
                            |)
                          |),
                          "core::io::borrowed_buf::BorrowedBuf",
                          "init"
                        |)
                      |);
                      BinOp.Wrap.add (|
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (|
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::io::borrowed_buf::BorrowedCursor",
                                "buf"
                              |)
                            |),
                            "core::io::borrowed_buf::BorrowedBuf",
                            "filled"
                          |)
                        |),
                        M.read (| n |)
                      |)
                    ]
                  |)
                |) in
              M.alloc (| M.read (| self |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_set_init : M.IsAssociatedFunction Self "set_init" set_init.
      
      (*
          pub fn append(&mut self, buf: &[u8]) {
              assert!(self.capacity() >= buf.len());
      
              // SAFETY: we do not de-initialize any of the elements of the slice
              unsafe {
                  MaybeUninit::copy_from_slice(&mut self.as_mut()[..buf.len()], buf);
              }
      
              // SAFETY: We just added the entire contents of buf to the filled section.
              unsafe {
                  self.set_init(buf.len());
              }
              self.buf.filled += buf.len();
          }
      *)
      Definition append (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; buf ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let buf := M.alloc (| buf |) in
            M.read (|
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              UnOp.not (|
                                BinOp.ge (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::io::borrowed_buf::BorrowedCursor",
                                      "capacity",
                                      []
                                    |),
                                    [ M.read (| self |) ]
                                  |),
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                      "len",
                                      []
                                    |),
                                    [ M.read (| buf |) ]
                                  |)
                                |)
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.call_closure (|
                              M.get_function (| "core::panicking::panic", [] |),
                              [
                                M.read (|
                                  Value.String "assertion failed: self.capacity() >= buf.len()"
                                |)
                              ]
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ _ :=
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                          []
                          [ Ty.path "u8" ],
                        "copy_from_slice",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::index::IndexMut",
                            Ty.apply
                              (Ty.path "slice")
                              []
                              [
                                Ty.apply
                                  (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                  []
                                  [ Ty.path "u8" ]
                              ],
                            [ Ty.apply (Ty.path "core::ops::range::RangeTo") [] [ Ty.path "usize" ]
                            ],
                            "index_mut",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::io::borrowed_buf::BorrowedCursor",
                                "as_mut",
                                []
                              |),
                              [ M.read (| self |) ]
                            |);
                            Value.StructRecord
                              "core::ops::range::RangeTo"
                              [
                                ("end_",
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                      "len",
                                      []
                                    |),
                                    [ M.read (| buf |) ]
                                  |))
                              ]
                          ]
                        |);
                        M.read (| buf |)
                      ]
                    |)
                  |) in
                M.alloc (| Value.Tuple [] |) in
              let~ _ :=
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "core::io::borrowed_buf::BorrowedCursor",
                        "set_init",
                        []
                      |),
                      [
                        M.read (| self |);
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                            "len",
                            []
                          |),
                          [ M.read (| buf |) ]
                        |)
                      ]
                    |)
                  |) in
                M.alloc (| Value.Tuple [] |) in
              let~ _ :=
                let β :=
                  M.SubPointer.get_struct_record_field (|
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::io::borrowed_buf::BorrowedCursor",
                        "buf"
                      |)
                    |),
                    "core::io::borrowed_buf::BorrowedBuf",
                    "filled"
                  |) in
                M.write (|
                  β,
                  BinOp.Wrap.add (|
                    M.read (| β |),
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                        "len",
                        []
                      |),
                      [ M.read (| buf |) ]
                    |)
                  |)
                |) in
              M.alloc (| Value.Tuple [] |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_append : M.IsAssociatedFunction Self "append" append.
    End Impl_core_io_borrowed_buf_BorrowedCursor.
  End borrowed_buf.
End io.
