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

Module net.
  Module parser.
    (* Trait *)
    (* Empty module 'ReadNumberHelper' *)
    
    Module Impl_core_net_parser_ReadNumberHelper_for_u8.
      Definition Self : Ty.t := Ty.path "u8".
      
      (*         const ZERO: Self = 0; *)
      (* Ty.path "u8" *)
      Definition value_ZERO : Value.t :=
        M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U8 0 |))).
      
      (*
              fn checked_mul(&self, other: u32) -> Option<Self> {
                  Self::checked_mul( *self, other.try_into().ok()?)
              }
      *)
      Definition checked_mul (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.call_closure (|
                  M.get_associated_function (| Ty.path "u8", "checked_mul", [] |),
                  [
                    M.read (| M.read (| self |) |);
                    M.read (|
                      M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::try_trait::Try",
                              Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u8" ],
                              [],
                              "branch",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "core::result::Result")
                                    []
                                    [ Ty.path "u8"; Ty.path "core::num::error::TryFromIntError" ],
                                  "ok",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::convert::TryInto",
                                      Ty.path "u32",
                                      [ Ty.path "u8" ],
                                      "try_into",
                                      []
                                    |),
                                    [ M.read (| other |) ]
                                  |)
                                ]
                              |)
                            ]
                          |)
                        |),
                        [
                          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::option::Option")
                                            []
                                            [ Ty.path "u8" ],
                                          [
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [ Ty.path "core::convert::Infallible" ]
                                          ],
                                          "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))
                        ]
                      |)
                    |)
                  ]
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
              fn checked_add(&self, other: u32) -> Option<Self> {
                  Self::checked_add( *self, other.try_into().ok()?)
              }
      *)
      Definition checked_add (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.call_closure (|
                  M.get_associated_function (| Ty.path "u8", "checked_add", [] |),
                  [
                    M.read (| M.read (| self |) |);
                    M.read (|
                      M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::try_trait::Try",
                              Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u8" ],
                              [],
                              "branch",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "core::result::Result")
                                    []
                                    [ Ty.path "u8"; Ty.path "core::num::error::TryFromIntError" ],
                                  "ok",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::convert::TryInto",
                                      Ty.path "u32",
                                      [ Ty.path "u8" ],
                                      "try_into",
                                      []
                                    |),
                                    [ M.read (| other |) ]
                                  |)
                                ]
                              |)
                            ]
                          |)
                        |),
                        [
                          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::option::Option")
                                            []
                                            [ Ty.path "u8" ],
                                          [
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [ Ty.path "core::convert::Infallible" ]
                                          ],
                                          "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))
                        ]
                      |)
                    |)
                  ]
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::net::parser::ReadNumberHelper"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("value_ZERO", InstanceField.Constant value_ZERO);
            ("checked_mul", InstanceField.Method checked_mul);
            ("checked_add", InstanceField.Method checked_add)
          ].
    End Impl_core_net_parser_ReadNumberHelper_for_u8.
    
    Module Impl_core_net_parser_ReadNumberHelper_for_u16.
      Definition Self : Ty.t := Ty.path "u16".
      
      (*         const ZERO: Self = 0; *)
      (* Ty.path "u16" *)
      Definition value_ZERO : Value.t :=
        M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U16 0 |))).
      
      (*
              fn checked_mul(&self, other: u32) -> Option<Self> {
                  Self::checked_mul( *self, other.try_into().ok()?)
              }
      *)
      Definition checked_mul (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.call_closure (|
                  M.get_associated_function (| Ty.path "u16", "checked_mul", [] |),
                  [
                    M.read (| M.read (| self |) |);
                    M.read (|
                      M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::try_trait::Try",
                              Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u16" ],
                              [],
                              "branch",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "core::result::Result")
                                    []
                                    [ Ty.path "u16"; Ty.path "core::num::error::TryFromIntError" ],
                                  "ok",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::convert::TryInto",
                                      Ty.path "u32",
                                      [ Ty.path "u16" ],
                                      "try_into",
                                      []
                                    |),
                                    [ M.read (| other |) ]
                                  |)
                                ]
                              |)
                            ]
                          |)
                        |),
                        [
                          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::option::Option")
                                            []
                                            [ Ty.path "u16" ],
                                          [
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [ Ty.path "core::convert::Infallible" ]
                                          ],
                                          "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))
                        ]
                      |)
                    |)
                  ]
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
              fn checked_add(&self, other: u32) -> Option<Self> {
                  Self::checked_add( *self, other.try_into().ok()?)
              }
      *)
      Definition checked_add (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.call_closure (|
                  M.get_associated_function (| Ty.path "u16", "checked_add", [] |),
                  [
                    M.read (| M.read (| self |) |);
                    M.read (|
                      M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::try_trait::Try",
                              Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u16" ],
                              [],
                              "branch",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "core::result::Result")
                                    []
                                    [ Ty.path "u16"; Ty.path "core::num::error::TryFromIntError" ],
                                  "ok",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::convert::TryInto",
                                      Ty.path "u32",
                                      [ Ty.path "u16" ],
                                      "try_into",
                                      []
                                    |),
                                    [ M.read (| other |) ]
                                  |)
                                ]
                              |)
                            ]
                          |)
                        |),
                        [
                          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::option::Option")
                                            []
                                            [ Ty.path "u16" ],
                                          [
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [ Ty.path "core::convert::Infallible" ]
                                          ],
                                          "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))
                        ]
                      |)
                    |)
                  ]
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::net::parser::ReadNumberHelper"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("value_ZERO", InstanceField.Constant value_ZERO);
            ("checked_mul", InstanceField.Method checked_mul);
            ("checked_add", InstanceField.Method checked_add)
          ].
    End Impl_core_net_parser_ReadNumberHelper_for_u16.
    
    Module Impl_core_net_parser_ReadNumberHelper_for_u32.
      Definition Self : Ty.t := Ty.path "u32".
      
      (*         const ZERO: Self = 0; *)
      (* Ty.path "u32" *)
      Definition value_ZERO : Value.t :=
        M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U32 0 |))).
      
      (*
              fn checked_mul(&self, other: u32) -> Option<Self> {
                  Self::checked_mul( *self, other.try_into().ok()?)
              }
      *)
      Definition checked_mul (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.call_closure (|
                  M.get_associated_function (| Ty.path "u32", "checked_mul", [] |),
                  [
                    M.read (| M.read (| self |) |);
                    M.read (|
                      M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::try_trait::Try",
                              Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u32" ],
                              [],
                              "branch",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "core::result::Result")
                                    []
                                    [ Ty.path "u32"; Ty.path "core::convert::Infallible" ],
                                  "ok",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::convert::TryInto",
                                      Ty.path "u32",
                                      [ Ty.path "u32" ],
                                      "try_into",
                                      []
                                    |),
                                    [ M.read (| other |) ]
                                  |)
                                ]
                              |)
                            ]
                          |)
                        |),
                        [
                          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::option::Option")
                                            []
                                            [ Ty.path "u32" ],
                                          [
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [ Ty.path "core::convert::Infallible" ]
                                          ],
                                          "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))
                        ]
                      |)
                    |)
                  ]
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
              fn checked_add(&self, other: u32) -> Option<Self> {
                  Self::checked_add( *self, other.try_into().ok()?)
              }
      *)
      Definition checked_add (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.call_closure (|
                  M.get_associated_function (| Ty.path "u32", "checked_add", [] |),
                  [
                    M.read (| M.read (| self |) |);
                    M.read (|
                      M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::try_trait::Try",
                              Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u32" ],
                              [],
                              "branch",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "core::result::Result")
                                    []
                                    [ Ty.path "u32"; Ty.path "core::convert::Infallible" ],
                                  "ok",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::convert::TryInto",
                                      Ty.path "u32",
                                      [ Ty.path "u32" ],
                                      "try_into",
                                      []
                                    |),
                                    [ M.read (| other |) ]
                                  |)
                                ]
                              |)
                            ]
                          |)
                        |),
                        [
                          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::option::Option")
                                            []
                                            [ Ty.path "u32" ],
                                          [
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [ Ty.path "core::convert::Infallible" ]
                                          ],
                                          "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))
                        ]
                      |)
                    |)
                  ]
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::net::parser::ReadNumberHelper"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("value_ZERO", InstanceField.Constant value_ZERO);
            ("checked_mul", InstanceField.Method checked_mul);
            ("checked_add", InstanceField.Method checked_add)
          ].
    End Impl_core_net_parser_ReadNumberHelper_for_u32.
    
    (* StructRecord
      {
        name := "Parser";
        const_params := [];
        ty_params := [];
        fields :=
          [ ("state", Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ])
          ];
      } *)
    
    Module Impl_core_net_parser_Parser.
      Definition Self : Ty.t := Ty.path "core::net::parser::Parser".
      
      (*
          fn new(input: &'a [u8]) -> Parser<'a> {
              Parser { state: input }
          }
      *)
      Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ input ] =>
          ltac:(M.monadic
            (let input := M.alloc (| input |) in
            Value.StructRecord "core::net::parser::Parser" [ ("state", M.read (| input |)) ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
      
      (*
          fn read_atomically<T, F>(&mut self, inner: F) -> Option<T>
          where
              F: FnOnce(&mut Parser<'_>) -> Option<T>,
          {
              let state = self.state;
              let result = inner(self);
              if result.is_none() {
                  self.state = state;
              }
              result
          }
      *)
      Definition read_atomically (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ T; F ], [ self; inner ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let inner := M.alloc (| inner |) in
            M.read (|
              let~ state :=
                M.copy (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::net::parser::Parser",
                    "state"
                  |)
                |) in
              let~ result :=
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::function::FnOnce",
                      F,
                      [
                        Ty.tuple
                          [ Ty.apply (Ty.path "&mut") [] [ Ty.path "core::net::parser::Parser" ] ]
                      ],
                      "call_once",
                      []
                    |),
                    [ M.read (| inner |); Value.Tuple [ M.read (| self |) ] ]
                  |)
                |) in
              let~ _ :=
                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 "core::option::Option") [] [ T ],
                                  "is_none",
                                  []
                                |),
                                [ result ]
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ _ :=
                          M.write (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "core::net::parser::Parser",
                              "state"
                            |),
                            M.read (| state |)
                          |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              result
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_read_atomically :
        M.IsAssociatedFunction Self "read_atomically" read_atomically.
      
      (*
          fn parse_with<T, F>(&mut self, inner: F, kind: AddrKind) -> Result<T, AddrParseError>
          where
              F: FnOnce(&mut Parser<'_>) -> Option<T>,
          {
              let result = inner(self);
              if self.state.is_empty() { result } else { None }.ok_or(AddrParseError(kind))
          }
      *)
      Definition parse_with (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ T; F ], [ self; inner; kind ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let inner := M.alloc (| inner |) in
            let kind := M.alloc (| kind |) in
            M.read (|
              let~ result :=
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::function::FnOnce",
                      F,
                      [
                        Ty.tuple
                          [ Ty.apply (Ty.path "&mut") [] [ Ty.path "core::net::parser::Parser" ] ]
                      ],
                      "call_once",
                      []
                    |),
                    [ M.read (| inner |); Value.Tuple [ M.read (| self |) ] ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::option::Option") [] [ T ],
                    "ok_or",
                    [ Ty.path "core::net::parser::AddrParseError" ]
                  |),
                  [
                    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_empty",
                                        []
                                      |),
                                      [
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "core::net::parser::Parser",
                                            "state"
                                          |)
                                        |)
                                      ]
                                    |)
                                  |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              result));
                          fun γ =>
                            ltac:(M.monadic
                              (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                        ]
                      |)
                    |);
                    Value.StructTuple "core::net::parser::AddrParseError" [ M.read (| kind |) ]
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_parse_with : M.IsAssociatedFunction Self "parse_with" parse_with.
      
      (*
          fn peek_char(&self) -> Option<char> {
              self.state.first().map(|&b| char::from(b))
          }
      *)
      Definition peek_char (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "core::option::Option")
                  []
                  [ Ty.apply (Ty.path "&") [] [ Ty.path "u8" ] ],
                "map",
                [
                  Ty.path "char";
                  Ty.function
                    [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ Ty.path "u8" ] ] ]
                    (Ty.path "char")
                ]
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                    "first",
                    []
                  |),
                  [
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::net::parser::Parser",
                        "state"
                      |)
                    |)
                  ]
                |);
                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 b := M.copy (| γ |) in
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::convert::From",
                                      Ty.path "char",
                                      [ Ty.path "u8" ],
                                      "from",
                                      []
                                    |),
                                    [ M.read (| b |) ]
                                  |)))
                            ]
                          |)))
                      | _ => M.impossible "wrong number of arguments"
                      end))
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_peek_char : M.IsAssociatedFunction Self "peek_char" peek_char.
      
      (*
          fn read_char(&mut self) -> Option<char> {
              self.state.split_first().map(|(&b, tail)| {
                  self.state = tail;
                  char::from(b)
              })
          }
      *)
      Definition read_char (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "core::option::Option")
                  []
                  [
                    Ty.tuple
                      [
                        Ty.apply (Ty.path "&") [] [ Ty.path "u8" ];
                        Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ]
                      ]
                  ],
                "map",
                [
                  Ty.path "char";
                  Ty.function
                    [
                      Ty.tuple
                        [
                          Ty.tuple
                            [
                              Ty.apply (Ty.path "&") [] [ Ty.path "u8" ];
                              Ty.apply
                                (Ty.path "&")
                                []
                                [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ]
                            ]
                        ]
                    ]
                    (Ty.path "char")
                ]
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                    "split_first",
                    []
                  |),
                  [
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::net::parser::Parser",
                        "state"
                      |)
                    |)
                  ]
                |);
                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 γ0_0 := M.read (| γ0_0 |) in
                                  let b := M.copy (| γ0_0 |) in
                                  let tail := M.copy (| γ0_1 |) in
                                  M.read (|
                                    let~ _ :=
                                      M.write (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "core::net::parser::Parser",
                                          "state"
                                        |),
                                        M.read (| tail |)
                                      |) in
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::convert::From",
                                          Ty.path "char",
                                          [ Ty.path "u8" ],
                                          "from",
                                          []
                                        |),
                                        [ M.read (| b |) ]
                                      |)
                                    |)
                                  |)))
                            ]
                          |)))
                      | _ => M.impossible "wrong number of arguments"
                      end))
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_read_char : M.IsAssociatedFunction Self "read_char" read_char.
      
      (*
          fn read_given_char(&mut self, target: char) -> Option<()> {
              self.read_atomically(|p| {
                  p.read_char().and_then(|c| if c == target { Some(()) } else { None })
              })
          }
      *)
      Definition read_given_char (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; target ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let target := M.alloc (| target |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "core::net::parser::Parser",
                "read_atomically",
                [
                  Ty.tuple [];
                  Ty.function
                    [
                      Ty.tuple
                        [ Ty.apply (Ty.path "&mut") [] [ Ty.path "core::net::parser::Parser" ] ]
                    ]
                    (Ty.apply (Ty.path "core::option::Option") [] [ Ty.tuple [] ])
                ]
              |),
              [
                M.read (| self |);
                M.closure
                  (fun γ =>
                    ltac:(M.monadic
                      match γ with
                      | [ α0 ] =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| α0 |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let p := M.copy (| γ |) in
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "core::option::Option")
                                        []
                                        [ Ty.path "char" ],
                                      "and_then",
                                      [
                                        Ty.tuple [];
                                        Ty.function
                                          [ Ty.tuple [ Ty.path "char" ] ]
                                          (Ty.apply
                                            (Ty.path "core::option::Option")
                                            []
                                            [ Ty.tuple [] ])
                                      ]
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "core::net::parser::Parser",
                                          "read_char",
                                          []
                                        |),
                                        [ M.read (| p |) ]
                                      |);
                                      M.closure
                                        (fun γ =>
                                          ltac:(M.monadic
                                            match γ with
                                            | [ α0 ] =>
                                              ltac:(M.monadic
                                                (M.match_operator (|
                                                  M.alloc (| α0 |),
                                                  [
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (let c := M.copy (| γ |) in
                                                        M.read (|
                                                          M.match_operator (|
                                                            M.alloc (| Value.Tuple [] |),
                                                            [
                                                              fun γ =>
                                                                ltac:(M.monadic
                                                                  (let γ :=
                                                                    M.use
                                                                      (M.alloc (|
                                                                        BinOp.eq (|
                                                                          M.read (| c |),
                                                                          M.read (| target |)
                                                                        |)
                                                                      |)) in
                                                                  let _ :=
                                                                    M.is_constant_or_break_match (|
                                                                      M.read (| γ |),
                                                                      Value.Bool true
                                                                    |) in
                                                                  M.alloc (|
                                                                    Value.StructTuple
                                                                      "core::option::Option::Some"
                                                                      [ Value.Tuple [] ]
                                                                  |)));
                                                              fun γ =>
                                                                ltac:(M.monadic
                                                                  (M.alloc (|
                                                                    Value.StructTuple
                                                                      "core::option::Option::None"
                                                                      []
                                                                  |)))
                                                            ]
                                                          |)
                                                        |)))
                                                  ]
                                                |)))
                                            | _ => M.impossible "wrong number of arguments"
                                            end))
                                    ]
                                  |)))
                            ]
                          |)))
                      | _ => M.impossible "wrong number of arguments"
                      end))
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_read_given_char :
        M.IsAssociatedFunction Self "read_given_char" read_given_char.
      
      (*
          fn read_separator<T, F>(&mut self, sep: char, index: usize, inner: F) -> Option<T>
          where
              F: FnOnce(&mut Parser<'_>) -> Option<T>,
          {
              self.read_atomically(move |p| {
                  if index > 0 {
                      p.read_given_char(sep)?;
                  }
                  inner(p)
              })
          }
      *)
      Definition read_separator (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ T; F ], [ self; sep; index; inner ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let sep := M.alloc (| sep |) in
            let index := M.alloc (| index |) in
            let inner := M.alloc (| inner |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "core::net::parser::Parser",
                "read_atomically",
                [
                  T;
                  Ty.function
                    [
                      Ty.tuple
                        [ Ty.apply (Ty.path "&mut") [] [ Ty.path "core::net::parser::Parser" ] ]
                    ]
                    (Ty.apply (Ty.path "core::option::Option") [] [ T ])
                ]
              |),
              [
                M.read (| self |);
                M.closure
                  (fun γ =>
                    ltac:(M.monadic
                      match γ with
                      | [ α0 ] =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| α0 |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let p := M.copy (| γ |) in
                                  M.read (|
                                    let~ _ :=
                                      M.match_operator (|
                                        M.alloc (| Value.Tuple [] |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let γ :=
                                                M.use
                                                  (M.alloc (|
                                                    BinOp.gt (|
                                                      M.read (| index |),
                                                      Value.Integer IntegerKind.Usize 0
                                                    |)
                                                  |)) in
                                              let _ :=
                                                M.is_constant_or_break_match (|
                                                  M.read (| γ |),
                                                  Value.Bool true
                                                |) in
                                              let~ _ :=
                                                M.match_operator (|
                                                  M.alloc (|
                                                    M.call_closure (|
                                                      M.get_trait_method (|
                                                        "core::ops::try_trait::Try",
                                                        Ty.apply
                                                          (Ty.path "core::option::Option")
                                                          []
                                                          [ Ty.tuple [] ],
                                                        [],
                                                        "branch",
                                                        []
                                                      |),
                                                      [
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.path "core::net::parser::Parser",
                                                            "read_given_char",
                                                            []
                                                          |),
                                                          [ M.read (| p |); M.read (| sep |) ]
                                                        |)
                                                      ]
                                                    |)
                                                  |),
                                                  [
                                                    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::option::Option")
                                                                      []
                                                                      [ T ],
                                                                    [
                                                                      Ty.apply
                                                                        (Ty.path
                                                                          "core::option::Option")
                                                                        []
                                                                        [
                                                                          Ty.path
                                                                            "core::convert::Infallible"
                                                                        ]
                                                                    ],
                                                                    "from_residual",
                                                                    []
                                                                  |),
                                                                  [ M.read (| residual |) ]
                                                                |)
                                                              |)
                                                            |)
                                                          |)
                                                        |)));
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (let γ0_0 :=
                                                          M.SubPointer.get_struct_tuple_field (|
                                                            γ,
                                                            "core::ops::control_flow::ControlFlow::Continue",
                                                            0
                                                          |) in
                                                        let val := M.copy (| γ0_0 |) in
                                                        val))
                                                  ]
                                                |) in
                                              M.alloc (| Value.Tuple [] |)));
                                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                        ]
                                      |) in
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::ops::function::FnOnce",
                                          F,
                                          [
                                            Ty.tuple
                                              [
                                                Ty.apply
                                                  (Ty.path "&mut")
                                                  []
                                                  [ Ty.path "core::net::parser::Parser" ]
                                              ]
                                          ],
                                          "call_once",
                                          []
                                        |),
                                        [ M.read (| inner |); Value.Tuple [ M.read (| p |) ] ]
                                      |)
                                    |)
                                  |)))
                            ]
                          |)))
                      | _ => M.impossible "wrong number of arguments"
                      end))
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_read_separator :
        M.IsAssociatedFunction Self "read_separator" read_separator.
      
      (*
          fn read_number<T: ReadNumberHelper + TryFrom<u32>>(
              &mut self,
              radix: u32,
              max_digits: Option<usize>,
              allow_zero_prefix: bool,
          ) -> Option<T> {
              self.read_atomically(move |p| {
                  let mut digit_count = 0;
                  let has_leading_zero = p.peek_char() == Some('0');
      
                  // If max_digits.is_some(), then we are parsing a `u8` or `u16` and
                  // don't need to use checked arithmetic since it fits within a `u32`.
                  let result = if let Some(max_digits) = max_digits {
                      // u32::MAX = 4_294_967_295u32, which is 10 digits long.
                      // `max_digits` must be less than 10 to not overflow a `u32`.
                      debug_assert!(max_digits < 10);
      
                      let mut result = 0_u32;
                      while let Some(digit) = p.read_atomically(|p| p.read_char()?.to_digit(radix)) {
                          result *= radix;
                          result += digit;
                          digit_count += 1;
      
                          if digit_count > max_digits {
                              return None;
                          }
                      }
      
                      result.try_into().ok()
                  } else {
                      let mut result = T::ZERO;
      
                      while let Some(digit) = p.read_atomically(|p| p.read_char()?.to_digit(radix)) {
                          result = result.checked_mul(radix)?;
                          result = result.checked_add(digit)?;
                          digit_count += 1;
                      }
      
                      Some(result)
                  };
      
                  if digit_count == 0 {
                      None
                  } else if !allow_zero_prefix && has_leading_zero && digit_count > 1 {
                      None
                  } else {
                      result
                  }
              })
          }
      *)
      Definition read_number (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ T ], [ self; radix; max_digits; allow_zero_prefix ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let radix := M.alloc (| radix |) in
            let max_digits := M.alloc (| max_digits |) in
            let allow_zero_prefix := M.alloc (| allow_zero_prefix |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "core::net::parser::Parser",
                "read_atomically",
                [
                  T;
                  Ty.function
                    [
                      Ty.tuple
                        [ Ty.apply (Ty.path "&mut") [] [ Ty.path "core::net::parser::Parser" ] ]
                    ]
                    (Ty.apply (Ty.path "core::option::Option") [] [ T ])
                ]
              |),
              [
                M.read (| self |);
                M.closure
                  (fun γ =>
                    ltac:(M.monadic
                      match γ with
                      | [ α0 ] =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| α0 |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let p := M.copy (| γ |) in
                                  M.read (|
                                    let~ digit_count :=
                                      M.alloc (| Value.Integer IntegerKind.Usize 0 |) in
                                    let~ has_leading_zero :=
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::cmp::PartialEq",
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [ Ty.path "char" ],
                                            [
                                              Ty.apply
                                                (Ty.path "core::option::Option")
                                                []
                                                [ Ty.path "char" ]
                                            ],
                                            "eq",
                                            []
                                          |),
                                          [
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path "core::net::parser::Parser",
                                                  "peek_char",
                                                  []
                                                |),
                                                [ M.read (| p |) ]
                                              |)
                                            |);
                                            M.alloc (|
                                              Value.StructTuple
                                                "core::option::Option::Some"
                                                [ Value.UnicodeChar 48 ]
                                            |)
                                          ]
                                        |)
                                      |) in
                                    let~ result :=
                                      M.copy (|
                                        M.match_operator (|
                                          M.alloc (| Value.Tuple [] |),
                                          [
                                            fun γ =>
                                              ltac:(M.monadic
                                                (let γ := max_digits in
                                                let γ0_0 :=
                                                  M.SubPointer.get_struct_tuple_field (|
                                                    γ,
                                                    "core::option::Option::Some",
                                                    0
                                                  |) in
                                                let max_digits := M.copy (| γ0_0 |) 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.lt (|
                                                                              M.read (|
                                                                                max_digits
                                                                              |),
                                                                              Value.Integer
                                                                                IntegerKind.Usize
                                                                                10
                                                                            |)
                                                                          |)
                                                                        |)) 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: max_digits < 10"
                                                                            |)
                                                                          ]
                                                                        |)
                                                                      |)
                                                                    |)));
                                                                fun γ =>
                                                                  ltac:(M.monadic
                                                                    (M.alloc (| Value.Tuple [] |)))
                                                              ]
                                                            |) in
                                                          M.alloc (| Value.Tuple [] |)));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (M.alloc (| Value.Tuple [] |)))
                                                    ]
                                                  |) in
                                                let~ result :=
                                                  M.alloc (| Value.Integer IntegerKind.U32 0 |) in
                                                let~ _ :=
                                                  M.loop (|
                                                    ltac:(M.monadic
                                                      (M.match_operator (|
                                                        M.alloc (| Value.Tuple [] |),
                                                        [
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ :=
                                                                M.alloc (|
                                                                  M.call_closure (|
                                                                    M.get_associated_function (|
                                                                      Ty.path
                                                                        "core::net::parser::Parser",
                                                                      "read_atomically",
                                                                      [
                                                                        Ty.path "u32";
                                                                        Ty.function
                                                                          [
                                                                            Ty.tuple
                                                                              [
                                                                                Ty.apply
                                                                                  (Ty.path "&mut")
                                                                                  []
                                                                                  [
                                                                                    Ty.path
                                                                                      "core::net::parser::Parser"
                                                                                  ]
                                                                              ]
                                                                          ]
                                                                          (Ty.apply
                                                                            (Ty.path
                                                                              "core::option::Option")
                                                                            []
                                                                            [ Ty.path "u32" ])
                                                                      ]
                                                                    |),
                                                                    [
                                                                      M.read (| p |);
                                                                      M.closure
                                                                        (fun γ =>
                                                                          ltac:(M.monadic
                                                                            match γ with
                                                                            | [ α0 ] =>
                                                                              ltac:(M.monadic
                                                                                (M.match_operator (|
                                                                                  M.alloc (| α0 |),
                                                                                  [
                                                                                    fun γ =>
                                                                                      ltac:(M.monadic
                                                                                        (let p :=
                                                                                          M.copy (|
                                                                                            γ
                                                                                          |) in
                                                                                        M.call_closure (|
                                                                                          M.get_associated_function (|
                                                                                            Ty.path
                                                                                              "char",
                                                                                            "to_digit",
                                                                                            []
                                                                                          |),
                                                                                          [
                                                                                            M.read (|
                                                                                              M.match_operator (|
                                                                                                M.alloc (|
                                                                                                  M.call_closure (|
                                                                                                    M.get_trait_method (|
                                                                                                      "core::ops::try_trait::Try",
                                                                                                      Ty.apply
                                                                                                        (Ty.path
                                                                                                          "core::option::Option")
                                                                                                        []
                                                                                                        [
                                                                                                          Ty.path
                                                                                                            "char"
                                                                                                        ],
                                                                                                      [],
                                                                                                      "branch",
                                                                                                      []
                                                                                                    |),
                                                                                                    [
                                                                                                      M.call_closure (|
                                                                                                        M.get_associated_function (|
                                                                                                          Ty.path
                                                                                                            "core::net::parser::Parser",
                                                                                                          "read_char",
                                                                                                          []
                                                                                                        |),
                                                                                                        [
                                                                                                          M.read (|
                                                                                                            p
                                                                                                          |)
                                                                                                        ]
                                                                                                      |)
                                                                                                    ]
                                                                                                  |)
                                                                                                |),
                                                                                                [
                                                                                                  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::option::Option")
                                                                                                                    []
                                                                                                                    [
                                                                                                                      Ty.path
                                                                                                                        "u32"
                                                                                                                    ],
                                                                                                                  [
                                                                                                                    Ty.apply
                                                                                                                      (Ty.path
                                                                                                                        "core::option::Option")
                                                                                                                      []
                                                                                                                      [
                                                                                                                        Ty.path
                                                                                                                          "core::convert::Infallible"
                                                                                                                      ]
                                                                                                                  ],
                                                                                                                  "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))
                                                                                                ]
                                                                                              |)
                                                                                            |);
                                                                                            M.read (|
                                                                                              radix
                                                                                            |)
                                                                                          ]
                                                                                        |)))
                                                                                  ]
                                                                                |)))
                                                                            | _ =>
                                                                              M.impossible
                                                                                "wrong number of arguments"
                                                                            end))
                                                                    ]
                                                                  |)
                                                                |) in
                                                              let γ0_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "core::option::Option::Some",
                                                                  0
                                                                |) in
                                                              let digit := M.copy (| γ0_0 |) in
                                                              let~ _ :=
                                                                let β := result in
                                                                M.write (|
                                                                  β,
                                                                  BinOp.Wrap.mul (|
                                                                    M.read (| β |),
                                                                    M.read (| radix |)
                                                                  |)
                                                                |) in
                                                              let~ _ :=
                                                                let β := result in
                                                                M.write (|
                                                                  β,
                                                                  BinOp.Wrap.add (|
                                                                    M.read (| β |),
                                                                    M.read (| digit |)
                                                                  |)
                                                                |) in
                                                              let~ _ :=
                                                                let β := digit_count in
                                                                M.write (|
                                                                  β,
                                                                  BinOp.Wrap.add (|
                                                                    M.read (| β |),
                                                                    Value.Integer
                                                                      IntegerKind.Usize
                                                                      1
                                                                  |)
                                                                |) in
                                                              M.match_operator (|
                                                                M.alloc (| Value.Tuple [] |),
                                                                [
                                                                  fun γ =>
                                                                    ltac:(M.monadic
                                                                      (let γ :=
                                                                        M.use
                                                                          (M.alloc (|
                                                                            BinOp.gt (|
                                                                              M.read (|
                                                                                digit_count
                                                                              |),
                                                                              M.read (|
                                                                                max_digits
                                                                              |)
                                                                            |)
                                                                          |)) in
                                                                      let _ :=
                                                                        M.is_constant_or_break_match (|
                                                                          M.read (| γ |),
                                                                          Value.Bool true
                                                                        |) in
                                                                      M.alloc (|
                                                                        M.never_to_any (|
                                                                          M.read (|
                                                                            M.return_ (|
                                                                              Value.StructTuple
                                                                                "core::option::Option::None"
                                                                                []
                                                                            |)
                                                                          |)
                                                                        |)
                                                                      |)));
                                                                  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
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.apply
                                                        (Ty.path "core::result::Result")
                                                        []
                                                        [ T; Ty.associated ],
                                                      "ok",
                                                      []
                                                    |),
                                                    [
                                                      M.call_closure (|
                                                        M.get_trait_method (|
                                                          "core::convert::TryInto",
                                                          Ty.path "u32",
                                                          [ T ],
                                                          "try_into",
                                                          []
                                                        |),
                                                        [ M.read (| result |) ]
                                                      |)
                                                    ]
                                                  |)
                                                |)));
                                            fun γ =>
                                              ltac:(M.monadic
                                                (let~ result :=
                                                  M.copy (|
                                                    M.get_constant (|
                                                      "core::net::parser::ReadNumberHelper::ZERO"
                                                    |)
                                                  |) in
                                                let~ _ :=
                                                  M.loop (|
                                                    ltac:(M.monadic
                                                      (M.match_operator (|
                                                        M.alloc (| Value.Tuple [] |),
                                                        [
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ :=
                                                                M.alloc (|
                                                                  M.call_closure (|
                                                                    M.get_associated_function (|
                                                                      Ty.path
                                                                        "core::net::parser::Parser",
                                                                      "read_atomically",
                                                                      [
                                                                        Ty.path "u32";
                                                                        Ty.function
                                                                          [
                                                                            Ty.tuple
                                                                              [
                                                                                Ty.apply
                                                                                  (Ty.path "&mut")
                                                                                  []
                                                                                  [
                                                                                    Ty.path
                                                                                      "core::net::parser::Parser"
                                                                                  ]
                                                                              ]
                                                                          ]
                                                                          (Ty.apply
                                                                            (Ty.path
                                                                              "core::option::Option")
                                                                            []
                                                                            [ Ty.path "u32" ])
                                                                      ]
                                                                    |),
                                                                    [
                                                                      M.read (| p |);
                                                                      M.closure
                                                                        (fun γ =>
                                                                          ltac:(M.monadic
                                                                            match γ with
                                                                            | [ α0 ] =>
                                                                              ltac:(M.monadic
                                                                                (M.match_operator (|
                                                                                  M.alloc (| α0 |),
                                                                                  [
                                                                                    fun γ =>
                                                                                      ltac:(M.monadic
                                                                                        (let p :=
                                                                                          M.copy (|
                                                                                            γ
                                                                                          |) in
                                                                                        M.call_closure (|
                                                                                          M.get_associated_function (|
                                                                                            Ty.path
                                                                                              "char",
                                                                                            "to_digit",
                                                                                            []
                                                                                          |),
                                                                                          [
                                                                                            M.read (|
                                                                                              M.match_operator (|
                                                                                                M.alloc (|
                                                                                                  M.call_closure (|
                                                                                                    M.get_trait_method (|
                                                                                                      "core::ops::try_trait::Try",
                                                                                                      Ty.apply
                                                                                                        (Ty.path
                                                                                                          "core::option::Option")
                                                                                                        []
                                                                                                        [
                                                                                                          Ty.path
                                                                                                            "char"
                                                                                                        ],
                                                                                                      [],
                                                                                                      "branch",
                                                                                                      []
                                                                                                    |),
                                                                                                    [
                                                                                                      M.call_closure (|
                                                                                                        M.get_associated_function (|
                                                                                                          Ty.path
                                                                                                            "core::net::parser::Parser",
                                                                                                          "read_char",
                                                                                                          []
                                                                                                        |),
                                                                                                        [
                                                                                                          M.read (|
                                                                                                            p
                                                                                                          |)
                                                                                                        ]
                                                                                                      |)
                                                                                                    ]
                                                                                                  |)
                                                                                                |),
                                                                                                [
                                                                                                  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::option::Option")
                                                                                                                    []
                                                                                                                    [
                                                                                                                      Ty.path
                                                                                                                        "u32"
                                                                                                                    ],
                                                                                                                  [
                                                                                                                    Ty.apply
                                                                                                                      (Ty.path
                                                                                                                        "core::option::Option")
                                                                                                                      []
                                                                                                                      [
                                                                                                                        Ty.path
                                                                                                                          "core::convert::Infallible"
                                                                                                                      ]
                                                                                                                  ],
                                                                                                                  "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))
                                                                                                ]
                                                                                              |)
                                                                                            |);
                                                                                            M.read (|
                                                                                              radix
                                                                                            |)
                                                                                          ]
                                                                                        |)))
                                                                                  ]
                                                                                |)))
                                                                            | _ =>
                                                                              M.impossible
                                                                                "wrong number of arguments"
                                                                            end))
                                                                    ]
                                                                  |)
                                                                |) in
                                                              let γ0_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "core::option::Option::Some",
                                                                  0
                                                                |) in
                                                              let digit := M.copy (| γ0_0 |) in
                                                              let~ _ :=
                                                                M.write (|
                                                                  result,
                                                                  M.read (|
                                                                    M.match_operator (|
                                                                      M.alloc (|
                                                                        M.call_closure (|
                                                                          M.get_trait_method (|
                                                                            "core::ops::try_trait::Try",
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "core::option::Option")
                                                                              []
                                                                              [ T ],
                                                                            [],
                                                                            "branch",
                                                                            []
                                                                          |),
                                                                          [
                                                                            M.call_closure (|
                                                                              M.get_trait_method (|
                                                                                "core::net::parser::ReadNumberHelper",
                                                                                T,
                                                                                [],
                                                                                "checked_mul",
                                                                                []
                                                                              |),
                                                                              [
                                                                                result;
                                                                                M.read (| radix |)
                                                                              ]
                                                                            |)
                                                                          ]
                                                                        |)
                                                                      |),
                                                                      [
                                                                        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::option::Option")
                                                                                          []
                                                                                          [ T ],
                                                                                        [
                                                                                          Ty.apply
                                                                                            (Ty.path
                                                                                              "core::option::Option")
                                                                                            []
                                                                                            [
                                                                                              Ty.path
                                                                                                "core::convert::Infallible"
                                                                                            ]
                                                                                        ],
                                                                                        "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 (|
                                                                  result,
                                                                  M.read (|
                                                                    M.match_operator (|
                                                                      M.alloc (|
                                                                        M.call_closure (|
                                                                          M.get_trait_method (|
                                                                            "core::ops::try_trait::Try",
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "core::option::Option")
                                                                              []
                                                                              [ T ],
                                                                            [],
                                                                            "branch",
                                                                            []
                                                                          |),
                                                                          [
                                                                            M.call_closure (|
                                                                              M.get_trait_method (|
                                                                                "core::net::parser::ReadNumberHelper",
                                                                                T,
                                                                                [],
                                                                                "checked_add",
                                                                                []
                                                                              |),
                                                                              [
                                                                                result;
                                                                                M.read (| digit |)
                                                                              ]
                                                                            |)
                                                                          ]
                                                                        |)
                                                                      |),
                                                                      [
                                                                        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::option::Option")
                                                                                          []
                                                                                          [ T ],
                                                                                        [
                                                                                          Ty.apply
                                                                                            (Ty.path
                                                                                              "core::option::Option")
                                                                                            []
                                                                                            [
                                                                                              Ty.path
                                                                                                "core::convert::Infallible"
                                                                                            ]
                                                                                        ],
                                                                                        "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~ _ :=
                                                                let β := digit_count in
                                                                M.write (|
                                                                  β,
                                                                  BinOp.Wrap.add (|
                                                                    M.read (| β |),
                                                                    Value.Integer
                                                                      IntegerKind.Usize
                                                                      1
                                                                  |)
                                                                |) in
                                                              M.alloc (| Value.Tuple [] |)));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (M.alloc (|
                                                                M.never_to_any (|
                                                                  M.read (|
                                                                    let~ _ :=
                                                                      M.alloc (|
                                                                        M.never_to_any (|
                                                                          M.read (| M.break (||) |)
                                                                        |)
                                                                      |) in
                                                                    M.alloc (| Value.Tuple [] |)
                                                                  |)
                                                                |)
                                                              |)))
                                                        ]
                                                      |)))
                                                  |) in
                                                M.alloc (|
                                                  Value.StructTuple
                                                    "core::option::Option::Some"
                                                    [ M.read (| result |) ]
                                                |)))
                                          ]
                                        |)
                                      |) in
                                    M.match_operator (|
                                      M.alloc (| Value.Tuple [] |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ :=
                                              M.use
                                                (M.alloc (|
                                                  BinOp.eq (|
                                                    M.read (| digit_count |),
                                                    Value.Integer IntegerKind.Usize 0
                                                  |)
                                                |)) in
                                            let _ :=
                                              M.is_constant_or_break_match (|
                                                M.read (| γ |),
                                                Value.Bool true
                                              |) in
                                            M.alloc (|
                                              Value.StructTuple "core::option::Option::None" []
                                            |)));
                                        fun γ =>
                                          ltac:(M.monadic
                                            (M.match_operator (|
                                              M.alloc (| Value.Tuple [] |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let γ :=
                                                      M.use
                                                        (M.alloc (|
                                                          LogicalOp.and (|
                                                            LogicalOp.and (|
                                                              UnOp.not (|
                                                                M.read (| allow_zero_prefix |)
                                                              |),
                                                              ltac:(M.monadic
                                                                (M.read (| has_leading_zero |)))
                                                            |),
                                                            ltac:(M.monadic
                                                              (BinOp.gt (|
                                                                M.read (| digit_count |),
                                                                Value.Integer IntegerKind.Usize 1
                                                              |)))
                                                          |)
                                                        |)) in
                                                    let _ :=
                                                      M.is_constant_or_break_match (|
                                                        M.read (| γ |),
                                                        Value.Bool true
                                                      |) in
                                                    M.alloc (|
                                                      Value.StructTuple
                                                        "core::option::Option::None"
                                                        []
                                                    |)));
                                                fun γ => ltac:(M.monadic result)
                                              ]
                                            |)))
                                      ]
                                    |)
                                  |)))
                            ]
                          |)))
                      | _ => M.impossible "wrong number of arguments"
                      end))
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_read_number : M.IsAssociatedFunction Self "read_number" read_number.
      
      (*
          fn read_ipv4_addr(&mut self) -> Option<Ipv4Addr> {
              self.read_atomically(|p| {
                  let mut groups = [0; 4];
      
                  for (i, slot) in groups.iter_mut().enumerate() {
                      *slot = p.read_separator('.', i, |p| {
                          // Disallow octal number in IP string.
                          // https://tools.ietf.org/html/rfc6943#section-3.1.1
                          p.read_number(10, Some(3), false)
                      })?;
                  }
      
                  Some(groups.into())
              })
          }
      *)
      Definition read_ipv4_addr (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "core::net::parser::Parser",
                "read_atomically",
                [
                  Ty.path "core::net::ip_addr::Ipv4Addr";
                  Ty.function
                    [
                      Ty.tuple
                        [ Ty.apply (Ty.path "&mut") [] [ Ty.path "core::net::parser::Parser" ] ]
                    ]
                    (Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [ Ty.path "core::net::ip_addr::Ipv4Addr" ])
                ]
              |),
              [
                M.read (| self |);
                M.closure
                  (fun γ =>
                    ltac:(M.monadic
                      match γ with
                      | [ α0 ] =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| α0 |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let p := M.copy (| γ |) in
                                  M.read (|
                                    let~ groups :=
                                      M.alloc (|
                                        repeat (|
                                          Value.Integer IntegerKind.U8 0,
                                          Value.Integer IntegerKind.Usize 4
                                        |)
                                      |) in
                                    let~ _ :=
                                      M.use
                                        (M.match_operator (|
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::iter::traits::collect::IntoIterator",
                                                Ty.apply
                                                  (Ty.path
                                                    "core::iter::adapters::enumerate::Enumerate")
                                                  []
                                                  [
                                                    Ty.apply
                                                      (Ty.path "core::slice::iter::IterMut")
                                                      []
                                                      [ Ty.path "u8" ]
                                                  ],
                                                [],
                                                "into_iter",
                                                []
                                              |),
                                              [
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::iter::traits::iterator::Iterator",
                                                    Ty.apply
                                                      (Ty.path "core::slice::iter::IterMut")
                                                      []
                                                      [ Ty.path "u8" ],
                                                    [],
                                                    "enumerate",
                                                    []
                                                  |),
                                                  [
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.apply
                                                          (Ty.path "slice")
                                                          []
                                                          [ Ty.path "u8" ],
                                                        "iter_mut",
                                                        []
                                                      |),
                                                      [ groups ]
                                                    |)
                                                  ]
                                                |)
                                              ]
                                            |)
                                          |),
                                          [
                                            fun γ =>
                                              ltac:(M.monadic
                                                (let iter := M.copy (| γ |) in
                                                M.loop (|
                                                  ltac:(M.monadic
                                                    (let~ _ :=
                                                      M.match_operator (|
                                                        M.alloc (|
                                                          M.call_closure (|
                                                            M.get_trait_method (|
                                                              "core::iter::traits::iterator::Iterator",
                                                              Ty.apply
                                                                (Ty.path
                                                                  "core::iter::adapters::enumerate::Enumerate")
                                                                []
                                                                [
                                                                  Ty.apply
                                                                    (Ty.path
                                                                      "core::slice::iter::IterMut")
                                                                    []
                                                                    [ Ty.path "u8" ]
                                                                ],
                                                              [],
                                                              "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 γ1_0 :=
                                                                M.SubPointer.get_tuple_field (|
                                                                  γ0_0,
                                                                  0
                                                                |) in
                                                              let γ1_1 :=
                                                                M.SubPointer.get_tuple_field (|
                                                                  γ0_0,
                                                                  1
                                                                |) in
                                                              let i := M.copy (| γ1_0 |) in
                                                              let slot := M.copy (| γ1_1 |) in
                                                              let~ _ :=
                                                                M.write (|
                                                                  M.read (| slot |),
                                                                  M.read (|
                                                                    M.match_operator (|
                                                                      M.alloc (|
                                                                        M.call_closure (|
                                                                          M.get_trait_method (|
                                                                            "core::ops::try_trait::Try",
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "core::option::Option")
                                                                              []
                                                                              [ Ty.path "u8" ],
                                                                            [],
                                                                            "branch",
                                                                            []
                                                                          |),
                                                                          [
                                                                            M.call_closure (|
                                                                              M.get_associated_function (|
                                                                                Ty.path
                                                                                  "core::net::parser::Parser",
                                                                                "read_separator",
                                                                                [
                                                                                  Ty.path "u8";
                                                                                  Ty.function
                                                                                    [
                                                                                      Ty.tuple
                                                                                        [
                                                                                          Ty.apply
                                                                                            (Ty.path
                                                                                              "&mut")
                                                                                            []
                                                                                            [
                                                                                              Ty.path
                                                                                                "core::net::parser::Parser"
                                                                                            ]
                                                                                        ]
                                                                                    ]
                                                                                    (Ty.apply
                                                                                      (Ty.path
                                                                                        "core::option::Option")
                                                                                      []
                                                                                      [ Ty.path "u8"
                                                                                      ])
                                                                                ]
                                                                              |),
                                                                              [
                                                                                M.read (| p |);
                                                                                Value.UnicodeChar
                                                                                  46;
                                                                                M.read (| i |);
                                                                                M.closure
                                                                                  (fun γ =>
                                                                                    ltac:(M.monadic
                                                                                      match γ with
                                                                                      | [ α0 ] =>
                                                                                        ltac:(M.monadic
                                                                                          (M.match_operator (|
                                                                                            M.alloc (|
                                                                                              α0
                                                                                            |),
                                                                                            [
                                                                                              fun
                                                                                                  γ =>
                                                                                                ltac:(M.monadic
                                                                                                  (let
                                                                                                        p :=
                                                                                                    M.copy (|
                                                                                                      γ
                                                                                                    |) in
                                                                                                  M.call_closure (|
                                                                                                    M.get_associated_function (|
                                                                                                      Ty.path
                                                                                                        "core::net::parser::Parser",
                                                                                                      "read_number",
                                                                                                      [
                                                                                                        Ty.path
                                                                                                          "u8"
                                                                                                      ]
                                                                                                    |),
                                                                                                    [
                                                                                                      M.read (|
                                                                                                        p
                                                                                                      |);
                                                                                                      Value.Integer
                                                                                                        IntegerKind.U32
                                                                                                        10;
                                                                                                      Value.StructTuple
                                                                                                        "core::option::Option::Some"
                                                                                                        [
                                                                                                          Value.Integer
                                                                                                            IntegerKind.Usize
                                                                                                            3
                                                                                                        ];
                                                                                                      Value.Bool
                                                                                                        false
                                                                                                    ]
                                                                                                  |)))
                                                                                            ]
                                                                                          |)))
                                                                                      | _ =>
                                                                                        M.impossible
                                                                                          "wrong number of arguments"
                                                                                      end))
                                                                              ]
                                                                            |)
                                                                          ]
                                                                        |)
                                                                      |),
                                                                      [
                                                                        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::option::Option")
                                                                                          []
                                                                                          [
                                                                                            Ty.path
                                                                                              "core::net::ip_addr::Ipv4Addr"
                                                                                          ],
                                                                                        [
                                                                                          Ty.apply
                                                                                            (Ty.path
                                                                                              "core::option::Option")
                                                                                            []
                                                                                            [
                                                                                              Ty.path
                                                                                                "core::convert::Infallible"
                                                                                            ]
                                                                                        ],
                                                                                        "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::option::Option::Some"
                                        [
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::convert::Into",
                                              Ty.apply
                                                (Ty.path "array")
                                                [ Value.Integer IntegerKind.Usize 4 ]
                                                [ Ty.path "u8" ],
                                              [ Ty.path "core::net::ip_addr::Ipv4Addr" ],
                                              "into",
                                              []
                                            |),
                                            [ M.read (| groups |) ]
                                          |)
                                        ]
                                    |)
                                  |)))
                            ]
                          |)))
                      | _ => M.impossible "wrong number of arguments"
                      end))
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_read_ipv4_addr :
        M.IsAssociatedFunction Self "read_ipv4_addr" read_ipv4_addr.
      
      (*
          fn read_ipv6_addr(&mut self) -> Option<Ipv6Addr> {
              /// Read a chunk of an IPv6 address into `groups`. Returns the number
              /// of groups read, along with a bool indicating if an embedded
              /// trailing IPv4 address was read. Specifically, read a series of
              /// colon-separated IPv6 groups (0x0000 - 0xFFFF), with an optional
              /// trailing embedded IPv4 address.
              fn read_groups(p: &mut Parser<'_>, groups: &mut [u16]) -> (usize, bool) {
                  let limit = groups.len();
      
                  for (i, slot) in groups.iter_mut().enumerate() {
                      // Try to read a trailing embedded IPv4 address. There must be
                      // at least two groups left.
                      if i < limit - 1 {
                          let ipv4 = p.read_separator(':', i, |p| p.read_ipv4_addr());
      
                          if let Some(v4_addr) = ipv4 {
                              let [one, two, three, four] = v4_addr.octets();
                              groups[i + 0] = u16::from_be_bytes([one, two]);
                              groups[i + 1] = u16::from_be_bytes([three, four]);
                              return (i + 2, true);
                          }
                      }
      
                      let group = p.read_separator(':', i, |p| p.read_number(16, Some(4), true));
      
                      match group {
                          Some(g) => *slot = g,
                          None => return (i, false),
                      }
                  }
                  (groups.len(), false)
              }
      
              self.read_atomically(|p| {
                  // Read the front part of the address; either the whole thing, or up
                  // to the first ::
                  let mut head = [0; 8];
                  let (head_size, head_ipv4) = read_groups(p, &mut head);
      
                  if head_size == 8 {
                      return Some(head.into());
                  }
      
                  // IPv4 part is not allowed before `::`
                  if head_ipv4 {
                      return None;
                  }
      
                  // Read `::` if previous code parsed less than 8 groups.
                  // `::` indicates one or more groups of 16 bits of zeros.
                  p.read_given_char(':')?;
                  p.read_given_char(':')?;
      
                  // Read the back part of the address. The :: must contain at least one
                  // set of zeroes, so our max length is 7.
                  let mut tail = [0; 7];
                  let limit = 8 - (head_size + 1);
                  let (tail_size, _) = read_groups(p, &mut tail[..limit]);
      
                  // Concat the head and tail of the IP address
                  head[(8 - tail_size)..8].copy_from_slice(&tail[..tail_size]);
      
                  Some(head.into())
              })
          }
      *)
      Definition read_ipv6_addr (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "core::net::parser::Parser",
                "read_atomically",
                [
                  Ty.path "core::net::ip_addr::Ipv6Addr";
                  Ty.function
                    [
                      Ty.tuple
                        [ Ty.apply (Ty.path "&mut") [] [ Ty.path "core::net::parser::Parser" ] ]
                    ]
                    (Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [ Ty.path "core::net::ip_addr::Ipv6Addr" ])
                ]
              |),
              [
                M.read (| self |);
                M.closure
                  (fun γ =>
                    ltac:(M.monadic
                      match γ with
                      | [ α0 ] =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| α0 |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let p := M.copy (| γ |) in
                                  M.read (|
                                    let~ head :=
                                      M.alloc (|
                                        repeat (|
                                          Value.Integer IntegerKind.U16 0,
                                          Value.Integer IntegerKind.Usize 8
                                        |)
                                      |) in
                                    M.match_operator (|
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Self,
                                            "read_groups.read_ipv6_addr",
                                            []
                                          |),
                                          [ M.read (| p |); head ]
                                        |)
                                      |),
                                      [
                                        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 head_size := M.copy (| γ0_0 |) in
                                            let head_ipv4 := M.copy (| γ0_1 |) in
                                            let~ _ :=
                                              M.match_operator (|
                                                M.alloc (| Value.Tuple [] |),
                                                [
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ :=
                                                        M.use
                                                          (M.alloc (|
                                                            BinOp.eq (|
                                                              M.read (| head_size |),
                                                              Value.Integer IntegerKind.Usize 8
                                                            |)
                                                          |)) in
                                                      let _ :=
                                                        M.is_constant_or_break_match (|
                                                          M.read (| γ |),
                                                          Value.Bool true
                                                        |) in
                                                      M.alloc (|
                                                        M.never_to_any (|
                                                          M.read (|
                                                            M.return_ (|
                                                              Value.StructTuple
                                                                "core::option::Option::Some"
                                                                [
                                                                  M.call_closure (|
                                                                    M.get_trait_method (|
                                                                      "core::convert::Into",
                                                                      Ty.apply
                                                                        (Ty.path "array")
                                                                        [
                                                                          Value.Integer
                                                                            IntegerKind.Usize
                                                                            8
                                                                        ]
                                                                        [ Ty.path "u16" ],
                                                                      [
                                                                        Ty.path
                                                                          "core::net::ip_addr::Ipv6Addr"
                                                                      ],
                                                                      "into",
                                                                      []
                                                                    |),
                                                                    [ M.read (| head |) ]
                                                                  |)
                                                                ]
                                                            |)
                                                          |)
                                                        |)
                                                      |)));
                                                  fun γ =>
                                                    ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                                ]
                                              |) in
                                            let~ _ :=
                                              M.match_operator (|
                                                M.alloc (| Value.Tuple [] |),
                                                [
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ := M.use head_ipv4 in
                                                      let _ :=
                                                        M.is_constant_or_break_match (|
                                                          M.read (| γ |),
                                                          Value.Bool true
                                                        |) in
                                                      M.alloc (|
                                                        M.never_to_any (|
                                                          M.read (|
                                                            M.return_ (|
                                                              Value.StructTuple
                                                                "core::option::Option::None"
                                                                []
                                                            |)
                                                          |)
                                                        |)
                                                      |)));
                                                  fun γ =>
                                                    ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                                ]
                                              |) in
                                            let~ _ :=
                                              M.match_operator (|
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_trait_method (|
                                                      "core::ops::try_trait::Try",
                                                      Ty.apply
                                                        (Ty.path "core::option::Option")
                                                        []
                                                        [ Ty.tuple [] ],
                                                      [],
                                                      "branch",
                                                      []
                                                    |),
                                                    [
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path "core::net::parser::Parser",
                                                          "read_given_char",
                                                          []
                                                        |),
                                                        [ M.read (| p |); Value.UnicodeChar 58 ]
                                                      |)
                                                    ]
                                                  |)
                                                |),
                                                [
                                                  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::option::Option")
                                                                    []
                                                                    [
                                                                      Ty.path
                                                                        "core::net::ip_addr::Ipv6Addr"
                                                                    ],
                                                                  [
                                                                    Ty.apply
                                                                      (Ty.path
                                                                        "core::option::Option")
                                                                      []
                                                                      [
                                                                        Ty.path
                                                                          "core::convert::Infallible"
                                                                      ]
                                                                  ],
                                                                  "from_residual",
                                                                  []
                                                                |),
                                                                [ M.read (| residual |) ]
                                                              |)
                                                            |)
                                                          |)
                                                        |)
                                                      |)));
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ0_0 :=
                                                        M.SubPointer.get_struct_tuple_field (|
                                                          γ,
                                                          "core::ops::control_flow::ControlFlow::Continue",
                                                          0
                                                        |) in
                                                      let val := M.copy (| γ0_0 |) in
                                                      val))
                                                ]
                                              |) in
                                            let~ _ :=
                                              M.match_operator (|
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_trait_method (|
                                                      "core::ops::try_trait::Try",
                                                      Ty.apply
                                                        (Ty.path "core::option::Option")
                                                        []
                                                        [ Ty.tuple [] ],
                                                      [],
                                                      "branch",
                                                      []
                                                    |),
                                                    [
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path "core::net::parser::Parser",
                                                          "read_given_char",
                                                          []
                                                        |),
                                                        [ M.read (| p |); Value.UnicodeChar 58 ]
                                                      |)
                                                    ]
                                                  |)
                                                |),
                                                [
                                                  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::option::Option")
                                                                    []
                                                                    [
                                                                      Ty.path
                                                                        "core::net::ip_addr::Ipv6Addr"
                                                                    ],
                                                                  [
                                                                    Ty.apply
                                                                      (Ty.path
                                                                        "core::option::Option")
                                                                      []
                                                                      [
                                                                        Ty.path
                                                                          "core::convert::Infallible"
                                                                      ]
                                                                  ],
                                                                  "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~ tail :=
                                              M.alloc (|
                                                repeat (|
                                                  Value.Integer IntegerKind.U16 0,
                                                  Value.Integer IntegerKind.Usize 7
                                                |)
                                              |) in
                                            let~ limit :=
                                              M.alloc (|
                                                BinOp.Wrap.sub (|
                                                  Value.Integer IntegerKind.Usize 8,
                                                  BinOp.Wrap.add (|
                                                    M.read (| head_size |),
                                                    Value.Integer IntegerKind.Usize 1
                                                  |)
                                                |)
                                              |) in
                                            M.match_operator (|
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Self,
                                                    "read_groups.read_ipv6_addr",
                                                    []
                                                  |),
                                                  [
                                                    M.read (| p |);
                                                    M.call_closure (|
                                                      M.get_trait_method (|
                                                        "core::ops::index::IndexMut",
                                                        Ty.apply
                                                          (Ty.path "array")
                                                          [ Value.Integer IntegerKind.Usize 7 ]
                                                          [ Ty.path "u16" ],
                                                        [
                                                          Ty.apply
                                                            (Ty.path "core::ops::range::RangeTo")
                                                            []
                                                            [ Ty.path "usize" ]
                                                        ],
                                                        "index_mut",
                                                        []
                                                      |),
                                                      [
                                                        tail;
                                                        Value.StructRecord
                                                          "core::ops::range::RangeTo"
                                                          [ ("end_", M.read (| limit |)) ]
                                                      ]
                                                    |)
                                                  ]
                                                |)
                                              |),
                                              [
                                                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 tail_size := M.copy (| γ0_0 |) in
                                                    let~ _ :=
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.apply
                                                              (Ty.path "slice")
                                                              []
                                                              [ Ty.path "u16" ],
                                                            "copy_from_slice",
                                                            []
                                                          |),
                                                          [
                                                            M.call_closure (|
                                                              M.get_trait_method (|
                                                                "core::ops::index::IndexMut",
                                                                Ty.apply
                                                                  (Ty.path "array")
                                                                  [
                                                                    Value.Integer
                                                                      IntegerKind.Usize
                                                                      8
                                                                  ]
                                                                  [ Ty.path "u16" ],
                                                                [
                                                                  Ty.apply
                                                                    (Ty.path
                                                                      "core::ops::range::Range")
                                                                    []
                                                                    [ Ty.path "usize" ]
                                                                ],
                                                                "index_mut",
                                                                []
                                                              |),
                                                              [
                                                                head;
                                                                Value.StructRecord
                                                                  "core::ops::range::Range"
                                                                  [
                                                                    ("start",
                                                                      BinOp.Wrap.sub (|
                                                                        Value.Integer
                                                                          IntegerKind.Usize
                                                                          8,
                                                                        M.read (| tail_size |)
                                                                      |));
                                                                    ("end_",
                                                                      Value.Integer
                                                                        IntegerKind.Usize
                                                                        8)
                                                                  ]
                                                              ]
                                                            |);
                                                            M.call_closure (|
                                                              M.get_trait_method (|
                                                                "core::ops::index::Index",
                                                                Ty.apply
                                                                  (Ty.path "array")
                                                                  [
                                                                    Value.Integer
                                                                      IntegerKind.Usize
                                                                      7
                                                                  ]
                                                                  [ Ty.path "u16" ],
                                                                [
                                                                  Ty.apply
                                                                    (Ty.path
                                                                      "core::ops::range::RangeTo")
                                                                    []
                                                                    [ Ty.path "usize" ]
                                                                ],
                                                                "index",
                                                                []
                                                              |),
                                                              [
                                                                tail;
                                                                Value.StructRecord
                                                                  "core::ops::range::RangeTo"
                                                                  [ ("end_", M.read (| tail_size |))
                                                                  ]
                                                              ]
                                                            |)
                                                          ]
                                                        |)
                                                      |) in
                                                    M.alloc (|
                                                      Value.StructTuple
                                                        "core::option::Option::Some"
                                                        [
                                                          M.call_closure (|
                                                            M.get_trait_method (|
                                                              "core::convert::Into",
                                                              Ty.apply
                                                                (Ty.path "array")
                                                                [ Value.Integer IntegerKind.Usize 8
                                                                ]
                                                                [ Ty.path "u16" ],
                                                              [
                                                                Ty.path
                                                                  "core::net::ip_addr::Ipv6Addr"
                                                              ],
                                                              "into",
                                                              []
                                                            |),
                                                            [ M.read (| head |) ]
                                                          |)
                                                        ]
                                                    |)))
                                              ]
                                            |)))
                                      ]
                                    |)
                                  |)))
                            ]
                          |)))
                      | _ => M.impossible "wrong number of arguments"
                      end))
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_read_ipv6_addr :
        M.IsAssociatedFunction Self "read_ipv6_addr" read_ipv6_addr.
      
      (*
          fn read_ip_addr(&mut self) -> Option<IpAddr> {
              self.read_ipv4_addr().map(IpAddr::V4).or_else(move || self.read_ipv6_addr().map(IpAddr::V6))
          }
      *)
      Definition read_ip_addr (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "core::option::Option")
                  []
                  [ Ty.path "core::net::ip_addr::IpAddr" ],
                "or_else",
                [
                  Ty.function
                    [ Ty.tuple [] ]
                    (Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [ Ty.path "core::net::ip_addr::IpAddr" ])
                ]
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [ Ty.path "core::net::ip_addr::Ipv4Addr" ],
                    "map",
                    [
                      Ty.path "core::net::ip_addr::IpAddr";
                      Ty.function
                        [ Ty.path "core::net::ip_addr::Ipv4Addr" ]
                        (Ty.path "core::net::ip_addr::IpAddr")
                    ]
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "core::net::parser::Parser",
                        "read_ipv4_addr",
                        []
                      |),
                      [ M.read (| self |) ]
                    |);
                    M.constructor_as_closure "core::net::ip_addr::IpAddr::V4"
                  ]
                |);
                M.closure
                  (fun γ =>
                    ltac:(M.monadic
                      match γ with
                      | [ α0 ] =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| α0 |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "core::option::Option")
                                        []
                                        [ Ty.path "core::net::ip_addr::Ipv6Addr" ],
                                      "map",
                                      [
                                        Ty.path "core::net::ip_addr::IpAddr";
                                        Ty.function
                                          [ Ty.path "core::net::ip_addr::Ipv6Addr" ]
                                          (Ty.path "core::net::ip_addr::IpAddr")
                                      ]
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "core::net::parser::Parser",
                                          "read_ipv6_addr",
                                          []
                                        |),
                                        [ M.read (| self |) ]
                                      |);
                                      M.constructor_as_closure "core::net::ip_addr::IpAddr::V6"
                                    ]
                                  |)))
                            ]
                          |)))
                      | _ => M.impossible "wrong number of arguments"
                      end))
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_read_ip_addr :
        M.IsAssociatedFunction Self "read_ip_addr" read_ip_addr.
      
      (*
          fn read_port(&mut self) -> Option<u16> {
              self.read_atomically(|p| {
                  p.read_given_char(':')?;
                  p.read_number(10, None, true)
              })
          }
      *)
      Definition read_port (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "core::net::parser::Parser",
                "read_atomically",
                [
                  Ty.path "u16";
                  Ty.function
                    [
                      Ty.tuple
                        [ Ty.apply (Ty.path "&mut") [] [ Ty.path "core::net::parser::Parser" ] ]
                    ]
                    (Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u16" ])
                ]
              |),
              [
                M.read (| self |);
                M.closure
                  (fun γ =>
                    ltac:(M.monadic
                      match γ with
                      | [ α0 ] =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| α0 |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let p := M.copy (| γ |) in
                                  M.read (|
                                    let~ _ :=
                                      M.match_operator (|
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::ops::try_trait::Try",
                                              Ty.apply
                                                (Ty.path "core::option::Option")
                                                []
                                                [ Ty.tuple [] ],
                                              [],
                                              "branch",
                                              []
                                            |),
                                            [
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path "core::net::parser::Parser",
                                                  "read_given_char",
                                                  []
                                                |),
                                                [ M.read (| p |); Value.UnicodeChar 58 ]
                                              |)
                                            ]
                                          |)
                                        |),
                                        [
                                          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::option::Option")
                                                            []
                                                            [ Ty.path "u16" ],
                                                          [
                                                            Ty.apply
                                                              (Ty.path "core::option::Option")
                                                              []
                                                              [ Ty.path "core::convert::Infallible"
                                                              ]
                                                          ],
                                                          "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 (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "core::net::parser::Parser",
                                          "read_number",
                                          [ Ty.path "u16" ]
                                        |),
                                        [
                                          M.read (| p |);
                                          Value.Integer IntegerKind.U32 10;
                                          Value.StructTuple "core::option::Option::None" [];
                                          Value.Bool true
                                        ]
                                      |)
                                    |)
                                  |)))
                            ]
                          |)))
                      | _ => M.impossible "wrong number of arguments"
                      end))
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_read_port : M.IsAssociatedFunction Self "read_port" read_port.
      
      (*
          fn read_scope_id(&mut self) -> Option<u32> {
              self.read_atomically(|p| {
                  p.read_given_char('%')?;
                  p.read_number(10, None, true)
              })
          }
      *)
      Definition read_scope_id (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "core::net::parser::Parser",
                "read_atomically",
                [
                  Ty.path "u32";
                  Ty.function
                    [
                      Ty.tuple
                        [ Ty.apply (Ty.path "&mut") [] [ Ty.path "core::net::parser::Parser" ] ]
                    ]
                    (Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u32" ])
                ]
              |),
              [
                M.read (| self |);
                M.closure
                  (fun γ =>
                    ltac:(M.monadic
                      match γ with
                      | [ α0 ] =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| α0 |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let p := M.copy (| γ |) in
                                  M.read (|
                                    let~ _ :=
                                      M.match_operator (|
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::ops::try_trait::Try",
                                              Ty.apply
                                                (Ty.path "core::option::Option")
                                                []
                                                [ Ty.tuple [] ],
                                              [],
                                              "branch",
                                              []
                                            |),
                                            [
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path "core::net::parser::Parser",
                                                  "read_given_char",
                                                  []
                                                |),
                                                [ M.read (| p |); Value.UnicodeChar 37 ]
                                              |)
                                            ]
                                          |)
                                        |),
                                        [
                                          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::option::Option")
                                                            []
                                                            [ Ty.path "u32" ],
                                                          [
                                                            Ty.apply
                                                              (Ty.path "core::option::Option")
                                                              []
                                                              [ Ty.path "core::convert::Infallible"
                                                              ]
                                                          ],
                                                          "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 (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "core::net::parser::Parser",
                                          "read_number",
                                          [ Ty.path "u32" ]
                                        |),
                                        [
                                          M.read (| p |);
                                          Value.Integer IntegerKind.U32 10;
                                          Value.StructTuple "core::option::Option::None" [];
                                          Value.Bool true
                                        ]
                                      |)
                                    |)
                                  |)))
                            ]
                          |)))
                      | _ => M.impossible "wrong number of arguments"
                      end))
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_read_scope_id :
        M.IsAssociatedFunction Self "read_scope_id" read_scope_id.
      
      (*
          fn read_socket_addr_v4(&mut self) -> Option<SocketAddrV4> {
              self.read_atomically(|p| {
                  let ip = p.read_ipv4_addr()?;
                  let port = p.read_port()?;
                  Some(SocketAddrV4::new(ip, port))
              })
          }
      *)
      Definition read_socket_addr_v4 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "core::net::parser::Parser",
                "read_atomically",
                [
                  Ty.path "core::net::socket_addr::SocketAddrV4";
                  Ty.function
                    [
                      Ty.tuple
                        [ Ty.apply (Ty.path "&mut") [] [ Ty.path "core::net::parser::Parser" ] ]
                    ]
                    (Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [ Ty.path "core::net::socket_addr::SocketAddrV4" ])
                ]
              |),
              [
                M.read (| self |);
                M.closure
                  (fun γ =>
                    ltac:(M.monadic
                      match γ with
                      | [ α0 ] =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| α0 |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let p := M.copy (| γ |) in
                                  M.read (|
                                    let~ ip :=
                                      M.copy (|
                                        M.match_operator (|
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::ops::try_trait::Try",
                                                Ty.apply
                                                  (Ty.path "core::option::Option")
                                                  []
                                                  [ Ty.path "core::net::ip_addr::Ipv4Addr" ],
                                                [],
                                                "branch",
                                                []
                                              |),
                                              [
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.path "core::net::parser::Parser",
                                                    "read_ipv4_addr",
                                                    []
                                                  |),
                                                  [ M.read (| p |) ]
                                                |)
                                              ]
                                            |)
                                          |),
                                          [
                                            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::option::Option")
                                                              []
                                                              [
                                                                Ty.path
                                                                  "core::net::socket_addr::SocketAddrV4"
                                                              ],
                                                            [
                                                              Ty.apply
                                                                (Ty.path "core::option::Option")
                                                                []
                                                                [
                                                                  Ty.path
                                                                    "core::convert::Infallible"
                                                                ]
                                                            ],
                                                            "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~ port :=
                                      M.copy (|
                                        M.match_operator (|
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::ops::try_trait::Try",
                                                Ty.apply
                                                  (Ty.path "core::option::Option")
                                                  []
                                                  [ Ty.path "u16" ],
                                                [],
                                                "branch",
                                                []
                                              |),
                                              [
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.path "core::net::parser::Parser",
                                                    "read_port",
                                                    []
                                                  |),
                                                  [ M.read (| p |) ]
                                                |)
                                              ]
                                            |)
                                          |),
                                          [
                                            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::option::Option")
                                                              []
                                                              [
                                                                Ty.path
                                                                  "core::net::socket_addr::SocketAddrV4"
                                                              ],
                                                            [
                                                              Ty.apply
                                                                (Ty.path "core::option::Option")
                                                                []
                                                                [
                                                                  Ty.path
                                                                    "core::convert::Infallible"
                                                                ]
                                                            ],
                                                            "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.StructTuple
                                        "core::option::Option::Some"
                                        [
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "core::net::socket_addr::SocketAddrV4",
                                              "new",
                                              []
                                            |),
                                            [ M.read (| ip |); M.read (| port |) ]
                                          |)
                                        ]
                                    |)
                                  |)))
                            ]
                          |)))
                      | _ => M.impossible "wrong number of arguments"
                      end))
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_read_socket_addr_v4 :
        M.IsAssociatedFunction Self "read_socket_addr_v4" read_socket_addr_v4.
      
      (*
          fn read_socket_addr_v6(&mut self) -> Option<SocketAddrV6> {
              self.read_atomically(|p| {
                  p.read_given_char('[')?;
                  let ip = p.read_ipv6_addr()?;
                  let scope_id = p.read_scope_id().unwrap_or(0);
                  p.read_given_char(']')?;
      
                  let port = p.read_port()?;
                  Some(SocketAddrV6::new(ip, port, 0, scope_id))
              })
          }
      *)
      Definition read_socket_addr_v6 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "core::net::parser::Parser",
                "read_atomically",
                [
                  Ty.path "core::net::socket_addr::SocketAddrV6";
                  Ty.function
                    [
                      Ty.tuple
                        [ Ty.apply (Ty.path "&mut") [] [ Ty.path "core::net::parser::Parser" ] ]
                    ]
                    (Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [ Ty.path "core::net::socket_addr::SocketAddrV6" ])
                ]
              |),
              [
                M.read (| self |);
                M.closure
                  (fun γ =>
                    ltac:(M.monadic
                      match γ with
                      | [ α0 ] =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| α0 |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let p := M.copy (| γ |) in
                                  M.read (|
                                    let~ _ :=
                                      M.match_operator (|
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::ops::try_trait::Try",
                                              Ty.apply
                                                (Ty.path "core::option::Option")
                                                []
                                                [ Ty.tuple [] ],
                                              [],
                                              "branch",
                                              []
                                            |),
                                            [
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path "core::net::parser::Parser",
                                                  "read_given_char",
                                                  []
                                                |),
                                                [ M.read (| p |); Value.UnicodeChar 91 ]
                                              |)
                                            ]
                                          |)
                                        |),
                                        [
                                          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::option::Option")
                                                            []
                                                            [
                                                              Ty.path
                                                                "core::net::socket_addr::SocketAddrV6"
                                                            ],
                                                          [
                                                            Ty.apply
                                                              (Ty.path "core::option::Option")
                                                              []
                                                              [ Ty.path "core::convert::Infallible"
                                                              ]
                                                          ],
                                                          "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~ ip :=
                                      M.copy (|
                                        M.match_operator (|
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::ops::try_trait::Try",
                                                Ty.apply
                                                  (Ty.path "core::option::Option")
                                                  []
                                                  [ Ty.path "core::net::ip_addr::Ipv6Addr" ],
                                                [],
                                                "branch",
                                                []
                                              |),
                                              [
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.path "core::net::parser::Parser",
                                                    "read_ipv6_addr",
                                                    []
                                                  |),
                                                  [ M.read (| p |) ]
                                                |)
                                              ]
                                            |)
                                          |),
                                          [
                                            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::option::Option")
                                                              []
                                                              [
                                                                Ty.path
                                                                  "core::net::socket_addr::SocketAddrV6"
                                                              ],
                                                            [
                                                              Ty.apply
                                                                (Ty.path "core::option::Option")
                                                                []
                                                                [
                                                                  Ty.path
                                                                    "core::convert::Infallible"
                                                                ]
                                                            ],
                                                            "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~ scope_id :=
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [ Ty.path "u32" ],
                                            "unwrap_or",
                                            []
                                          |),
                                          [
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.path "core::net::parser::Parser",
                                                "read_scope_id",
                                                []
                                              |),
                                              [ M.read (| p |) ]
                                            |);
                                            Value.Integer IntegerKind.U32 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::option::Option")
                                                []
                                                [ Ty.tuple [] ],
                                              [],
                                              "branch",
                                              []
                                            |),
                                            [
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path "core::net::parser::Parser",
                                                  "read_given_char",
                                                  []
                                                |),
                                                [ M.read (| p |); Value.UnicodeChar 93 ]
                                              |)
                                            ]
                                          |)
                                        |),
                                        [
                                          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::option::Option")
                                                            []
                                                            [
                                                              Ty.path
                                                                "core::net::socket_addr::SocketAddrV6"
                                                            ],
                                                          [
                                                            Ty.apply
                                                              (Ty.path "core::option::Option")
                                                              []
                                                              [ Ty.path "core::convert::Infallible"
                                                              ]
                                                          ],
                                                          "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~ port :=
                                      M.copy (|
                                        M.match_operator (|
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::ops::try_trait::Try",
                                                Ty.apply
                                                  (Ty.path "core::option::Option")
                                                  []
                                                  [ Ty.path "u16" ],
                                                [],
                                                "branch",
                                                []
                                              |),
                                              [
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.path "core::net::parser::Parser",
                                                    "read_port",
                                                    []
                                                  |),
                                                  [ M.read (| p |) ]
                                                |)
                                              ]
                                            |)
                                          |),
                                          [
                                            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::option::Option")
                                                              []
                                                              [
                                                                Ty.path
                                                                  "core::net::socket_addr::SocketAddrV6"
                                                              ],
                                                            [
                                                              Ty.apply
                                                                (Ty.path "core::option::Option")
                                                                []
                                                                [
                                                                  Ty.path
                                                                    "core::convert::Infallible"
                                                                ]
                                                            ],
                                                            "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.StructTuple
                                        "core::option::Option::Some"
                                        [
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "core::net::socket_addr::SocketAddrV6",
                                              "new",
                                              []
                                            |),
                                            [
                                              M.read (| ip |);
                                              M.read (| port |);
                                              Value.Integer IntegerKind.U32 0;
                                              M.read (| scope_id |)
                                            ]
                                          |)
                                        ]
                                    |)
                                  |)))
                            ]
                          |)))
                      | _ => M.impossible "wrong number of arguments"
                      end))
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_read_socket_addr_v6 :
        M.IsAssociatedFunction Self "read_socket_addr_v6" read_socket_addr_v6.
      
      (*
          fn read_socket_addr(&mut self) -> Option<SocketAddr> {
              self.read_socket_addr_v4()
                  .map(SocketAddr::V4)
                  .or_else(|| self.read_socket_addr_v6().map(SocketAddr::V6))
          }
      *)
      Definition read_socket_addr (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "core::option::Option")
                  []
                  [ Ty.path "core::net::socket_addr::SocketAddr" ],
                "or_else",
                [
                  Ty.function
                    [ Ty.tuple [] ]
                    (Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [ Ty.path "core::net::socket_addr::SocketAddr" ])
                ]
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [ Ty.path "core::net::socket_addr::SocketAddrV4" ],
                    "map",
                    [
                      Ty.path "core::net::socket_addr::SocketAddr";
                      Ty.function
                        [ Ty.path "core::net::socket_addr::SocketAddrV4" ]
                        (Ty.path "core::net::socket_addr::SocketAddr")
                    ]
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "core::net::parser::Parser",
                        "read_socket_addr_v4",
                        []
                      |),
                      [ M.read (| self |) ]
                    |);
                    M.constructor_as_closure "core::net::socket_addr::SocketAddr::V4"
                  ]
                |);
                M.closure
                  (fun γ =>
                    ltac:(M.monadic
                      match γ with
                      | [ α0 ] =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| α0 |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "core::option::Option")
                                        []
                                        [ Ty.path "core::net::socket_addr::SocketAddrV6" ],
                                      "map",
                                      [
                                        Ty.path "core::net::socket_addr::SocketAddr";
                                        Ty.function
                                          [ Ty.path "core::net::socket_addr::SocketAddrV6" ]
                                          (Ty.path "core::net::socket_addr::SocketAddr")
                                      ]
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "core::net::parser::Parser",
                                          "read_socket_addr_v6",
                                          []
                                        |),
                                        [ M.read (| self |) ]
                                      |);
                                      M.constructor_as_closure
                                        "core::net::socket_addr::SocketAddr::V6"
                                    ]
                                  |)))
                            ]
                          |)))
                      | _ => M.impossible "wrong number of arguments"
                      end))
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_read_socket_addr :
        M.IsAssociatedFunction Self "read_socket_addr" read_socket_addr.
    End Impl_core_net_parser_Parser.
    
    Module Impl_core_net_ip_addr_IpAddr.
      Definition Self : Ty.t := Ty.path "core::net::ip_addr::IpAddr".
      
      (*
          pub fn parse_ascii(b: &[u8]) -> Result<Self, AddrParseError> {
              Parser::new(b).parse_with(|p| p.read_ip_addr(), AddrKind::Ip)
          }
      *)
      Definition parse_ascii (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ b ] =>
          ltac:(M.monadic
            (let b := M.alloc (| b |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "core::net::parser::Parser",
                "parse_with",
                [
                  Ty.path "core::net::ip_addr::IpAddr";
                  Ty.function
                    [
                      Ty.tuple
                        [ Ty.apply (Ty.path "&mut") [] [ Ty.path "core::net::parser::Parser" ] ]
                    ]
                    (Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [ Ty.path "core::net::ip_addr::IpAddr" ])
                ]
              |),
              [
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "core::net::parser::Parser", "new", [] |),
                    [ M.read (| b |) ]
                  |)
                |);
                M.closure
                  (fun γ =>
                    ltac:(M.monadic
                      match γ with
                      | [ α0 ] =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| α0 |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let p := M.copy (| γ |) in
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::net::parser::Parser",
                                      "read_ip_addr",
                                      []
                                    |),
                                    [ M.read (| p |) ]
                                  |)))
                            ]
                          |)))
                      | _ => M.impossible "wrong number of arguments"
                      end));
                Value.StructTuple "core::net::parser::AddrKind::Ip" []
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_parse_ascii : M.IsAssociatedFunction Self "parse_ascii" parse_ascii.
    End Impl_core_net_ip_addr_IpAddr.
    
    Module Impl_core_str_traits_FromStr_for_core_net_ip_addr_IpAddr.
      Definition Self : Ty.t := Ty.path "core::net::ip_addr::IpAddr".
      
      (*     type Err = AddrParseError; *)
      Definition _Err : Ty.t := Ty.path "core::net::parser::AddrParseError".
      
      (*
          fn from_str(s: &str) -> Result<IpAddr, AddrParseError> {
              Self::parse_ascii(s.as_bytes())
          }
      *)
      Definition from_str (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ s ] =>
          ltac:(M.monadic
            (let s := M.alloc (| s |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "core::net::ip_addr::IpAddr",
                "parse_ascii",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (| Ty.path "str", "as_bytes", [] |),
                  [ M.read (| s |) ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::str::traits::FromStr"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Err", InstanceField.Ty _Err); ("from_str", InstanceField.Method from_str) ].
    End Impl_core_str_traits_FromStr_for_core_net_ip_addr_IpAddr.
    
    Module Impl_core_net_ip_addr_Ipv4Addr.
      Definition Self : Ty.t := Ty.path "core::net::ip_addr::Ipv4Addr".
      
      (*
          pub fn parse_ascii(b: &[u8]) -> Result<Self, AddrParseError> {
              // don't try to parse if too long
              if b.len() > 15 {
                  Err(AddrParseError(AddrKind::Ipv4))
              } else {
                  Parser::new(b).parse_with(|p| p.read_ipv4_addr(), AddrKind::Ipv4)
              }
          }
      *)
      Definition parse_ascii (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ b ] =>
          ltac:(M.monadic
            (let b := M.alloc (| b |) in
            M.read (|
              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 (| b |) ]
                              |),
                              Value.Integer IntegerKind.Usize 15
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::result::Result::Err"
                          [
                            Value.StructTuple
                              "core::net::parser::AddrParseError"
                              [ Value.StructTuple "core::net::parser::AddrKind::Ipv4" [] ]
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::net::parser::Parser",
                            "parse_with",
                            [
                              Ty.path "core::net::ip_addr::Ipv4Addr";
                              Ty.function
                                [
                                  Ty.tuple
                                    [
                                      Ty.apply
                                        (Ty.path "&mut")
                                        []
                                        [ Ty.path "core::net::parser::Parser" ]
                                    ]
                                ]
                                (Ty.apply
                                  (Ty.path "core::option::Option")
                                  []
                                  [ Ty.path "core::net::ip_addr::Ipv4Addr" ])
                            ]
                          |),
                          [
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::net::parser::Parser",
                                  "new",
                                  []
                                |),
                                [ M.read (| b |) ]
                              |)
                            |);
                            M.closure
                              (fun γ =>
                                ltac:(M.monadic
                                  match γ with
                                  | [ α0 ] =>
                                    ltac:(M.monadic
                                      (M.match_operator (|
                                        M.alloc (| α0 |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let p := M.copy (| γ |) in
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path "core::net::parser::Parser",
                                                  "read_ipv4_addr",
                                                  []
                                                |),
                                                [ M.read (| p |) ]
                                              |)))
                                        ]
                                      |)))
                                  | _ => M.impossible "wrong number of arguments"
                                  end));
                            Value.StructTuple "core::net::parser::AddrKind::Ipv4" []
                          ]
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_parse_ascii : M.IsAssociatedFunction Self "parse_ascii" parse_ascii.
    End Impl_core_net_ip_addr_Ipv4Addr.
    
    Module Impl_core_str_traits_FromStr_for_core_net_ip_addr_Ipv4Addr.
      Definition Self : Ty.t := Ty.path "core::net::ip_addr::Ipv4Addr".
      
      (*     type Err = AddrParseError; *)
      Definition _Err : Ty.t := Ty.path "core::net::parser::AddrParseError".
      
      (*
          fn from_str(s: &str) -> Result<Ipv4Addr, AddrParseError> {
              Self::parse_ascii(s.as_bytes())
          }
      *)
      Definition from_str (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ s ] =>
          ltac:(M.monadic
            (let s := M.alloc (| s |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "core::net::ip_addr::Ipv4Addr",
                "parse_ascii",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (| Ty.path "str", "as_bytes", [] |),
                  [ M.read (| s |) ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::str::traits::FromStr"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Err", InstanceField.Ty _Err); ("from_str", InstanceField.Method from_str) ].
    End Impl_core_str_traits_FromStr_for_core_net_ip_addr_Ipv4Addr.
    
    Module Impl_core_net_ip_addr_Ipv6Addr.
      Definition Self : Ty.t := Ty.path "core::net::ip_addr::Ipv6Addr".
      
      (*
          pub fn parse_ascii(b: &[u8]) -> Result<Self, AddrParseError> {
              Parser::new(b).parse_with(|p| p.read_ipv6_addr(), AddrKind::Ipv6)
          }
      *)
      Definition parse_ascii (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ b ] =>
          ltac:(M.monadic
            (let b := M.alloc (| b |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "core::net::parser::Parser",
                "parse_with",
                [
                  Ty.path "core::net::ip_addr::Ipv6Addr";
                  Ty.function
                    [
                      Ty.tuple
                        [ Ty.apply (Ty.path "&mut") [] [ Ty.path "core::net::parser::Parser" ] ]
                    ]
                    (Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [ Ty.path "core::net::ip_addr::Ipv6Addr" ])
                ]
              |),
              [
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "core::net::parser::Parser", "new", [] |),
                    [ M.read (| b |) ]
                  |)
                |);
                M.closure
                  (fun γ =>
                    ltac:(M.monadic
                      match γ with
                      | [ α0 ] =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| α0 |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let p := M.copy (| γ |) in
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::net::parser::Parser",
                                      "read_ipv6_addr",
                                      []
                                    |),
                                    [ M.read (| p |) ]
                                  |)))
                            ]
                          |)))
                      | _ => M.impossible "wrong number of arguments"
                      end));
                Value.StructTuple "core::net::parser::AddrKind::Ipv6" []
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_parse_ascii : M.IsAssociatedFunction Self "parse_ascii" parse_ascii.
    End Impl_core_net_ip_addr_Ipv6Addr.
    
    Module Impl_core_str_traits_FromStr_for_core_net_ip_addr_Ipv6Addr.
      Definition Self : Ty.t := Ty.path "core::net::ip_addr::Ipv6Addr".
      
      (*     type Err = AddrParseError; *)
      Definition _Err : Ty.t := Ty.path "core::net::parser::AddrParseError".
      
      (*
          fn from_str(s: &str) -> Result<Ipv6Addr, AddrParseError> {
              Self::parse_ascii(s.as_bytes())
          }
      *)
      Definition from_str (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ s ] =>
          ltac:(M.monadic
            (let s := M.alloc (| s |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "core::net::ip_addr::Ipv6Addr",
                "parse_ascii",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (| Ty.path "str", "as_bytes", [] |),
                  [ M.read (| s |) ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::str::traits::FromStr"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Err", InstanceField.Ty _Err); ("from_str", InstanceField.Method from_str) ].
    End Impl_core_str_traits_FromStr_for_core_net_ip_addr_Ipv6Addr.
    
    Module Impl_core_net_socket_addr_SocketAddrV4.
      Definition Self : Ty.t := Ty.path "core::net::socket_addr::SocketAddrV4".
      
      (*
          pub fn parse_ascii(b: &[u8]) -> Result<Self, AddrParseError> {
              Parser::new(b).parse_with(|p| p.read_socket_addr_v4(), AddrKind::SocketV4)
          }
      *)
      Definition parse_ascii (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ b ] =>
          ltac:(M.monadic
            (let b := M.alloc (| b |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "core::net::parser::Parser",
                "parse_with",
                [
                  Ty.path "core::net::socket_addr::SocketAddrV4";
                  Ty.function
                    [
                      Ty.tuple
                        [ Ty.apply (Ty.path "&mut") [] [ Ty.path "core::net::parser::Parser" ] ]
                    ]
                    (Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [ Ty.path "core::net::socket_addr::SocketAddrV4" ])
                ]
              |),
              [
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "core::net::parser::Parser", "new", [] |),
                    [ M.read (| b |) ]
                  |)
                |);
                M.closure
                  (fun γ =>
                    ltac:(M.monadic
                      match γ with
                      | [ α0 ] =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| α0 |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let p := M.copy (| γ |) in
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::net::parser::Parser",
                                      "read_socket_addr_v4",
                                      []
                                    |),
                                    [ M.read (| p |) ]
                                  |)))
                            ]
                          |)))
                      | _ => M.impossible "wrong number of arguments"
                      end));
                Value.StructTuple "core::net::parser::AddrKind::SocketV4" []
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_parse_ascii : M.IsAssociatedFunction Self "parse_ascii" parse_ascii.
    End Impl_core_net_socket_addr_SocketAddrV4.
    
    Module Impl_core_str_traits_FromStr_for_core_net_socket_addr_SocketAddrV4.
      Definition Self : Ty.t := Ty.path "core::net::socket_addr::SocketAddrV4".
      
      (*     type Err = AddrParseError; *)
      Definition _Err : Ty.t := Ty.path "core::net::parser::AddrParseError".
      
      (*
          fn from_str(s: &str) -> Result<SocketAddrV4, AddrParseError> {
              Self::parse_ascii(s.as_bytes())
          }
      *)
      Definition from_str (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ s ] =>
          ltac:(M.monadic
            (let s := M.alloc (| s |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "core::net::socket_addr::SocketAddrV4",
                "parse_ascii",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (| Ty.path "str", "as_bytes", [] |),
                  [ M.read (| s |) ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::str::traits::FromStr"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Err", InstanceField.Ty _Err); ("from_str", InstanceField.Method from_str) ].
    End Impl_core_str_traits_FromStr_for_core_net_socket_addr_SocketAddrV4.
    
    Module Impl_core_net_socket_addr_SocketAddrV6.
      Definition Self : Ty.t := Ty.path "core::net::socket_addr::SocketAddrV6".
      
      (*
          pub fn parse_ascii(b: &[u8]) -> Result<Self, AddrParseError> {
              Parser::new(b).parse_with(|p| p.read_socket_addr_v6(), AddrKind::SocketV6)
          }
      *)
      Definition parse_ascii (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ b ] =>
          ltac:(M.monadic
            (let b := M.alloc (| b |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "core::net::parser::Parser",
                "parse_with",
                [
                  Ty.path "core::net::socket_addr::SocketAddrV6";
                  Ty.function
                    [
                      Ty.tuple
                        [ Ty.apply (Ty.path "&mut") [] [ Ty.path "core::net::parser::Parser" ] ]
                    ]
                    (Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [ Ty.path "core::net::socket_addr::SocketAddrV6" ])
                ]
              |),
              [
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "core::net::parser::Parser", "new", [] |),
                    [ M.read (| b |) ]
                  |)
                |);
                M.closure
                  (fun γ =>
                    ltac:(M.monadic
                      match γ with
                      | [ α0 ] =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| α0 |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let p := M.copy (| γ |) in
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::net::parser::Parser",
                                      "read_socket_addr_v6",
                                      []
                                    |),
                                    [ M.read (| p |) ]
                                  |)))
                            ]
                          |)))
                      | _ => M.impossible "wrong number of arguments"
                      end));
                Value.StructTuple "core::net::parser::AddrKind::SocketV6" []
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_parse_ascii : M.IsAssociatedFunction Self "parse_ascii" parse_ascii.
    End Impl_core_net_socket_addr_SocketAddrV6.
    
    Module Impl_core_str_traits_FromStr_for_core_net_socket_addr_SocketAddrV6.
      Definition Self : Ty.t := Ty.path "core::net::socket_addr::SocketAddrV6".
      
      (*     type Err = AddrParseError; *)
      Definition _Err : Ty.t := Ty.path "core::net::parser::AddrParseError".
      
      (*
          fn from_str(s: &str) -> Result<SocketAddrV6, AddrParseError> {
              Self::parse_ascii(s.as_bytes())
          }
      *)
      Definition from_str (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ s ] =>
          ltac:(M.monadic
            (let s := M.alloc (| s |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "core::net::socket_addr::SocketAddrV6",
                "parse_ascii",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (| Ty.path "str", "as_bytes", [] |),
                  [ M.read (| s |) ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::str::traits::FromStr"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Err", InstanceField.Ty _Err); ("from_str", InstanceField.Method from_str) ].
    End Impl_core_str_traits_FromStr_for_core_net_socket_addr_SocketAddrV6.
    
    Module Impl_core_net_socket_addr_SocketAddr.
      Definition Self : Ty.t := Ty.path "core::net::socket_addr::SocketAddr".
      
      (*
          pub fn parse_ascii(b: &[u8]) -> Result<Self, AddrParseError> {
              Parser::new(b).parse_with(|p| p.read_socket_addr(), AddrKind::Socket)
          }
      *)
      Definition parse_ascii (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ b ] =>
          ltac:(M.monadic
            (let b := M.alloc (| b |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "core::net::parser::Parser",
                "parse_with",
                [
                  Ty.path "core::net::socket_addr::SocketAddr";
                  Ty.function
                    [
                      Ty.tuple
                        [ Ty.apply (Ty.path "&mut") [] [ Ty.path "core::net::parser::Parser" ] ]
                    ]
                    (Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [ Ty.path "core::net::socket_addr::SocketAddr" ])
                ]
              |),
              [
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "core::net::parser::Parser", "new", [] |),
                    [ M.read (| b |) ]
                  |)
                |);
                M.closure
                  (fun γ =>
                    ltac:(M.monadic
                      match γ with
                      | [ α0 ] =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| α0 |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let p := M.copy (| γ |) in
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::net::parser::Parser",
                                      "read_socket_addr",
                                      []
                                    |),
                                    [ M.read (| p |) ]
                                  |)))
                            ]
                          |)))
                      | _ => M.impossible "wrong number of arguments"
                      end));
                Value.StructTuple "core::net::parser::AddrKind::Socket" []
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_parse_ascii : M.IsAssociatedFunction Self "parse_ascii" parse_ascii.
    End Impl_core_net_socket_addr_SocketAddr.
    
    Module Impl_core_str_traits_FromStr_for_core_net_socket_addr_SocketAddr.
      Definition Self : Ty.t := Ty.path "core::net::socket_addr::SocketAddr".
      
      (*     type Err = AddrParseError; *)
      Definition _Err : Ty.t := Ty.path "core::net::parser::AddrParseError".
      
      (*
          fn from_str(s: &str) -> Result<SocketAddr, AddrParseError> {
              Self::parse_ascii(s.as_bytes())
          }
      *)
      Definition from_str (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ s ] =>
          ltac:(M.monadic
            (let s := M.alloc (| s |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "core::net::socket_addr::SocketAddr",
                "parse_ascii",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (| Ty.path "str", "as_bytes", [] |),
                  [ M.read (| s |) ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::str::traits::FromStr"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Err", InstanceField.Ty _Err); ("from_str", InstanceField.Method from_str) ].
    End Impl_core_str_traits_FromStr_for_core_net_socket_addr_SocketAddr.
    
    (*
    Enum AddrKind
    {
      const_params := [];
      ty_params := [];
      variants :=
        [
          {
            name := "Ip";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "Ipv4";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "Ipv6";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "Socket";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "SocketV4";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "SocketV6";
            item := StructTuple [];
            discriminant := None;
          }
        ];
    }
    *)
    
    Module Impl_core_fmt_Debug_for_core_net_parser_AddrKind.
      Definition Self : Ty.t := Ty.path "core::net::parser::AddrKind".
      
      (* Debug *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.call_closure (|
              M.get_associated_function (| Ty.path "core::fmt::Formatter", "write_str", [] |),
              [
                M.read (| f |);
                M.read (|
                  M.match_operator (|
                    self,
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ := M.is_struct_tuple (| γ, "core::net::parser::AddrKind::Ip" |) in
                          M.alloc (| M.read (| Value.String "Ip" |) |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ := M.is_struct_tuple (| γ, "core::net::parser::AddrKind::Ipv4" |) in
                          M.alloc (| M.read (| Value.String "Ipv4" |) |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ := M.is_struct_tuple (| γ, "core::net::parser::AddrKind::Ipv6" |) in
                          M.alloc (| M.read (| Value.String "Ipv6" |) |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (| γ, "core::net::parser::AddrKind::Socket" |) in
                          M.alloc (| M.read (| Value.String "Socket" |) |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (| γ, "core::net::parser::AddrKind::SocketV4" |) in
                          M.alloc (| M.read (| Value.String "SocketV4" |) |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (| γ, "core::net::parser::AddrKind::SocketV6" |) in
                          M.alloc (| M.read (| Value.String "SocketV6" |) |)))
                    ]
                  |)
                |)
              ]
            |)))
        | _, _, _ => 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_net_parser_AddrKind.
    
    Module Impl_core_clone_Clone_for_core_net_parser_AddrKind.
      Definition Self : Ty.t := Ty.path "core::net::parser::AddrKind".
      
      (* Clone *)
      Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                self,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ := M.is_struct_tuple (| γ, "core::net::parser::AddrKind::Ip" |) in
                      M.alloc (| Value.StructTuple "core::net::parser::AddrKind::Ip" [] |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ := M.is_struct_tuple (| γ, "core::net::parser::AddrKind::Ipv4" |) in
                      M.alloc (| Value.StructTuple "core::net::parser::AddrKind::Ipv4" [] |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ := M.is_struct_tuple (| γ, "core::net::parser::AddrKind::Ipv6" |) in
                      M.alloc (| Value.StructTuple "core::net::parser::AddrKind::Ipv6" [] |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ := M.is_struct_tuple (| γ, "core::net::parser::AddrKind::Socket" |) in
                      M.alloc (| Value.StructTuple "core::net::parser::AddrKind::Socket" [] |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ := M.is_struct_tuple (| γ, "core::net::parser::AddrKind::SocketV4" |) in
                      M.alloc (| Value.StructTuple "core::net::parser::AddrKind::SocketV4" [] |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ := M.is_struct_tuple (| γ, "core::net::parser::AddrKind::SocketV6" |) in
                      M.alloc (| Value.StructTuple "core::net::parser::AddrKind::SocketV6" [] |)))
                ]
              |)
            |)))
        | _, _, _ => 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_net_parser_AddrKind.
    
    Module Impl_core_marker_StructuralPartialEq_for_core_net_parser_AddrKind.
      Definition Self : Ty.t := Ty.path "core::net::parser::AddrKind".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_core_net_parser_AddrKind.
    
    Module Impl_core_cmp_PartialEq_for_core_net_parser_AddrKind.
      Definition Self : Ty.t := Ty.path "core::net::parser::AddrKind".
      
      (* PartialEq *)
      Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let~ __self_discr :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::discriminant_value",
                      [ Ty.path "core::net::parser::AddrKind" ]
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              let~ __arg1_discr :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::discriminant_value",
                      [ Ty.path "core::net::parser::AddrKind" ]
                    |),
                    [ M.read (| other |) ]
                  |)
                |) in
              M.alloc (| BinOp.eq (| M.read (| __self_discr |), M.read (| __arg1_discr |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq) ].
    End Impl_core_cmp_PartialEq_for_core_net_parser_AddrKind.
    
    Module Impl_core_cmp_Eq_for_core_net_parser_AddrKind.
      Definition Self : Ty.t := Ty.path "core::net::parser::AddrKind".
      
      (* Eq *)
      Definition assert_receiver_is_total_eq
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            Value.Tuple []))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::Eq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
    End Impl_core_cmp_Eq_for_core_net_parser_AddrKind.
    
    (* StructTuple
      {
        name := "AddrParseError";
        const_params := [];
        ty_params := [];
        fields := [ Ty.path "core::net::parser::AddrKind" ];
      } *)
    
    Module Impl_core_fmt_Debug_for_core_net_parser_AddrParseError.
      Definition Self : Ty.t := Ty.path "core::net::parser::AddrParseError".
      
      (* Debug *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "core::fmt::Formatter",
                "debug_tuple_field1_finish",
                []
              |),
              [
                M.read (| f |);
                M.read (| Value.String "AddrParseError" |);
                M.alloc (|
                  M.SubPointer.get_struct_tuple_field (|
                    M.read (| self |),
                    "core::net::parser::AddrParseError",
                    0
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::fmt::Debug"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
    End Impl_core_fmt_Debug_for_core_net_parser_AddrParseError.
    
    Module Impl_core_clone_Clone_for_core_net_parser_AddrParseError.
      Definition Self : Ty.t := Ty.path "core::net::parser::AddrParseError".
      
      (* 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::net::parser::AddrParseError"
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.path "core::net::parser::AddrKind",
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_tuple_field (|
                      M.read (| self |),
                      "core::net::parser::AddrParseError",
                      0
                    |)
                  ]
                |)
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::clone::Clone"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("clone", InstanceField.Method clone) ].
    End Impl_core_clone_Clone_for_core_net_parser_AddrParseError.
    
    Module Impl_core_marker_StructuralPartialEq_for_core_net_parser_AddrParseError.
      Definition Self : Ty.t := Ty.path "core::net::parser::AddrParseError".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_core_net_parser_AddrParseError.
    
    Module Impl_core_cmp_PartialEq_for_core_net_parser_AddrParseError.
      Definition Self : Ty.t := Ty.path "core::net::parser::AddrParseError".
      
      (* PartialEq *)
      Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.path "core::net::parser::AddrKind",
                [ Ty.path "core::net::parser::AddrKind" ],
                "eq",
                []
              |),
              [
                M.SubPointer.get_struct_tuple_field (|
                  M.read (| self |),
                  "core::net::parser::AddrParseError",
                  0
                |);
                M.SubPointer.get_struct_tuple_field (|
                  M.read (| other |),
                  "core::net::parser::AddrParseError",
                  0
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq) ].
    End Impl_core_cmp_PartialEq_for_core_net_parser_AddrParseError.
    
    Module Impl_core_cmp_Eq_for_core_net_parser_AddrParseError.
      Definition Self : Ty.t := Ty.path "core::net::parser::AddrParseError".
      
      (* Eq *)
      Definition assert_receiver_is_total_eq
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                Value.DeclaredButUndefined,
                [ fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::Eq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
    End Impl_core_cmp_Eq_for_core_net_parser_AddrParseError.
    
    Module Impl_core_fmt_Display_for_core_net_parser_AddrParseError.
      Definition Self : Ty.t := Ty.path "core::net::parser::AddrParseError".
      
      (*
          fn fmt(&self, fmt: &mut fmt::Formatter<'_>) -> fmt::Result {
              fmt.write_str(self.description())
          }
      *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; fmt ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let fmt := M.alloc (| fmt |) in
            M.call_closure (|
              M.get_associated_function (| Ty.path "core::fmt::Formatter", "write_str", [] |),
              [
                M.read (| fmt |);
                M.call_closure (|
                  M.get_trait_method (|
                    "core::error::Error",
                    Ty.path "core::net::parser::AddrParseError",
                    [],
                    "description",
                    []
                  |),
                  [ M.read (| self |) ]
                |)
              ]
            |)))
        | _, _, _ => 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_net_parser_AddrParseError.
    
    Module Impl_core_error_Error_for_core_net_parser_AddrParseError.
      Definition Self : Ty.t := Ty.path "core::net::parser::AddrParseError".
      
      (*
          fn description(&self) -> &str {
              match self.0 {
                  AddrKind::Ip => "invalid IP address syntax",
                  AddrKind::Ipv4 => "invalid IPv4 address syntax",
                  AddrKind::Ipv6 => "invalid IPv6 address syntax",
                  AddrKind::Socket => "invalid socket address syntax",
                  AddrKind::SocketV4 => "invalid IPv4 socket address syntax",
                  AddrKind::SocketV6 => "invalid IPv6 socket address syntax",
              }
          }
      *)
      Definition description (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                M.SubPointer.get_struct_tuple_field (|
                  M.read (| self |),
                  "core::net::parser::AddrParseError",
                  0
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let _ := M.is_struct_tuple (| γ, "core::net::parser::AddrKind::Ip" |) in
                      M.alloc (| M.read (| Value.String "invalid IP address syntax" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let _ := M.is_struct_tuple (| γ, "core::net::parser::AddrKind::Ipv4" |) in
                      M.alloc (| M.read (| Value.String "invalid IPv4 address syntax" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let _ := M.is_struct_tuple (| γ, "core::net::parser::AddrKind::Ipv6" |) in
                      M.alloc (| M.read (| Value.String "invalid IPv6 address syntax" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let _ := M.is_struct_tuple (| γ, "core::net::parser::AddrKind::Socket" |) in
                      M.alloc (| M.read (| Value.String "invalid socket address syntax" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let _ :=
                        M.is_struct_tuple (| γ, "core::net::parser::AddrKind::SocketV4" |) in
                      M.alloc (|
                        M.read (| Value.String "invalid IPv4 socket address syntax" |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let _ :=
                        M.is_struct_tuple (| γ, "core::net::parser::AddrKind::SocketV6" |) in
                      M.alloc (| M.read (| Value.String "invalid IPv6 socket address syntax" |) |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::error::Error"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("description", InstanceField.Method description) ].
    End Impl_core_error_Error_for_core_net_parser_AddrParseError.
  End parser.
End net.
