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

Module slice.
  Module ascii.
    Module Impl_slice_u8.
      Definition Self : Ty.t := Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ].
      
      (*
          pub const fn is_ascii(&self) -> bool {
              is_ascii(self)
          }
      *)
      Definition is_ascii (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_function (| "core::slice::ascii::is_ascii", [] |),
              [ M.read (| self |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_is_ascii : M.IsAssociatedFunction Self "is_ascii" is_ascii.
      
      (*
          pub const fn as_ascii(&self) -> Option<&[ascii::Char]> {
              if self.is_ascii() {
                  // SAFETY: Just checked that it's ASCII
                  Some(unsafe { self.as_ascii_unchecked() })
              } else {
                  None
              }
          }
      *)
      Definition as_ascii (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                "is_ascii",
                                []
                              |),
                              [ M.read (| self |) ]
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                "as_ascii_unchecked",
                                []
                              |),
                              [ M.read (| self |) ]
                            |)
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_as_ascii : M.IsAssociatedFunction Self "as_ascii" as_ascii.
      
      (*
          pub const unsafe fn as_ascii_unchecked(&self) -> &[ascii::Char] {
              let byte_ptr: *const [u8] = self;
              let ascii_ptr = byte_ptr as *const [ascii::Char];
              // SAFETY: The caller promised all the bytes are ASCII
              unsafe { &*ascii_ptr }
          }
      *)
      Definition as_ascii_unchecked (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              let~ byte_ptr := M.alloc (| M.read (| self |) |) in
              let~ ascii_ptr := M.alloc (| M.rust_cast (M.read (| byte_ptr |)) |) in
              M.alloc (| M.read (| ascii_ptr |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_as_ascii_unchecked :
        M.IsAssociatedFunction Self "as_ascii_unchecked" as_ascii_unchecked.
      
      (*
          pub fn eq_ignore_ascii_case(&self, other: &[u8]) -> bool {
              self.len() == other.len() && iter::zip(self, other).all(|(a, b)| a.eq_ignore_ascii_case(b))
          }
      *)
      Definition eq_ignore_ascii_case (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            LogicalOp.and (|
              BinOp.eq (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                    "len",
                    []
                  |),
                  [ M.read (| self |) ]
                |),
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                    "len",
                    []
                  |),
                  [ M.read (| other |) ]
                |)
              |),
              ltac:(M.monadic
                (M.call_closure (|
                  M.get_trait_method (|
                    "core::iter::traits::iterator::Iterator",
                    Ty.apply
                      (Ty.path "core::iter::adapters::zip::Zip")
                      []
                      [
                        Ty.apply (Ty.path "core::slice::iter::Iter") [] [ Ty.path "u8" ];
                        Ty.apply (Ty.path "core::slice::iter::Iter") [] [ Ty.path "u8" ]
                      ],
                    [],
                    "all",
                    [
                      Ty.function
                        [
                          Ty.tuple
                            [
                              Ty.tuple
                                [
                                  Ty.apply (Ty.path "&") [] [ Ty.path "u8" ];
                                  Ty.apply (Ty.path "&") [] [ Ty.path "u8" ]
                                ]
                            ]
                        ]
                        (Ty.path "bool")
                    ]
                  |),
                  [
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (|
                          "core::iter::adapters::zip::zip",
                          [
                            Ty.apply
                              (Ty.path "&")
                              []
                              [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ];
                            Ty.apply
                              (Ty.path "&")
                              []
                              [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ]
                          ]
                        |),
                        [ M.read (| self |); M.read (| other |) ]
                      |)
                    |);
                    M.closure
                      (fun γ =>
                        ltac:(M.monadic
                          match γ with
                          | [ α0 ] =>
                            ltac:(M.monadic
                              (M.match_operator (|
                                M.alloc (| α0 |),
                                [
                                  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 a := M.copy (| γ0_0 |) in
                                      let b := M.copy (| γ0_1 |) in
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "u8",
                                          "eq_ignore_ascii_case",
                                          []
                                        |),
                                        [ M.read (| a |); M.read (| b |) ]
                                      |)))
                                ]
                              |)))
                          | _ => M.impossible "wrong number of arguments"
                          end))
                  ]
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_eq_ignore_ascii_case :
        M.IsAssociatedFunction Self "eq_ignore_ascii_case" eq_ignore_ascii_case.
      
      (*
          pub const fn make_ascii_uppercase(&mut self) {
              // FIXME(const-hack): We would like to simply iterate using `for` loops but this isn't currently allowed in constant expressions.
              let mut i = 0;
              while i < self.len() {
                  let byte = &mut self[i];
                  byte.make_ascii_uppercase();
                  i += 1;
              }
          }
      *)
      Definition make_ascii_uppercase (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              let~ i := M.alloc (| Value.Integer IntegerKind.Usize 0 |) in
              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 (| self |) ]
                                  |)
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          let~ byte :=
                            M.alloc (| M.SubPointer.get_array_field (| M.read (| self |), i |) |) in
                          let~ _ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "u8",
                                  "make_ascii_uppercase",
                                  []
                                |),
                                [ M.read (| byte |) ]
                              |)
                            |) 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 [] |)
                              |)
                            |)
                          |)))
                    ]
                  |)))
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_make_ascii_uppercase :
        M.IsAssociatedFunction Self "make_ascii_uppercase" make_ascii_uppercase.
      
      (*
          pub const fn make_ascii_lowercase(&mut self) {
              // FIXME(const-hack): We would like to simply iterate using `for` loops but this isn't currently allowed in constant expressions.
              let mut i = 0;
              while i < self.len() {
                  let byte = &mut self[i];
                  byte.make_ascii_lowercase();
                  i += 1;
              }
          }
      *)
      Definition make_ascii_lowercase (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              let~ i := M.alloc (| Value.Integer IntegerKind.Usize 0 |) in
              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 (| self |) ]
                                  |)
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          let~ byte :=
                            M.alloc (| M.SubPointer.get_array_field (| M.read (| self |), i |) |) in
                          let~ _ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "u8",
                                  "make_ascii_lowercase",
                                  []
                                |),
                                [ M.read (| byte |) ]
                              |)
                            |) 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 [] |)
                              |)
                            |)
                          |)))
                    ]
                  |)))
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_make_ascii_lowercase :
        M.IsAssociatedFunction Self "make_ascii_lowercase" make_ascii_lowercase.
      
      (*
          pub fn escape_ascii(&self) -> EscapeAscii<'_> {
              EscapeAscii { inner: self.iter().flat_map(EscapeByte) }
          }
      *)
      Definition escape_ascii (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            Value.StructRecord
              "core::slice::ascii::EscapeAscii"
              [
                ("inner",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::iterator::Iterator",
                      Ty.apply (Ty.path "core::slice::iter::Iter") [] [ Ty.path "u8" ],
                      [],
                      "flat_map",
                      [
                        Ty.path "core::ascii::EscapeDefault";
                        Ty.path "core::slice::ascii::EscapeByte"
                      ]
                    |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                          "iter",
                          []
                        |),
                        [ M.read (| self |) ]
                      |);
                      Value.StructTuple "core::slice::ascii::EscapeByte" []
                    ]
                  |))
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_escape_ascii :
        M.IsAssociatedFunction Self "escape_ascii" escape_ascii.
      
      (*
          pub const fn trim_ascii_start(&self) -> &[u8] {
              let mut bytes = self;
              // Note: A pattern matching based approach (instead of indexing) allows
              // making the function const.
              while let [first, rest @ ..] = bytes {
                  if first.is_ascii_whitespace() {
                      bytes = rest;
                  } else {
                      break;
                  }
              }
              bytes
          }
      *)
      Definition trim_ascii_start (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              let~ bytes := M.copy (| self |) in
              let~ _ :=
                M.loop (|
                  ltac:(M.monadic
                    (M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := bytes in
                            let γ := M.read (| γ |) in
                            let γ1_0 := M.SubPointer.get_slice_index (| γ, 0 |) in
                            let γ1_rest := M.SubPointer.get_slice_rest (| γ, 1, 0 |) in
                            let first := M.alloc (| γ1_0 |) in
                            let rest := M.alloc (| γ1_rest |) in
                            M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "u8",
                                              "is_ascii_whitespace",
                                              []
                                            |),
                                            [ M.read (| first |) ]
                                          |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    let~ _ := M.write (| bytes, M.read (| rest |) |) in
                                    M.alloc (| Value.Tuple [] |)));
                                fun γ =>
                                  ltac:(M.monadic
                                    (M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |)))
                              ]
                            |)));
                        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.read (| bytes |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_trim_ascii_start :
        M.IsAssociatedFunction Self "trim_ascii_start" trim_ascii_start.
      
      (*
          pub const fn trim_ascii_end(&self) -> &[u8] {
              let mut bytes = self;
              // Note: A pattern matching based approach (instead of indexing) allows
              // making the function const.
              while let [rest @ .., last] = bytes {
                  if last.is_ascii_whitespace() {
                      bytes = rest;
                  } else {
                      break;
                  }
              }
              bytes
          }
      *)
      Definition trim_ascii_end (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              let~ bytes := M.copy (| self |) in
              let~ _ :=
                M.loop (|
                  ltac:(M.monadic
                    (M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := bytes in
                            let γ := M.read (| γ |) in
                            let γ1_rest := M.SubPointer.get_slice_rest (| γ, 0, 1 |) in
                            let γ1_rev0 := M.SubPointer.get_slice_rev_index (| γ, 0 |) in
                            let rest := M.alloc (| γ1_rest |) in
                            let last := M.alloc (| γ1_rev0 |) in
                            M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "u8",
                                              "is_ascii_whitespace",
                                              []
                                            |),
                                            [ M.read (| last |) ]
                                          |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    let~ _ := M.write (| bytes, M.read (| rest |) |) in
                                    M.alloc (| Value.Tuple [] |)));
                                fun γ =>
                                  ltac:(M.monadic
                                    (M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |)))
                              ]
                            |)));
                        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.read (| bytes |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_trim_ascii_end :
        M.IsAssociatedFunction Self "trim_ascii_end" trim_ascii_end.
      
      (*
          pub const fn trim_ascii(&self) -> &[u8] {
              self.trim_ascii_start().trim_ascii_end()
          }
      *)
      Definition trim_ascii (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                "trim_ascii_end",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                    "trim_ascii_start",
                    []
                  |),
                  [ M.read (| self |) ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_trim_ascii : M.IsAssociatedFunction Self "trim_ascii" trim_ascii.
    End Impl_slice_u8.
    
    Module Impl_core_clone_Clone_for_core_slice_ascii_EscapeByte.
      Definition Self : Ty.t := Ty.path "core::slice::ascii::EscapeByte".
      
      (*     Clone *)
      Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            Value.StructTuple "core::slice::ascii::EscapeByte" []))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::clone::Clone"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("clone", InstanceField.Method clone) ].
    End Impl_core_clone_Clone_for_core_slice_ascii_EscapeByte.
    
    (* StructRecord
      {
        name := "EscapeAscii";
        const_params := [];
        ty_params := [];
        fields :=
          [
            ("inner",
              Ty.apply
                (Ty.path "core::iter::adapters::flatten::FlatMap")
                []
                [
                  Ty.apply (Ty.path "core::slice::iter::Iter") [] [ Ty.path "u8" ];
                  Ty.path "core::ascii::EscapeDefault";
                  Ty.path "core::slice::ascii::EscapeByte"
                ])
          ];
      } *)
    
    Module Impl_core_clone_Clone_for_core_slice_ascii_EscapeAscii.
      Definition Self : Ty.t := Ty.path "core::slice::ascii::EscapeAscii".
      
      (* Clone *)
      Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            Value.StructRecord
              "core::slice::ascii::EscapeAscii"
              [
                ("inner",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::clone::Clone",
                      Ty.apply
                        (Ty.path "core::iter::adapters::flatten::FlatMap")
                        []
                        [
                          Ty.apply (Ty.path "core::slice::iter::Iter") [] [ Ty.path "u8" ];
                          Ty.path "core::ascii::EscapeDefault";
                          Ty.path "core::slice::ascii::EscapeByte"
                        ],
                      [],
                      "clone",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::slice::ascii::EscapeAscii",
                        "inner"
                      |)
                    ]
                  |))
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::clone::Clone"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("clone", InstanceField.Method clone) ].
    End Impl_core_clone_Clone_for_core_slice_ascii_EscapeAscii.
    
    Module Impl_core_iter_traits_iterator_Iterator_for_core_slice_ascii_EscapeAscii.
      Definition Self : Ty.t := Ty.path "core::slice::ascii::EscapeAscii".
      
      (*     type Item = u8; *)
      Definition _Item : Ty.t := Ty.path "u8".
      
      (*
          fn next(&mut self) -> Option<u8> {
              self.inner.next()
          }
      *)
      Definition next (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::iter::traits::iterator::Iterator",
                Ty.apply
                  (Ty.path "core::iter::adapters::flatten::FlatMap")
                  []
                  [
                    Ty.apply (Ty.path "core::slice::iter::Iter") [] [ Ty.path "u8" ];
                    Ty.path "core::ascii::EscapeDefault";
                    Ty.path "core::slice::ascii::EscapeByte"
                  ],
                [],
                "next",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::slice::ascii::EscapeAscii",
                  "inner"
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn size_hint(&self) -> (usize, Option<usize>) {
              self.inner.size_hint()
          }
      *)
      Definition size_hint (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::iter::traits::iterator::Iterator",
                Ty.apply
                  (Ty.path "core::iter::adapters::flatten::FlatMap")
                  []
                  [
                    Ty.apply (Ty.path "core::slice::iter::Iter") [] [ Ty.path "u8" ];
                    Ty.path "core::ascii::EscapeDefault";
                    Ty.path "core::slice::ascii::EscapeByte"
                  ],
                [],
                "size_hint",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::slice::ascii::EscapeAscii",
                  "inner"
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn try_fold<Acc, Fold, R>(&mut self, init: Acc, fold: Fold) -> R
          where
              Fold: FnMut(Acc, Self::Item) -> R,
              R: ops::Try<Output = Acc>,
          {
              self.inner.try_fold(init, fold)
          }
      *)
      Definition try_fold (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ Acc; Fold; R ], [ self; init; fold ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let init := M.alloc (| init |) in
            let fold := M.alloc (| fold |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::iter::traits::iterator::Iterator",
                Ty.apply
                  (Ty.path "core::iter::adapters::flatten::FlatMap")
                  []
                  [
                    Ty.apply (Ty.path "core::slice::iter::Iter") [] [ Ty.path "u8" ];
                    Ty.path "core::ascii::EscapeDefault";
                    Ty.path "core::slice::ascii::EscapeByte"
                  ],
                [],
                "try_fold",
                [ Acc; Fold; R ]
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::slice::ascii::EscapeAscii",
                  "inner"
                |);
                M.read (| init |);
                M.read (| fold |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn fold<Acc, Fold>(self, init: Acc, fold: Fold) -> Acc
          where
              Fold: FnMut(Acc, Self::Item) -> Acc,
          {
              self.inner.fold(init, fold)
          }
      *)
      Definition fold (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ Acc; Fold ], [ self; init; fold ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let init := M.alloc (| init |) in
            let fold := M.alloc (| fold |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::iter::traits::iterator::Iterator",
                Ty.apply
                  (Ty.path "core::iter::adapters::flatten::FlatMap")
                  []
                  [
                    Ty.apply (Ty.path "core::slice::iter::Iter") [] [ Ty.path "u8" ];
                    Ty.path "core::ascii::EscapeDefault";
                    Ty.path "core::slice::ascii::EscapeByte"
                  ],
                [],
                "fold",
                [ Acc; Fold ]
              |),
              [
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    self,
                    "core::slice::ascii::EscapeAscii",
                    "inner"
                  |)
                |);
                M.read (| init |);
                M.read (| fold |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn last(mut self) -> Option<u8> {
              self.next_back()
          }
      *)
      Definition last (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::iter::traits::double_ended::DoubleEndedIterator",
                Ty.path "core::slice::ascii::EscapeAscii",
                [],
                "next_back",
                []
              |),
              [ self ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::iter::traits::iterator::Iterator"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("Item", InstanceField.Ty _Item);
            ("next", InstanceField.Method next);
            ("size_hint", InstanceField.Method size_hint);
            ("try_fold", InstanceField.Method try_fold);
            ("fold", InstanceField.Method fold);
            ("last", InstanceField.Method last)
          ].
    End Impl_core_iter_traits_iterator_Iterator_for_core_slice_ascii_EscapeAscii.
    
    Module Impl_core_iter_traits_double_ended_DoubleEndedIterator_for_core_slice_ascii_EscapeAscii.
      Definition Self : Ty.t := Ty.path "core::slice::ascii::EscapeAscii".
      
      (*
          fn next_back(&mut self) -> Option<u8> {
              self.inner.next_back()
          }
      *)
      Definition next_back (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::iter::traits::double_ended::DoubleEndedIterator",
                Ty.apply
                  (Ty.path "core::iter::adapters::flatten::FlatMap")
                  []
                  [
                    Ty.apply (Ty.path "core::slice::iter::Iter") [] [ Ty.path "u8" ];
                    Ty.path "core::ascii::EscapeDefault";
                    Ty.path "core::slice::ascii::EscapeByte"
                  ],
                [],
                "next_back",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::slice::ascii::EscapeAscii",
                  "inner"
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::iter::traits::double_ended::DoubleEndedIterator"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("next_back", InstanceField.Method next_back) ].
    End Impl_core_iter_traits_double_ended_DoubleEndedIterator_for_core_slice_ascii_EscapeAscii.
    
    Module Impl_core_iter_traits_marker_FusedIterator_for_core_slice_ascii_EscapeAscii.
      Definition Self : Ty.t := Ty.path "core::slice::ascii::EscapeAscii".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::iter::traits::marker::FusedIterator"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_iter_traits_marker_FusedIterator_for_core_slice_ascii_EscapeAscii.
    
    Module Impl_core_fmt_Display_for_core_slice_ascii_EscapeAscii.
      Definition Self : Ty.t := Ty.path "core::slice::ascii::EscapeAscii".
      
      (*
          fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
              // disassemble iterator, including front/back parts of flatmap in case it has been partially consumed
              let (front, slice, back) = self.clone().inner.into_parts();
              let front = front.unwrap_or(EscapeDefault::empty());
              let mut bytes = slice.unwrap_or_default().as_slice();
              let back = back.unwrap_or(EscapeDefault::empty());
      
              // usually empty, so the formatter won't have to do any work
              for byte in front {
                  f.write_char(byte as char)?;
              }
      
              fn needs_escape(b: u8) -> bool {
                  b > 0x7E || b < 0x20 || b == b'\\' || b == b'\'' || b == b'"'
              }
      
              while bytes.len() > 0 {
                  // fast path for the printable, non-escaped subset of ascii
                  let prefix = bytes.iter().take_while(|&&b| !needs_escape(b)).count();
                  // SAFETY: prefix length was derived by counting bytes in the same splice, so it's in-bounds
                  let (prefix, remainder) = unsafe { bytes.split_at_unchecked(prefix) };
                  // SAFETY: prefix is a valid utf8 sequence, as it's a subset of ASCII
                  let prefix = unsafe { crate::str::from_utf8_unchecked(prefix) };
      
                  f.write_str(prefix)?; // the fast part
      
                  bytes = remainder;
      
                  if let Some(&b) = bytes.first() {
                      // guaranteed to be non-empty, better to write it as a str
                      f.write_str(ascii::escape_default(b).as_str())?;
                      bytes = &bytes[1..];
                  }
              }
      
              // also usually empty
              for byte in back {
                  f.write_char(byte as char)?;
              }
              Ok(())
          }
      "
      *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  M.match_operator (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "core::iter::adapters::flatten::FlatMap")
                            []
                            [
                              Ty.apply (Ty.path "core::slice::iter::Iter") [] [ Ty.path "u8" ];
                              Ty.path "core::ascii::EscapeDefault";
                              Ty.path "core::slice::ascii::EscapeByte"
                            ],
                          "into_parts",
                          []
                        |),
                        [
                          M.read (|
                            M.SubPointer.get_struct_record_field (|
                              M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::clone::Clone",
                                    Ty.path "core::slice::ascii::EscapeAscii",
                                    [],
                                    "clone",
                                    []
                                  |),
                                  [ M.read (| self |) ]
                                |)
                              |),
                              "core::slice::ascii::EscapeAscii",
                              "inner"
                            |)
                          |)
                        ]
                      |)
                    |),
                    [
                      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 front := M.copy (| γ0_0 |) in
                          let slice := M.copy (| γ0_1 |) in
                          let back := M.copy (| γ0_2 |) in
                          let~ front :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "core::option::Option")
                                    []
                                    [ Ty.path "core::ascii::EscapeDefault" ],
                                  "unwrap_or",
                                  []
                                |),
                                [
                                  M.read (| front |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::ascii::EscapeDefault",
                                      "empty",
                                      []
                                    |),
                                    []
                                  |)
                                ]
                              |)
                            |) in
                          let~ bytes :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "core::slice::iter::Iter") [] [ Ty.path "u8" ],
                                  "as_slice",
                                  []
                                |),
                                [
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "core::option::Option")
                                          []
                                          [
                                            Ty.apply
                                              (Ty.path "core::slice::iter::Iter")
                                              []
                                              [ Ty.path "u8" ]
                                          ],
                                        "unwrap_or_default",
                                        []
                                      |),
                                      [ M.read (| slice |) ]
                                    |)
                                  |)
                                ]
                              |)
                            |) in
                          let~ back :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "core::option::Option")
                                    []
                                    [ Ty.path "core::ascii::EscapeDefault" ],
                                  "unwrap_or",
                                  []
                                |),
                                [
                                  M.read (| back |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::ascii::EscapeDefault",
                                      "empty",
                                      []
                                    |),
                                    []
                                  |)
                                ]
                              |)
                            |) in
                          let~ _ :=
                            M.use
                              (M.match_operator (|
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::iter::traits::collect::IntoIterator",
                                      Ty.path "core::ascii::EscapeDefault",
                                      [],
                                      "into_iter",
                                      []
                                    |),
                                    [ M.read (| front |) ]
                                  |)
                                |),
                                [
                                  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.path "core::ascii::EscapeDefault",
                                                    [],
                                                    "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 byte := M.copy (| γ0_0 |) in
                                                    let~ _ :=
                                                      M.match_operator (|
                                                        M.alloc (|
                                                          M.call_closure (|
                                                            M.get_trait_method (|
                                                              "core::ops::try_trait::Try",
                                                              Ty.apply
                                                                (Ty.path "core::result::Result")
                                                                []
                                                                [
                                                                  Ty.tuple [];
                                                                  Ty.path "core::fmt::Error"
                                                                ],
                                                              [],
                                                              "branch",
                                                              []
                                                            |),
                                                            [
                                                              M.call_closure (|
                                                                M.get_trait_method (|
                                                                  "core::fmt::Write",
                                                                  Ty.path "core::fmt::Formatter",
                                                                  [],
                                                                  "write_char",
                                                                  []
                                                                |),
                                                                [
                                                                  M.read (| f |);
                                                                  M.rust_cast (M.read (| byte |))
                                                                ]
                                                              |)
                                                            ]
                                                          |)
                                                        |),
                                                        [
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ0_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "core::ops::control_flow::ControlFlow::Break",
                                                                  0
                                                                |) in
                                                              let residual := M.copy (| γ0_0 |) in
                                                              M.alloc (|
                                                                M.never_to_any (|
                                                                  M.read (|
                                                                    M.return_ (|
                                                                      M.call_closure (|
                                                                        M.get_trait_method (|
                                                                          "core::ops::try_trait::FromResidual",
                                                                          Ty.apply
                                                                            (Ty.path
                                                                              "core::result::Result")
                                                                            []
                                                                            [
                                                                              Ty.tuple [];
                                                                              Ty.path
                                                                                "core::fmt::Error"
                                                                            ],
                                                                          [
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "core::result::Result")
                                                                              []
                                                                              [
                                                                                Ty.path
                                                                                  "core::convert::Infallible";
                                                                                Ty.path
                                                                                  "core::fmt::Error"
                                                                              ]
                                                                          ],
                                                                          "from_residual",
                                                                          []
                                                                        |),
                                                                        [ M.read (| residual |) ]
                                                                      |)
                                                                    |)
                                                                  |)
                                                                |)
                                                              |)));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ0_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "core::ops::control_flow::ControlFlow::Continue",
                                                                  0
                                                                |) in
                                                              let val := M.copy (| γ0_0 |) in
                                                              val))
                                                        ]
                                                      |) in
                                                    M.alloc (| Value.Tuple [] |)))
                                              ]
                                            |) in
                                          M.alloc (| Value.Tuple [] |)))
                                      |)))
                                ]
                              |)) 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.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                                    "len",
                                                    []
                                                  |),
                                                  [ M.read (| bytes |) ]
                                                |),
                                                Value.Integer IntegerKind.Usize 0
                                              |)
                                            |)) in
                                        let _ :=
                                          M.is_constant_or_break_match (|
                                            M.read (| γ |),
                                            Value.Bool true
                                          |) in
                                        let~ prefix :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::iter::traits::iterator::Iterator",
                                                Ty.apply
                                                  (Ty.path
                                                    "core::iter::adapters::take_while::TakeWhile")
                                                  []
                                                  [
                                                    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" ],
                                                    [],
                                                    "take_while",
                                                    [
                                                      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 (| bytes |) ]
                                                    |);
                                                    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 b := M.copy (| γ |) in
                                                                      UnOp.not (|
                                                                        M.call_closure (|
                                                                          M.get_associated_function (|
                                                                            Self,
                                                                            "needs_escape.fmt",
                                                                            []
                                                                          |),
                                                                          [ M.read (| b |) ]
                                                                        |)
                                                                      |)))
                                                                ]
                                                              |)))
                                                          | _ =>
                                                            M.impossible "wrong number of arguments"
                                                          end))
                                                  ]
                                                |)
                                              ]
                                            |)
                                          |) in
                                        M.match_operator (|
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                                "split_at_unchecked",
                                                []
                                              |),
                                              [ M.read (| bytes |); M.read (| prefix |) ]
                                            |)
                                          |),
                                          [
                                            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 prefix := M.copy (| γ0_0 |) in
                                                let remainder := M.copy (| γ0_1 |) in
                                                let~ prefix :=
                                                  M.alloc (|
                                                    M.call_closure (|
                                                      M.get_function (|
                                                        "core::str::converts::from_utf8_unchecked",
                                                        []
                                                      |),
                                                      [ M.read (| prefix |) ]
                                                    |)
                                                  |) in
                                                let~ _ :=
                                                  M.match_operator (|
                                                    M.alloc (|
                                                      M.call_closure (|
                                                        M.get_trait_method (|
                                                          "core::ops::try_trait::Try",
                                                          Ty.apply
                                                            (Ty.path "core::result::Result")
                                                            []
                                                            [
                                                              Ty.tuple [];
                                                              Ty.path "core::fmt::Error"
                                                            ],
                                                          [],
                                                          "branch",
                                                          []
                                                        |),
                                                        [
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.path "core::fmt::Formatter",
                                                              "write_str",
                                                              []
                                                            |),
                                                            [ M.read (| f |); M.read (| prefix |) ]
                                                          |)
                                                        ]
                                                      |)
                                                    |),
                                                    [
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ0_0 :=
                                                            M.SubPointer.get_struct_tuple_field (|
                                                              γ,
                                                              "core::ops::control_flow::ControlFlow::Break",
                                                              0
                                                            |) in
                                                          let residual := M.copy (| γ0_0 |) in
                                                          M.alloc (|
                                                            M.never_to_any (|
                                                              M.read (|
                                                                M.return_ (|
                                                                  M.call_closure (|
                                                                    M.get_trait_method (|
                                                                      "core::ops::try_trait::FromResidual",
                                                                      Ty.apply
                                                                        (Ty.path
                                                                          "core::result::Result")
                                                                        []
                                                                        [
                                                                          Ty.tuple [];
                                                                          Ty.path "core::fmt::Error"
                                                                        ],
                                                                      [
                                                                        Ty.apply
                                                                          (Ty.path
                                                                            "core::result::Result")
                                                                          []
                                                                          [
                                                                            Ty.path
                                                                              "core::convert::Infallible";
                                                                            Ty.path
                                                                              "core::fmt::Error"
                                                                          ]
                                                                      ],
                                                                      "from_residual",
                                                                      []
                                                                    |),
                                                                    [ M.read (| residual |) ]
                                                                  |)
                                                                |)
                                                              |)
                                                            |)
                                                          |)));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ0_0 :=
                                                            M.SubPointer.get_struct_tuple_field (|
                                                              γ,
                                                              "core::ops::control_flow::ControlFlow::Continue",
                                                              0
                                                            |) in
                                                          let val := M.copy (| γ0_0 |) in
                                                          val))
                                                    ]
                                                  |) in
                                                let~ _ :=
                                                  M.write (| bytes, M.read (| remainder |) |) in
                                                M.match_operator (|
                                                  M.alloc (| Value.Tuple [] |),
                                                  [
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (let γ :=
                                                          M.alloc (|
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.apply
                                                                  (Ty.path "slice")
                                                                  []
                                                                  [ Ty.path "u8" ],
                                                                "first",
                                                                []
                                                              |),
                                                              [ M.read (| bytes |) ]
                                                            |)
                                                          |) in
                                                        let γ0_0 :=
                                                          M.SubPointer.get_struct_tuple_field (|
                                                            γ,
                                                            "core::option::Option::Some",
                                                            0
                                                          |) in
                                                        let γ0_0 := M.read (| γ0_0 |) in
                                                        let b := M.copy (| γ0_0 |) in
                                                        let~ _ :=
                                                          M.match_operator (|
                                                            M.alloc (|
                                                              M.call_closure (|
                                                                M.get_trait_method (|
                                                                  "core::ops::try_trait::Try",
                                                                  Ty.apply
                                                                    (Ty.path "core::result::Result")
                                                                    []
                                                                    [
                                                                      Ty.tuple [];
                                                                      Ty.path "core::fmt::Error"
                                                                    ],
                                                                  [],
                                                                  "branch",
                                                                  []
                                                                |),
                                                                [
                                                                  M.call_closure (|
                                                                    M.get_associated_function (|
                                                                      Ty.path
                                                                        "core::fmt::Formatter",
                                                                      "write_str",
                                                                      []
                                                                    |),
                                                                    [
                                                                      M.read (| f |);
                                                                      M.call_closure (|
                                                                        M.get_associated_function (|
                                                                          Ty.path
                                                                            "core::ascii::EscapeDefault",
                                                                          "as_str",
                                                                          []
                                                                        |),
                                                                        [
                                                                          M.alloc (|
                                                                            M.call_closure (|
                                                                              M.get_function (|
                                                                                "core::ascii::escape_default",
                                                                                []
                                                                              |),
                                                                              [ M.read (| b |) ]
                                                                            |)
                                                                          |)
                                                                        ]
                                                                      |)
                                                                    ]
                                                                  |)
                                                                ]
                                                              |)
                                                            |),
                                                            [
                                                              fun γ =>
                                                                ltac:(M.monadic
                                                                  (let γ0_0 :=
                                                                    M.SubPointer.get_struct_tuple_field (|
                                                                      γ,
                                                                      "core::ops::control_flow::ControlFlow::Break",
                                                                      0
                                                                    |) in
                                                                  let residual :=
                                                                    M.copy (| γ0_0 |) in
                                                                  M.alloc (|
                                                                    M.never_to_any (|
                                                                      M.read (|
                                                                        M.return_ (|
                                                                          M.call_closure (|
                                                                            M.get_trait_method (|
                                                                              "core::ops::try_trait::FromResidual",
                                                                              Ty.apply
                                                                                (Ty.path
                                                                                  "core::result::Result")
                                                                                []
                                                                                [
                                                                                  Ty.tuple [];
                                                                                  Ty.path
                                                                                    "core::fmt::Error"
                                                                                ],
                                                                              [
                                                                                Ty.apply
                                                                                  (Ty.path
                                                                                    "core::result::Result")
                                                                                  []
                                                                                  [
                                                                                    Ty.path
                                                                                      "core::convert::Infallible";
                                                                                    Ty.path
                                                                                      "core::fmt::Error"
                                                                                  ]
                                                                              ],
                                                                              "from_residual",
                                                                              []
                                                                            |),
                                                                            [ M.read (| residual |)
                                                                            ]
                                                                          |)
                                                                        |)
                                                                      |)
                                                                    |)
                                                                  |)));
                                                              fun γ =>
                                                                ltac:(M.monadic
                                                                  (let γ0_0 :=
                                                                    M.SubPointer.get_struct_tuple_field (|
                                                                      γ,
                                                                      "core::ops::control_flow::ControlFlow::Continue",
                                                                      0
                                                                    |) in
                                                                  let val := M.copy (| γ0_0 |) in
                                                                  val))
                                                            ]
                                                          |) in
                                                        let~ _ :=
                                                          M.write (|
                                                            bytes,
                                                            M.call_closure (|
                                                              M.get_trait_method (|
                                                                "core::ops::index::Index",
                                                                Ty.apply
                                                                  (Ty.path "slice")
                                                                  []
                                                                  [ Ty.path "u8" ],
                                                                [
                                                                  Ty.apply
                                                                    (Ty.path
                                                                      "core::ops::range::RangeFrom")
                                                                    []
                                                                    [ Ty.path "usize" ]
                                                                ],
                                                                "index",
                                                                []
                                                              |),
                                                              [
                                                                M.read (| bytes |);
                                                                Value.StructRecord
                                                                  "core::ops::range::RangeFrom"
                                                                  [
                                                                    ("start",
                                                                      Value.Integer
                                                                        IntegerKind.Usize
                                                                        1)
                                                                  ]
                                                              ]
                                                            |)
                                                          |) in
                                                        M.alloc (| Value.Tuple [] |)));
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (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~ _ :=
                            M.use
                              (M.match_operator (|
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::iter::traits::collect::IntoIterator",
                                      Ty.path "core::ascii::EscapeDefault",
                                      [],
                                      "into_iter",
                                      []
                                    |),
                                    [ M.read (| back |) ]
                                  |)
                                |),
                                [
                                  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.path "core::ascii::EscapeDefault",
                                                    [],
                                                    "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 byte := M.copy (| γ0_0 |) in
                                                    let~ _ :=
                                                      M.match_operator (|
                                                        M.alloc (|
                                                          M.call_closure (|
                                                            M.get_trait_method (|
                                                              "core::ops::try_trait::Try",
                                                              Ty.apply
                                                                (Ty.path "core::result::Result")
                                                                []
                                                                [
                                                                  Ty.tuple [];
                                                                  Ty.path "core::fmt::Error"
                                                                ],
                                                              [],
                                                              "branch",
                                                              []
                                                            |),
                                                            [
                                                              M.call_closure (|
                                                                M.get_trait_method (|
                                                                  "core::fmt::Write",
                                                                  Ty.path "core::fmt::Formatter",
                                                                  [],
                                                                  "write_char",
                                                                  []
                                                                |),
                                                                [
                                                                  M.read (| f |);
                                                                  M.rust_cast (M.read (| byte |))
                                                                ]
                                                              |)
                                                            ]
                                                          |)
                                                        |),
                                                        [
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ0_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "core::ops::control_flow::ControlFlow::Break",
                                                                  0
                                                                |) in
                                                              let residual := M.copy (| γ0_0 |) in
                                                              M.alloc (|
                                                                M.never_to_any (|
                                                                  M.read (|
                                                                    M.return_ (|
                                                                      M.call_closure (|
                                                                        M.get_trait_method (|
                                                                          "core::ops::try_trait::FromResidual",
                                                                          Ty.apply
                                                                            (Ty.path
                                                                              "core::result::Result")
                                                                            []
                                                                            [
                                                                              Ty.tuple [];
                                                                              Ty.path
                                                                                "core::fmt::Error"
                                                                            ],
                                                                          [
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "core::result::Result")
                                                                              []
                                                                              [
                                                                                Ty.path
                                                                                  "core::convert::Infallible";
                                                                                Ty.path
                                                                                  "core::fmt::Error"
                                                                              ]
                                                                          ],
                                                                          "from_residual",
                                                                          []
                                                                        |),
                                                                        [ M.read (| residual |) ]
                                                                      |)
                                                                    |)
                                                                  |)
                                                                |)
                                                              |)));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ0_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "core::ops::control_flow::ControlFlow::Continue",
                                                                  0
                                                                |) in
                                                              let val := M.copy (| γ0_0 |) in
                                                              val))
                                                        ]
                                                      |) in
                                                    M.alloc (| Value.Tuple [] |)))
                                              ]
                                            |) in
                                          M.alloc (| Value.Tuple [] |)))
                                      |)))
                                ]
                              |)) in
                          M.alloc (|
                            Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ]
                          |)))
                    ]
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::fmt::Display"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
    End Impl_core_fmt_Display_for_core_slice_ascii_EscapeAscii.
    
    Module Impl_core_fmt_Debug_for_core_slice_ascii_EscapeAscii.
      Definition Self : Ty.t := Ty.path "core::slice::ascii::EscapeAscii".
      
      (*
          fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
              f.debug_struct("EscapeAscii").finish_non_exhaustive()
          }
      *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "core::fmt::builders::DebugStruct",
                "finish_non_exhaustive",
                []
              |),
              [
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "core::fmt::Formatter",
                      "debug_struct",
                      []
                    |),
                    [ M.read (| f |); M.read (| Value.String "EscapeAscii" |) ]
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::fmt::Debug"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
    End Impl_core_fmt_Debug_for_core_slice_ascii_EscapeAscii.
    
    (*
    const fn contains_nonascii(v: usize) -> bool {
        const NONASCII_MASK: usize = usize::repeat_u8(0x80);
        (NONASCII_MASK & v) != 0
    }
    *)
    Definition contains_nonascii (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ v ] =>
        ltac:(M.monadic
          (let v := M.alloc (| v |) in
          BinOp.ne (|
            BinOp.bit_and
              (M.read (|
                M.get_constant (| "core::slice::ascii::contains_nonascii::NONASCII_MASK" |)
              |))
              (M.read (| v |)),
            Value.Integer IntegerKind.Usize 0
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_contains_nonascii :
      M.IsFunction "core::slice::ascii::contains_nonascii" contains_nonascii.
    
    Module contains_nonascii.
      Definition value_NONASCII_MASK : 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 ]
              |)
            |))).
    End contains_nonascii.
    
    (*
    pub const fn is_ascii_simple(mut bytes: &[u8]) -> bool {
        while let [rest @ .., last] = bytes {
            if !last.is_ascii() {
                break;
            }
            bytes = rest;
        }
        bytes.is_empty()
    }
    *)
    Definition is_ascii_simple (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ bytes ] =>
        ltac:(M.monadic
          (let bytes := M.alloc (| bytes |) in
          M.read (|
            let~ _ :=
              M.loop (|
                ltac:(M.monadic
                  (M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := bytes in
                          let γ := M.read (| γ |) in
                          let γ1_rest := M.SubPointer.get_slice_rest (| γ, 0, 1 |) in
                          let γ1_rev0 := M.SubPointer.get_slice_rev_index (| γ, 0 |) in
                          let rest := M.alloc (| γ1_rest |) in
                          let last := M.alloc (| γ1_rev0 |) in
                          let~ _ :=
                            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.path "u8",
                                                "is_ascii",
                                                []
                                              |),
                                              [ M.read (| last |) ]
                                            |)
                                          |)
                                        |)) 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~ _ := M.write (| bytes, M.read (| rest |) |) 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_associated_function (|
                  Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                  "is_empty",
                  []
                |),
                [ M.read (| bytes |) ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_is_ascii_simple :
      M.IsFunction "core::slice::ascii::is_ascii_simple" is_ascii_simple.
    
    (*
    const fn is_ascii(s: &[u8]) -> bool {
        const USIZE_SIZE: usize = mem::size_of::<usize>();
    
        let len = s.len();
        let align_offset = s.as_ptr().align_offset(USIZE_SIZE);
    
        // If we wouldn't gain anything from the word-at-a-time implementation, fall
        // back to a scalar loop.
        //
        // We also do this for architectures where `size_of::<usize>()` isn't
        // sufficient alignment for `usize`, because it's a weird edge case.
        if len < USIZE_SIZE || len < align_offset || USIZE_SIZE < mem::align_of::<usize>() {
            return is_ascii_simple(s);
        }
    
        // We always read the first word unaligned, which means `align_offset` is
        // 0, we'd read the same value again for the aligned read.
        let offset_to_aligned = if align_offset == 0 { USIZE_SIZE } else { align_offset };
    
        let start = s.as_ptr();
        // SAFETY: We verify `len < USIZE_SIZE` above.
        let first_word = unsafe { (start as *const usize).read_unaligned() };
    
        if contains_nonascii(first_word) {
            return false;
        }
        // We checked this above, somewhat implicitly. Note that `offset_to_aligned`
        // is either `align_offset` or `USIZE_SIZE`, both of are explicitly checked
        // above.
        debug_assert!(offset_to_aligned <= len);
    
        // SAFETY: word_ptr is the (properly aligned) usize ptr we use to read the
        // middle chunk of the slice.
        let mut word_ptr = unsafe { start.add(offset_to_aligned) as *const usize };
    
        // `byte_pos` is the byte index of `word_ptr`, used for loop end checks.
        let mut byte_pos = offset_to_aligned;
    
        // Paranoia check about alignment, since we're about to do a bunch of
        // unaligned loads. In practice this should be impossible barring a bug in
        // `align_offset` though.
        // While this method is allowed to spuriously fail in CTFE, if it doesn't
        // have alignment information it should have given a `usize::MAX` for
        // `align_offset` earlier, sending things through the scalar path instead of
        // this one, so this check should pass if it's reachable.
        debug_assert!(word_ptr.is_aligned_to(mem::align_of::<usize>()));
    
        // Read subsequent words until the last aligned word, excluding the last
        // aligned word by itself to be done in tail check later, to ensure that
        // tail is always one `usize` at most to extra branch `byte_pos == len`.
        while byte_pos < len - USIZE_SIZE {
            // Sanity check that the read is in bounds
            debug_assert!(byte_pos + USIZE_SIZE <= len);
            // And that our assumptions about `byte_pos` hold.
            debug_assert!(matches!(
                word_ptr.cast::<u8>().guaranteed_eq(start.wrapping_add(byte_pos)),
                // These are from the same allocation, so will hopefully always be
                // known to match even in CTFE, but if it refuses to compare them
                // that's ok since it's just a debug check anyway.
                None | Some(true),
            ));
    
            // SAFETY: We know `word_ptr` is properly aligned (because of
            // `align_offset`), and we know that we have enough bytes between `word_ptr` and the end
            let word = unsafe { word_ptr.read() };
            if contains_nonascii(word) {
                return false;
            }
    
            byte_pos += USIZE_SIZE;
            // SAFETY: We know that `byte_pos <= len - USIZE_SIZE`, which means that
            // after this `add`, `word_ptr` will be at most one-past-the-end.
            word_ptr = unsafe { word_ptr.add(1) };
        }
    
        // Sanity check to ensure there really is only one `usize` left. This should
        // be guaranteed by our loop condition.
        debug_assert!(byte_pos <= len && len - byte_pos <= USIZE_SIZE);
    
        // SAFETY: This relies on `len >= USIZE_SIZE`, which we check at the start.
        let last_word = unsafe { (start.add(len - USIZE_SIZE) as *const usize).read_unaligned() };
    
        !contains_nonascii(last_word)
    }
    *)
    Definition is_ascii (ε : 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 (|
                let~ len :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                        "len",
                        []
                      |),
                      [ M.read (| s |) ]
                    |)
                  |) in
                let~ align_offset :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "*const") [] [ Ty.path "u8" ],
                        "align_offset",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                            "as_ptr",
                            []
                          |),
                          [ M.read (| s |) ]
                        |);
                        M.read (| M.get_constant (| "core::slice::ascii::is_ascii::USIZE_SIZE" |) |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                LogicalOp.or (|
                                  LogicalOp.or (|
                                    BinOp.lt (|
                                      M.read (| len |),
                                      M.read (|
                                        M.get_constant (|
                                          "core::slice::ascii::is_ascii::USIZE_SIZE"
                                        |)
                                      |)
                                    |),
                                    ltac:(M.monadic
                                      (BinOp.lt (| M.read (| len |), M.read (| align_offset |) |)))
                                  |),
                                  ltac:(M.monadic
                                    (BinOp.lt (|
                                      M.read (|
                                        M.get_constant (|
                                          "core::slice::ascii::is_ascii::USIZE_SIZE"
                                        |)
                                      |),
                                      M.call_closure (|
                                        M.get_function (|
                                          "core::mem::align_of",
                                          [ Ty.path "usize" ]
                                        |),
                                        []
                                      |)
                                    |)))
                                |)
                              |)) 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::ascii::is_ascii_simple", [] |),
                                    [ M.read (| s |) ]
                                  |)
                                |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ offset_to_aligned :=
                  M.copy (|
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  BinOp.eq (|
                                    M.read (| align_offset |),
                                    Value.Integer IntegerKind.Usize 0
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.get_constant (| "core::slice::ascii::is_ascii::USIZE_SIZE" |)));
                        fun γ => ltac:(M.monadic align_offset)
                      ]
                    |)
                  |) in
                let~ start :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                        "as_ptr",
                        []
                      |),
                      [ M.read (| s |) ]
                    |)
                  |) in
                let~ first_word :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "*const") [] [ Ty.path "usize" ],
                        "read_unaligned",
                        []
                      |),
                      [ M.rust_cast (M.read (| start |)) ]
                    |)
                  |) 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::slice::ascii::contains_nonascii", [] |),
                                  [ M.read (| first_word |) ]
                                |)
                              |)) 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.Bool false |) |) |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.use (M.alloc (| Value.Bool true |)) 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 (|
                                          UnOp.not (|
                                            BinOp.le (|
                                              M.read (| offset_to_aligned |),
                                              M.read (| len |)
                                            |)
                                          |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    M.alloc (|
                                      M.never_to_any (|
                                        M.call_closure (|
                                          M.get_function (| "core::panicking::panic", [] |),
                                          [
                                            M.read (|
                                              Value.String
                                                "assertion failed: offset_to_aligned <= len"
                                            |)
                                          ]
                                        |)
                                      |)
                                    |)));
                                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                              ]
                            |) in
                          M.alloc (| Value.Tuple [] |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ word_ptr :=
                  M.alloc (|
                    M.rust_cast
                      (M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "*const") [] [ Ty.path "u8" ],
                          "add",
                          []
                        |),
                        [ M.read (| start |); M.read (| offset_to_aligned |) ]
                      |))
                  |) in
                let~ byte_pos := M.copy (| offset_to_aligned |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.use (M.alloc (| Value.Bool true |)) 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 (|
                                          UnOp.not (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply (Ty.path "*const") [] [ Ty.path "usize" ],
                                                "is_aligned_to",
                                                []
                                              |),
                                              [
                                                M.read (| word_ptr |);
                                                M.call_closure (|
                                                  M.get_function (|
                                                    "core::mem::align_of",
                                                    [ Ty.path "usize" ]
                                                  |),
                                                  []
                                                |)
                                              ]
                                            |)
                                          |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    M.alloc (|
                                      M.never_to_any (|
                                        M.call_closure (|
                                          M.get_function (| "core::panicking::panic", [] |),
                                          [
                                            M.read (|
                                              Value.String
                                                "assertion failed: word_ptr.is_aligned_to(mem::align_of::<usize>())"
                                            |)
                                          ]
                                        |)
                                      |)
                                    |)));
                                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                              ]
                            |) in
                          M.alloc (| Value.Tuple [] |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) 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 (| byte_pos |),
                                      BinOp.Wrap.sub (|
                                        M.read (| len |),
                                        M.read (|
                                          M.get_constant (|
                                            "core::slice::ascii::is_ascii::USIZE_SIZE"
                                          |)
                                        |)
                                      |)
                                    |)
                                  |)) 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 (| Value.Bool true |)) 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 (|
                                                        UnOp.not (|
                                                          BinOp.le (|
                                                            BinOp.Wrap.add (|
                                                              M.read (| byte_pos |),
                                                              M.read (|
                                                                M.get_constant (|
                                                                  "core::slice::ascii::is_ascii::USIZE_SIZE"
                                                                |)
                                                              |)
                                                            |),
                                                            M.read (| len |)
                                                          |)
                                                        |)
                                                      |)) in
                                                  let _ :=
                                                    M.is_constant_or_break_match (|
                                                      M.read (| γ |),
                                                      Value.Bool true
                                                    |) in
                                                  M.alloc (|
                                                    M.never_to_any (|
                                                      M.call_closure (|
                                                        M.get_function (|
                                                          "core::panicking::panic",
                                                          []
                                                        |),
                                                        [
                                                          M.read (|
                                                            Value.String
                                                              "assertion failed: byte_pos + USIZE_SIZE <= len"
                                                          |)
                                                        ]
                                                      |)
                                                    |)
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                            ]
                                          |) in
                                        M.alloc (| Value.Tuple [] |)));
                                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                  ]
                                |) in
                              let~ _ :=
                                M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ := M.use (M.alloc (| Value.Bool true |)) 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 (|
                                                        UnOp.not (|
                                                          M.read (|
                                                            M.match_operator (|
                                                              M.alloc (|
                                                                M.call_closure (|
                                                                  M.get_associated_function (|
                                                                    Ty.apply
                                                                      (Ty.path "*const")
                                                                      []
                                                                      [ Ty.path "u8" ],
                                                                    "guaranteed_eq",
                                                                    []
                                                                  |),
                                                                  [
                                                                    M.call_closure (|
                                                                      M.get_associated_function (|
                                                                        Ty.apply
                                                                          (Ty.path "*const")
                                                                          []
                                                                          [ Ty.path "usize" ],
                                                                        "cast",
                                                                        [ Ty.path "u8" ]
                                                                      |),
                                                                      [ M.read (| word_ptr |) ]
                                                                    |);
                                                                    M.call_closure (|
                                                                      M.get_associated_function (|
                                                                        Ty.apply
                                                                          (Ty.path "*const")
                                                                          []
                                                                          [ Ty.path "u8" ],
                                                                        "wrapping_add",
                                                                        []
                                                                      |),
                                                                      [
                                                                        M.read (| start |);
                                                                        M.read (| byte_pos |)
                                                                      ]
                                                                    |)
                                                                  ]
                                                                |)
                                                              |),
                                                              [
                                                                fun γ =>
                                                                  ltac:(M.monadic
                                                                    (M.find_or_pattern (|
                                                                      γ,
                                                                      [
                                                                        fun γ =>
                                                                          ltac:(M.monadic
                                                                            (let _ :=
                                                                              M.is_struct_tuple (|
                                                                                γ,
                                                                                "core::option::Option::None"
                                                                              |) in
                                                                            Value.Tuple []));
                                                                        fun γ =>
                                                                          ltac:(M.monadic
                                                                            (let γ0_0 :=
                                                                              M.SubPointer.get_struct_tuple_field (|
                                                                                γ,
                                                                                "core::option::Option::Some",
                                                                                0
                                                                              |) in
                                                                            let _ :=
                                                                              M.is_constant_or_break_match (|
                                                                                M.read (| γ0_0 |),
                                                                                Value.Bool true
                                                                              |) in
                                                                            Value.Tuple []))
                                                                      ],
                                                                      M.closure
                                                                        (fun γ =>
                                                                          ltac:(M.monadic
                                                                            match γ with
                                                                            | [] =>
                                                                              ltac:(M.monadic
                                                                                (M.alloc (|
                                                                                  Value.Bool true
                                                                                |)))
                                                                            | _ =>
                                                                              M.impossible
                                                                                "wrong number of arguments"
                                                                            end))
                                                                    |)));
                                                                fun γ =>
                                                                  ltac:(M.monadic
                                                                    (M.alloc (|
                                                                      Value.Bool false
                                                                    |)))
                                                              ]
                                                            |)
                                                          |)
                                                        |)
                                                      |)) in
                                                  let _ :=
                                                    M.is_constant_or_break_match (|
                                                      M.read (| γ |),
                                                      Value.Bool true
                                                    |) in
                                                  M.alloc (|
                                                    M.never_to_any (|
                                                      M.call_closure (|
                                                        M.get_function (|
                                                          "core::panicking::panic",
                                                          []
                                                        |),
                                                        [
                                                          M.read (|
                                                            Value.String
                                                              "assertion failed: matches!(word_ptr.cast::<u8>().guaranteed_eq(start.wrapping_add(byte_pos)),
    None | Some(true),)"
                                                          |)
                                                        ]
                                                      |)
                                                    |)
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                            ]
                                          |) in
                                        M.alloc (| Value.Tuple [] |)));
                                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                  ]
                                |) in
                              let~ word :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "*const") [] [ Ty.path "usize" ],
                                      "read",
                                      []
                                    |),
                                    [ M.read (| word_ptr |) ]
                                  |)
                                |) 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::slice::ascii::contains_nonascii",
                                                  []
                                                |),
                                                [ M.read (| word |) ]
                                              |)
                                            |)) 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.Bool false |) |)
                                          |)
                                        |)));
                                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                  ]
                                |) in
                              let~ _ :=
                                let β := byte_pos in
                                M.write (|
                                  β,
                                  BinOp.Wrap.add (|
                                    M.read (| β |),
                                    M.read (|
                                      M.get_constant (|
                                        "core::slice::ascii::is_ascii::USIZE_SIZE"
                                      |)
                                    |)
                                  |)
                                |) in
                              let~ _ :=
                                M.write (|
                                  word_ptr,
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "*const") [] [ Ty.path "usize" ],
                                      "add",
                                      []
                                    |),
                                    [ M.read (| word_ptr |); 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
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.use (M.alloc (| Value.Bool true |)) 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 (|
                                          UnOp.not (|
                                            LogicalOp.and (|
                                              BinOp.le (|
                                                M.read (| byte_pos |),
                                                M.read (| len |)
                                              |),
                                              ltac:(M.monadic
                                                (BinOp.le (|
                                                  BinOp.Wrap.sub (|
                                                    M.read (| len |),
                                                    M.read (| byte_pos |)
                                                  |),
                                                  M.read (|
                                                    M.get_constant (|
                                                      "core::slice::ascii::is_ascii::USIZE_SIZE"
                                                    |)
                                                  |)
                                                |)))
                                            |)
                                          |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    M.alloc (|
                                      M.never_to_any (|
                                        M.call_closure (|
                                          M.get_function (| "core::panicking::panic", [] |),
                                          [
                                            M.read (|
                                              Value.String
                                                "assertion failed: byte_pos <= len && len - byte_pos <= USIZE_SIZE"
                                            |)
                                          ]
                                        |)
                                      |)
                                    |)));
                                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                              ]
                            |) in
                          M.alloc (| Value.Tuple [] |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ last_word :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "*const") [] [ Ty.path "usize" ],
                        "read_unaligned",
                        []
                      |),
                      [
                        M.rust_cast
                          (M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "*const") [] [ Ty.path "u8" ],
                              "add",
                              []
                            |),
                            [
                              M.read (| start |);
                              BinOp.Wrap.sub (|
                                M.read (| len |),
                                M.read (|
                                  M.get_constant (| "core::slice::ascii::is_ascii::USIZE_SIZE" |)
                                |)
                              |)
                            ]
                          |))
                      ]
                    |)
                  |) in
                M.alloc (|
                  UnOp.not (|
                    M.call_closure (|
                      M.get_function (| "core::slice::ascii::contains_nonascii", [] |),
                      [ M.read (| last_word |) ]
                    |)
                  |)
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_is_ascii : M.IsFunction "core::slice::ascii::is_ascii" is_ascii.
    
    Module is_ascii.
      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" ] |),
                []
              |)
            |))).
    End is_ascii.
  End ascii.
End slice.
