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

Module str.
  Module count.
    Definition value_USIZE_SIZE : Value.t :=
      M.run
        ltac:(M.monadic
          (M.alloc (|
            M.call_closure (| M.get_function (| "core::mem::size_of", [ Ty.path "usize" ] |), [] |)
          |))).
    
    Definition value_UNROLL_INNER : Value.t :=
      M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.Usize 4 |))).
    
    (*
    pub(super) fn count_chars(s: &str) -> usize {
        if cfg!(feature = "optimize_for_size") || s.len() < USIZE_SIZE * UNROLL_INNER {
            // Avoid entering the optimized implementation for strings where the
            // difference is not likely to matter, or where it might even be slower.
            // That said, a ton of thought was not spent on the particular threshold
            // here, beyond "this value seems to make sense".
            char_count_general_case(s.as_bytes())
        } else {
            do_count_chars(s)
        }
    }
    *)
    Definition count_chars (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ s ] =>
        ltac:(M.monadic
          (let s := M.alloc (| s |) in
          M.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          LogicalOp.or (|
                            Value.Bool false,
                            ltac:(M.monadic
                              (BinOp.lt (|
                                M.call_closure (|
                                  M.get_associated_function (| Ty.path "str", "len", [] |),
                                  [ M.read (| s |) ]
                                |),
                                BinOp.Wrap.mul (|
                                  M.read (| M.get_constant (| "core::str::count::USIZE_SIZE" |) |),
                                  M.read (| M.get_constant (| "core::str::count::UNROLL_INNER" |) |)
                                |)
                              |)))
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (| "core::str::count::char_count_general_case", [] |),
                        [
                          M.call_closure (|
                            M.get_associated_function (| Ty.path "str", "as_bytes", [] |),
                            [ M.read (| s |) ]
                          |)
                        ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (M.alloc (|
                      M.call_closure (|
                        M.get_function (| "core::str::count::do_count_chars", [] |),
                        [ M.read (| s |) ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_count_chars : M.IsFunction "core::str::count::count_chars" count_chars.
    
    (*
    fn do_count_chars(s: &str) -> usize {
        // For correctness, `CHUNK_SIZE` must be:
        //
        // - Less than or equal to 255, otherwise we'll overflow bytes in `counts`.
        // - A multiple of `UNROLL_INNER`, otherwise our `break` inside the
        //   `body.chunks(CHUNK_SIZE)` loop is incorrect.
        //
        // For performance, `CHUNK_SIZE` should be:
        // - Relatively cheap to `/` against (so some simple sum of powers of two).
        // - Large enough to avoid paying for the cost of the `sum_bytes_in_usize`
        //   too often.
        const CHUNK_SIZE: usize = 192;
    
        // Check the properties of `CHUNK_SIZE` and `UNROLL_INNER` that are required
        // for correctness.
        const _: () = assert!(CHUNK_SIZE < 256);
        const _: () = assert!(CHUNK_SIZE % UNROLL_INNER == 0);
    
        // SAFETY: transmuting `[u8]` to `[usize]` is safe except for size
        // differences which are handled by `align_to`.
        let (head, body, tail) = unsafe { s.as_bytes().align_to::<usize>() };
    
        // This should be quite rare, and basically exists to handle the degenerate
        // cases where align_to fails (as well as miri under symbolic alignment
        // mode).
        //
        // The `unlikely` helps discourage LLVM from inlining the body, which is
        // nice, as we would rather not mark the `char_count_general_case` function
        // as cold.
        if unlikely(body.is_empty() || head.len() > USIZE_SIZE || tail.len() > USIZE_SIZE) {
            return char_count_general_case(s.as_bytes());
        }
    
        let mut total = char_count_general_case(head) + char_count_general_case(tail);
        // Split `body` into `CHUNK_SIZE` chunks to reduce the frequency with which
        // we call `sum_bytes_in_usize`.
        for chunk in body.chunks(CHUNK_SIZE) {
            // We accumulate intermediate sums in `counts`, where each byte contains
            // a subset of the sum of this chunk, like a `[u8; size_of::<usize>()]`.
            let mut counts = 0;
    
            let (unrolled_chunks, remainder) = chunk.as_chunks::<UNROLL_INNER>();
            for unrolled in unrolled_chunks {
                for &word in unrolled {
                    // Because `CHUNK_SIZE` is < 256, this addition can't cause the
                    // count in any of the bytes to overflow into a subsequent byte.
                    counts += contains_non_continuation_byte(word);
                }
            }
    
            // Sum the values in `counts` (which, again, is conceptually a `[u8;
            // size_of::<usize>()]`), and accumulate the result into `total`.
            total += sum_bytes_in_usize(counts);
    
            // If there's any data in `remainder`, then handle it. This will only
            // happen for the last `chunk` in `body.chunks()` (because `CHUNK_SIZE`
            // is divisible by `UNROLL_INNER`), so we explicitly break at the end
            // (which seems to help LLVM out).
            if !remainder.is_empty() {
                // Accumulate all the data in the remainder.
                let mut counts = 0;
                for &word in remainder {
                    counts += contains_non_continuation_byte(word);
                }
                total += sum_bytes_in_usize(counts);
                break;
            }
        }
        total
    }
    *)
    Definition do_count_chars (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ s ] =>
        ltac:(M.monadic
          (let s := M.alloc (| s |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                        "align_to",
                        [ Ty.path "usize" ]
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (| Ty.path "str", "as_bytes", [] |),
                          [ M.read (| s |) ]
                        |)
                      ]
                    |)
                  |),
                  [
                    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 head := M.copy (| γ0_0 |) in
                        let body := M.copy (| γ0_1 |) in
                        let tail := M.copy (| γ0_2 |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        M.call_closure (|
                                          M.get_function (| "core::intrinsics::unlikely", [] |),
                                          [
                                            LogicalOp.or (|
                                              LogicalOp.or (|
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply
                                                      (Ty.path "slice")
                                                      []
                                                      [ Ty.path "usize" ],
                                                    "is_empty",
                                                    []
                                                  |),
                                                  [ M.read (| body |) ]
                                                |),
                                                ltac:(M.monadic
                                                  (BinOp.gt (|
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.apply
                                                          (Ty.path "slice")
                                                          []
                                                          [ Ty.path "u8" ],
                                                        "len",
                                                        []
                                                      |),
                                                      [ M.read (| head |) ]
                                                    |),
                                                    M.read (|
                                                      M.get_constant (|
                                                        "core::str::count::USIZE_SIZE"
                                                      |)
                                                    |)
                                                  |)))
                                              |),
                                              ltac:(M.monadic
                                                (BinOp.gt (|
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.apply
                                                        (Ty.path "slice")
                                                        []
                                                        [ Ty.path "u8" ],
                                                      "len",
                                                      []
                                                    |),
                                                    [ M.read (| tail |) ]
                                                  |),
                                                  M.read (|
                                                    M.get_constant (|
                                                      "core::str::count::USIZE_SIZE"
                                                    |)
                                                  |)
                                                |)))
                                            |)
                                          ]
                                        |)
                                      |)) 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::str::count::char_count_general_case",
                                              []
                                            |),
                                            [
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path "str",
                                                  "as_bytes",
                                                  []
                                                |),
                                                [ M.read (| s |) ]
                                              |)
                                            ]
                                          |)
                                        |)
                                      |)
                                    |)
                                  |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |) in
                        let~ total :=
                          M.alloc (|
                            BinOp.Wrap.add (|
                              M.call_closure (|
                                M.get_function (|
                                  "core::str::count::char_count_general_case",
                                  []
                                |),
                                [ M.read (| head |) ]
                              |),
                              M.call_closure (|
                                M.get_function (|
                                  "core::str::count::char_count_general_case",
                                  []
                                |),
                                [ M.read (| tail |) ]
                              |)
                            |)
                          |) in
                        let~ _ :=
                          M.use
                            (M.match_operator (|
                              M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::iter::traits::collect::IntoIterator",
                                    Ty.apply
                                      (Ty.path "core::slice::iter::Chunks")
                                      []
                                      [ Ty.path "usize" ],
                                    [],
                                    "into_iter",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply (Ty.path "slice") [] [ Ty.path "usize" ],
                                        "chunks",
                                        []
                                      |),
                                      [
                                        M.read (| body |);
                                        M.read (|
                                          M.get_constant (|
                                            "core::str::count::do_count_chars::CHUNK_SIZE"
                                          |)
                                        |)
                                      ]
                                    |)
                                  ]
                                |)
                              |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let iter := M.copy (| γ |) in
                                    M.loop (|
                                      ltac:(M.monadic
                                        (let~ _ :=
                                          M.match_operator (|
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::iter::traits::iterator::Iterator",
                                                  Ty.apply
                                                    (Ty.path "core::slice::iter::Chunks")
                                                    []
                                                    [ Ty.path "usize" ],
                                                  [],
                                                  "next",
                                                  []
                                                |),
                                                [ iter ]
                                              |)
                                            |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let _ :=
                                                    M.is_struct_tuple (|
                                                      γ,
                                                      "core::option::Option::None"
                                                    |) in
                                                  M.alloc (|
                                                    M.never_to_any (| M.read (| M.break (||) |) |)
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ0_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "core::option::Option::Some",
                                                      0
                                                    |) in
                                                  let chunk := M.copy (| γ0_0 |) in
                                                  let~ counts :=
                                                    M.alloc (|
                                                      Value.Integer IntegerKind.Usize 0
                                                    |) in
                                                  M.match_operator (|
                                                    M.alloc (|
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.apply
                                                            (Ty.path "slice")
                                                            []
                                                            [ Ty.path "usize" ],
                                                          "as_chunks",
                                                          []
                                                        |),
                                                        [ M.read (| chunk |) ]
                                                      |)
                                                    |),
                                                    [
                                                      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 unrolled_chunks :=
                                                            M.copy (| γ0_0 |) in
                                                          let remainder := M.copy (| γ0_1 |) in
                                                          let~ _ :=
                                                            M.use
                                                              (M.match_operator (|
                                                                M.alloc (|
                                                                  M.call_closure (|
                                                                    M.get_trait_method (|
                                                                      "core::iter::traits::collect::IntoIterator",
                                                                      Ty.apply
                                                                        (Ty.path "&")
                                                                        []
                                                                        [
                                                                          Ty.apply
                                                                            (Ty.path "slice")
                                                                            []
                                                                            [
                                                                              Ty.apply
                                                                                (Ty.path "array")
                                                                                [
                                                                                  Value.Integer
                                                                                    IntegerKind.Usize
                                                                                    4
                                                                                ]
                                                                                [ Ty.path "usize" ]
                                                                            ]
                                                                        ],
                                                                      [],
                                                                      "into_iter",
                                                                      []
                                                                    |),
                                                                    [ M.read (| unrolled_chunks |) ]
                                                                  |)
                                                                |),
                                                                [
                                                                  fun γ =>
                                                                    ltac:(M.monadic
                                                                      (let iter := M.copy (| γ |) in
                                                                      M.loop (|
                                                                        ltac:(M.monadic
                                                                          (let~ _ :=
                                                                            M.match_operator (|
                                                                              M.alloc (|
                                                                                M.call_closure (|
                                                                                  M.get_trait_method (|
                                                                                    "core::iter::traits::iterator::Iterator",
                                                                                    Ty.apply
                                                                                      (Ty.path
                                                                                        "core::slice::iter::Iter")
                                                                                      []
                                                                                      [
                                                                                        Ty.apply
                                                                                          (Ty.path
                                                                                            "array")
                                                                                          [
                                                                                            Value.Integer
                                                                                              IntegerKind.Usize
                                                                                              4
                                                                                          ]
                                                                                          [
                                                                                            Ty.path
                                                                                              "usize"
                                                                                          ]
                                                                                      ],
                                                                                    [],
                                                                                    "next",
                                                                                    []
                                                                                  |),
                                                                                  [ iter ]
                                                                                |)
                                                                              |),
                                                                              [
                                                                                fun γ =>
                                                                                  ltac:(M.monadic
                                                                                    (let _ :=
                                                                                      M.is_struct_tuple (|
                                                                                        γ,
                                                                                        "core::option::Option::None"
                                                                                      |) in
                                                                                    M.alloc (|
                                                                                      M.never_to_any (|
                                                                                        M.read (|
                                                                                          M.break (||)
                                                                                        |)
                                                                                      |)
                                                                                    |)));
                                                                                fun γ =>
                                                                                  ltac:(M.monadic
                                                                                    (let γ0_0 :=
                                                                                      M.SubPointer.get_struct_tuple_field (|
                                                                                        γ,
                                                                                        "core::option::Option::Some",
                                                                                        0
                                                                                      |) in
                                                                                    let unrolled :=
                                                                                      M.copy (|
                                                                                        γ0_0
                                                                                      |) in
                                                                                    M.use
                                                                                      (M.match_operator (|
                                                                                        M.alloc (|
                                                                                          M.call_closure (|
                                                                                            M.get_trait_method (|
                                                                                              "core::iter::traits::collect::IntoIterator",
                                                                                              Ty.apply
                                                                                                (Ty.path
                                                                                                  "&")
                                                                                                []
                                                                                                [
                                                                                                  Ty.apply
                                                                                                    (Ty.path
                                                                                                      "array")
                                                                                                    [
                                                                                                      Value.Integer
                                                                                                        IntegerKind.Usize
                                                                                                        4
                                                                                                    ]
                                                                                                    [
                                                                                                      Ty.path
                                                                                                        "usize"
                                                                                                    ]
                                                                                                ],
                                                                                              [],
                                                                                              "into_iter",
                                                                                              []
                                                                                            |),
                                                                                            [
                                                                                              M.read (|
                                                                                                unrolled
                                                                                              |)
                                                                                            ]
                                                                                          |)
                                                                                        |),
                                                                                        [
                                                                                          fun γ =>
                                                                                            ltac:(M.monadic
                                                                                              (let
                                                                                                    iter :=
                                                                                                M.copy (|
                                                                                                  γ
                                                                                                |) in
                                                                                              M.loop (|
                                                                                                ltac:(M.monadic
                                                                                                  (let~
                                                                                                        _ :=
                                                                                                    M.match_operator (|
                                                                                                      M.alloc (|
                                                                                                        M.call_closure (|
                                                                                                          M.get_trait_method (|
                                                                                                            "core::iter::traits::iterator::Iterator",
                                                                                                            Ty.apply
                                                                                                              (Ty.path
                                                                                                                "core::slice::iter::Iter")
                                                                                                              []
                                                                                                              [
                                                                                                                Ty.path
                                                                                                                  "usize"
                                                                                                              ],
                                                                                                            [],
                                                                                                            "next",
                                                                                                            []
                                                                                                          |),
                                                                                                          [
                                                                                                            iter
                                                                                                          ]
                                                                                                        |)
                                                                                                      |),
                                                                                                      [
                                                                                                        fun
                                                                                                            γ =>
                                                                                                          ltac:(M.monadic
                                                                                                            (let
                                                                                                                  _ :=
                                                                                                              M.is_struct_tuple (|
                                                                                                                γ,
                                                                                                                "core::option::Option::None"
                                                                                                              |) in
                                                                                                            M.alloc (|
                                                                                                              M.never_to_any (|
                                                                                                                M.read (|
                                                                                                                  M.break (||)
                                                                                                                |)
                                                                                                              |)
                                                                                                            |)));
                                                                                                        fun
                                                                                                            γ =>
                                                                                                          ltac:(M.monadic
                                                                                                            (let
                                                                                                                  γ0_0 :=
                                                                                                              M.SubPointer.get_struct_tuple_field (|
                                                                                                                γ,
                                                                                                                "core::option::Option::Some",
                                                                                                                0
                                                                                                              |) in
                                                                                                            let
                                                                                                                  γ0_0 :=
                                                                                                              M.read (|
                                                                                                                γ0_0
                                                                                                              |) in
                                                                                                            let
                                                                                                                  word :=
                                                                                                              M.copy (|
                                                                                                                γ0_0
                                                                                                              |) in
                                                                                                            let~
                                                                                                                  _ :=
                                                                                                              let
                                                                                                                    β :=
                                                                                                                counts in
                                                                                                              M.write (|
                                                                                                                β,
                                                                                                                BinOp.Wrap.add (|
                                                                                                                  M.read (|
                                                                                                                    β
                                                                                                                  |),
                                                                                                                  M.call_closure (|
                                                                                                                    M.get_function (|
                                                                                                                      "core::str::count::contains_non_continuation_byte",
                                                                                                                      []
                                                                                                                    |),
                                                                                                                    [
                                                                                                                      M.read (|
                                                                                                                        word
                                                                                                                      |)
                                                                                                                    ]
                                                                                                                  |)
                                                                                                                |)
                                                                                                              |) in
                                                                                                            M.alloc (|
                                                                                                              Value.Tuple
                                                                                                                []
                                                                                                            |)))
                                                                                                      ]
                                                                                                    |) in
                                                                                                  M.alloc (|
                                                                                                    Value.Tuple
                                                                                                      []
                                                                                                  |)))
                                                                                              |)))
                                                                                        ]
                                                                                      |))))
                                                                              ]
                                                                            |) in
                                                                          M.alloc (|
                                                                            Value.Tuple []
                                                                          |)))
                                                                      |)))
                                                                ]
                                                              |)) in
                                                          let~ _ :=
                                                            let β := total in
                                                            M.write (|
                                                              β,
                                                              BinOp.Wrap.add (|
                                                                M.read (| β |),
                                                                M.call_closure (|
                                                                  M.get_function (|
                                                                    "core::str::count::sum_bytes_in_usize",
                                                                    []
                                                                  |),
                                                                  [ M.read (| counts |) ]
                                                                |)
                                                              |)
                                                            |) in
                                                          M.match_operator (|
                                                            M.alloc (| Value.Tuple [] |),
                                                            [
                                                              fun γ =>
                                                                ltac:(M.monadic
                                                                  (let γ :=
                                                                    M.use
                                                                      (M.alloc (|
                                                                        UnOp.not (|
                                                                          M.call_closure (|
                                                                            M.get_associated_function (|
                                                                              Ty.apply
                                                                                (Ty.path "slice")
                                                                                []
                                                                                [ Ty.path "usize" ],
                                                                              "is_empty",
                                                                              []
                                                                            |),
                                                                            [ M.read (| remainder |)
                                                                            ]
                                                                          |)
                                                                        |)
                                                                      |)) in
                                                                  let _ :=
                                                                    M.is_constant_or_break_match (|
                                                                      M.read (| γ |),
                                                                      Value.Bool true
                                                                    |) in
                                                                  M.alloc (|
                                                                    M.never_to_any (|
                                                                      M.read (|
                                                                        let~ counts :=
                                                                          M.alloc (|
                                                                            Value.Integer
                                                                              IntegerKind.Usize
                                                                              0
                                                                          |) in
                                                                        let~ _ :=
                                                                          M.use
                                                                            (M.match_operator (|
                                                                              M.alloc (|
                                                                                M.call_closure (|
                                                                                  M.get_trait_method (|
                                                                                    "core::iter::traits::collect::IntoIterator",
                                                                                    Ty.apply
                                                                                      (Ty.path "&")
                                                                                      []
                                                                                      [
                                                                                        Ty.apply
                                                                                          (Ty.path
                                                                                            "slice")
                                                                                          []
                                                                                          [
                                                                                            Ty.path
                                                                                              "usize"
                                                                                          ]
                                                                                      ],
                                                                                    [],
                                                                                    "into_iter",
                                                                                    []
                                                                                  |),
                                                                                  [
                                                                                    M.read (|
                                                                                      remainder
                                                                                    |)
                                                                                  ]
                                                                                |)
                                                                              |),
                                                                              [
                                                                                fun γ =>
                                                                                  ltac:(M.monadic
                                                                                    (let iter :=
                                                                                      M.copy (|
                                                                                        γ
                                                                                      |) in
                                                                                    M.loop (|
                                                                                      ltac:(M.monadic
                                                                                        (let~ _ :=
                                                                                          M.match_operator (|
                                                                                            M.alloc (|
                                                                                              M.call_closure (|
                                                                                                M.get_trait_method (|
                                                                                                  "core::iter::traits::iterator::Iterator",
                                                                                                  Ty.apply
                                                                                                    (Ty.path
                                                                                                      "core::slice::iter::Iter")
                                                                                                    []
                                                                                                    [
                                                                                                      Ty.path
                                                                                                        "usize"
                                                                                                    ],
                                                                                                  [],
                                                                                                  "next",
                                                                                                  []
                                                                                                |),
                                                                                                [
                                                                                                  iter
                                                                                                ]
                                                                                              |)
                                                                                            |),
                                                                                            [
                                                                                              fun
                                                                                                  γ =>
                                                                                                ltac:(M.monadic
                                                                                                  (let
                                                                                                        _ :=
                                                                                                    M.is_struct_tuple (|
                                                                                                      γ,
                                                                                                      "core::option::Option::None"
                                                                                                    |) in
                                                                                                  M.alloc (|
                                                                                                    M.never_to_any (|
                                                                                                      M.read (|
                                                                                                        M.break (||)
                                                                                                      |)
                                                                                                    |)
                                                                                                  |)));
                                                                                              fun
                                                                                                  γ =>
                                                                                                ltac:(M.monadic
                                                                                                  (let
                                                                                                        γ0_0 :=
                                                                                                    M.SubPointer.get_struct_tuple_field (|
                                                                                                      γ,
                                                                                                      "core::option::Option::Some",
                                                                                                      0
                                                                                                    |) in
                                                                                                  let
                                                                                                        γ0_0 :=
                                                                                                    M.read (|
                                                                                                      γ0_0
                                                                                                    |) in
                                                                                                  let
                                                                                                        word :=
                                                                                                    M.copy (|
                                                                                                      γ0_0
                                                                                                    |) in
                                                                                                  let~
                                                                                                        _ :=
                                                                                                    let
                                                                                                          β :=
                                                                                                      counts in
                                                                                                    M.write (|
                                                                                                      β,
                                                                                                      BinOp.Wrap.add (|
                                                                                                        M.read (|
                                                                                                          β
                                                                                                        |),
                                                                                                        M.call_closure (|
                                                                                                          M.get_function (|
                                                                                                            "core::str::count::contains_non_continuation_byte",
                                                                                                            []
                                                                                                          |),
                                                                                                          [
                                                                                                            M.read (|
                                                                                                              word
                                                                                                            |)
                                                                                                          ]
                                                                                                        |)
                                                                                                      |)
                                                                                                    |) in
                                                                                                  M.alloc (|
                                                                                                    Value.Tuple
                                                                                                      []
                                                                                                  |)))
                                                                                            ]
                                                                                          |) in
                                                                                        M.alloc (|
                                                                                          Value.Tuple
                                                                                            []
                                                                                        |)))
                                                                                    |)))
                                                                              ]
                                                                            |)) in
                                                                        let~ _ :=
                                                                          let β := total in
                                                                          M.write (|
                                                                            β,
                                                                            BinOp.Wrap.add (|
                                                                              M.read (| β |),
                                                                              M.call_closure (|
                                                                                M.get_function (|
                                                                                  "core::str::count::sum_bytes_in_usize",
                                                                                  []
                                                                                |),
                                                                                [
                                                                                  M.read (|
                                                                                    counts
                                                                                  |)
                                                                                ]
                                                                              |)
                                                                            |)
                                                                          |) in
                                                                        M.break (||)
                                                                      |)
                                                                    |)
                                                                  |)));
                                                              fun γ =>
                                                                ltac:(M.monadic
                                                                  (M.alloc (| Value.Tuple [] |)))
                                                            ]
                                                          |)))
                                                    ]
                                                  |)))
                                            ]
                                          |) in
                                        M.alloc (| Value.Tuple [] |)))
                                    |)))
                              ]
                            |)) in
                        total))
                  ]
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_do_count_chars : M.IsFunction "core::str::count::do_count_chars" do_count_chars.
    
    Module do_count_chars.
      Definition value_CHUNK_SIZE : Value.t :=
        M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.Usize 192 |))).
    End do_count_chars.
    
    (*
    fn contains_non_continuation_byte(w: usize) -> usize {
        const LSB: usize = usize::repeat_u8(0x01);
        ((!w >> 7) | (w >> 6)) & LSB
    }
    *)
    Definition contains_non_continuation_byte
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ w ] =>
        ltac:(M.monadic
          (let w := M.alloc (| w |) in
          BinOp.bit_and
            (BinOp.bit_or
              (BinOp.Wrap.shr (| UnOp.not (| M.read (| w |) |), Value.Integer IntegerKind.I32 7 |))
              (BinOp.Wrap.shr (| M.read (| w |), Value.Integer IntegerKind.I32 6 |)))
            (M.read (|
              M.get_constant (| "core::str::count::contains_non_continuation_byte::LSB" |)
            |))))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_contains_non_continuation_byte :
      M.IsFunction
        "core::str::count::contains_non_continuation_byte"
        contains_non_continuation_byte.
    
    Module contains_non_continuation_byte.
      Definition value_LSB : 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 ]
              |)
            |))).
    End contains_non_continuation_byte.
    
    (*
    fn sum_bytes_in_usize(values: usize) -> usize {
        const LSB_SHORTS: usize = usize::repeat_u16(0x0001);
        const SKIP_BYTES: usize = usize::repeat_u16(0x00ff);
    
        let pair_sum: usize = (values & SKIP_BYTES) + ((values >> 8) & SKIP_BYTES);
        pair_sum.wrapping_mul(LSB_SHORTS) >> ((USIZE_SIZE - 2) * 8)
    }
    *)
    Definition sum_bytes_in_usize (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ values ] =>
        ltac:(M.monadic
          (let values := M.alloc (| values |) in
          M.read (|
            let~ pair_sum :=
              M.alloc (|
                BinOp.Wrap.add (|
                  BinOp.bit_and
                    (M.read (| values |))
                    (M.read (|
                      M.get_constant (| "core::str::count::sum_bytes_in_usize::SKIP_BYTES" |)
                    |)),
                  BinOp.bit_and
                    (BinOp.Wrap.shr (| M.read (| values |), Value.Integer IntegerKind.I32 8 |))
                    (M.read (|
                      M.get_constant (| "core::str::count::sum_bytes_in_usize::SKIP_BYTES" |)
                    |))
                |)
              |) in
            M.alloc (|
              BinOp.Wrap.shr (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "usize", "wrapping_mul", [] |),
                  [
                    M.read (| pair_sum |);
                    M.read (|
                      M.get_constant (| "core::str::count::sum_bytes_in_usize::LSB_SHORTS" |)
                    |)
                  ]
                |),
                BinOp.Wrap.mul (|
                  BinOp.Wrap.sub (|
                    M.read (| M.get_constant (| "core::str::count::USIZE_SIZE" |) |),
                    Value.Integer IntegerKind.Usize 2
                  |),
                  Value.Integer IntegerKind.Usize 8
                |)
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_sum_bytes_in_usize :
      M.IsFunction "core::str::count::sum_bytes_in_usize" sum_bytes_in_usize.
    
    Module sum_bytes_in_usize.
      Definition value_LSB_SHORTS : Value.t :=
        M.run
          ltac:(M.monadic
            (M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "usize", "repeat_u16", [] |),
                [ Value.Integer IntegerKind.U16 1 ]
              |)
            |))).
      
      Definition value_SKIP_BYTES : Value.t :=
        M.run
          ltac:(M.monadic
            (M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "usize", "repeat_u16", [] |),
                [ Value.Integer IntegerKind.U16 255 ]
              |)
            |))).
    End sum_bytes_in_usize.
    
    (*
    fn char_count_general_case(s: &[u8]) -> usize {
        s.iter().filter(|&&byte| !super::validations::utf8_is_cont_byte(byte)).count()
    }
    *)
    Definition char_count_general_case (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ s ] =>
        ltac:(M.monadic
          (let s := M.alloc (| s |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::iter::traits::iterator::Iterator",
              Ty.apply
                (Ty.path "core::iter::adapters::filter::Filter")
                []
                [
                  Ty.apply (Ty.path "core::slice::iter::Iter") [] [ Ty.path "u8" ];
                  Ty.function
                    [
                      Ty.tuple
                        [ Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "&") [] [ Ty.path "u8" ] ] ]
                    ]
                    (Ty.path "bool")
                ],
              [],
              "count",
              []
            |),
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::iterator::Iterator",
                  Ty.apply (Ty.path "core::slice::iter::Iter") [] [ Ty.path "u8" ],
                  [],
                  "filter",
                  [
                    Ty.function
                      [
                        Ty.tuple
                          [ Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "&") [] [ Ty.path "u8" ] ]
                          ]
                      ]
                      (Ty.path "bool")
                  ]
                |),
                [
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                      "iter",
                      []
                    |),
                    [ M.read (| s |) ]
                  |);
                  M.closure
                    (fun γ =>
                      ltac:(M.monadic
                        match γ with
                        | [ α0 ] =>
                          ltac:(M.monadic
                            (M.match_operator (|
                              M.alloc (| α0 |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ := M.read (| γ |) in
                                    let γ := M.read (| γ |) in
                                    let byte := M.copy (| γ |) in
                                    UnOp.not (|
                                      M.call_closure (|
                                        M.get_function (|
                                          "core::str::validations::utf8_is_cont_byte",
                                          []
                                        |),
                                        [ M.read (| byte |) ]
                                      |)
                                    |)))
                              ]
                            |)))
                        | _ => M.impossible "wrong number of arguments"
                        end))
                ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_char_count_general_case :
      M.IsFunction "core::str::count::char_count_general_case" char_count_general_case.
  End count.
End str.
