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

Module slice.
  Module memchr.
    Definition value_LO_USIZE : Value.t :=
      M.run
        ltac:(M.monadic
          (M.alloc (|
            M.call_closure (|
              M.get_associated_function (| Ty.path "usize", "repeat_u8", [] |),
              [ Value.Integer IntegerKind.U8 1 ]
            |)
          |))).
    
    Definition value_HI_USIZE : Value.t :=
      M.run
        ltac:(M.monadic
          (M.alloc (|
            M.call_closure (|
              M.get_associated_function (| Ty.path "usize", "repeat_u8", [] |),
              [ Value.Integer IntegerKind.U8 128 ]
            |)
          |))).
    
    Definition value_USIZE_BYTES : Value.t :=
      M.run
        ltac:(M.monadic
          (M.alloc (|
            M.call_closure (| M.get_function (| "core::mem::size_of", [ Ty.path "usize" ] |), [] |)
          |))).
    
    (*
    const fn contains_zero_byte(x: usize) -> bool {
        x.wrapping_sub(LO_USIZE) & !x & HI_USIZE != 0
    }
    *)
    Definition contains_zero_byte (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ x ] =>
        ltac:(M.monadic
          (let x := M.alloc (| x |) in
          BinOp.ne (|
            BinOp.bit_and
              (BinOp.bit_and
                (M.call_closure (|
                  M.get_associated_function (| Ty.path "usize", "wrapping_sub", [] |),
                  [
                    M.read (| x |);
                    M.read (| M.get_constant (| "core::slice::memchr::LO_USIZE" |) |)
                  ]
                |))
                (UnOp.not (| M.read (| x |) |)))
              (M.read (| M.get_constant (| "core::slice::memchr::HI_USIZE" |) |)),
            Value.Integer IntegerKind.Usize 0
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_contains_zero_byte :
      M.IsFunction "core::slice::memchr::contains_zero_byte" contains_zero_byte.
    
    (*
    pub const fn memchr(x: u8, text: &[u8]) -> Option<usize> {
        // Fast path for small slices.
        if text.len() < 2 * USIZE_BYTES {
            return memchr_naive(x, text);
        }
    
        memchr_aligned(x, text)
    }
    *)
    Definition memchr (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ x; text ] =>
        ltac:(M.monadic
          (let x := M.alloc (| x |) in
          let text := M.alloc (| text |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.lt (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                      "len",
                                      []
                                    |),
                                    [ M.read (| text |) ]
                                  |),
                                  BinOp.Wrap.mul (|
                                    Value.Integer IntegerKind.Usize 2,
                                    M.read (|
                                      M.get_constant (| "core::slice::memchr::USIZE_BYTES" |)
                                    |)
                                  |)
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                M.return_ (|
                                  M.call_closure (|
                                    M.get_function (| "core::slice::memchr::memchr_naive", [] |),
                                    [ M.read (| x |); M.read (| text |) ]
                                  |)
                                |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "core::slice::memchr::memchr_aligned", [] |),
                    [ M.read (| x |); M.read (| text |) ]
                  |)
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_memchr : M.IsFunction "core::slice::memchr::memchr" memchr.
    
    (*
    const fn memchr_naive(x: u8, text: &[u8]) -> Option<usize> {
        let mut i = 0;
    
        // FIXME(const-hack): Replace with `text.iter().pos(|c| *c == x)`.
        while i < text.len() {
            if text[i] == x {
                return Some(i);
            }
    
            i += 1;
        }
    
        None
    }
    *)
    Definition memchr_naive (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ x; text ] =>
        ltac:(M.monadic
          (let x := M.alloc (| x |) in
          let text := M.alloc (| text |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ i := 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.lt (|
                                      M.read (| i |),
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                          "len",
                                          []
                                        |),
                                        [ M.read (| text |) ]
                                      |)
                                    |)
                                  |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              let~ _ :=
                                M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ :=
                                          M.use
                                            (M.alloc (|
                                              BinOp.eq (|
                                                M.read (|
                                                  M.SubPointer.get_array_field (|
                                                    M.read (| text |),
                                                    i
                                                  |)
                                                |),
                                                M.read (| x |)
                                              |)
                                            |)) in
                                        let _ :=
                                          M.is_constant_or_break_match (|
                                            M.read (| γ |),
                                            Value.Bool true
                                          |) in
                                        M.alloc (|
                                          M.never_to_any (|
                                            M.read (|
                                              M.return_ (|
                                                Value.StructTuple
                                                  "core::option::Option::Some"
                                                  [ M.read (| i |) ]
                                              |)
                                            |)
                                          |)
                                        |)));
                                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                  ]
                                |) in
                              let~ _ :=
                                let β := i 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
                M.alloc (| Value.StructTuple "core::option::Option::None" [] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_memchr_naive : M.IsFunction "core::slice::memchr::memchr_naive" memchr_naive.
    
    (*
    const fn memchr_aligned(x: u8, text: &[u8]) -> Option<usize> {
        // Scan for a single byte value by reading two `usize` words at a time.
        //
        // Split `text` in three parts
        // - unaligned initial part, before the first word aligned address in text
        // - body, scan by 2 words at a time
        // - the last remaining part, < 2 word size
    
        // search up to an aligned boundary
        let len = text.len();
        let ptr = text.as_ptr();
        let mut offset = ptr.align_offset(USIZE_BYTES);
    
        if offset > 0 {
            // FIXME(const-hack, fee1-dead): replace with min
            offset = if offset < len { offset } else { len };
            // FIXME(const-hack, fee1-dead): replace with range slicing
            // SAFETY: offset is within bounds
            let slice = unsafe { super::from_raw_parts(text.as_ptr(), offset) };
            if let Some(index) = memchr_naive(x, slice) {
                return Some(index);
            }
        }
    
        // search the body of the text
        let repeated_x = usize::repeat_u8(x);
        while offset <= len - 2 * USIZE_BYTES {
            // SAFETY: the while's predicate guarantees a distance of at least 2 * usize_bytes
            // between the offset and the end of the slice.
            unsafe {
                let u = *(ptr.add(offset) as *const usize);
                let v = *(ptr.add(offset + USIZE_BYTES) as *const usize);
    
                // break if there is a matching byte
                let zu = contains_zero_byte(u ^ repeated_x);
                let zv = contains_zero_byte(v ^ repeated_x);
                if zu || zv {
                    break;
                }
            }
            offset += USIZE_BYTES * 2;
        }
    
        // Find the byte after the point the body loop stopped.
        // FIXME(const-hack): Use `?` instead.
        // FIXME(const-hack, fee1-dead): use range slicing
        // SAFETY: offset is within bounds
        let slice = unsafe { super::from_raw_parts(text.as_ptr().add(offset), text.len() - offset) };
        if let Some(i) = memchr_naive(x, slice) { Some(offset + i) } else { None }
    }
    *)
    Definition memchr_aligned (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ x; text ] =>
        ltac:(M.monadic
          (let x := M.alloc (| x |) in
          let text := M.alloc (| text |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ len :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                        "len",
                        []
                      |),
                      [ M.read (| text |) ]
                    |)
                  |) in
                let~ ptr :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                        "as_ptr",
                        []
                      |),
                      [ M.read (| text |) ]
                    |)
                  |) in
                let~ offset :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "*const") [] [ Ty.path "u8" ],
                        "align_offset",
                        []
                      |),
                      [
                        M.read (| ptr |);
                        M.read (| M.get_constant (| "core::slice::memchr::USIZE_BYTES" |) |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.gt (|
                                  M.read (| offset |),
                                  Value.Integer IntegerKind.Usize 0
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          let~ _ :=
                            M.write (|
                              offset,
                              M.read (|
                                M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ :=
                                          M.use
                                            (M.alloc (|
                                              BinOp.lt (| M.read (| offset |), M.read (| len |) |)
                                            |)) in
                                        let _ :=
                                          M.is_constant_or_break_match (|
                                            M.read (| γ |),
                                            Value.Bool true
                                          |) in
                                        offset));
                                    fun γ => ltac:(M.monadic len)
                                  ]
                                |)
                              |)
                            |) in
                          let~ slice :=
                            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 (| text |) ]
                                  |);
                                  M.read (| offset |)
                                ]
                              |)
                            |) in
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_function (|
                                          "core::slice::memchr::memchr_naive",
                                          []
                                        |),
                                        [ M.read (| x |); M.read (| slice |) ]
                                      |)
                                    |) in
                                  let γ0_0 :=
                                    M.SubPointer.get_struct_tuple_field (|
                                      γ,
                                      "core::option::Option::Some",
                                      0
                                    |) in
                                  let index := M.copy (| γ0_0 |) in
                                  M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        M.return_ (|
                                          Value.StructTuple
                                            "core::option::Option::Some"
                                            [ M.read (| index |) ]
                                        |)
                                      |)
                                    |)
                                  |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ repeated_x :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "usize", "repeat_u8", [] |),
                      [ M.read (| x |) ]
                    |)
                  |) in
                let~ _ :=
                  M.loop (|
                    ltac:(M.monadic
                      (M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.use
                                  (M.alloc (|
                                    BinOp.le (|
                                      M.read (| offset |),
                                      BinOp.Wrap.sub (|
                                        M.read (| len |),
                                        BinOp.Wrap.mul (|
                                          Value.Integer IntegerKind.Usize 2,
                                          M.read (|
                                            M.get_constant (| "core::slice::memchr::USIZE_BYTES" |)
                                          |)
                                        |)
                                      |)
                                    |)
                                  |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              let~ _ :=
                                let~ u :=
                                  M.copy (|
                                    M.rust_cast
                                      (M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply (Ty.path "*const") [] [ Ty.path "u8" ],
                                          "add",
                                          []
                                        |),
                                        [ M.read (| ptr |); M.read (| offset |) ]
                                      |))
                                  |) in
                                let~ v :=
                                  M.copy (|
                                    M.rust_cast
                                      (M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply (Ty.path "*const") [] [ Ty.path "u8" ],
                                          "add",
                                          []
                                        |),
                                        [
                                          M.read (| ptr |);
                                          BinOp.Wrap.add (|
                                            M.read (| offset |),
                                            M.read (|
                                              M.get_constant (|
                                                "core::slice::memchr::USIZE_BYTES"
                                              |)
                                            |)
                                          |)
                                        ]
                                      |))
                                  |) in
                                let~ zu :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_function (|
                                        "core::slice::memchr::contains_zero_byte",
                                        []
                                      |),
                                      [ BinOp.bit_xor (M.read (| u |)) (M.read (| repeated_x |)) ]
                                    |)
                                  |) in
                                let~ zv :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_function (|
                                        "core::slice::memchr::contains_zero_byte",
                                        []
                                      |),
                                      [ BinOp.bit_xor (M.read (| v |)) (M.read (| repeated_x |)) ]
                                    |)
                                  |) in
                                M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ :=
                                          M.use
                                            (M.alloc (|
                                              LogicalOp.or (|
                                                M.read (| zu |),
                                                ltac:(M.monadic (M.read (| zv |)))
                                              |)
                                            |)) in
                                        let _ :=
                                          M.is_constant_or_break_match (|
                                            M.read (| γ |),
                                            Value.Bool true
                                          |) in
                                        M.alloc (|
                                          M.never_to_any (| M.read (| M.break (||) |) |)
                                        |)));
                                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                  ]
                                |) in
                              let~ _ :=
                                let β := offset in
                                M.write (|
                                  β,
                                  BinOp.Wrap.add (|
                                    M.read (| β |),
                                    BinOp.Wrap.mul (|
                                      M.read (|
                                        M.get_constant (| "core::slice::memchr::USIZE_BYTES" |)
                                      |),
                                      Value.Integer IntegerKind.Usize 2
                                    |)
                                  |)
                                |) in
                              M.alloc (| Value.Tuple [] |)));
                          fun γ =>
                            ltac:(M.monadic
                              (M.alloc (|
                                M.never_to_any (|
                                  M.read (|
                                    let~ _ :=
                                      M.alloc (|
                                        M.never_to_any (| M.read (| M.break (||) |) |)
                                      |) in
                                    M.alloc (| Value.Tuple [] |)
                                  |)
                                |)
                              |)))
                        ]
                      |)))
                  |) in
                let~ slice :=
                  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 "*const") [] [ Ty.path "u8" ],
                            "add",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                "as_ptr",
                                []
                              |),
                              [ M.read (| text |) ]
                            |);
                            M.read (| offset |)
                          ]
                        |);
                        BinOp.Wrap.sub (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                              "len",
                              []
                            |),
                            [ M.read (| text |) ]
                          |),
                          M.read (| offset |)
                        |)
                      ]
                    |)
                  |) in
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_function (| "core::slice::memchr::memchr_naive", [] |),
                              [ M.read (| x |); M.read (| slice |) ]
                            |)
                          |) in
                        let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::option::Option::Some",
                            0
                          |) in
                        let i := M.copy (| γ0_0 |) in
                        M.alloc (|
                          Value.StructTuple
                            "core::option::Option::Some"
                            [ BinOp.Wrap.add (| M.read (| offset |), M.read (| i |) |) ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                  ]
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_memchr_aligned :
      M.IsFunction "core::slice::memchr::memchr_aligned" memchr_aligned.
    
    (*
    pub fn memrchr(x: u8, text: &[u8]) -> Option<usize> {
        // Scan for a single byte value by reading two `usize` words at a time.
        //
        // Split `text` in three parts:
        // - unaligned tail, after the last word aligned address in text,
        // - body, scanned by 2 words at a time,
        // - the first remaining bytes, < 2 word size.
        let len = text.len();
        let ptr = text.as_ptr();
        type Chunk = usize;
    
        let (min_aligned_offset, max_aligned_offset) = {
            // We call this just to obtain the length of the prefix and suffix.
            // In the middle we always process two chunks at once.
            // SAFETY: transmuting `[u8]` to `[usize]` is safe except for size differences
            // which are handled by `align_to`.
            let (prefix, _, suffix) = unsafe { text.align_to::<(Chunk, Chunk)>() };
            (prefix.len(), len - suffix.len())
        };
    
        let mut offset = max_aligned_offset;
        if let Some(index) = text[offset..].iter().rposition(|elt| *elt == x) {
            return Some(offset + index);
        }
    
        // Search the body of the text, make sure we don't cross min_aligned_offset.
        // offset is always aligned, so just testing `>` is sufficient and avoids possible
        // overflow.
        let repeated_x = usize::repeat_u8(x);
        let chunk_bytes = mem::size_of::<Chunk>();
    
        while offset > min_aligned_offset {
            // SAFETY: offset starts at len - suffix.len(), as long as it is greater than
            // min_aligned_offset (prefix.len()) the remaining distance is at least 2 * chunk_bytes.
            unsafe {
                let u = *(ptr.add(offset - 2 * chunk_bytes) as *const Chunk);
                let v = *(ptr.add(offset - chunk_bytes) as *const Chunk);
    
                // Break if there is a matching byte.
                let zu = contains_zero_byte(u ^ repeated_x);
                let zv = contains_zero_byte(v ^ repeated_x);
                if zu || zv {
                    break;
                }
            }
            offset -= 2 * chunk_bytes;
        }
    
        // Find the byte before the point the body loop stopped.
        text[..offset].iter().rposition(|elt| *elt == x)
    }
    *)
    Definition memrchr (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ x; text ] =>
        ltac:(M.monadic
          (let x := M.alloc (| x |) in
          let text := M.alloc (| text |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ len :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                        "len",
                        []
                      |),
                      [ M.read (| text |) ]
                    |)
                  |) in
                let~ ptr :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                        "as_ptr",
                        []
                      |),
                      [ M.read (| text |) ]
                    |)
                  |) in
                M.match_operator (|
                  M.match_operator (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                          "align_to",
                          [ Ty.tuple [ Ty.path "usize"; Ty.path "usize" ] ]
                        |),
                        [ M.read (| text |) ]
                      |)
                    |),
                    [
                      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_2 := M.SubPointer.get_tuple_field (| γ, 2 |) in
                          let prefix := M.copy (| γ0_0 |) in
                          let suffix := M.copy (| γ0_2 |) in
                          M.alloc (|
                            Value.Tuple
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                    "len",
                                    []
                                  |),
                                  [ M.read (| prefix |) ]
                                |);
                                BinOp.Wrap.sub (|
                                  M.read (| len |),
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                      "len",
                                      []
                                    |),
                                    [ M.read (| suffix |) ]
                                  |)
                                |)
                              ]
                          |)))
                    ]
                  |),
                  [
                    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 min_aligned_offset := M.copy (| γ0_0 |) in
                        let max_aligned_offset := M.copy (| γ0_1 |) in
                        let~ offset := M.copy (| max_aligned_offset |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::iterator::Iterator",
                                          Ty.apply
                                            (Ty.path "core::slice::iter::Iter")
                                            []
                                            [ Ty.path "u8" ],
                                          [],
                                          "rposition",
                                          [
                                            Ty.function
                                              [
                                                Ty.tuple
                                                  [ Ty.apply (Ty.path "&") [] [ Ty.path "u8" ] ]
                                              ]
                                              (Ty.path "bool")
                                          ]
                                        |),
                                        [
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                                "iter",
                                                []
                                              |),
                                              [
                                                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 (| text |);
                                                    Value.StructRecord
                                                      "core::ops::range::RangeFrom"
                                                      [ ("start", M.read (| offset |)) ]
                                                  ]
                                                |)
                                              ]
                                            |)
                                          |);
                                          M.closure
                                            (fun γ =>
                                              ltac:(M.monadic
                                                match γ with
                                                | [ α0 ] =>
                                                  ltac:(M.monadic
                                                    (M.match_operator (|
                                                      M.alloc (| α0 |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let elt := M.copy (| γ |) in
                                                            BinOp.eq (|
                                                              M.read (| M.read (| elt |) |),
                                                              M.read (| x |)
                                                            |)))
                                                      ]
                                                    |)))
                                                | _ => M.impossible "wrong number of arguments"
                                                end))
                                        ]
                                      |)
                                    |) in
                                  let γ0_0 :=
                                    M.SubPointer.get_struct_tuple_field (|
                                      γ,
                                      "core::option::Option::Some",
                                      0
                                    |) in
                                  let index := M.copy (| γ0_0 |) in
                                  M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        M.return_ (|
                                          Value.StructTuple
                                            "core::option::Option::Some"
                                            [
                                              BinOp.Wrap.add (|
                                                M.read (| offset |),
                                                M.read (| index |)
                                              |)
                                            ]
                                        |)
                                      |)
                                    |)
                                  |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |) in
                        let~ repeated_x :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (| Ty.path "usize", "repeat_u8", [] |),
                              [ M.read (| x |) ]
                            |)
                          |) in
                        let~ chunk_bytes :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_function (| "core::mem::size_of", [ Ty.path "usize" ] |),
                              []
                            |)
                          |) in
                        let~ _ :=
                          M.loop (|
                            ltac:(M.monadic
                              (M.match_operator (|
                                M.alloc (| Value.Tuple [] |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ :=
                                        M.use
                                          (M.alloc (|
                                            BinOp.gt (|
                                              M.read (| offset |),
                                              M.read (| min_aligned_offset |)
                                            |)
                                          |)) in
                                      let _ :=
                                        M.is_constant_or_break_match (|
                                          M.read (| γ |),
                                          Value.Bool true
                                        |) in
                                      let~ _ :=
                                        let~ u :=
                                          M.copy (|
                                            M.rust_cast
                                              (M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.apply (Ty.path "*const") [] [ Ty.path "u8" ],
                                                  "add",
                                                  []
                                                |),
                                                [
                                                  M.read (| ptr |);
                                                  BinOp.Wrap.sub (|
                                                    M.read (| offset |),
                                                    BinOp.Wrap.mul (|
                                                      Value.Integer IntegerKind.Usize 2,
                                                      M.read (| chunk_bytes |)
                                                    |)
                                                  |)
                                                ]
                                              |))
                                          |) in
                                        let~ v :=
                                          M.copy (|
                                            M.rust_cast
                                              (M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.apply (Ty.path "*const") [] [ Ty.path "u8" ],
                                                  "add",
                                                  []
                                                |),
                                                [
                                                  M.read (| ptr |);
                                                  BinOp.Wrap.sub (|
                                                    M.read (| offset |),
                                                    M.read (| chunk_bytes |)
                                                  |)
                                                ]
                                              |))
                                          |) in
                                        let~ zu :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_function (|
                                                "core::slice::memchr::contains_zero_byte",
                                                []
                                              |),
                                              [
                                                BinOp.bit_xor
                                                  (M.read (| u |))
                                                  (M.read (| repeated_x |))
                                              ]
                                            |)
                                          |) in
                                        let~ zv :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_function (|
                                                "core::slice::memchr::contains_zero_byte",
                                                []
                                              |),
                                              [
                                                BinOp.bit_xor
                                                  (M.read (| v |))
                                                  (M.read (| repeated_x |))
                                              ]
                                            |)
                                          |) in
                                        M.match_operator (|
                                          M.alloc (| Value.Tuple [] |),
                                          [
                                            fun γ =>
                                              ltac:(M.monadic
                                                (let γ :=
                                                  M.use
                                                    (M.alloc (|
                                                      LogicalOp.or (|
                                                        M.read (| zu |),
                                                        ltac:(M.monadic (M.read (| zv |)))
                                                      |)
                                                    |)) in
                                                let _ :=
                                                  M.is_constant_or_break_match (|
                                                    M.read (| γ |),
                                                    Value.Bool true
                                                  |) in
                                                M.alloc (|
                                                  M.never_to_any (| M.read (| M.break (||) |) |)
                                                |)));
                                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                          ]
                                        |) in
                                      let~ _ :=
                                        let β := offset in
                                        M.write (|
                                          β,
                                          BinOp.Wrap.sub (|
                                            M.read (| β |),
                                            BinOp.Wrap.mul (|
                                              Value.Integer IntegerKind.Usize 2,
                                              M.read (| chunk_bytes |)
                                            |)
                                          |)
                                        |) in
                                      M.alloc (| Value.Tuple [] |)));
                                  fun γ =>
                                    ltac:(M.monadic
                                      (M.alloc (|
                                        M.never_to_any (|
                                          M.read (|
                                            let~ _ :=
                                              M.alloc (|
                                                M.never_to_any (| M.read (| M.break (||) |) |)
                                              |) in
                                            M.alloc (| Value.Tuple [] |)
                                          |)
                                        |)
                                      |)))
                                ]
                              |)))
                          |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::iter::traits::iterator::Iterator",
                              Ty.apply (Ty.path "core::slice::iter::Iter") [] [ Ty.path "u8" ],
                              [],
                              "rposition",
                              [
                                Ty.function
                                  [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ Ty.path "u8" ] ] ]
                                  (Ty.path "bool")
                              ]
                            |),
                            [
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                    "iter",
                                    []
                                  |),
                                  [
                                    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::RangeTo")
                                            []
                                            [ Ty.path "usize" ]
                                        ],
                                        "index",
                                        []
                                      |),
                                      [
                                        M.read (| text |);
                                        Value.StructRecord
                                          "core::ops::range::RangeTo"
                                          [ ("end_", M.read (| offset |)) ]
                                      ]
                                    |)
                                  ]
                                |)
                              |);
                              M.closure
                                (fun γ =>
                                  ltac:(M.monadic
                                    match γ with
                                    | [ α0 ] =>
                                      ltac:(M.monadic
                                        (M.match_operator (|
                                          M.alloc (| α0 |),
                                          [
                                            fun γ =>
                                              ltac:(M.monadic
                                                (let elt := M.copy (| γ |) in
                                                BinOp.eq (|
                                                  M.read (| M.read (| elt |) |),
                                                  M.read (| x |)
                                                |)))
                                          ]
                                        |)))
                                    | _ => M.impossible "wrong number of arguments"
                                    end))
                            ]
                          |)
                        |)))
                  ]
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_memrchr : M.IsFunction "core::slice::memchr::memrchr" memrchr.
    
    Module memrchr.
      Axiom Chunk : (Ty.path "core::slice::memchr::memrchr::Chunk") = (Ty.path "usize").
    End memrchr.
  End memchr.
End slice.
