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

Module num.
  Module flt2dec.
    Module strategy.
      Module grisu.
        Definition value_ALPHA : Value.t :=
          M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.I16 (-60) |))).
        
        Definition value_GAMMA : Value.t :=
          M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.I16 (-32) |))).
        
        Definition value_CACHED_POW10 : Value.t :=
          M.run
            ltac:(M.monadic
              (M.alloc (|
                M.alloc (|
                  Value.Array
                    [
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 16580792590934885855;
                          Value.Integer IntegerKind.I16 (-1087);
                          Value.Integer IntegerKind.I16 (-308)
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 12353653155963782858;
                          Value.Integer IntegerKind.I16 (-1060);
                          Value.Integer IntegerKind.I16 (-300)
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 18408377700990114895;
                          Value.Integer IntegerKind.I16 (-1034);
                          Value.Integer IntegerKind.I16 (-292)
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 13715310171984221708;
                          Value.Integer IntegerKind.I16 (-1007);
                          Value.Integer IntegerKind.I16 (-284)
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 10218702384817765436;
                          Value.Integer IntegerKind.I16 (-980);
                          Value.Integer IntegerKind.I16 (-276)
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 15227053142812498563;
                          Value.Integer IntegerKind.I16 (-954);
                          Value.Integer IntegerKind.I16 (-268)
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 11345038669416679861;
                          Value.Integer IntegerKind.I16 (-927);
                          Value.Integer IntegerKind.I16 (-260)
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 16905424996341287883;
                          Value.Integer IntegerKind.I16 (-901);
                          Value.Integer IntegerKind.I16 (-252)
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 12595523146049147757;
                          Value.Integer IntegerKind.I16 (-874);
                          Value.Integer IntegerKind.I16 (-244)
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 9384396036005875287;
                          Value.Integer IntegerKind.I16 (-847);
                          Value.Integer IntegerKind.I16 (-236)
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 13983839803942852151;
                          Value.Integer IntegerKind.I16 (-821);
                          Value.Integer IntegerKind.I16 (-228)
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 10418772551374772303;
                          Value.Integer IntegerKind.I16 (-794);
                          Value.Integer IntegerKind.I16 (-220)
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 15525180923007089351;
                          Value.Integer IntegerKind.I16 (-768);
                          Value.Integer IntegerKind.I16 (-212)
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 11567161174868858868;
                          Value.Integer IntegerKind.I16 (-741);
                          Value.Integer IntegerKind.I16 (-204)
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 17236413322193710309;
                          Value.Integer IntegerKind.I16 (-715);
                          Value.Integer IntegerKind.I16 (-196)
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 12842128665889583758;
                          Value.Integer IntegerKind.I16 (-688);
                          Value.Integer IntegerKind.I16 (-188)
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 9568131466127621947;
                          Value.Integer IntegerKind.I16 (-661);
                          Value.Integer IntegerKind.I16 (-180)
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 14257626930069360058;
                          Value.Integer IntegerKind.I16 (-635);
                          Value.Integer IntegerKind.I16 (-172)
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 10622759856335341974;
                          Value.Integer IntegerKind.I16 (-608);
                          Value.Integer IntegerKind.I16 (-164)
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 15829145694278690180;
                          Value.Integer IntegerKind.I16 (-582);
                          Value.Integer IntegerKind.I16 (-156)
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 11793632577567316726;
                          Value.Integer IntegerKind.I16 (-555);
                          Value.Integer IntegerKind.I16 (-148)
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 17573882009934360870;
                          Value.Integer IntegerKind.I16 (-529);
                          Value.Integer IntegerKind.I16 (-140)
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 13093562431584567480;
                          Value.Integer IntegerKind.I16 (-502);
                          Value.Integer IntegerKind.I16 (-132)
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 9755464219737475723;
                          Value.Integer IntegerKind.I16 (-475);
                          Value.Integer IntegerKind.I16 (-124)
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 14536774485912137811;
                          Value.Integer IntegerKind.I16 (-449);
                          Value.Integer IntegerKind.I16 (-116)
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 10830740992659433045;
                          Value.Integer IntegerKind.I16 (-422);
                          Value.Integer IntegerKind.I16 (-108)
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 16139061738043178685;
                          Value.Integer IntegerKind.I16 (-396);
                          Value.Integer IntegerKind.I16 (-100)
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 12024538023802026127;
                          Value.Integer IntegerKind.I16 (-369);
                          Value.Integer IntegerKind.I16 (-92)
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 17917957937422433684;
                          Value.Integer IntegerKind.I16 (-343);
                          Value.Integer IntegerKind.I16 (-84)
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 13349918974505688015;
                          Value.Integer IntegerKind.I16 (-316);
                          Value.Integer IntegerKind.I16 (-76)
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 9946464728195732843;
                          Value.Integer IntegerKind.I16 (-289);
                          Value.Integer IntegerKind.I16 (-68)
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 14821387422376473014;
                          Value.Integer IntegerKind.I16 (-263);
                          Value.Integer IntegerKind.I16 (-60)
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 11042794154864902060;
                          Value.Integer IntegerKind.I16 (-236);
                          Value.Integer IntegerKind.I16 (-52)
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 16455045573212060422;
                          Value.Integer IntegerKind.I16 (-210);
                          Value.Integer IntegerKind.I16 (-44)
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 12259964326927110867;
                          Value.Integer IntegerKind.I16 (-183);
                          Value.Integer IntegerKind.I16 (-36)
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 18268770466636286478;
                          Value.Integer IntegerKind.I16 (-157);
                          Value.Integer IntegerKind.I16 (-28)
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 13611294676837538539;
                          Value.Integer IntegerKind.I16 (-130);
                          Value.Integer IntegerKind.I16 (-20)
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 10141204801825835212;
                          Value.Integer IntegerKind.I16 (-103);
                          Value.Integer IntegerKind.I16 (-12)
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 15111572745182864684;
                          Value.Integer IntegerKind.I16 (-77);
                          Value.Integer IntegerKind.I16 (-4)
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 11258999068426240000;
                          Value.Integer IntegerKind.I16 (-50);
                          Value.Integer IntegerKind.I16 4
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 16777216000000000000;
                          Value.Integer IntegerKind.I16 (-24);
                          Value.Integer IntegerKind.I16 12
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 12500000000000000000;
                          Value.Integer IntegerKind.I16 3;
                          Value.Integer IntegerKind.I16 20
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 9313225746154785156;
                          Value.Integer IntegerKind.I16 30;
                          Value.Integer IntegerKind.I16 28
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 13877787807814456755;
                          Value.Integer IntegerKind.I16 56;
                          Value.Integer IntegerKind.I16 36
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 10339757656912845936;
                          Value.Integer IntegerKind.I16 83;
                          Value.Integer IntegerKind.I16 44
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 15407439555097886824;
                          Value.Integer IntegerKind.I16 109;
                          Value.Integer IntegerKind.I16 52
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 11479437019748901445;
                          Value.Integer IntegerKind.I16 136;
                          Value.Integer IntegerKind.I16 60
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 17105694144590052135;
                          Value.Integer IntegerKind.I16 162;
                          Value.Integer IntegerKind.I16 68
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 12744735289059618216;
                          Value.Integer IntegerKind.I16 189;
                          Value.Integer IntegerKind.I16 76
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 9495567745759798747;
                          Value.Integer IntegerKind.I16 216;
                          Value.Integer IntegerKind.I16 84
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 14149498560666738074;
                          Value.Integer IntegerKind.I16 242;
                          Value.Integer IntegerKind.I16 92
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 10542197943230523224;
                          Value.Integer IntegerKind.I16 269;
                          Value.Integer IntegerKind.I16 100
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 15709099088952724970;
                          Value.Integer IntegerKind.I16 295;
                          Value.Integer IntegerKind.I16 108
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 11704190886730495818;
                          Value.Integer IntegerKind.I16 322;
                          Value.Integer IntegerKind.I16 116
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 17440603504673385349;
                          Value.Integer IntegerKind.I16 348;
                          Value.Integer IntegerKind.I16 124
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 12994262207056124023;
                          Value.Integer IntegerKind.I16 375;
                          Value.Integer IntegerKind.I16 132
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 9681479787123295682;
                          Value.Integer IntegerKind.I16 402;
                          Value.Integer IntegerKind.I16 140
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 14426529090290212157;
                          Value.Integer IntegerKind.I16 428;
                          Value.Integer IntegerKind.I16 148
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 10748601772107342003;
                          Value.Integer IntegerKind.I16 455;
                          Value.Integer IntegerKind.I16 156
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 16016664761464807395;
                          Value.Integer IntegerKind.I16 481;
                          Value.Integer IntegerKind.I16 164
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 11933345169920330789;
                          Value.Integer IntegerKind.I16 508;
                          Value.Integer IntegerKind.I16 172
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 17782069995880619868;
                          Value.Integer IntegerKind.I16 534;
                          Value.Integer IntegerKind.I16 180
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 13248674568444952270;
                          Value.Integer IntegerKind.I16 561;
                          Value.Integer IntegerKind.I16 188
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 9871031767461413346;
                          Value.Integer IntegerKind.I16 588;
                          Value.Integer IntegerKind.I16 196
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 14708983551653345445;
                          Value.Integer IntegerKind.I16 614;
                          Value.Integer IntegerKind.I16 204
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 10959046745042015199;
                          Value.Integer IntegerKind.I16 641;
                          Value.Integer IntegerKind.I16 212
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 16330252207878254650;
                          Value.Integer IntegerKind.I16 667;
                          Value.Integer IntegerKind.I16 220
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 12166986024289022870;
                          Value.Integer IntegerKind.I16 694;
                          Value.Integer IntegerKind.I16 228
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 18130221999122236476;
                          Value.Integer IntegerKind.I16 720;
                          Value.Integer IntegerKind.I16 236
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 13508068024458167312;
                          Value.Integer IntegerKind.I16 747;
                          Value.Integer IntegerKind.I16 244
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 10064294952495520794;
                          Value.Integer IntegerKind.I16 774;
                          Value.Integer IntegerKind.I16 252
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 14996968138956309548;
                          Value.Integer IntegerKind.I16 800;
                          Value.Integer IntegerKind.I16 260
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 11173611982879273257;
                          Value.Integer IntegerKind.I16 827;
                          Value.Integer IntegerKind.I16 268
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 16649979327439178909;
                          Value.Integer IntegerKind.I16 853;
                          Value.Integer IntegerKind.I16 276
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 12405201291620119593;
                          Value.Integer IntegerKind.I16 880;
                          Value.Integer IntegerKind.I16 284
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 9242595204427927429;
                          Value.Integer IntegerKind.I16 907;
                          Value.Integer IntegerKind.I16 292
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 13772540099066387757;
                          Value.Integer IntegerKind.I16 933;
                          Value.Integer IntegerKind.I16 300
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 10261342003245940623;
                          Value.Integer IntegerKind.I16 960;
                          Value.Integer IntegerKind.I16 308
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 15290591125556738113;
                          Value.Integer IntegerKind.I16 986;
                          Value.Integer IntegerKind.I16 316
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 11392378155556871081;
                          Value.Integer IntegerKind.I16 1013;
                          Value.Integer IntegerKind.I16 324
                        ];
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.U64 16975966327722178521;
                          Value.Integer IntegerKind.I16 1039;
                          Value.Integer IntegerKind.I16 332
                        ]
                    ]
                |)
              |))).
        
        Definition value_CACHED_POW10_FIRST_E : Value.t :=
          M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.I16 (-1087) |))).
        
        Definition value_CACHED_POW10_LAST_E : Value.t :=
          M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.I16 1039 |))).
        
        (*
        pub fn cached_power(alpha: i16, gamma: i16) -> (i16, Fp) {
            let offset = CACHED_POW10_FIRST_E as i32;
            let range = (CACHED_POW10.len() as i32) - 1;
            let domain = (CACHED_POW10_LAST_E - CACHED_POW10_FIRST_E) as i32;
            let idx = ((gamma as i32) - offset) * range / domain;
            let (f, e, k) = CACHED_POW10[idx as usize];
            debug_assert!(alpha <= e && e <= gamma);
            (k, Fp { f, e })
        }
        *)
        Definition cached_power (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ alpha; gamma ] =>
            ltac:(M.monadic
              (let alpha := M.alloc (| alpha |) in
              let gamma := M.alloc (| gamma |) in
              M.read (|
                let~ offset :=
                  M.alloc (|
                    M.rust_cast
                      (M.read (|
                        M.get_constant (|
                          "core::num::flt2dec::strategy::grisu::CACHED_POW10_FIRST_E"
                        |)
                      |))
                  |) in
                let~ range :=
                  M.alloc (|
                    BinOp.Wrap.sub (|
                      M.rust_cast
                        (M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "slice")
                              []
                              [ Ty.tuple [ Ty.path "u64"; Ty.path "i16"; Ty.path "i16" ] ],
                            "len",
                            []
                          |),
                          [
                            M.read (|
                              M.get_constant (|
                                "core::num::flt2dec::strategy::grisu::CACHED_POW10"
                              |)
                            |)
                          ]
                        |)),
                      Value.Integer IntegerKind.I32 1
                    |)
                  |) in
                let~ domain :=
                  M.alloc (|
                    M.rust_cast
                      (BinOp.Wrap.sub (|
                        M.read (|
                          M.get_constant (|
                            "core::num::flt2dec::strategy::grisu::CACHED_POW10_LAST_E"
                          |)
                        |),
                        M.read (|
                          M.get_constant (|
                            "core::num::flt2dec::strategy::grisu::CACHED_POW10_FIRST_E"
                          |)
                        |)
                      |))
                  |) in
                let~ idx :=
                  M.alloc (|
                    BinOp.Wrap.div (|
                      BinOp.Wrap.mul (|
                        BinOp.Wrap.sub (| M.rust_cast (M.read (| gamma |)), M.read (| offset |) |),
                        M.read (| range |)
                      |),
                      M.read (| domain |)
                    |)
                  |) in
                M.match_operator (|
                  M.SubPointer.get_array_field (|
                    M.read (|
                      M.get_constant (| "core::num::flt2dec::strategy::grisu::CACHED_POW10" |)
                    |),
                    M.alloc (| M.rust_cast (M.read (| idx |)) |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                        let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                        let γ0_2 := M.SubPointer.get_tuple_field (| γ, 2 |) in
                        let f := M.copy (| γ0_0 |) in
                        let e := M.copy (| γ0_1 |) in
                        let k := M.copy (| γ0_2 |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ := M.use (M.alloc (| Value.Bool true |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  let~ _ :=
                                    M.match_operator (|
                                      M.alloc (| Value.Tuple [] |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ :=
                                              M.use
                                                (M.alloc (|
                                                  UnOp.not (|
                                                    LogicalOp.and (|
                                                      BinOp.le (|
                                                        M.read (| alpha |),
                                                        M.read (| e |)
                                                      |),
                                                      ltac:(M.monadic
                                                        (BinOp.le (|
                                                          M.read (| e |),
                                                          M.read (| gamma |)
                                                        |)))
                                                    |)
                                                  |)
                                                |)) 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: alpha <= e && e <= gamma"
                                                    |)
                                                  ]
                                                |)
                                              |)
                                            |)));
                                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                      ]
                                    |) in
                                  M.alloc (| Value.Tuple [] |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |) in
                        M.alloc (|
                          Value.Tuple
                            [
                              M.read (| k |);
                              Value.StructRecord
                                "core::num::diy_float::Fp"
                                [ ("f", M.read (| f |)); ("e", M.read (| e |)) ]
                            ]
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Function_cached_power :
          M.IsFunction "core::num::flt2dec::strategy::grisu::cached_power" cached_power.
        
        (*
        pub fn max_pow10_no_more_than(x: u32) -> (u8, u32) {
            debug_assert!(x > 0);
        
            const X9: u32 = 10_0000_0000;
            const X8: u32 = 1_0000_0000;
            const X7: u32 = 1000_0000;
            const X6: u32 = 100_0000;
            const X5: u32 = 10_0000;
            const X4: u32 = 1_0000;
            const X3: u32 = 1000;
            const X2: u32 = 100;
            const X1: u32 = 10;
        
            if x < X4 {
                if x < X2 {
                    if x < X1 { (0, 1) } else { (1, X1) }
                } else {
                    if x < X3 { (2, X2) } else { (3, X3) }
                }
            } else {
                if x < X6 {
                    if x < X5 { (4, X4) } else { (5, X5) }
                } else if x < X8 {
                    if x < X7 { (6, X6) } else { (7, X7) }
                } else {
                    if x < X9 { (8, X8) } else { (9, X9) }
                }
            }
        }
        *)
        Definition max_pow10_no_more_than
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [], [ x ] =>
            ltac:(M.monadic
              (let x := M.alloc (| x |) in
              M.read (|
                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.gt (|
                                              M.read (| x |),
                                              Value.Integer IntegerKind.U32 0
                                            |)
                                          |)
                                        |)) 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: x > 0" |) ]
                                        |)
                                      |)
                                    |)));
                                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                              ]
                            |) in
                          M.alloc (| Value.Tuple [] |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.lt (|
                                M.read (| x |),
                                M.read (|
                                  M.get_constant (|
                                    "core::num::flt2dec::strategy::grisu::max_pow10_no_more_than::X4"
                                  |)
                                |)
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      BinOp.lt (|
                                        M.read (| x |),
                                        M.read (|
                                          M.get_constant (|
                                            "core::num::flt2dec::strategy::grisu::max_pow10_no_more_than::X2"
                                          |)
                                        |)
                                      |)
                                    |)) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ :=
                                          M.use
                                            (M.alloc (|
                                              BinOp.lt (|
                                                M.read (| x |),
                                                M.read (|
                                                  M.get_constant (|
                                                    "core::num::flt2dec::strategy::grisu::max_pow10_no_more_than::X1"
                                                  |)
                                                |)
                                              |)
                                            |)) in
                                        let _ :=
                                          M.is_constant_or_break_match (|
                                            M.read (| γ |),
                                            Value.Bool true
                                          |) in
                                        M.alloc (|
                                          Value.Tuple
                                            [
                                              Value.Integer IntegerKind.U8 0;
                                              Value.Integer IntegerKind.U32 1
                                            ]
                                        |)));
                                    fun γ =>
                                      ltac:(M.monadic
                                        (M.alloc (|
                                          Value.Tuple
                                            [
                                              Value.Integer IntegerKind.U8 1;
                                              M.read (|
                                                M.get_constant (|
                                                  "core::num::flt2dec::strategy::grisu::max_pow10_no_more_than::X1"
                                                |)
                                              |)
                                            ]
                                        |)))
                                  ]
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ :=
                                          M.use
                                            (M.alloc (|
                                              BinOp.lt (|
                                                M.read (| x |),
                                                M.read (|
                                                  M.get_constant (|
                                                    "core::num::flt2dec::strategy::grisu::max_pow10_no_more_than::X3"
                                                  |)
                                                |)
                                              |)
                                            |)) in
                                        let _ :=
                                          M.is_constant_or_break_match (|
                                            M.read (| γ |),
                                            Value.Bool true
                                          |) in
                                        M.alloc (|
                                          Value.Tuple
                                            [
                                              Value.Integer IntegerKind.U8 2;
                                              M.read (|
                                                M.get_constant (|
                                                  "core::num::flt2dec::strategy::grisu::max_pow10_no_more_than::X2"
                                                |)
                                              |)
                                            ]
                                        |)));
                                    fun γ =>
                                      ltac:(M.monadic
                                        (M.alloc (|
                                          Value.Tuple
                                            [
                                              Value.Integer IntegerKind.U8 3;
                                              M.read (|
                                                M.get_constant (|
                                                  "core::num::flt2dec::strategy::grisu::max_pow10_no_more_than::X3"
                                                |)
                                              |)
                                            ]
                                        |)))
                                  ]
                                |)))
                          ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      BinOp.lt (|
                                        M.read (| x |),
                                        M.read (|
                                          M.get_constant (|
                                            "core::num::flt2dec::strategy::grisu::max_pow10_no_more_than::X6"
                                          |)
                                        |)
                                      |)
                                    |)) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ :=
                                          M.use
                                            (M.alloc (|
                                              BinOp.lt (|
                                                M.read (| x |),
                                                M.read (|
                                                  M.get_constant (|
                                                    "core::num::flt2dec::strategy::grisu::max_pow10_no_more_than::X5"
                                                  |)
                                                |)
                                              |)
                                            |)) in
                                        let _ :=
                                          M.is_constant_or_break_match (|
                                            M.read (| γ |),
                                            Value.Bool true
                                          |) in
                                        M.alloc (|
                                          Value.Tuple
                                            [
                                              Value.Integer IntegerKind.U8 4;
                                              M.read (|
                                                M.get_constant (|
                                                  "core::num::flt2dec::strategy::grisu::max_pow10_no_more_than::X4"
                                                |)
                                              |)
                                            ]
                                        |)));
                                    fun γ =>
                                      ltac:(M.monadic
                                        (M.alloc (|
                                          Value.Tuple
                                            [
                                              Value.Integer IntegerKind.U8 5;
                                              M.read (|
                                                M.get_constant (|
                                                  "core::num::flt2dec::strategy::grisu::max_pow10_no_more_than::X5"
                                                |)
                                              |)
                                            ]
                                        |)))
                                  ]
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ :=
                                          M.use
                                            (M.alloc (|
                                              BinOp.lt (|
                                                M.read (| x |),
                                                M.read (|
                                                  M.get_constant (|
                                                    "core::num::flt2dec::strategy::grisu::max_pow10_no_more_than::X8"
                                                  |)
                                                |)
                                              |)
                                            |)) in
                                        let _ :=
                                          M.is_constant_or_break_match (|
                                            M.read (| γ |),
                                            Value.Bool true
                                          |) in
                                        M.match_operator (|
                                          M.alloc (| Value.Tuple [] |),
                                          [
                                            fun γ =>
                                              ltac:(M.monadic
                                                (let γ :=
                                                  M.use
                                                    (M.alloc (|
                                                      BinOp.lt (|
                                                        M.read (| x |),
                                                        M.read (|
                                                          M.get_constant (|
                                                            "core::num::flt2dec::strategy::grisu::max_pow10_no_more_than::X7"
                                                          |)
                                                        |)
                                                      |)
                                                    |)) in
                                                let _ :=
                                                  M.is_constant_or_break_match (|
                                                    M.read (| γ |),
                                                    Value.Bool true
                                                  |) in
                                                M.alloc (|
                                                  Value.Tuple
                                                    [
                                                      Value.Integer IntegerKind.U8 6;
                                                      M.read (|
                                                        M.get_constant (|
                                                          "core::num::flt2dec::strategy::grisu::max_pow10_no_more_than::X6"
                                                        |)
                                                      |)
                                                    ]
                                                |)));
                                            fun γ =>
                                              ltac:(M.monadic
                                                (M.alloc (|
                                                  Value.Tuple
                                                    [
                                                      Value.Integer IntegerKind.U8 7;
                                                      M.read (|
                                                        M.get_constant (|
                                                          "core::num::flt2dec::strategy::grisu::max_pow10_no_more_than::X7"
                                                        |)
                                                      |)
                                                    ]
                                                |)))
                                          ]
                                        |)));
                                    fun γ =>
                                      ltac:(M.monadic
                                        (M.match_operator (|
                                          M.alloc (| Value.Tuple [] |),
                                          [
                                            fun γ =>
                                              ltac:(M.monadic
                                                (let γ :=
                                                  M.use
                                                    (M.alloc (|
                                                      BinOp.lt (|
                                                        M.read (| x |),
                                                        M.read (|
                                                          M.get_constant (|
                                                            "core::num::flt2dec::strategy::grisu::max_pow10_no_more_than::X9"
                                                          |)
                                                        |)
                                                      |)
                                                    |)) in
                                                let _ :=
                                                  M.is_constant_or_break_match (|
                                                    M.read (| γ |),
                                                    Value.Bool true
                                                  |) in
                                                M.alloc (|
                                                  Value.Tuple
                                                    [
                                                      Value.Integer IntegerKind.U8 8;
                                                      M.read (|
                                                        M.get_constant (|
                                                          "core::num::flt2dec::strategy::grisu::max_pow10_no_more_than::X8"
                                                        |)
                                                      |)
                                                    ]
                                                |)));
                                            fun γ =>
                                              ltac:(M.monadic
                                                (M.alloc (|
                                                  Value.Tuple
                                                    [
                                                      Value.Integer IntegerKind.U8 9;
                                                      M.read (|
                                                        M.get_constant (|
                                                          "core::num::flt2dec::strategy::grisu::max_pow10_no_more_than::X9"
                                                        |)
                                                      |)
                                                    ]
                                                |)))
                                          ]
                                        |)))
                                  ]
                                |)))
                          ]
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Function_max_pow10_no_more_than :
          M.IsFunction
            "core::num::flt2dec::strategy::grisu::max_pow10_no_more_than"
            max_pow10_no_more_than.
        
        Module max_pow10_no_more_than.
          Definition value_X9 : Value.t :=
            M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U32 1000000000 |))).
          
          Definition value_X8 : Value.t :=
            M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U32 100000000 |))).
          
          Definition value_X7 : Value.t :=
            M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U32 10000000 |))).
          
          Definition value_X6 : Value.t :=
            M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U32 1000000 |))).
          
          Definition value_X5 : Value.t :=
            M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U32 100000 |))).
          
          Definition value_X4 : Value.t :=
            M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U32 10000 |))).
          
          Definition value_X3 : Value.t :=
            M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U32 1000 |))).
          
          Definition value_X2 : Value.t :=
            M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U32 100 |))).
          
          Definition value_X1 : Value.t :=
            M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U32 10 |))).
        End max_pow10_no_more_than.
        
        (*
        pub fn format_shortest_opt<'a>(
            d: &Decoded,
            buf: &'a mut [MaybeUninit<u8>],
        ) -> Option<(/*digits*/ &'a [u8], /*exp*/ i16)> {
            assert!(d.mant > 0);
            assert!(d.minus > 0);
            assert!(d.plus > 0);
            assert!(d.mant.checked_add(d.plus).is_some());
            assert!(d.mant.checked_sub(d.minus).is_some());
            assert!(buf.len() >= MAX_SIG_DIGITS);
            assert!(d.mant + d.plus < (1 << 61)); // we need at least three bits of additional precision
        
            // start with the normalized values with the shared exponent
            let plus = Fp { f: d.mant + d.plus, e: d.exp }.normalize();
            let minus = Fp { f: d.mant - d.minus, e: d.exp }.normalize_to(plus.e);
            let v = Fp { f: d.mant, e: d.exp }.normalize_to(plus.e);
        
            // find any `cached = 10^minusk` such that `ALPHA <= minusk + plus.e + 64 <= GAMMA`.
            // since `plus` is normalized, this means `2^(62 + ALPHA) <= plus * cached < 2^(64 + GAMMA)`;
            // given our choices of `ALPHA` and `GAMMA`, this puts `plus * cached` into `[4, 2^32)`.
            //
            // it is obviously desirable to maximize `GAMMA - ALPHA`,
            // so that we don't need many cached powers of 10, but there are some considerations:
            //
            // 1. we want to keep `floor(plus * cached)` within `u32` since it needs a costly division.
            //    (this is not really avoidable, remainder is required for accuracy estimation.)
            // 2. the remainder of `floor(plus * cached)` repeatedly gets multiplied by 10,
            //    and it should not overflow.
            //
            // the first gives `64 + GAMMA <= 32`, while the second gives `10 * 2^-ALPHA <= 2^64`;
            // -60 and -32 is the maximal range with this constraint, and V8 also uses them.
            let (minusk, cached) = cached_power(ALPHA - plus.e - 64, GAMMA - plus.e - 64);
        
            // scale fps. this gives the maximal error of 1 ulp (proved from Theorem 5.1).
            let plus = plus.mul(&cached);
            let minus = minus.mul(&cached);
            let v = v.mul(&cached);
            debug_assert_eq!(plus.e, minus.e);
            debug_assert_eq!(plus.e, v.e);
        
            //         +- actual range of minus
            //   | <---|---------------------- unsafe region --------------------------> |
            //   |     |                                                                 |
            //   |  |<--->|  | <--------------- safe region ---------------> |           |
            //   |  |     |  |                                               |           |
            //   |1 ulp|1 ulp|                 |1 ulp|1 ulp|                 |1 ulp|1 ulp|
            //   |<--->|<--->|                 |<--->|<--->|                 |<--->|<--->|
            //   |-----|-----|-------...-------|-----|-----|-------...-------|-----|-----|
            //   |   minus   |                 |     v     |                 |   plus    |
            // minus1     minus0           v - 1 ulp   v + 1 ulp           plus0       plus1
            //
            // above `minus`, `v` and `plus` are *quantized* approximations (error < 1 ulp).
            // as we don't know the error is positive or negative, we use two approximations spaced equally
            // and have the maximal error of 2 ulps.
            //
            // the "unsafe region" is a liberal interval which we initially generate.
            // the "safe region" is a conservative interval which we only accept.
            // we start with the correct repr within the unsafe region, and try to find the closest repr
            // to `v` which is also within the safe region. if we can't, we give up.
            let plus1 = plus.f + 1;
            //  let plus0 = plus.f - 1; // only for explanation
            //  let minus0 = minus.f + 1; // only for explanation
            let minus1 = minus.f - 1;
            let e = -plus.e as usize; // shared exponent
        
            // divide `plus1` into integral and fractional parts.
            // integral parts are guaranteed to fit in u32, since cached power guarantees `plus < 2^32`
            // and normalized `plus.f` is always less than `2^64 - 2^4` due to the precision requirement.
            let plus1int = (plus1 >> e) as u32;
            let plus1frac = plus1 & ((1 << e) - 1);
        
            // calculate the largest `10^max_kappa` no more than `plus1` (thus `plus1 < 10^(max_kappa+1)`).
            // this is an upper bound of `kappa` below.
            let (max_kappa, max_ten_kappa) = max_pow10_no_more_than(plus1int);
        
            let mut i = 0;
            let exp = max_kappa as i16 - minusk + 1;
        
            // Theorem 6.2: if `k` is the greatest integer s.t. `0 <= y mod 10^k <= y - x`,
            //              then `V = floor(y / 10^k) * 10^k` is in `[x, y]` and one of the shortest
            //              representations (with the minimal number of significant digits) in that range.
            //
            // find the digit length `kappa` between `(minus1, plus1)` as per Theorem 6.2.
            // Theorem 6.2 can be adopted to exclude `x` by requiring `y mod 10^k < y - x` instead.
            // (e.g., `x` = 32000, `y` = 32777; `kappa` = 2 since `y mod 10^3 = 777 < y - x = 777`.)
            // the algorithm relies on the later verification phase to exclude `y`.
            let delta1 = plus1 - minus1;
            //  let delta1int = (delta1 >> e) as usize; // only for explanation
            let delta1frac = delta1 & ((1 << e) - 1);
        
            // render integral parts, while checking for the accuracy at each step.
            let mut ten_kappa = max_ten_kappa; // 10^kappa
            let mut remainder = plus1int; // digits yet to be rendered
            loop {
                // we always have at least one digit to render, as `plus1 >= 10^kappa`
                // invariants:
                // - `delta1int <= remainder < 10^(kappa+1)`
                // - `plus1int = d[0..n-1] * 10^(kappa+1) + remainder`
                //   (it follows that `remainder = plus1int % 10^(kappa+1)`)
        
                // divide `remainder` by `10^kappa`. both are scaled by `2^-e`.
                let q = remainder / ten_kappa;
                let r = remainder % ten_kappa;
                debug_assert!(q < 10);
                buf[i] = MaybeUninit::new(b'0' + q as u8);
                i += 1;
        
                let plus1rem = ((r as u64) << e) + plus1frac; // == (plus1 % 10^kappa) * 2^e
                if plus1rem < delta1 {
                    // `plus1 % 10^kappa < delta1 = plus1 - minus1`; we've found the correct `kappa`.
                    let ten_kappa = (ten_kappa as u64) << e; // scale 10^kappa back to the shared exponent
                    return round_and_weed(
                        // SAFETY: we initialized that memory above.
                        unsafe { MaybeUninit::slice_assume_init_mut(&mut buf[..i]) },
                        exp,
                        plus1rem,
                        delta1,
                        plus1 - v.f,
                        ten_kappa,
                        1,
                    );
                }
        
                // break the loop when we have rendered all integral digits.
                // the exact number of digits is `max_kappa + 1` as `plus1 < 10^(max_kappa+1)`.
                if i > max_kappa as usize {
                    debug_assert_eq!(ten_kappa, 1);
                    break;
                }
        
                // restore invariants
                ten_kappa /= 10;
                remainder = r;
            }
        
            // render fractional parts, while checking for the accuracy at each step.
            // this time we rely on repeated multiplications, as division will lose the precision.
            let mut remainder = plus1frac;
            let mut threshold = delta1frac;
            let mut ulp = 1;
            loop {
                // the next digit should be significant as we've tested that before breaking out
                // invariants, where `m = max_kappa + 1` (# of digits in the integral part):
                // - `remainder < 2^e`
                // - `plus1frac * 10^(n-m) = d[m..n-1] * 2^e + remainder`
        
                remainder *= 10; // won't overflow, `2^e * 10 < 2^64`
                threshold *= 10;
                ulp *= 10;
        
                // divide `remainder` by `10^kappa`.
                // both are scaled by `2^e / 10^kappa`, so the latter is implicit here.
                let q = remainder >> e;
                let r = remainder & ((1 << e) - 1);
                debug_assert!(q < 10);
                buf[i] = MaybeUninit::new(b'0' + q as u8);
                i += 1;
        
                if r < threshold {
                    let ten_kappa = 1 << e; // implicit divisor
                    return round_and_weed(
                        // SAFETY: we initialized that memory above.
                        unsafe { MaybeUninit::slice_assume_init_mut(&mut buf[..i]) },
                        exp,
                        r,
                        threshold,
                        (plus1 - v.f) * ulp,
                        ten_kappa,
                        ulp,
                    );
                }
        
                // restore invariants
                remainder = r;
            }
        
            // we've generated all significant digits of `plus1`, but not sure if it's the optimal one.
            // for example, if `minus1` is 3.14153... and `plus1` is 3.14158..., there are 5 different
            // shortest representation from 3.14154 to 3.14158 but we only have the greatest one.
            // we have to successively decrease the last digit and check if this is the optimal repr.
            // there are at most 9 candidates (..1 to ..9), so this is fairly quick. ("rounding" phase)
            //
            // the function checks if this "optimal" repr is actually within the ulp ranges,
            // and also, it is possible that the "second-to-optimal" repr can actually be optimal
            // due to the rounding error. in either cases this returns `None`. ("weeding" phase)
            //
            // all arguments here are scaled by the common (but implicit) value `k`, so that:
            // - `remainder = (plus1 % 10^kappa) * k`
            // - `threshold = (plus1 - minus1) * k` (and also, `remainder < threshold`)
            // - `plus1v = (plus1 - v) * k` (and also, `threshold > plus1v` from prior invariants)
            // - `ten_kappa = 10^kappa * k`
            // - `ulp = 2^-e * k`
            fn round_and_weed(
                buf: &mut [u8],
                exp: i16,
                remainder: u64,
                threshold: u64,
                plus1v: u64,
                ten_kappa: u64,
                ulp: u64,
            ) -> Option<(&[u8], i16)> {
                assert!(!buf.is_empty());
        
                // produce two approximations to `v` (actually `plus1 - v`) within 1.5 ulps.
                // the resulting representation should be the closest representation to both.
                //
                // here `plus1 - v` is used since calculations are done with respect to `plus1`
                // in order to avoid overflow/underflow (hence the seemingly swapped names).
                let plus1v_down = plus1v + ulp; // plus1 - (v - 1 ulp)
                let plus1v_up = plus1v - ulp; // plus1 - (v + 1 ulp)
        
                // decrease the last digit and stop at the closest representation to `v + 1 ulp`.
                let mut plus1w = remainder; // plus1w(n) = plus1 - w(n)
                {
                    let last = buf.last_mut().unwrap();
        
                    // we work with the approximated digits `w(n)`, which is initially equal to `plus1 -
                    // plus1 % 10^kappa`. after running the loop body `n` times, `w(n) = plus1 -
                    // plus1 % 10^kappa - n * 10^kappa`. we set `plus1w(n) = plus1 - w(n) =
                    // plus1 % 10^kappa + n * 10^kappa` (thus `remainder = plus1w(0)`) to simplify checks.
                    // note that `plus1w(n)` is always increasing.
                    //
                    // we have three conditions to terminate. any of them will make the loop unable to
                    // proceed, but we then have at least one valid representation known to be closest to
                    // `v + 1 ulp` anyway. we will denote them as TC1 through TC3 for brevity.
                    //
                    // TC1: `w(n) <= v + 1 ulp`, i.e., this is the last repr that can be the closest one.
                    // this is equivalent to `plus1 - w(n) = plus1w(n) >= plus1 - (v + 1 ulp) = plus1v_up`.
                    // combined with TC2 (which checks if `w(n+1)` is valid), this prevents the possible
                    // overflow on the calculation of `plus1w(n)`.
                    //
                    // TC2: `w(n+1) < minus1`, i.e., the next repr definitely does not round to `v`.
                    // this is equivalent to `plus1 - w(n) + 10^kappa = plus1w(n) + 10^kappa >
                    // plus1 - minus1 = threshold`. the left hand side can overflow, but we know
                    // `threshold > plus1v`, so if TC1 is false, `threshold - plus1w(n) >
                    // threshold - (plus1v - 1 ulp) > 1 ulp` and we can safely test if
                    // `threshold - plus1w(n) < 10^kappa` instead.
                    //
                    // TC3: `abs(w(n) - (v + 1 ulp)) <= abs(w(n+1) - (v + 1 ulp))`, i.e., the next repr is
                    // no closer to `v + 1 ulp` than the current repr. given `z(n) = plus1v_up - plus1w(n)`,
                    // this becomes `abs(z(n)) <= abs(z(n+1))`. again assuming that TC1 is false, we have
                    // `z(n) > 0`. we have two cases to consider:
                    //
                    // - when `z(n+1) >= 0`: TC3 becomes `z(n) <= z(n+1)`. as `plus1w(n)` is increasing,
                    //   `z(n)` should be decreasing and this is clearly false.
                    // - when `z(n+1) < 0`:
                    //   - TC3a: the precondition is `plus1v_up < plus1w(n) + 10^kappa`. assuming TC2 is
                    //     false, `threshold >= plus1w(n) + 10^kappa` so it cannot overflow.
                    //   - TC3b: TC3 becomes `z(n) <= -z(n+1)`, i.e., `plus1v_up - plus1w(n) >=
                    //     plus1w(n+1) - plus1v_up = plus1w(n) + 10^kappa - plus1v_up`. the negated TC1
                    //     gives `plus1v_up > plus1w(n)`, so it cannot overflow or underflow when
                    //     combined with TC3a.
                    //
                    // consequently, we should stop when `TC1 || TC2 || (TC3a && TC3b)`. the following is
                    // equal to its inverse, `!TC1 && !TC2 && (!TC3a || !TC3b)`.
                    while plus1w < plus1v_up
                        && threshold - plus1w >= ten_kappa
                        && (plus1w + ten_kappa < plus1v_up
                            || plus1v_up - plus1w >= plus1w + ten_kappa - plus1v_up)
                    {
                        *last -= 1;
                        debug_assert!( *last > b'0'); // the shortest repr cannot end with `0`
                        plus1w += ten_kappa;
                    }
                }
        
                // check if this representation is also the closest representation to `v - 1 ulp`.
                //
                // this is simply same to the terminating conditions for `v + 1 ulp`, with all `plus1v_up`
                // replaced by `plus1v_down` instead. overflow analysis equally holds.
                if plus1w < plus1v_down
                    && threshold - plus1w >= ten_kappa
                    && (plus1w + ten_kappa < plus1v_down
                        || plus1v_down - plus1w >= plus1w + ten_kappa - plus1v_down)
                {
                    return None;
                }
        
                // now we have the closest representation to `v` between `plus1` and `minus1`.
                // this is too liberal, though, so we reject any `w(n)` not between `plus0` and `minus0`,
                // i.e., `plus1 - plus1w(n) <= minus0` or `plus1 - plus1w(n) >= plus0`. we utilize the facts
                // that `threshold = plus1 - minus1` and `plus1 - plus0 = minus0 - minus1 = 2 ulp`.
                if 2 * ulp <= plus1w && plus1w <= threshold - 4 * ulp { Some((buf, exp)) } else { None }
            }
        }
        *)
        Definition format_shortest_opt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ d; buf ] =>
            ltac:(M.monadic
              (let d := M.alloc (| d |) in
              let buf := M.alloc (| buf |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.never_to_any (|
                    M.read (|
                      let~ _ :=
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      UnOp.not (|
                                        BinOp.gt (|
                                          M.read (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| d |),
                                              "core::num::flt2dec::decoder::Decoded",
                                              "mant"
                                            |)
                                          |),
                                          Value.Integer IntegerKind.U64 0
                                        |)
                                      |)
                                    |)) 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: d.mant > 0" |) ]
                                    |)
                                  |)
                                |)));
                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                          ]
                        |) in
                      let~ _ :=
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      UnOp.not (|
                                        BinOp.gt (|
                                          M.read (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| d |),
                                              "core::num::flt2dec::decoder::Decoded",
                                              "minus"
                                            |)
                                          |),
                                          Value.Integer IntegerKind.U64 0
                                        |)
                                      |)
                                    |)) 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: d.minus > 0" |) ]
                                    |)
                                  |)
                                |)));
                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                          ]
                        |) in
                      let~ _ :=
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      UnOp.not (|
                                        BinOp.gt (|
                                          M.read (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| d |),
                                              "core::num::flt2dec::decoder::Decoded",
                                              "plus"
                                            |)
                                          |),
                                          Value.Integer IntegerKind.U64 0
                                        |)
                                      |)
                                    |)) 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: d.plus > 0" |) ]
                                    |)
                                  |)
                                |)));
                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                          ]
                        |) in
                      let~ _ :=
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      UnOp.not (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [ Ty.path "u64" ],
                                            "is_some",
                                            []
                                          |),
                                          [
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path "u64",
                                                  "checked_add",
                                                  []
                                                |),
                                                [
                                                  M.read (|
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| d |),
                                                      "core::num::flt2dec::decoder::Decoded",
                                                      "mant"
                                                    |)
                                                  |);
                                                  M.read (|
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| d |),
                                                      "core::num::flt2dec::decoder::Decoded",
                                                      "plus"
                                                    |)
                                                  |)
                                                ]
                                              |)
                                            |)
                                          ]
                                        |)
                                      |)
                                    |)) 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: d.mant.checked_add(d.plus).is_some()"
                                        |)
                                      ]
                                    |)
                                  |)
                                |)));
                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                          ]
                        |) in
                      let~ _ :=
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      UnOp.not (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [ Ty.path "u64" ],
                                            "is_some",
                                            []
                                          |),
                                          [
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path "u64",
                                                  "checked_sub",
                                                  []
                                                |),
                                                [
                                                  M.read (|
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| d |),
                                                      "core::num::flt2dec::decoder::Decoded",
                                                      "mant"
                                                    |)
                                                  |);
                                                  M.read (|
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| d |),
                                                      "core::num::flt2dec::decoder::Decoded",
                                                      "minus"
                                                    |)
                                                  |)
                                                ]
                                              |)
                                            |)
                                          ]
                                        |)
                                      |)
                                    |)) 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: d.mant.checked_sub(d.minus).is_some()"
                                        |)
                                      ]
                                    |)
                                  |)
                                |)));
                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                          ]
                        |) in
                      let~ _ :=
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      UnOp.not (|
                                        BinOp.ge (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply
                                                (Ty.path "slice")
                                                []
                                                [
                                                  Ty.apply
                                                    (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                                    []
                                                    [ Ty.path "u8" ]
                                                ],
                                              "len",
                                              []
                                            |),
                                            [ M.read (| buf |) ]
                                          |),
                                          M.read (|
                                            M.get_constant (|
                                              "core::num::flt2dec::MAX_SIG_DIGITS"
                                            |)
                                          |)
                                        |)
                                      |)
                                    |)) 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: buf.len() >= MAX_SIG_DIGITS"
                                        |)
                                      ]
                                    |)
                                  |)
                                |)));
                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                          ]
                        |) in
                      let~ _ :=
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      UnOp.not (|
                                        BinOp.lt (|
                                          BinOp.Wrap.add (|
                                            M.read (|
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| d |),
                                                "core::num::flt2dec::decoder::Decoded",
                                                "mant"
                                              |)
                                            |),
                                            M.read (|
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| d |),
                                                "core::num::flt2dec::decoder::Decoded",
                                                "plus"
                                              |)
                                            |)
                                          |),
                                          BinOp.Wrap.shl (|
                                            Value.Integer IntegerKind.U64 1,
                                            Value.Integer IntegerKind.I32 61
                                          |)
                                        |)
                                      |)
                                    |)) 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: d.mant + d.plus < (1 << 61)"
                                        |)
                                      ]
                                    |)
                                  |)
                                |)));
                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                          ]
                        |) in
                      let~ plus :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::num::diy_float::Fp",
                              "normalize",
                              []
                            |),
                            [
                              M.alloc (|
                                Value.StructRecord
                                  "core::num::diy_float::Fp"
                                  [
                                    ("f",
                                      BinOp.Wrap.add (|
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| d |),
                                            "core::num::flt2dec::decoder::Decoded",
                                            "mant"
                                          |)
                                        |),
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| d |),
                                            "core::num::flt2dec::decoder::Decoded",
                                            "plus"
                                          |)
                                        |)
                                      |));
                                    ("e",
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| d |),
                                          "core::num::flt2dec::decoder::Decoded",
                                          "exp"
                                        |)
                                      |))
                                  ]
                              |)
                            ]
                          |)
                        |) in
                      let~ minus :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::num::diy_float::Fp",
                              "normalize_to",
                              []
                            |),
                            [
                              M.alloc (|
                                Value.StructRecord
                                  "core::num::diy_float::Fp"
                                  [
                                    ("f",
                                      BinOp.Wrap.sub (|
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| d |),
                                            "core::num::flt2dec::decoder::Decoded",
                                            "mant"
                                          |)
                                        |),
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| d |),
                                            "core::num::flt2dec::decoder::Decoded",
                                            "minus"
                                          |)
                                        |)
                                      |));
                                    ("e",
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| d |),
                                          "core::num::flt2dec::decoder::Decoded",
                                          "exp"
                                        |)
                                      |))
                                  ]
                              |);
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  plus,
                                  "core::num::diy_float::Fp",
                                  "e"
                                |)
                              |)
                            ]
                          |)
                        |) in
                      let~ v :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::num::diy_float::Fp",
                              "normalize_to",
                              []
                            |),
                            [
                              M.alloc (|
                                Value.StructRecord
                                  "core::num::diy_float::Fp"
                                  [
                                    ("f",
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| d |),
                                          "core::num::flt2dec::decoder::Decoded",
                                          "mant"
                                        |)
                                      |));
                                    ("e",
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| d |),
                                          "core::num::flt2dec::decoder::Decoded",
                                          "exp"
                                        |)
                                      |))
                                  ]
                              |);
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  plus,
                                  "core::num::diy_float::Fp",
                                  "e"
                                |)
                              |)
                            ]
                          |)
                        |) in
                      M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_function (|
                              "core::num::flt2dec::strategy::grisu::cached_power",
                              []
                            |),
                            [
                              BinOp.Wrap.sub (|
                                BinOp.Wrap.sub (|
                                  M.read (|
                                    M.get_constant (|
                                      "core::num::flt2dec::strategy::grisu::ALPHA"
                                    |)
                                  |),
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      plus,
                                      "core::num::diy_float::Fp",
                                      "e"
                                    |)
                                  |)
                                |),
                                Value.Integer IntegerKind.I16 64
                              |);
                              BinOp.Wrap.sub (|
                                BinOp.Wrap.sub (|
                                  M.read (|
                                    M.get_constant (|
                                      "core::num::flt2dec::strategy::grisu::GAMMA"
                                    |)
                                  |),
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      plus,
                                      "core::num::diy_float::Fp",
                                      "e"
                                    |)
                                  |)
                                |),
                                Value.Integer IntegerKind.I16 64
                              |)
                            ]
                          |)
                        |),
                        [
                          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 minusk := M.copy (| γ0_0 |) in
                              let cached := M.copy (| γ0_1 |) in
                              let~ plus :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::num::diy_float::Fp",
                                      "mul",
                                      []
                                    |),
                                    [ plus; cached ]
                                  |)
                                |) in
                              let~ minus :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::num::diy_float::Fp",
                                      "mul",
                                      []
                                    |),
                                    [ minus; cached ]
                                  |)
                                |) in
                              let~ v :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::num::diy_float::Fp",
                                      "mul",
                                      []
                                    |),
                                    [ v; cached ]
                                  |)
                                |) 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
                                                [
                                                  M.SubPointer.get_struct_record_field (|
                                                    plus,
                                                    "core::num::diy_float::Fp",
                                                    "e"
                                                  |);
                                                  M.SubPointer.get_struct_record_field (|
                                                    minus,
                                                    "core::num::diy_float::Fp",
                                                    "e"
                                                  |)
                                                ]
                                            |),
                                            [
                                              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 left_val := M.copy (| γ0_0 |) in
                                                  let right_val := M.copy (| γ0_1 |) in
                                                  M.match_operator (|
                                                    M.alloc (| Value.Tuple [] |),
                                                    [
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ :=
                                                            M.use
                                                              (M.alloc (|
                                                                UnOp.not (|
                                                                  BinOp.eq (|
                                                                    M.read (|
                                                                      M.read (| left_val |)
                                                                    |),
                                                                    M.read (|
                                                                      M.read (| right_val |)
                                                                    |)
                                                                  |)
                                                                |)
                                                              |)) in
                                                          let _ :=
                                                            M.is_constant_or_break_match (|
                                                              M.read (| γ |),
                                                              Value.Bool true
                                                            |) in
                                                          M.alloc (|
                                                            M.never_to_any (|
                                                              M.read (|
                                                                let~ kind :=
                                                                  M.alloc (|
                                                                    Value.StructTuple
                                                                      "core::panicking::AssertKind::Eq"
                                                                      []
                                                                  |) in
                                                                M.alloc (|
                                                                  M.call_closure (|
                                                                    M.get_function (|
                                                                      "core::panicking::assert_failed",
                                                                      [ Ty.path "i16"; Ty.path "i16"
                                                                      ]
                                                                    |),
                                                                    [
                                                                      M.read (| kind |);
                                                                      M.read (| left_val |);
                                                                      M.read (| right_val |);
                                                                      Value.StructTuple
                                                                        "core::option::Option::None"
                                                                        []
                                                                    ]
                                                                  |)
                                                                |)
                                                              |)
                                                            |)
                                                          |)));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (M.alloc (| Value.Tuple [] |)))
                                                    ]
                                                  |)))
                                            ]
                                          |) in
                                        M.alloc (| Value.Tuple [] |)));
                                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                  ]
                                |) in
                              let~ _ :=
                                M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ := M.use (M.alloc (| Value.Bool true |)) in
                                        let _ :=
                                          M.is_constant_or_break_match (|
                                            M.read (| γ |),
                                            Value.Bool true
                                          |) in
                                        let~ _ :=
                                          M.match_operator (|
                                            M.alloc (|
                                              Value.Tuple
                                                [
                                                  M.SubPointer.get_struct_record_field (|
                                                    plus,
                                                    "core::num::diy_float::Fp",
                                                    "e"
                                                  |);
                                                  M.SubPointer.get_struct_record_field (|
                                                    v,
                                                    "core::num::diy_float::Fp",
                                                    "e"
                                                  |)
                                                ]
                                            |),
                                            [
                                              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 left_val := M.copy (| γ0_0 |) in
                                                  let right_val := M.copy (| γ0_1 |) in
                                                  M.match_operator (|
                                                    M.alloc (| Value.Tuple [] |),
                                                    [
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ :=
                                                            M.use
                                                              (M.alloc (|
                                                                UnOp.not (|
                                                                  BinOp.eq (|
                                                                    M.read (|
                                                                      M.read (| left_val |)
                                                                    |),
                                                                    M.read (|
                                                                      M.read (| right_val |)
                                                                    |)
                                                                  |)
                                                                |)
                                                              |)) in
                                                          let _ :=
                                                            M.is_constant_or_break_match (|
                                                              M.read (| γ |),
                                                              Value.Bool true
                                                            |) in
                                                          M.alloc (|
                                                            M.never_to_any (|
                                                              M.read (|
                                                                let~ kind :=
                                                                  M.alloc (|
                                                                    Value.StructTuple
                                                                      "core::panicking::AssertKind::Eq"
                                                                      []
                                                                  |) in
                                                                M.alloc (|
                                                                  M.call_closure (|
                                                                    M.get_function (|
                                                                      "core::panicking::assert_failed",
                                                                      [ Ty.path "i16"; Ty.path "i16"
                                                                      ]
                                                                    |),
                                                                    [
                                                                      M.read (| kind |);
                                                                      M.read (| left_val |);
                                                                      M.read (| right_val |);
                                                                      Value.StructTuple
                                                                        "core::option::Option::None"
                                                                        []
                                                                    ]
                                                                  |)
                                                                |)
                                                              |)
                                                            |)
                                                          |)));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (M.alloc (| Value.Tuple [] |)))
                                                    ]
                                                  |)))
                                            ]
                                          |) in
                                        M.alloc (| Value.Tuple [] |)));
                                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                  ]
                                |) in
                              let~ plus1 :=
                                M.alloc (|
                                  BinOp.Wrap.add (|
                                    M.read (|
                                      M.SubPointer.get_struct_record_field (|
                                        plus,
                                        "core::num::diy_float::Fp",
                                        "f"
                                      |)
                                    |),
                                    Value.Integer IntegerKind.U64 1
                                  |)
                                |) in
                              let~ minus1 :=
                                M.alloc (|
                                  BinOp.Wrap.sub (|
                                    M.read (|
                                      M.SubPointer.get_struct_record_field (|
                                        minus,
                                        "core::num::diy_float::Fp",
                                        "f"
                                      |)
                                    |),
                                    Value.Integer IntegerKind.U64 1
                                  |)
                                |) in
                              let~ e :=
                                M.alloc (|
                                  M.rust_cast
                                    (UnOp.neg (|
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          plus,
                                          "core::num::diy_float::Fp",
                                          "e"
                                        |)
                                      |)
                                    |))
                                |) in
                              let~ plus1int :=
                                M.alloc (|
                                  M.rust_cast
                                    (BinOp.Wrap.shr (| M.read (| plus1 |), M.read (| e |) |))
                                |) in
                              let~ plus1frac :=
                                M.alloc (|
                                  BinOp.bit_and
                                    (M.read (| plus1 |))
                                    (BinOp.Wrap.sub (|
                                      BinOp.Wrap.shl (|
                                        Value.Integer IntegerKind.U64 1,
                                        M.read (| e |)
                                      |),
                                      Value.Integer IntegerKind.U64 1
                                    |))
                                |) in
                              M.match_operator (|
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_function (|
                                      "core::num::flt2dec::strategy::grisu::max_pow10_no_more_than",
                                      []
                                    |),
                                    [ M.read (| plus1int |) ]
                                  |)
                                |),
                                [
                                  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 max_kappa := M.copy (| γ0_0 |) in
                                      let max_ten_kappa := M.copy (| γ0_1 |) in
                                      let~ i := M.alloc (| Value.Integer IntegerKind.Usize 0 |) in
                                      let~ exp :=
                                        M.alloc (|
                                          BinOp.Wrap.add (|
                                            BinOp.Wrap.sub (|
                                              M.rust_cast (M.read (| max_kappa |)),
                                              M.read (| minusk |)
                                            |),
                                            Value.Integer IntegerKind.I16 1
                                          |)
                                        |) in
                                      let~ delta1 :=
                                        M.alloc (|
                                          BinOp.Wrap.sub (|
                                            M.read (| plus1 |),
                                            M.read (| minus1 |)
                                          |)
                                        |) in
                                      let~ delta1frac :=
                                        M.alloc (|
                                          BinOp.bit_and
                                            (M.read (| delta1 |))
                                            (BinOp.Wrap.sub (|
                                              BinOp.Wrap.shl (|
                                                Value.Integer IntegerKind.U64 1,
                                                M.read (| e |)
                                              |),
                                              Value.Integer IntegerKind.U64 1
                                            |))
                                        |) in
                                      let~ ten_kappa := M.copy (| max_ten_kappa |) in
                                      let~ remainder := M.copy (| plus1int |) in
                                      let~ _ :=
                                        M.loop (|
                                          ltac:(M.monadic
                                            (let~ q :=
                                              M.alloc (|
                                                BinOp.Wrap.div (|
                                                  M.read (| remainder |),
                                                  M.read (| ten_kappa |)
                                                |)
                                              |) in
                                            let~ r :=
                                              M.alloc (|
                                                BinOp.Wrap.rem (|
                                                  M.read (| remainder |),
                                                  M.read (| ten_kappa |)
                                                |)
                                              |) 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 (| q |),
                                                                          Value.Integer
                                                                            IntegerKind.U32
                                                                            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: q < 10"
                                                                        |)
                                                                      ]
                                                                    |)
                                                                  |)
                                                                |)));
                                                            fun γ =>
                                                              ltac:(M.monadic
                                                                (M.alloc (| Value.Tuple [] |)))
                                                          ]
                                                        |) in
                                                      M.alloc (| Value.Tuple [] |)));
                                                  fun γ =>
                                                    ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                                ]
                                              |) in
                                            let~ _ :=
                                              M.write (|
                                                M.SubPointer.get_array_field (|
                                                  M.read (| buf |),
                                                  i
                                                |),
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply
                                                      (Ty.path
                                                        "core::mem::maybe_uninit::MaybeUninit")
                                                      []
                                                      [ Ty.path "u8" ],
                                                    "new",
                                                    []
                                                  |),
                                                  [
                                                    BinOp.Wrap.add (|
                                                      M.read (| UnsupportedLiteral |),
                                                      M.rust_cast (M.read (| q |))
                                                    |)
                                                  ]
                                                |)
                                              |) in
                                            let~ _ :=
                                              let β := i in
                                              M.write (|
                                                β,
                                                BinOp.Wrap.add (|
                                                  M.read (| β |),
                                                  Value.Integer IntegerKind.Usize 1
                                                |)
                                              |) in
                                            let~ plus1rem :=
                                              M.alloc (|
                                                BinOp.Wrap.add (|
                                                  BinOp.Wrap.shl (|
                                                    M.rust_cast (M.read (| r |)),
                                                    M.read (| e |)
                                                  |),
                                                  M.read (| plus1frac |)
                                                |)
                                              |) in
                                            let~ _ :=
                                              M.match_operator (|
                                                M.alloc (| Value.Tuple [] |),
                                                [
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ :=
                                                        M.use
                                                          (M.alloc (|
                                                            BinOp.lt (|
                                                              M.read (| plus1rem |),
                                                              M.read (| delta1 |)
                                                            |)
                                                          |)) in
                                                      let _ :=
                                                        M.is_constant_or_break_match (|
                                                          M.read (| γ |),
                                                          Value.Bool true
                                                        |) in
                                                      M.alloc (|
                                                        M.never_to_any (|
                                                          M.read (|
                                                            let~ ten_kappa :=
                                                              M.alloc (|
                                                                BinOp.Wrap.shl (|
                                                                  M.rust_cast
                                                                    (M.read (| ten_kappa |)),
                                                                  M.read (| e |)
                                                                |)
                                                              |) in
                                                            M.return_ (|
                                                              M.call_closure (|
                                                                M.get_function (|
                                                                  "core::num::flt2dec::strategy::grisu::format_shortest_opt.round_and_weed",
                                                                  []
                                                                |),
                                                                [
                                                                  M.call_closure (|
                                                                    M.get_associated_function (|
                                                                      Ty.apply
                                                                        (Ty.path
                                                                          "core::mem::maybe_uninit::MaybeUninit")
                                                                        []
                                                                        [ Ty.path "u8" ],
                                                                      "slice_assume_init_mut",
                                                                      []
                                                                    |),
                                                                    [
                                                                      M.call_closure (|
                                                                        M.get_trait_method (|
                                                                          "core::ops::index::IndexMut",
                                                                          Ty.apply
                                                                            (Ty.path "slice")
                                                                            []
                                                                            [
                                                                              Ty.apply
                                                                                (Ty.path
                                                                                  "core::mem::maybe_uninit::MaybeUninit")
                                                                                []
                                                                                [ Ty.path "u8" ]
                                                                            ],
                                                                          [
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "core::ops::range::RangeTo")
                                                                              []
                                                                              [ Ty.path "usize" ]
                                                                          ],
                                                                          "index_mut",
                                                                          []
                                                                        |),
                                                                        [
                                                                          M.read (| buf |);
                                                                          Value.StructRecord
                                                                            "core::ops::range::RangeTo"
                                                                            [
                                                                              ("end_",
                                                                                M.read (| i |))
                                                                            ]
                                                                        ]
                                                                      |)
                                                                    ]
                                                                  |);
                                                                  M.read (| exp |);
                                                                  M.read (| plus1rem |);
                                                                  M.read (| delta1 |);
                                                                  BinOp.Wrap.sub (|
                                                                    M.read (| plus1 |),
                                                                    M.read (|
                                                                      M.SubPointer.get_struct_record_field (|
                                                                        v,
                                                                        "core::num::diy_float::Fp",
                                                                        "f"
                                                                      |)
                                                                    |)
                                                                  |);
                                                                  M.read (| ten_kappa |);
                                                                  Value.Integer IntegerKind.U64 1
                                                                ]
                                                              |)
                                                            |)
                                                          |)
                                                        |)
                                                      |)));
                                                  fun γ =>
                                                    ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                                ]
                                              |) in
                                            let~ _ :=
                                              M.match_operator (|
                                                M.alloc (| Value.Tuple [] |),
                                                [
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ :=
                                                        M.use
                                                          (M.alloc (|
                                                            BinOp.gt (|
                                                              M.read (| i |),
                                                              M.rust_cast (M.read (| max_kappa |))
                                                            |)
                                                          |)) in
                                                      let _ :=
                                                        M.is_constant_or_break_match (|
                                                          M.read (| γ |),
                                                          Value.Bool true
                                                        |) in
                                                      M.alloc (|
                                                        M.never_to_any (|
                                                          M.read (|
                                                            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
                                                                              [
                                                                                ten_kappa;
                                                                                M.alloc (|
                                                                                  Value.Integer
                                                                                    IntegerKind.U32
                                                                                    1
                                                                                |)
                                                                              ]
                                                                          |),
                                                                          [
                                                                            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 left_val :=
                                                                                  M.copy (|
                                                                                    γ0_0
                                                                                  |) in
                                                                                let right_val :=
                                                                                  M.copy (|
                                                                                    γ0_1
                                                                                  |) in
                                                                                M.match_operator (|
                                                                                  M.alloc (|
                                                                                    Value.Tuple []
                                                                                  |),
                                                                                  [
                                                                                    fun γ =>
                                                                                      ltac:(M.monadic
                                                                                        (let γ :=
                                                                                          M.use
                                                                                            (M.alloc (|
                                                                                              UnOp.not (|
                                                                                                BinOp.eq (|
                                                                                                  M.read (|
                                                                                                    M.read (|
                                                                                                      left_val
                                                                                                    |)
                                                                                                  |),
                                                                                                  M.read (|
                                                                                                    M.read (|
                                                                                                      right_val
                                                                                                    |)
                                                                                                  |)
                                                                                                |)
                                                                                              |)
                                                                                            |)) in
                                                                                        let _ :=
                                                                                          M.is_constant_or_break_match (|
                                                                                            M.read (|
                                                                                              γ
                                                                                            |),
                                                                                            Value.Bool
                                                                                              true
                                                                                          |) in
                                                                                        M.alloc (|
                                                                                          M.never_to_any (|
                                                                                            M.read (|
                                                                                              let~
                                                                                                    kind :=
                                                                                                M.alloc (|
                                                                                                  Value.StructTuple
                                                                                                    "core::panicking::AssertKind::Eq"
                                                                                                    []
                                                                                                |) in
                                                                                              M.alloc (|
                                                                                                M.call_closure (|
                                                                                                  M.get_function (|
                                                                                                    "core::panicking::assert_failed",
                                                                                                    [
                                                                                                      Ty.path
                                                                                                        "u32";
                                                                                                      Ty.path
                                                                                                        "u32"
                                                                                                    ]
                                                                                                  |),
                                                                                                  [
                                                                                                    M.read (|
                                                                                                      kind
                                                                                                    |);
                                                                                                    M.read (|
                                                                                                      left_val
                                                                                                    |);
                                                                                                    M.read (|
                                                                                                      right_val
                                                                                                    |);
                                                                                                    Value.StructTuple
                                                                                                      "core::option::Option::None"
                                                                                                      []
                                                                                                  ]
                                                                                                |)
                                                                                              |)
                                                                                            |)
                                                                                          |)
                                                                                        |)));
                                                                                    fun γ =>
                                                                                      ltac:(M.monadic
                                                                                        (M.alloc (|
                                                                                          Value.Tuple
                                                                                            []
                                                                                        |)))
                                                                                  ]
                                                                                |)))
                                                                          ]
                                                                        |) in
                                                                      M.alloc (|
                                                                        Value.Tuple []
                                                                      |)));
                                                                  fun γ =>
                                                                    ltac:(M.monadic
                                                                      (M.alloc (|
                                                                        Value.Tuple []
                                                                      |)))
                                                                ]
                                                              |) in
                                                            M.break (||)
                                                          |)
                                                        |)
                                                      |)));
                                                  fun γ =>
                                                    ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                                ]
                                              |) in
                                            let~ _ :=
                                              let β := ten_kappa in
                                              M.write (|
                                                β,
                                                BinOp.Wrap.div (|
                                                  M.read (| β |),
                                                  Value.Integer IntegerKind.U32 10
                                                |)
                                              |) in
                                            let~ _ := M.write (| remainder, M.read (| r |) |) in
                                            M.alloc (| Value.Tuple [] |)))
                                        |) in
                                      let~ remainder := M.copy (| plus1frac |) in
                                      let~ threshold := M.copy (| delta1frac |) in
                                      let~ ulp := M.alloc (| Value.Integer IntegerKind.U64 1 |) in
                                      let~ _ :=
                                        M.alloc (|
                                          M.never_to_any (|
                                            M.read (|
                                              M.loop (|
                                                ltac:(M.monadic
                                                  (let~ _ :=
                                                    let β := remainder in
                                                    M.write (|
                                                      β,
                                                      BinOp.Wrap.mul (|
                                                        M.read (| β |),
                                                        Value.Integer IntegerKind.U64 10
                                                      |)
                                                    |) in
                                                  let~ _ :=
                                                    let β := threshold in
                                                    M.write (|
                                                      β,
                                                      BinOp.Wrap.mul (|
                                                        M.read (| β |),
                                                        Value.Integer IntegerKind.U64 10
                                                      |)
                                                    |) in
                                                  let~ _ :=
                                                    let β := ulp in
                                                    M.write (|
                                                      β,
                                                      BinOp.Wrap.mul (|
                                                        M.read (| β |),
                                                        Value.Integer IntegerKind.U64 10
                                                      |)
                                                    |) in
                                                  let~ q :=
                                                    M.alloc (|
                                                      BinOp.Wrap.shr (|
                                                        M.read (| remainder |),
                                                        M.read (| e |)
                                                      |)
                                                    |) in
                                                  let~ r :=
                                                    M.alloc (|
                                                      BinOp.bit_and
                                                        (M.read (| remainder |))
                                                        (BinOp.Wrap.sub (|
                                                          BinOp.Wrap.shl (|
                                                            Value.Integer IntegerKind.U64 1,
                                                            M.read (| e |)
                                                          |),
                                                          Value.Integer IntegerKind.U64 1
                                                        |))
                                                    |) 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 (| q |),
                                                                                Value.Integer
                                                                                  IntegerKind.U64
                                                                                  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: q < 10"
                                                                              |)
                                                                            ]
                                                                          |)
                                                                        |)
                                                                      |)));
                                                                  fun γ =>
                                                                    ltac:(M.monadic
                                                                      (M.alloc (|
                                                                        Value.Tuple []
                                                                      |)))
                                                                ]
                                                              |) in
                                                            M.alloc (| Value.Tuple [] |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (M.alloc (| Value.Tuple [] |)))
                                                      ]
                                                    |) in
                                                  let~ _ :=
                                                    M.write (|
                                                      M.SubPointer.get_array_field (|
                                                        M.read (| buf |),
                                                        i
                                                      |),
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.apply
                                                            (Ty.path
                                                              "core::mem::maybe_uninit::MaybeUninit")
                                                            []
                                                            [ Ty.path "u8" ],
                                                          "new",
                                                          []
                                                        |),
                                                        [
                                                          BinOp.Wrap.add (|
                                                            M.read (| UnsupportedLiteral |),
                                                            M.rust_cast (M.read (| q |))
                                                          |)
                                                        ]
                                                      |)
                                                    |) in
                                                  let~ _ :=
                                                    let β := i in
                                                    M.write (|
                                                      β,
                                                      BinOp.Wrap.add (|
                                                        M.read (| β |),
                                                        Value.Integer IntegerKind.Usize 1
                                                      |)
                                                    |) in
                                                  let~ _ :=
                                                    M.match_operator (|
                                                      M.alloc (| Value.Tuple [] |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ :=
                                                              M.use
                                                                (M.alloc (|
                                                                  BinOp.lt (|
                                                                    M.read (| r |),
                                                                    M.read (| threshold |)
                                                                  |)
                                                                |)) in
                                                            let _ :=
                                                              M.is_constant_or_break_match (|
                                                                M.read (| γ |),
                                                                Value.Bool true
                                                              |) in
                                                            M.alloc (|
                                                              M.never_to_any (|
                                                                M.read (|
                                                                  let~ ten_kappa :=
                                                                    M.alloc (|
                                                                      BinOp.Wrap.shl (|
                                                                        Value.Integer
                                                                          IntegerKind.U64
                                                                          1,
                                                                        M.read (| e |)
                                                                      |)
                                                                    |) in
                                                                  M.return_ (|
                                                                    M.call_closure (|
                                                                      M.get_function (|
                                                                        "core::num::flt2dec::strategy::grisu::format_shortest_opt.round_and_weed",
                                                                        []
                                                                      |),
                                                                      [
                                                                        M.call_closure (|
                                                                          M.get_associated_function (|
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "core::mem::maybe_uninit::MaybeUninit")
                                                                              []
                                                                              [ Ty.path "u8" ],
                                                                            "slice_assume_init_mut",
                                                                            []
                                                                          |),
                                                                          [
                                                                            M.call_closure (|
                                                                              M.get_trait_method (|
                                                                                "core::ops::index::IndexMut",
                                                                                Ty.apply
                                                                                  (Ty.path "slice")
                                                                                  []
                                                                                  [
                                                                                    Ty.apply
                                                                                      (Ty.path
                                                                                        "core::mem::maybe_uninit::MaybeUninit")
                                                                                      []
                                                                                      [ Ty.path "u8"
                                                                                      ]
                                                                                  ],
                                                                                [
                                                                                  Ty.apply
                                                                                    (Ty.path
                                                                                      "core::ops::range::RangeTo")
                                                                                    []
                                                                                    [
                                                                                      Ty.path
                                                                                        "usize"
                                                                                    ]
                                                                                ],
                                                                                "index_mut",
                                                                                []
                                                                              |),
                                                                              [
                                                                                M.read (| buf |);
                                                                                Value.StructRecord
                                                                                  "core::ops::range::RangeTo"
                                                                                  [
                                                                                    ("end_",
                                                                                      M.read (|
                                                                                        i
                                                                                      |))
                                                                                  ]
                                                                              ]
                                                                            |)
                                                                          ]
                                                                        |);
                                                                        M.read (| exp |);
                                                                        M.read (| r |);
                                                                        M.read (| threshold |);
                                                                        BinOp.Wrap.mul (|
                                                                          BinOp.Wrap.sub (|
                                                                            M.read (| plus1 |),
                                                                            M.read (|
                                                                              M.SubPointer.get_struct_record_field (|
                                                                                v,
                                                                                "core::num::diy_float::Fp",
                                                                                "f"
                                                                              |)
                                                                            |)
                                                                          |),
                                                                          M.read (| ulp |)
                                                                        |);
                                                                        M.read (| ten_kappa |);
                                                                        M.read (| ulp |)
                                                                      ]
                                                                    |)
                                                                  |)
                                                                |)
                                                              |)
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (M.alloc (| Value.Tuple [] |)))
                                                      ]
                                                    |) in
                                                  let~ _ :=
                                                    M.write (| remainder, M.read (| r |) |) in
                                                  M.alloc (| Value.Tuple [] |)))
                                              |)
                                            |)
                                          |)
                                        |) in
                                      M.alloc (| Value.Tuple [] |)))
                                ]
                              |)))
                        ]
                      |)
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Function_format_shortest_opt :
          M.IsFunction
            "core::num::flt2dec::strategy::grisu::format_shortest_opt"
            format_shortest_opt.
        
        Module format_shortest_opt.
          (*
              fn round_and_weed(
                  buf: &mut [u8],
                  exp: i16,
                  remainder: u64,
                  threshold: u64,
                  plus1v: u64,
                  ten_kappa: u64,
                  ulp: u64,
              ) -> Option<(&[u8], i16)> {
                  assert!(!buf.is_empty());
          
                  // produce two approximations to `v` (actually `plus1 - v`) within 1.5 ulps.
                  // the resulting representation should be the closest representation to both.
                  //
                  // here `plus1 - v` is used since calculations are done with respect to `plus1`
                  // in order to avoid overflow/underflow (hence the seemingly swapped names).
                  let plus1v_down = plus1v + ulp; // plus1 - (v - 1 ulp)
                  let plus1v_up = plus1v - ulp; // plus1 - (v + 1 ulp)
          
                  // decrease the last digit and stop at the closest representation to `v + 1 ulp`.
                  let mut plus1w = remainder; // plus1w(n) = plus1 - w(n)
                  {
                      let last = buf.last_mut().unwrap();
          
                      // we work with the approximated digits `w(n)`, which is initially equal to `plus1 -
                      // plus1 % 10^kappa`. after running the loop body `n` times, `w(n) = plus1 -
                      // plus1 % 10^kappa - n * 10^kappa`. we set `plus1w(n) = plus1 - w(n) =
                      // plus1 % 10^kappa + n * 10^kappa` (thus `remainder = plus1w(0)`) to simplify checks.
                      // note that `plus1w(n)` is always increasing.
                      //
                      // we have three conditions to terminate. any of them will make the loop unable to
                      // proceed, but we then have at least one valid representation known to be closest to
                      // `v + 1 ulp` anyway. we will denote them as TC1 through TC3 for brevity.
                      //
                      // TC1: `w(n) <= v + 1 ulp`, i.e., this is the last repr that can be the closest one.
                      // this is equivalent to `plus1 - w(n) = plus1w(n) >= plus1 - (v + 1 ulp) = plus1v_up`.
                      // combined with TC2 (which checks if `w(n+1)` is valid), this prevents the possible
                      // overflow on the calculation of `plus1w(n)`.
                      //
                      // TC2: `w(n+1) < minus1`, i.e., the next repr definitely does not round to `v`.
                      // this is equivalent to `plus1 - w(n) + 10^kappa = plus1w(n) + 10^kappa >
                      // plus1 - minus1 = threshold`. the left hand side can overflow, but we know
                      // `threshold > plus1v`, so if TC1 is false, `threshold - plus1w(n) >
                      // threshold - (plus1v - 1 ulp) > 1 ulp` and we can safely test if
                      // `threshold - plus1w(n) < 10^kappa` instead.
                      //
                      // TC3: `abs(w(n) - (v + 1 ulp)) <= abs(w(n+1) - (v + 1 ulp))`, i.e., the next repr is
                      // no closer to `v + 1 ulp` than the current repr. given `z(n) = plus1v_up - plus1w(n)`,
                      // this becomes `abs(z(n)) <= abs(z(n+1))`. again assuming that TC1 is false, we have
                      // `z(n) > 0`. we have two cases to consider:
                      //
                      // - when `z(n+1) >= 0`: TC3 becomes `z(n) <= z(n+1)`. as `plus1w(n)` is increasing,
                      //   `z(n)` should be decreasing and this is clearly false.
                      // - when `z(n+1) < 0`:
                      //   - TC3a: the precondition is `plus1v_up < plus1w(n) + 10^kappa`. assuming TC2 is
                      //     false, `threshold >= plus1w(n) + 10^kappa` so it cannot overflow.
                      //   - TC3b: TC3 becomes `z(n) <= -z(n+1)`, i.e., `plus1v_up - plus1w(n) >=
                      //     plus1w(n+1) - plus1v_up = plus1w(n) + 10^kappa - plus1v_up`. the negated TC1
                      //     gives `plus1v_up > plus1w(n)`, so it cannot overflow or underflow when
                      //     combined with TC3a.
                      //
                      // consequently, we should stop when `TC1 || TC2 || (TC3a && TC3b)`. the following is
                      // equal to its inverse, `!TC1 && !TC2 && (!TC3a || !TC3b)`.
                      while plus1w < plus1v_up
                          && threshold - plus1w >= ten_kappa
                          && (plus1w + ten_kappa < plus1v_up
                              || plus1v_up - plus1w >= plus1w + ten_kappa - plus1v_up)
                      {
                          *last -= 1;
                          debug_assert!( *last > b'0'); // the shortest repr cannot end with `0`
                          plus1w += ten_kappa;
                      }
                  }
          
                  // check if this representation is also the closest representation to `v - 1 ulp`.
                  //
                  // this is simply same to the terminating conditions for `v + 1 ulp`, with all `plus1v_up`
                  // replaced by `plus1v_down` instead. overflow analysis equally holds.
                  if plus1w < plus1v_down
                      && threshold - plus1w >= ten_kappa
                      && (plus1w + ten_kappa < plus1v_down
                          || plus1v_down - plus1w >= plus1w + ten_kappa - plus1v_down)
                  {
                      return None;
                  }
          
                  // now we have the closest representation to `v` between `plus1` and `minus1`.
                  // this is too liberal, though, so we reject any `w(n)` not between `plus0` and `minus0`,
                  // i.e., `plus1 - plus1w(n) <= minus0` or `plus1 - plus1w(n) >= plus0`. we utilize the facts
                  // that `threshold = plus1 - minus1` and `plus1 - plus0 = minus0 - minus1 = 2 ulp`.
                  if 2 * ulp <= plus1w && plus1w <= threshold - 4 * ulp { Some((buf, exp)) } else { None }
              }
          *)
          Definition round_and_weed (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
            match ε, τ, α with
            | [], [], [ buf; exp; remainder; threshold; plus1v; ten_kappa; ulp ] =>
              ltac:(M.monadic
                (let buf := M.alloc (| buf |) in
                let exp := M.alloc (| exp |) in
                let remainder := M.alloc (| remainder |) in
                let threshold := M.alloc (| threshold |) in
                let plus1v := M.alloc (| plus1v |) in
                let ten_kappa := M.alloc (| ten_kappa |) in
                let ulp := M.alloc (| ulp |) in
                M.catch_return (|
                  ltac:(M.monadic
                    (M.read (|
                      let~ _ :=
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      UnOp.not (|
                                        UnOp.not (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                              "is_empty",
                                              []
                                            |),
                                            [ M.read (| buf |) ]
                                          |)
                                        |)
                                      |)
                                    |)) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.call_closure (|
                                      M.get_function (| "core::panicking::panic", [] |),
                                      [
                                        M.read (|
                                          Value.String "assertion failed: !buf.is_empty()"
                                        |)
                                      ]
                                    |)
                                  |)
                                |)));
                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                          ]
                        |) in
                      let~ plus1v_down :=
                        M.alloc (| BinOp.Wrap.add (| M.read (| plus1v |), M.read (| ulp |) |) |) in
                      let~ plus1v_up :=
                        M.alloc (| BinOp.Wrap.sub (| M.read (| plus1v |), M.read (| ulp |) |) |) in
                      let~ plus1w := M.copy (| remainder |) in
                      let~ _ :=
                        let~ last :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "core::option::Option")
                                  []
                                  [ Ty.apply (Ty.path "&mut") [] [ Ty.path "u8" ] ],
                                "unwrap",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                    "last_mut",
                                    []
                                  |),
                                  [ M.read (| buf |) ]
                                |)
                              ]
                            |)
                          |) in
                        M.loop (|
                          ltac:(M.monadic
                            (M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          LogicalOp.and (|
                                            LogicalOp.and (|
                                              BinOp.lt (|
                                                M.read (| plus1w |),
                                                M.read (| plus1v_up |)
                                              |),
                                              ltac:(M.monadic
                                                (BinOp.ge (|
                                                  BinOp.Wrap.sub (|
                                                    M.read (| threshold |),
                                                    M.read (| plus1w |)
                                                  |),
                                                  M.read (| ten_kappa |)
                                                |)))
                                            |),
                                            ltac:(M.monadic
                                              (LogicalOp.or (|
                                                BinOp.lt (|
                                                  BinOp.Wrap.add (|
                                                    M.read (| plus1w |),
                                                    M.read (| ten_kappa |)
                                                  |),
                                                  M.read (| plus1v_up |)
                                                |),
                                                ltac:(M.monadic
                                                  (BinOp.ge (|
                                                    BinOp.Wrap.sub (|
                                                      M.read (| plus1v_up |),
                                                      M.read (| plus1w |)
                                                    |),
                                                    BinOp.Wrap.sub (|
                                                      BinOp.Wrap.add (|
                                                        M.read (| plus1w |),
                                                        M.read (| ten_kappa |)
                                                      |),
                                                      M.read (| plus1v_up |)
                                                    |)
                                                  |)))
                                              |)))
                                          |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    let~ _ :=
                                      let β := M.read (| last |) in
                                      M.write (|
                                        β,
                                        BinOp.Wrap.sub (|
                                          M.read (| β |),
                                          Value.Integer IntegerKind.U8 1
                                        |)
                                      |) 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.gt (|
                                                                  M.read (| M.read (| last |) |),
                                                                  M.read (| UnsupportedLiteral |)
                                                                |)
                                                              |)
                                                            |)) 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: *last > b'0'"
                                                                |)
                                                              ]
                                                            |)
                                                          |)
                                                        |)));
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (M.alloc (| Value.Tuple [] |)))
                                                  ]
                                                |) in
                                              M.alloc (| Value.Tuple [] |)));
                                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                        ]
                                      |) in
                                    let~ _ :=
                                      let β := plus1w in
                                      M.write (|
                                        β,
                                        BinOp.Wrap.add (| M.read (| β |), M.read (| ten_kappa |) |)
                                      |) in
                                    M.alloc (| Value.Tuple [] |)));
                                fun γ =>
                                  ltac:(M.monadic
                                    (M.alloc (|
                                      M.never_to_any (|
                                        M.read (|
                                          let~ _ :=
                                            M.alloc (|
                                              M.never_to_any (| M.read (| M.break (||) |) |)
                                            |) in
                                          M.alloc (| Value.Tuple [] |)
                                        |)
                                      |)
                                    |)))
                              ]
                            |)))
                        |) in
                      let~ _ :=
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      LogicalOp.and (|
                                        LogicalOp.and (|
                                          BinOp.lt (|
                                            M.read (| plus1w |),
                                            M.read (| plus1v_down |)
                                          |),
                                          ltac:(M.monadic
                                            (BinOp.ge (|
                                              BinOp.Wrap.sub (|
                                                M.read (| threshold |),
                                                M.read (| plus1w |)
                                              |),
                                              M.read (| ten_kappa |)
                                            |)))
                                        |),
                                        ltac:(M.monadic
                                          (LogicalOp.or (|
                                            BinOp.lt (|
                                              BinOp.Wrap.add (|
                                                M.read (| plus1w |),
                                                M.read (| ten_kappa |)
                                              |),
                                              M.read (| plus1v_down |)
                                            |),
                                            ltac:(M.monadic
                                              (BinOp.ge (|
                                                BinOp.Wrap.sub (|
                                                  M.read (| plus1v_down |),
                                                  M.read (| plus1w |)
                                                |),
                                                BinOp.Wrap.sub (|
                                                  BinOp.Wrap.add (|
                                                    M.read (| plus1w |),
                                                    M.read (| ten_kappa |)
                                                  |),
                                                  M.read (| plus1v_down |)
                                                |)
                                              |)))
                                          |)))
                                      |)
                                    |)) 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
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.use
                                  (M.alloc (|
                                    LogicalOp.and (|
                                      BinOp.le (|
                                        BinOp.Wrap.mul (|
                                          Value.Integer IntegerKind.U64 2,
                                          M.read (| ulp |)
                                        |),
                                        M.read (| plus1w |)
                                      |),
                                      ltac:(M.monadic
                                        (BinOp.le (|
                                          M.read (| plus1w |),
                                          BinOp.Wrap.sub (|
                                            M.read (| threshold |),
                                            BinOp.Wrap.mul (|
                                              Value.Integer IntegerKind.U64 4,
                                              M.read (| ulp |)
                                            |)
                                          |)
                                        |)))
                                    |)
                                  |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              M.alloc (|
                                Value.StructTuple
                                  "core::option::Option::Some"
                                  [ Value.Tuple [ M.read (| buf |); M.read (| exp |) ] ]
                              |)));
                          fun γ =>
                            ltac:(M.monadic
                              (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                        ]
                      |)
                    |)))
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          Axiom Function_round_and_weed :
            M.IsFunction
              "core::num::flt2dec::strategy::grisu::format_shortest_opt::round_and_weed"
              round_and_weed.
        End format_shortest_opt.
        
        (*
        pub fn format_shortest<'a>(
            d: &Decoded,
            buf: &'a mut [MaybeUninit<u8>],
        ) -> (/*digits*/ &'a [u8], /*exp*/ i16) {
            use crate::num::flt2dec::strategy::dragon::format_shortest as fallback;
            // SAFETY: The borrow checker is not smart enough to let us use `buf`
            // in the second branch, so we launder the lifetime here. But we only re-use
            // `buf` if `format_shortest_opt` returned `None` so this is okay.
            match format_shortest_opt(d, unsafe { &mut *(buf as *mut _) }) {
                Some(ret) => ret,
                None => fallback(d, buf),
            }
        }
        *)
        Definition format_shortest (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ d; buf ] =>
            ltac:(M.monadic
              (let d := M.alloc (| d |) in
              let buf := M.alloc (| buf |) in
              M.read (|
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::num::flt2dec::strategy::grisu::format_shortest_opt",
                        []
                      |),
                      [ M.read (| d |); M.read (| M.use (M.alloc (| M.read (| buf |) |)) |) ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::option::Option::Some",
                            0
                          |) in
                        let ret := M.copy (| γ0_0 |) in
                        ret));
                    fun γ =>
                      ltac:(M.monadic
                        (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_function (|
                              "core::num::flt2dec::strategy::dragon::format_shortest",
                              []
                            |),
                            [ M.read (| d |); M.read (| buf |) ]
                          |)
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Function_format_shortest :
          M.IsFunction "core::num::flt2dec::strategy::grisu::format_shortest" format_shortest.
        
        (*
        pub fn format_exact_opt<'a>(
            d: &Decoded,
            buf: &'a mut [MaybeUninit<u8>],
            limit: i16,
        ) -> Option<(/*digits*/ &'a [u8], /*exp*/ i16)> {
            assert!(d.mant > 0);
            assert!(d.mant < (1 << 61)); // we need at least three bits of additional precision
            assert!(!buf.is_empty());
        
            // normalize and scale `v`.
            let v = Fp { f: d.mant, e: d.exp }.normalize();
            let (minusk, cached) = cached_power(ALPHA - v.e - 64, GAMMA - v.e - 64);
            let v = v.mul(&cached);
        
            // divide `v` into integral and fractional parts.
            let e = -v.e as usize;
            let vint = (v.f >> e) as u32;
            let vfrac = v.f & ((1 << e) - 1);
        
            let requested_digits = buf.len();
        
            const POW10_UP_TO_9: [u32; 10] =
                [1, 10, 100, 1000, 10_000, 100_000, 1_000_000, 10_000_000, 100_000_000, 1_000_000_000];
        
            // We deviate from the original algorithm here and do some early checks to determine if we can satisfy requested_digits.
            // If we determine that we can't, we exit early and avoid most of the heavy lifting that the algorithm otherwise does.
            //
            // When vfrac is zero, we can easily determine if vint can satisfy requested digits:
            //      If requested_digits >= 11, vint is not able to exhaust the count by itself since 10^(11 -1) > u32 max value >= vint.
            //      If vint < 10^(requested_digits - 1), vint cannot exhaust the count.
            //      Otherwise, vint might be able to exhaust the count and we need to execute the rest of the code.
            if (vfrac == 0) && ((requested_digits >= 11) || (vint < POW10_UP_TO_9[requested_digits - 1])) {
                return None;
            }
        
            // both old `v` and new `v` (scaled by `10^-k`) has an error of < 1 ulp (Theorem 5.1).
            // as we don't know the error is positive or negative, we use two approximations
            // spaced equally and have the maximal error of 2 ulps (same to the shortest case).
            //
            // the goal is to find the exactly rounded series of digits that are common to
            // both `v - 1 ulp` and `v + 1 ulp`, so that we are maximally confident.
            // if this is not possible, we don't know which one is the correct output for `v`,
            // so we give up and fall back.
            //
            // `err` is defined as `1 ulp * 2^e` here (same to the ulp in `vfrac`),
            // and we will scale it whenever `v` gets scaled.
            let mut err = 1;
        
            // calculate the largest `10^max_kappa` no more than `v` (thus `v < 10^(max_kappa+1)`).
            // this is an upper bound of `kappa` below.
            let (max_kappa, max_ten_kappa) = max_pow10_no_more_than(vint);
        
            let mut i = 0;
            let exp = max_kappa as i16 - minusk + 1;
        
            // if we are working with the last-digit limitation, we need to shorten the buffer
            // before the actual rendering in order to avoid double rounding.
            // note that we have to enlarge the buffer again when rounding up happens!
            let len = if exp <= limit {
                // oops, we cannot even produce *one* digit.
                // this is possible when, say, we've got something like 9.5 and it's being rounded to 10.
                //
                // in principle we can immediately call `possibly_round` with an empty buffer,
                // but scaling `max_ten_kappa << e` by 10 can result in overflow.
                // thus we are being sloppy here and widen the error range by a factor of 10.
                // this will increase the false negative rate, but only very, *very* slightly;
                // it can only matter noticeably when the mantissa is bigger than 60 bits.
                //
                // SAFETY: `len=0`, so the obligation of having initialized this memory is trivial.
                return unsafe {
                    possibly_round(buf, 0, exp, limit, v.f / 10, (max_ten_kappa as u64) << e, err << e)
                };
            } else if ((exp as i32 - limit as i32) as usize) < buf.len() {
                (exp - limit) as usize
            } else {
                buf.len()
            };
            debug_assert!(len > 0);
        
            // render integral parts.
            // the error is entirely fractional, so we don't need to check it in this part.
            let mut kappa = max_kappa as i16;
            let mut ten_kappa = max_ten_kappa; // 10^kappa
            let mut remainder = vint; // digits yet to be rendered
            loop {
                // we always have at least one digit to render
                // invariants:
                // - `remainder < 10^(kappa+1)`
                // - `vint = d[0..n-1] * 10^(kappa+1) + remainder`
                //   (it follows that `remainder = vint % 10^(kappa+1)`)
        
                // divide `remainder` by `10^kappa`. both are scaled by `2^-e`.
                let q = remainder / ten_kappa;
                let r = remainder % ten_kappa;
                debug_assert!(q < 10);
                buf[i] = MaybeUninit::new(b'0' + q as u8);
                i += 1;
        
                // is the buffer full? run the rounding pass with the remainder.
                if i == len {
                    let vrem = ((r as u64) << e) + vfrac; // == (v % 10^kappa) * 2^e
                    // SAFETY: we have initialized `len` many bytes.
                    return unsafe {
                        possibly_round(buf, len, exp, limit, vrem, (ten_kappa as u64) << e, err << e)
                    };
                }
        
                // break the loop when we have rendered all integral digits.
                // the exact number of digits is `max_kappa + 1` as `plus1 < 10^(max_kappa+1)`.
                if i > max_kappa as usize {
                    debug_assert_eq!(ten_kappa, 1);
                    debug_assert_eq!(kappa, 0);
                    break;
                }
        
                // restore invariants
                kappa -= 1;
                ten_kappa /= 10;
                remainder = r;
            }
        
            // render fractional parts.
            //
            // in principle we can continue to the last available digit and check for the accuracy.
            // unfortunately we are working with the finite-sized integers, so we need some criterion
            // to detect the overflow. V8 uses `remainder > err`, which becomes false when
            // the first `i` significant digits of `v - 1 ulp` and `v` differ. however this rejects
            // too many otherwise valid input.
            //
            // since the later phase has a correct overflow detection, we instead use tighter criterion:
            // we continue til `err` exceeds `10^kappa / 2`, so that the range between `v - 1 ulp` and
            // `v + 1 ulp` definitely contains two or more rounded representations. this is same to
            // the first two comparisons from `possibly_round`, for the reference.
            let mut remainder = vfrac;
            let maxerr = 1 << (e - 1);
            while err < maxerr {
                // invariants, where `m = max_kappa + 1` (# of digits in the integral part):
                // - `remainder < 2^e`
                // - `vfrac * 10^(n-m) = d[m..n-1] * 2^e + remainder`
                // - `err = 10^(n-m)`
        
                remainder *= 10; // won't overflow, `2^e * 10 < 2^64`
                err *= 10; // won't overflow, `err * 10 < 2^e * 5 < 2^64`
        
                // divide `remainder` by `10^kappa`.
                // both are scaled by `2^e / 10^kappa`, so the latter is implicit here.
                let q = remainder >> e;
                let r = remainder & ((1 << e) - 1);
                debug_assert!(q < 10);
                buf[i] = MaybeUninit::new(b'0' + q as u8);
                i += 1;
        
                // is the buffer full? run the rounding pass with the remainder.
                if i == len {
                    // SAFETY: we have initialized `len` many bytes.
                    return unsafe { possibly_round(buf, len, exp, limit, r, 1 << e, err) };
                }
        
                // restore invariants
                remainder = r;
            }
        
            // further calculation is useless (`possibly_round` definitely fails), so we give up.
            return None;
        
            // we've generated all requested digits of `v`, which should be also same to corresponding
            // digits of `v - 1 ulp`. now we check if there is a unique representation shared by
            // both `v - 1 ulp` and `v + 1 ulp`; this can be either same to generated digits, or
            // to the rounded-up version of those digits. if the range contains multiple representations
            // of the same length, we cannot be sure and should return `None` instead.
            //
            // all arguments here are scaled by the common (but implicit) value `k`, so that:
            // - `remainder = (v % 10^kappa) * k`
            // - `ten_kappa = 10^kappa * k`
            // - `ulp = 2^-e * k`
            //
            // SAFETY: the first `len` bytes of `buf` must be initialized.
            unsafe fn possibly_round(
                buf: &mut [MaybeUninit<u8>],
                mut len: usize,
                mut exp: i16,
                limit: i16,
                remainder: u64,
                ten_kappa: u64,
                ulp: u64,
            ) -> Option<(&[u8], i16)> {
                debug_assert!(remainder < ten_kappa);
        
                //           10^kappa
                //    :   :   :<->:   :
                //    :   :   :   :   :
                //    :|1 ulp|1 ulp|  :
                //    :|<--->|<--->|  :
                // ----|-----|-----|----
                //     |     v     |
                // v - 1 ulp   v + 1 ulp
                //
                // (for the reference, the dotted line indicates the exact value for
                // possible representations in given number of digits.)
                //
                // error is too large that there are at least three possible representations
                // between `v - 1 ulp` and `v + 1 ulp`. we cannot determine which one is correct.
                if ulp >= ten_kappa {
                    return None;
                }
        
                //    10^kappa
                //   :<------->:
                //   :         :
                //   : |1 ulp|1 ulp|
                //   : |<--->|<--->|
                // ----|-----|-----|----
                //     |     v     |
                // v - 1 ulp   v + 1 ulp
                //
                // in fact, 1/2 ulp is enough to introduce two possible representations.
                // (remember that we need a unique representation for both `v - 1 ulp` and `v + 1 ulp`.)
                // this won't overflow, as `ulp < ten_kappa` from the first check.
                if ten_kappa - ulp <= ulp {
                    return None;
                }
        
                //     remainder
                //       :<->|                           :
                //       :   |                           :
                //       :<--------- 10^kappa ---------->:
                //     | :   |                           :
                //     |1 ulp|1 ulp|                     :
                //     |<--->|<--->|                     :
                // ----|-----|-----|------------------------
                //     |     v     |
                // v - 1 ulp   v + 1 ulp
                //
                // if `v + 1 ulp` is closer to the rounded-down representation (which is already in `buf`),
                // then we can safely return. note that `v - 1 ulp` *can* be less than the current
                // representation, but as `1 ulp < 10^kappa / 2`, this condition is enough:
                // the distance between `v - 1 ulp` and the current representation
                // cannot exceed `10^kappa / 2`.
                //
                // the condition equals to `remainder + ulp < 10^kappa / 2`.
                // since this can easily overflow, first check if `remainder < 10^kappa / 2`.
                // we've already verified that `ulp < 10^kappa / 2`, so as long as
                // `10^kappa` did not overflow after all, the second check is fine.
                if ten_kappa - remainder > remainder && ten_kappa - 2 * remainder >= 2 * ulp {
                    // SAFETY: our caller initialized that memory.
                    return Some((unsafe { MaybeUninit::slice_assume_init_ref(&buf[..len]) }, exp));
                }
        
                //   :<------- remainder ------>|   :
                //   :                          |   :
                //   :<--------- 10^kappa --------->:
                //   :                    |     |   : |
                //   :                    |1 ulp|1 ulp|
                //   :                    |<--->|<--->|
                // -----------------------|-----|-----|-----
                //                        |     v     |
                //                    v - 1 ulp   v + 1 ulp
                //
                // on the other hands, if `v - 1 ulp` is closer to the rounded-up representation,
                // we should round up and return. for the same reason we don't need to check `v + 1 ulp`.
                //
                // the condition equals to `remainder - ulp >= 10^kappa / 2`.
                // again we first check if `remainder > ulp` (note that this is not `remainder >= ulp`,
                // as `10^kappa` is never zero). also note that `remainder - ulp <= 10^kappa`,
                // so the second check does not overflow.
                if remainder > ulp && ten_kappa - (remainder - ulp) <= remainder - ulp {
                    if let Some(c) =
                        // SAFETY: our caller must have initialized that memory.
                        round_up(unsafe { MaybeUninit::slice_assume_init_mut(&mut buf[..len]) })
                    {
                        // only add an additional digit when we've been requested the fixed precision.
                        // we also need to check that, if the original buffer was empty,
                        // the additional digit can only be added when `exp == limit` (edge case).
                        exp += 1;
                        if exp > limit && len < buf.len() {
                            buf[len] = MaybeUninit::new(c);
                            len += 1;
                        }
                    }
                    // SAFETY: we and our caller initialized that memory.
                    return Some((unsafe { MaybeUninit::slice_assume_init_ref(&buf[..len]) }, exp));
                }
        
                // otherwise we are doomed (i.e., some values between `v - 1 ulp` and `v + 1 ulp` are
                // rounding down and others are rounding up) and give up.
                None
            }
        }
        *)
        Definition format_exact_opt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ d; buf; limit ] =>
            ltac:(M.monadic
              (let d := M.alloc (| d |) in
              let buf := M.alloc (| buf |) in
              let limit := M.alloc (| limit |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.never_to_any (|
                    M.read (|
                      let~ _ :=
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      UnOp.not (|
                                        BinOp.gt (|
                                          M.read (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| d |),
                                              "core::num::flt2dec::decoder::Decoded",
                                              "mant"
                                            |)
                                          |),
                                          Value.Integer IntegerKind.U64 0
                                        |)
                                      |)
                                    |)) 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: d.mant > 0" |) ]
                                    |)
                                  |)
                                |)));
                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                          ]
                        |) in
                      let~ _ :=
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      UnOp.not (|
                                        BinOp.lt (|
                                          M.read (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| d |),
                                              "core::num::flt2dec::decoder::Decoded",
                                              "mant"
                                            |)
                                          |),
                                          BinOp.Wrap.shl (|
                                            Value.Integer IntegerKind.U64 1,
                                            Value.Integer IntegerKind.I32 61
                                          |)
                                        |)
                                      |)
                                    |)) 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: d.mant < (1 << 61)"
                                        |)
                                      ]
                                    |)
                                  |)
                                |)));
                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                          ]
                        |) in
                      let~ _ :=
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      UnOp.not (|
                                        UnOp.not (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply
                                                (Ty.path "slice")
                                                []
                                                [
                                                  Ty.apply
                                                    (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                                    []
                                                    [ Ty.path "u8" ]
                                                ],
                                              "is_empty",
                                              []
                                            |),
                                            [ M.read (| buf |) ]
                                          |)
                                        |)
                                      |)
                                    |)) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.call_closure (|
                                      M.get_function (| "core::panicking::panic", [] |),
                                      [
                                        M.read (|
                                          Value.String "assertion failed: !buf.is_empty()"
                                        |)
                                      ]
                                    |)
                                  |)
                                |)));
                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                          ]
                        |) in
                      let~ v :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::num::diy_float::Fp",
                              "normalize",
                              []
                            |),
                            [
                              M.alloc (|
                                Value.StructRecord
                                  "core::num::diy_float::Fp"
                                  [
                                    ("f",
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| d |),
                                          "core::num::flt2dec::decoder::Decoded",
                                          "mant"
                                        |)
                                      |));
                                    ("e",
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| d |),
                                          "core::num::flt2dec::decoder::Decoded",
                                          "exp"
                                        |)
                                      |))
                                  ]
                              |)
                            ]
                          |)
                        |) in
                      M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_function (|
                              "core::num::flt2dec::strategy::grisu::cached_power",
                              []
                            |),
                            [
                              BinOp.Wrap.sub (|
                                BinOp.Wrap.sub (|
                                  M.read (|
                                    M.get_constant (|
                                      "core::num::flt2dec::strategy::grisu::ALPHA"
                                    |)
                                  |),
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      v,
                                      "core::num::diy_float::Fp",
                                      "e"
                                    |)
                                  |)
                                |),
                                Value.Integer IntegerKind.I16 64
                              |);
                              BinOp.Wrap.sub (|
                                BinOp.Wrap.sub (|
                                  M.read (|
                                    M.get_constant (|
                                      "core::num::flt2dec::strategy::grisu::GAMMA"
                                    |)
                                  |),
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      v,
                                      "core::num::diy_float::Fp",
                                      "e"
                                    |)
                                  |)
                                |),
                                Value.Integer IntegerKind.I16 64
                              |)
                            ]
                          |)
                        |),
                        [
                          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 minusk := M.copy (| γ0_0 |) in
                              let cached := M.copy (| γ0_1 |) in
                              let~ v :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::num::diy_float::Fp",
                                      "mul",
                                      []
                                    |),
                                    [ v; cached ]
                                  |)
                                |) in
                              let~ e :=
                                M.alloc (|
                                  M.rust_cast
                                    (UnOp.neg (|
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          v,
                                          "core::num::diy_float::Fp",
                                          "e"
                                        |)
                                      |)
                                    |))
                                |) in
                              let~ vint :=
                                M.alloc (|
                                  M.rust_cast
                                    (BinOp.Wrap.shr (|
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          v,
                                          "core::num::diy_float::Fp",
                                          "f"
                                        |)
                                      |),
                                      M.read (| e |)
                                    |))
                                |) in
                              let~ vfrac :=
                                M.alloc (|
                                  BinOp.bit_and
                                    (M.read (|
                                      M.SubPointer.get_struct_record_field (|
                                        v,
                                        "core::num::diy_float::Fp",
                                        "f"
                                      |)
                                    |))
                                    (BinOp.Wrap.sub (|
                                      BinOp.Wrap.shl (|
                                        Value.Integer IntegerKind.U64 1,
                                        M.read (| e |)
                                      |),
                                      Value.Integer IntegerKind.U64 1
                                    |))
                                |) in
                              let~ requested_digits :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "slice")
                                        []
                                        [
                                          Ty.apply
                                            (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                            []
                                            [ Ty.path "u8" ]
                                        ],
                                      "len",
                                      []
                                    |),
                                    [ M.read (| buf |) ]
                                  |)
                                |) in
                              let~ _ :=
                                M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ :=
                                          M.use
                                            (M.alloc (|
                                              LogicalOp.and (|
                                                BinOp.eq (|
                                                  M.read (| vfrac |),
                                                  Value.Integer IntegerKind.U64 0
                                                |),
                                                ltac:(M.monadic
                                                  (LogicalOp.or (|
                                                    BinOp.ge (|
                                                      M.read (| requested_digits |),
                                                      Value.Integer IntegerKind.Usize 11
                                                    |),
                                                    ltac:(M.monadic
                                                      (BinOp.lt (|
                                                        M.read (| vint |),
                                                        M.read (|
                                                          M.SubPointer.get_array_field (|
                                                            M.get_constant (|
                                                              "core::num::flt2dec::strategy::grisu::format_exact_opt::POW10_UP_TO_9"
                                                            |),
                                                            M.alloc (|
                                                              BinOp.Wrap.sub (|
                                                                M.read (| requested_digits |),
                                                                Value.Integer IntegerKind.Usize 1
                                                              |)
                                                            |)
                                                          |)
                                                        |)
                                                      |)))
                                                  |)))
                                              |)
                                            |)) 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~ err := M.alloc (| Value.Integer IntegerKind.U64 1 |) in
                              M.match_operator (|
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_function (|
                                      "core::num::flt2dec::strategy::grisu::max_pow10_no_more_than",
                                      []
                                    |),
                                    [ M.read (| vint |) ]
                                  |)
                                |),
                                [
                                  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 max_kappa := M.copy (| γ0_0 |) in
                                      let max_ten_kappa := M.copy (| γ0_1 |) in
                                      let~ i := M.alloc (| Value.Integer IntegerKind.Usize 0 |) in
                                      let~ exp :=
                                        M.alloc (|
                                          BinOp.Wrap.add (|
                                            BinOp.Wrap.sub (|
                                              M.rust_cast (M.read (| max_kappa |)),
                                              M.read (| minusk |)
                                            |),
                                            Value.Integer IntegerKind.I16 1
                                          |)
                                        |) in
                                      let~ len :=
                                        M.copy (|
                                          M.match_operator (|
                                            M.alloc (| Value.Tuple [] |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ :=
                                                    M.use
                                                      (M.alloc (|
                                                        BinOp.le (|
                                                          M.read (| exp |),
                                                          M.read (| limit |)
                                                        |)
                                                      |)) in
                                                  let _ :=
                                                    M.is_constant_or_break_match (|
                                                      M.read (| γ |),
                                                      Value.Bool true
                                                    |) in
                                                  M.alloc (|
                                                    M.never_to_any (|
                                                      M.read (|
                                                        M.return_ (|
                                                          M.call_closure (|
                                                            M.get_function (|
                                                              "core::num::flt2dec::strategy::grisu::format_exact_opt.possibly_round",
                                                              []
                                                            |),
                                                            [
                                                              M.read (| buf |);
                                                              Value.Integer IntegerKind.Usize 0;
                                                              M.read (| exp |);
                                                              M.read (| limit |);
                                                              BinOp.Wrap.div (|
                                                                M.read (|
                                                                  M.SubPointer.get_struct_record_field (|
                                                                    v,
                                                                    "core::num::diy_float::Fp",
                                                                    "f"
                                                                  |)
                                                                |),
                                                                Value.Integer IntegerKind.U64 10
                                                              |);
                                                              BinOp.Wrap.shl (|
                                                                M.rust_cast
                                                                  (M.read (| max_ten_kappa |)),
                                                                M.read (| e |)
                                                              |);
                                                              BinOp.Wrap.shl (|
                                                                M.read (| err |),
                                                                M.read (| e |)
                                                              |)
                                                            ]
                                                          |)
                                                        |)
                                                      |)
                                                    |)
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (M.match_operator (|
                                                    M.alloc (| Value.Tuple [] |),
                                                    [
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ :=
                                                            M.use
                                                              (M.alloc (|
                                                                BinOp.lt (|
                                                                  M.rust_cast
                                                                    (BinOp.Wrap.sub (|
                                                                      M.rust_cast
                                                                        (M.read (| exp |)),
                                                                      M.rust_cast
                                                                        (M.read (| limit |))
                                                                    |)),
                                                                  M.call_closure (|
                                                                    M.get_associated_function (|
                                                                      Ty.apply
                                                                        (Ty.path "slice")
                                                                        []
                                                                        [
                                                                          Ty.apply
                                                                            (Ty.path
                                                                              "core::mem::maybe_uninit::MaybeUninit")
                                                                            []
                                                                            [ Ty.path "u8" ]
                                                                        ],
                                                                      "len",
                                                                      []
                                                                    |),
                                                                    [ M.read (| buf |) ]
                                                                  |)
                                                                |)
                                                              |)) in
                                                          let _ :=
                                                            M.is_constant_or_break_match (|
                                                              M.read (| γ |),
                                                              Value.Bool true
                                                            |) in
                                                          M.alloc (|
                                                            M.rust_cast
                                                              (BinOp.Wrap.sub (|
                                                                M.read (| exp |),
                                                                M.read (| limit |)
                                                              |))
                                                          |)));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (M.alloc (|
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.apply
                                                                  (Ty.path "slice")
                                                                  []
                                                                  [
                                                                    Ty.apply
                                                                      (Ty.path
                                                                        "core::mem::maybe_uninit::MaybeUninit")
                                                                      []
                                                                      [ Ty.path "u8" ]
                                                                  ],
                                                                "len",
                                                                []
                                                              |),
                                                              [ M.read (| buf |) ]
                                                            |)
                                                          |)))
                                                    ]
                                                  |)))
                                            ]
                                          |)
                                        |) 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.gt (|
                                                                    M.read (| len |),
                                                                    Value.Integer
                                                                      IntegerKind.Usize
                                                                      0
                                                                  |)
                                                                |)
                                                              |)) 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: len > 0"
                                                                  |)
                                                                ]
                                                              |)
                                                            |)
                                                          |)));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (M.alloc (| Value.Tuple [] |)))
                                                    ]
                                                  |) in
                                                M.alloc (| Value.Tuple [] |)));
                                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                          ]
                                        |) in
                                      let~ kappa :=
                                        M.alloc (| M.rust_cast (M.read (| max_kappa |)) |) in
                                      let~ ten_kappa := M.copy (| max_ten_kappa |) in
                                      let~ remainder := M.copy (| vint |) in
                                      let~ _ :=
                                        M.loop (|
                                          ltac:(M.monadic
                                            (let~ q :=
                                              M.alloc (|
                                                BinOp.Wrap.div (|
                                                  M.read (| remainder |),
                                                  M.read (| ten_kappa |)
                                                |)
                                              |) in
                                            let~ r :=
                                              M.alloc (|
                                                BinOp.Wrap.rem (|
                                                  M.read (| remainder |),
                                                  M.read (| ten_kappa |)
                                                |)
                                              |) 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 (| q |),
                                                                          Value.Integer
                                                                            IntegerKind.U32
                                                                            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: q < 10"
                                                                        |)
                                                                      ]
                                                                    |)
                                                                  |)
                                                                |)));
                                                            fun γ =>
                                                              ltac:(M.monadic
                                                                (M.alloc (| Value.Tuple [] |)))
                                                          ]
                                                        |) in
                                                      M.alloc (| Value.Tuple [] |)));
                                                  fun γ =>
                                                    ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                                ]
                                              |) in
                                            let~ _ :=
                                              M.write (|
                                                M.SubPointer.get_array_field (|
                                                  M.read (| buf |),
                                                  i
                                                |),
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply
                                                      (Ty.path
                                                        "core::mem::maybe_uninit::MaybeUninit")
                                                      []
                                                      [ Ty.path "u8" ],
                                                    "new",
                                                    []
                                                  |),
                                                  [
                                                    BinOp.Wrap.add (|
                                                      M.read (| UnsupportedLiteral |),
                                                      M.rust_cast (M.read (| q |))
                                                    |)
                                                  ]
                                                |)
                                              |) in
                                            let~ _ :=
                                              let β := i in
                                              M.write (|
                                                β,
                                                BinOp.Wrap.add (|
                                                  M.read (| β |),
                                                  Value.Integer IntegerKind.Usize 1
                                                |)
                                              |) in
                                            let~ _ :=
                                              M.match_operator (|
                                                M.alloc (| Value.Tuple [] |),
                                                [
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ :=
                                                        M.use
                                                          (M.alloc (|
                                                            BinOp.eq (|
                                                              M.read (| i |),
                                                              M.read (| len |)
                                                            |)
                                                          |)) in
                                                      let _ :=
                                                        M.is_constant_or_break_match (|
                                                          M.read (| γ |),
                                                          Value.Bool true
                                                        |) in
                                                      M.alloc (|
                                                        M.never_to_any (|
                                                          M.read (|
                                                            let~ vrem :=
                                                              M.alloc (|
                                                                BinOp.Wrap.add (|
                                                                  BinOp.Wrap.shl (|
                                                                    M.rust_cast (M.read (| r |)),
                                                                    M.read (| e |)
                                                                  |),
                                                                  M.read (| vfrac |)
                                                                |)
                                                              |) in
                                                            M.return_ (|
                                                              M.call_closure (|
                                                                M.get_function (|
                                                                  "core::num::flt2dec::strategy::grisu::format_exact_opt.possibly_round",
                                                                  []
                                                                |),
                                                                [
                                                                  M.read (| buf |);
                                                                  M.read (| len |);
                                                                  M.read (| exp |);
                                                                  M.read (| limit |);
                                                                  M.read (| vrem |);
                                                                  BinOp.Wrap.shl (|
                                                                    M.rust_cast
                                                                      (M.read (| ten_kappa |)),
                                                                    M.read (| e |)
                                                                  |);
                                                                  BinOp.Wrap.shl (|
                                                                    M.read (| err |),
                                                                    M.read (| e |)
                                                                  |)
                                                                ]
                                                              |)
                                                            |)
                                                          |)
                                                        |)
                                                      |)));
                                                  fun γ =>
                                                    ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                                ]
                                              |) in
                                            let~ _ :=
                                              M.match_operator (|
                                                M.alloc (| Value.Tuple [] |),
                                                [
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ :=
                                                        M.use
                                                          (M.alloc (|
                                                            BinOp.gt (|
                                                              M.read (| i |),
                                                              M.rust_cast (M.read (| max_kappa |))
                                                            |)
                                                          |)) in
                                                      let _ :=
                                                        M.is_constant_or_break_match (|
                                                          M.read (| γ |),
                                                          Value.Bool true
                                                        |) in
                                                      M.alloc (|
                                                        M.never_to_any (|
                                                          M.read (|
                                                            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
                                                                              [
                                                                                ten_kappa;
                                                                                M.alloc (|
                                                                                  Value.Integer
                                                                                    IntegerKind.U32
                                                                                    1
                                                                                |)
                                                                              ]
                                                                          |),
                                                                          [
                                                                            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 left_val :=
                                                                                  M.copy (|
                                                                                    γ0_0
                                                                                  |) in
                                                                                let right_val :=
                                                                                  M.copy (|
                                                                                    γ0_1
                                                                                  |) in
                                                                                M.match_operator (|
                                                                                  M.alloc (|
                                                                                    Value.Tuple []
                                                                                  |),
                                                                                  [
                                                                                    fun γ =>
                                                                                      ltac:(M.monadic
                                                                                        (let γ :=
                                                                                          M.use
                                                                                            (M.alloc (|
                                                                                              UnOp.not (|
                                                                                                BinOp.eq (|
                                                                                                  M.read (|
                                                                                                    M.read (|
                                                                                                      left_val
                                                                                                    |)
                                                                                                  |),
                                                                                                  M.read (|
                                                                                                    M.read (|
                                                                                                      right_val
                                                                                                    |)
                                                                                                  |)
                                                                                                |)
                                                                                              |)
                                                                                            |)) in
                                                                                        let _ :=
                                                                                          M.is_constant_or_break_match (|
                                                                                            M.read (|
                                                                                              γ
                                                                                            |),
                                                                                            Value.Bool
                                                                                              true
                                                                                          |) in
                                                                                        M.alloc (|
                                                                                          M.never_to_any (|
                                                                                            M.read (|
                                                                                              let~
                                                                                                    kind :=
                                                                                                M.alloc (|
                                                                                                  Value.StructTuple
                                                                                                    "core::panicking::AssertKind::Eq"
                                                                                                    []
                                                                                                |) in
                                                                                              M.alloc (|
                                                                                                M.call_closure (|
                                                                                                  M.get_function (|
                                                                                                    "core::panicking::assert_failed",
                                                                                                    [
                                                                                                      Ty.path
                                                                                                        "u32";
                                                                                                      Ty.path
                                                                                                        "u32"
                                                                                                    ]
                                                                                                  |),
                                                                                                  [
                                                                                                    M.read (|
                                                                                                      kind
                                                                                                    |);
                                                                                                    M.read (|
                                                                                                      left_val
                                                                                                    |);
                                                                                                    M.read (|
                                                                                                      right_val
                                                                                                    |);
                                                                                                    Value.StructTuple
                                                                                                      "core::option::Option::None"
                                                                                                      []
                                                                                                  ]
                                                                                                |)
                                                                                              |)
                                                                                            |)
                                                                                          |)
                                                                                        |)));
                                                                                    fun γ =>
                                                                                      ltac:(M.monadic
                                                                                        (M.alloc (|
                                                                                          Value.Tuple
                                                                                            []
                                                                                        |)))
                                                                                  ]
                                                                                |)))
                                                                          ]
                                                                        |) in
                                                                      M.alloc (|
                                                                        Value.Tuple []
                                                                      |)));
                                                                  fun γ =>
                                                                    ltac:(M.monadic
                                                                      (M.alloc (|
                                                                        Value.Tuple []
                                                                      |)))
                                                                ]
                                                              |) in
                                                            let~ _ :=
                                                              M.match_operator (|
                                                                M.alloc (| Value.Tuple [] |),
                                                                [
                                                                  fun γ =>
                                                                    ltac:(M.monadic
                                                                      (let γ :=
                                                                        M.use
                                                                          (M.alloc (|
                                                                            Value.Bool true
                                                                          |)) in
                                                                      let _ :=
                                                                        M.is_constant_or_break_match (|
                                                                          M.read (| γ |),
                                                                          Value.Bool true
                                                                        |) in
                                                                      let~ _ :=
                                                                        M.match_operator (|
                                                                          M.alloc (|
                                                                            Value.Tuple
                                                                              [
                                                                                kappa;
                                                                                M.alloc (|
                                                                                  Value.Integer
                                                                                    IntegerKind.I16
                                                                                    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 left_val :=
                                                                                  M.copy (|
                                                                                    γ0_0
                                                                                  |) in
                                                                                let right_val :=
                                                                                  M.copy (|
                                                                                    γ0_1
                                                                                  |) in
                                                                                M.match_operator (|
                                                                                  M.alloc (|
                                                                                    Value.Tuple []
                                                                                  |),
                                                                                  [
                                                                                    fun γ =>
                                                                                      ltac:(M.monadic
                                                                                        (let γ :=
                                                                                          M.use
                                                                                            (M.alloc (|
                                                                                              UnOp.not (|
                                                                                                BinOp.eq (|
                                                                                                  M.read (|
                                                                                                    M.read (|
                                                                                                      left_val
                                                                                                    |)
                                                                                                  |),
                                                                                                  M.read (|
                                                                                                    M.read (|
                                                                                                      right_val
                                                                                                    |)
                                                                                                  |)
                                                                                                |)
                                                                                              |)
                                                                                            |)) in
                                                                                        let _ :=
                                                                                          M.is_constant_or_break_match (|
                                                                                            M.read (|
                                                                                              γ
                                                                                            |),
                                                                                            Value.Bool
                                                                                              true
                                                                                          |) in
                                                                                        M.alloc (|
                                                                                          M.never_to_any (|
                                                                                            M.read (|
                                                                                              let~
                                                                                                    kind :=
                                                                                                M.alloc (|
                                                                                                  Value.StructTuple
                                                                                                    "core::panicking::AssertKind::Eq"
                                                                                                    []
                                                                                                |) in
                                                                                              M.alloc (|
                                                                                                M.call_closure (|
                                                                                                  M.get_function (|
                                                                                                    "core::panicking::assert_failed",
                                                                                                    [
                                                                                                      Ty.path
                                                                                                        "i16";
                                                                                                      Ty.path
                                                                                                        "i16"
                                                                                                    ]
                                                                                                  |),
                                                                                                  [
                                                                                                    M.read (|
                                                                                                      kind
                                                                                                    |);
                                                                                                    M.read (|
                                                                                                      left_val
                                                                                                    |);
                                                                                                    M.read (|
                                                                                                      right_val
                                                                                                    |);
                                                                                                    Value.StructTuple
                                                                                                      "core::option::Option::None"
                                                                                                      []
                                                                                                  ]
                                                                                                |)
                                                                                              |)
                                                                                            |)
                                                                                          |)
                                                                                        |)));
                                                                                    fun γ =>
                                                                                      ltac:(M.monadic
                                                                                        (M.alloc (|
                                                                                          Value.Tuple
                                                                                            []
                                                                                        |)))
                                                                                  ]
                                                                                |)))
                                                                          ]
                                                                        |) in
                                                                      M.alloc (|
                                                                        Value.Tuple []
                                                                      |)));
                                                                  fun γ =>
                                                                    ltac:(M.monadic
                                                                      (M.alloc (|
                                                                        Value.Tuple []
                                                                      |)))
                                                                ]
                                                              |) in
                                                            M.break (||)
                                                          |)
                                                        |)
                                                      |)));
                                                  fun γ =>
                                                    ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                                ]
                                              |) in
                                            let~ _ :=
                                              let β := kappa in
                                              M.write (|
                                                β,
                                                BinOp.Wrap.sub (|
                                                  M.read (| β |),
                                                  Value.Integer IntegerKind.I16 1
                                                |)
                                              |) in
                                            let~ _ :=
                                              let β := ten_kappa in
                                              M.write (|
                                                β,
                                                BinOp.Wrap.div (|
                                                  M.read (| β |),
                                                  Value.Integer IntegerKind.U32 10
                                                |)
                                              |) in
                                            let~ _ := M.write (| remainder, M.read (| r |) |) in
                                            M.alloc (| Value.Tuple [] |)))
                                        |) in
                                      let~ remainder := M.copy (| vfrac |) in
                                      let~ maxerr :=
                                        M.alloc (|
                                          BinOp.Wrap.shl (|
                                            Value.Integer IntegerKind.U64 1,
                                            BinOp.Wrap.sub (|
                                              M.read (| e |),
                                              Value.Integer IntegerKind.Usize 1
                                            |)
                                          |)
                                        |) in
                                      let~ _ :=
                                        M.loop (|
                                          ltac:(M.monadic
                                            (M.match_operator (|
                                              M.alloc (| Value.Tuple [] |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let γ :=
                                                      M.use
                                                        (M.alloc (|
                                                          BinOp.lt (|
                                                            M.read (| err |),
                                                            M.read (| maxerr |)
                                                          |)
                                                        |)) in
                                                    let _ :=
                                                      M.is_constant_or_break_match (|
                                                        M.read (| γ |),
                                                        Value.Bool true
                                                      |) in
                                                    let~ _ :=
                                                      let β := remainder in
                                                      M.write (|
                                                        β,
                                                        BinOp.Wrap.mul (|
                                                          M.read (| β |),
                                                          Value.Integer IntegerKind.U64 10
                                                        |)
                                                      |) in
                                                    let~ _ :=
                                                      let β := err in
                                                      M.write (|
                                                        β,
                                                        BinOp.Wrap.mul (|
                                                          M.read (| β |),
                                                          Value.Integer IntegerKind.U64 10
                                                        |)
                                                      |) in
                                                    let~ q :=
                                                      M.alloc (|
                                                        BinOp.Wrap.shr (|
                                                          M.read (| remainder |),
                                                          M.read (| e |)
                                                        |)
                                                      |) in
                                                    let~ r :=
                                                      M.alloc (|
                                                        BinOp.bit_and
                                                          (M.read (| remainder |))
                                                          (BinOp.Wrap.sub (|
                                                            BinOp.Wrap.shl (|
                                                              Value.Integer IntegerKind.U64 1,
                                                              M.read (| e |)
                                                            |),
                                                            Value.Integer IntegerKind.U64 1
                                                          |))
                                                      |) 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 (| q |),
                                                                                  Value.Integer
                                                                                    IntegerKind.U64
                                                                                    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: q < 10"
                                                                                |)
                                                                              ]
                                                                            |)
                                                                          |)
                                                                        |)));
                                                                    fun γ =>
                                                                      ltac:(M.monadic
                                                                        (M.alloc (|
                                                                          Value.Tuple []
                                                                        |)))
                                                                  ]
                                                                |) in
                                                              M.alloc (| Value.Tuple [] |)));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (M.alloc (| Value.Tuple [] |)))
                                                        ]
                                                      |) in
                                                    let~ _ :=
                                                      M.write (|
                                                        M.SubPointer.get_array_field (|
                                                          M.read (| buf |),
                                                          i
                                                        |),
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.apply
                                                              (Ty.path
                                                                "core::mem::maybe_uninit::MaybeUninit")
                                                              []
                                                              [ Ty.path "u8" ],
                                                            "new",
                                                            []
                                                          |),
                                                          [
                                                            BinOp.Wrap.add (|
                                                              M.read (| UnsupportedLiteral |),
                                                              M.rust_cast (M.read (| q |))
                                                            |)
                                                          ]
                                                        |)
                                                      |) in
                                                    let~ _ :=
                                                      let β := i in
                                                      M.write (|
                                                        β,
                                                        BinOp.Wrap.add (|
                                                          M.read (| β |),
                                                          Value.Integer IntegerKind.Usize 1
                                                        |)
                                                      |) in
                                                    let~ _ :=
                                                      M.match_operator (|
                                                        M.alloc (| Value.Tuple [] |),
                                                        [
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ :=
                                                                M.use
                                                                  (M.alloc (|
                                                                    BinOp.eq (|
                                                                      M.read (| i |),
                                                                      M.read (| len |)
                                                                    |)
                                                                  |)) in
                                                              let _ :=
                                                                M.is_constant_or_break_match (|
                                                                  M.read (| γ |),
                                                                  Value.Bool true
                                                                |) in
                                                              M.alloc (|
                                                                M.never_to_any (|
                                                                  M.read (|
                                                                    M.return_ (|
                                                                      M.call_closure (|
                                                                        M.get_function (|
                                                                          "core::num::flt2dec::strategy::grisu::format_exact_opt.possibly_round",
                                                                          []
                                                                        |),
                                                                        [
                                                                          M.read (| buf |);
                                                                          M.read (| len |);
                                                                          M.read (| exp |);
                                                                          M.read (| limit |);
                                                                          M.read (| r |);
                                                                          BinOp.Wrap.shl (|
                                                                            Value.Integer
                                                                              IntegerKind.U64
                                                                              1,
                                                                            M.read (| e |)
                                                                          |);
                                                                          M.read (| err |)
                                                                        ]
                                                                      |)
                                                                    |)
                                                                  |)
                                                                |)
                                                              |)));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (M.alloc (| Value.Tuple [] |)))
                                                        ]
                                                      |) in
                                                    let~ _ :=
                                                      M.write (| remainder, M.read (| r |) |) 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.return_ (|
                                        Value.StructTuple "core::option::Option::None" []
                                      |)))
                                ]
                              |)))
                        ]
                      |)
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Function_format_exact_opt :
          M.IsFunction "core::num::flt2dec::strategy::grisu::format_exact_opt" format_exact_opt.
        
        Module format_exact_opt.
          Definition value_POW10_UP_TO_9 : Value.t :=
            M.run
              ltac:(M.monadic
                (M.alloc (|
                  Value.Array
                    [
                      Value.Integer IntegerKind.U32 1;
                      Value.Integer IntegerKind.U32 10;
                      Value.Integer IntegerKind.U32 100;
                      Value.Integer IntegerKind.U32 1000;
                      Value.Integer IntegerKind.U32 10000;
                      Value.Integer IntegerKind.U32 100000;
                      Value.Integer IntegerKind.U32 1000000;
                      Value.Integer IntegerKind.U32 10000000;
                      Value.Integer IntegerKind.U32 100000000;
                      Value.Integer IntegerKind.U32 1000000000
                    ]
                |))).
          
          (*
              unsafe fn possibly_round(
                  buf: &mut [MaybeUninit<u8>],
                  mut len: usize,
                  mut exp: i16,
                  limit: i16,
                  remainder: u64,
                  ten_kappa: u64,
                  ulp: u64,
              ) -> Option<(&[u8], i16)> {
                  debug_assert!(remainder < ten_kappa);
          
                  //           10^kappa
                  //    :   :   :<->:   :
                  //    :   :   :   :   :
                  //    :|1 ulp|1 ulp|  :
                  //    :|<--->|<--->|  :
                  // ----|-----|-----|----
                  //     |     v     |
                  // v - 1 ulp   v + 1 ulp
                  //
                  // (for the reference, the dotted line indicates the exact value for
                  // possible representations in given number of digits.)
                  //
                  // error is too large that there are at least three possible representations
                  // between `v - 1 ulp` and `v + 1 ulp`. we cannot determine which one is correct.
                  if ulp >= ten_kappa {
                      return None;
                  }
          
                  //    10^kappa
                  //   :<------->:
                  //   :         :
                  //   : |1 ulp|1 ulp|
                  //   : |<--->|<--->|
                  // ----|-----|-----|----
                  //     |     v     |
                  // v - 1 ulp   v + 1 ulp
                  //
                  // in fact, 1/2 ulp is enough to introduce two possible representations.
                  // (remember that we need a unique representation for both `v - 1 ulp` and `v + 1 ulp`.)
                  // this won't overflow, as `ulp < ten_kappa` from the first check.
                  if ten_kappa - ulp <= ulp {
                      return None;
                  }
          
                  //     remainder
                  //       :<->|                           :
                  //       :   |                           :
                  //       :<--------- 10^kappa ---------->:
                  //     | :   |                           :
                  //     |1 ulp|1 ulp|                     :
                  //     |<--->|<--->|                     :
                  // ----|-----|-----|------------------------
                  //     |     v     |
                  // v - 1 ulp   v + 1 ulp
                  //
                  // if `v + 1 ulp` is closer to the rounded-down representation (which is already in `buf`),
                  // then we can safely return. note that `v - 1 ulp` *can* be less than the current
                  // representation, but as `1 ulp < 10^kappa / 2`, this condition is enough:
                  // the distance between `v - 1 ulp` and the current representation
                  // cannot exceed `10^kappa / 2`.
                  //
                  // the condition equals to `remainder + ulp < 10^kappa / 2`.
                  // since this can easily overflow, first check if `remainder < 10^kappa / 2`.
                  // we've already verified that `ulp < 10^kappa / 2`, so as long as
                  // `10^kappa` did not overflow after all, the second check is fine.
                  if ten_kappa - remainder > remainder && ten_kappa - 2 * remainder >= 2 * ulp {
                      // SAFETY: our caller initialized that memory.
                      return Some((unsafe { MaybeUninit::slice_assume_init_ref(&buf[..len]) }, exp));
                  }
          
                  //   :<------- remainder ------>|   :
                  //   :                          |   :
                  //   :<--------- 10^kappa --------->:
                  //   :                    |     |   : |
                  //   :                    |1 ulp|1 ulp|
                  //   :                    |<--->|<--->|
                  // -----------------------|-----|-----|-----
                  //                        |     v     |
                  //                    v - 1 ulp   v + 1 ulp
                  //
                  // on the other hands, if `v - 1 ulp` is closer to the rounded-up representation,
                  // we should round up and return. for the same reason we don't need to check `v + 1 ulp`.
                  //
                  // the condition equals to `remainder - ulp >= 10^kappa / 2`.
                  // again we first check if `remainder > ulp` (note that this is not `remainder >= ulp`,
                  // as `10^kappa` is never zero). also note that `remainder - ulp <= 10^kappa`,
                  // so the second check does not overflow.
                  if remainder > ulp && ten_kappa - (remainder - ulp) <= remainder - ulp {
                      if let Some(c) =
                          // SAFETY: our caller must have initialized that memory.
                          round_up(unsafe { MaybeUninit::slice_assume_init_mut(&mut buf[..len]) })
                      {
                          // only add an additional digit when we've been requested the fixed precision.
                          // we also need to check that, if the original buffer was empty,
                          // the additional digit can only be added when `exp == limit` (edge case).
                          exp += 1;
                          if exp > limit && len < buf.len() {
                              buf[len] = MaybeUninit::new(c);
                              len += 1;
                          }
                      }
                      // SAFETY: we and our caller initialized that memory.
                      return Some((unsafe { MaybeUninit::slice_assume_init_ref(&buf[..len]) }, exp));
                  }
          
                  // otherwise we are doomed (i.e., some values between `v - 1 ulp` and `v + 1 ulp` are
                  // rounding down and others are rounding up) and give up.
                  None
              }
          *)
          Definition possibly_round (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
            match ε, τ, α with
            | [], [], [ buf; len; exp; limit; remainder; ten_kappa; ulp ] =>
              ltac:(M.monadic
                (let buf := M.alloc (| buf |) in
                let len := M.alloc (| len |) in
                let exp := M.alloc (| exp |) in
                let limit := M.alloc (| limit |) in
                let remainder := M.alloc (| remainder |) in
                let ten_kappa := M.alloc (| ten_kappa |) in
                let ulp := M.alloc (| ulp |) in
                M.catch_return (|
                  ltac:(M.monadic
                    (M.read (|
                      let~ _ :=
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.use (M.alloc (| 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 (| remainder |),
                                                    M.read (| ten_kappa |)
                                                  |)
                                                |)
                                              |)) 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: remainder < ten_kappa"
                                                  |)
                                                ]
                                              |)
                                            |)
                                          |)));
                                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)));
                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                          ]
                        |) in
                      let~ _ :=
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      BinOp.ge (| M.read (| ulp |), M.read (| ten_kappa |) |)
                                    |)) 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 (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      BinOp.le (|
                                        BinOp.Wrap.sub (|
                                          M.read (| ten_kappa |),
                                          M.read (| ulp |)
                                        |),
                                        M.read (| ulp |)
                                      |)
                                    |)) 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 (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      LogicalOp.and (|
                                        BinOp.gt (|
                                          BinOp.Wrap.sub (|
                                            M.read (| ten_kappa |),
                                            M.read (| remainder |)
                                          |),
                                          M.read (| remainder |)
                                        |),
                                        ltac:(M.monadic
                                          (BinOp.ge (|
                                            BinOp.Wrap.sub (|
                                              M.read (| ten_kappa |),
                                              BinOp.Wrap.mul (|
                                                Value.Integer IntegerKind.U64 2,
                                                M.read (| remainder |)
                                              |)
                                            |),
                                            BinOp.Wrap.mul (|
                                              Value.Integer IntegerKind.U64 2,
                                              M.read (| ulp |)
                                            |)
                                          |)))
                                      |)
                                    |)) 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"
                                          [
                                            Value.Tuple
                                              [
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply
                                                      (Ty.path
                                                        "core::mem::maybe_uninit::MaybeUninit")
                                                      []
                                                      [ Ty.path "u8" ],
                                                    "slice_assume_init_ref",
                                                    []
                                                  |),
                                                  [
                                                    M.call_closure (|
                                                      M.get_trait_method (|
                                                        "core::ops::index::Index",
                                                        Ty.apply
                                                          (Ty.path "slice")
                                                          []
                                                          [
                                                            Ty.apply
                                                              (Ty.path
                                                                "core::mem::maybe_uninit::MaybeUninit")
                                                              []
                                                              [ Ty.path "u8" ]
                                                          ],
                                                        [
                                                          Ty.apply
                                                            (Ty.path "core::ops::range::RangeTo")
                                                            []
                                                            [ Ty.path "usize" ]
                                                        ],
                                                        "index",
                                                        []
                                                      |),
                                                      [
                                                        M.read (| buf |);
                                                        Value.StructRecord
                                                          "core::ops::range::RangeTo"
                                                          [ ("end_", M.read (| len |)) ]
                                                      ]
                                                    |)
                                                  ]
                                                |);
                                                M.read (| exp |)
                                              ]
                                          ]
                                      |)
                                    |)
                                  |)
                                |)));
                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                          ]
                        |) in
                      let~ _ :=
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      LogicalOp.and (|
                                        BinOp.gt (| M.read (| remainder |), M.read (| ulp |) |),
                                        ltac:(M.monadic
                                          (BinOp.le (|
                                            BinOp.Wrap.sub (|
                                              M.read (| ten_kappa |),
                                              BinOp.Wrap.sub (|
                                                M.read (| remainder |),
                                                M.read (| ulp |)
                                              |)
                                            |),
                                            BinOp.Wrap.sub (|
                                              M.read (| remainder |),
                                              M.read (| ulp |)
                                            |)
                                          |)))
                                      |)
                                    |)) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      let~ _ :=
                                        M.match_operator (|
                                          M.alloc (| Value.Tuple [] |),
                                          [
                                            fun γ =>
                                              ltac:(M.monadic
                                                (let γ :=
                                                  M.alloc (|
                                                    M.call_closure (|
                                                      M.get_function (|
                                                        "core::num::flt2dec::round_up",
                                                        []
                                                      |),
                                                      [
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.apply
                                                              (Ty.path
                                                                "core::mem::maybe_uninit::MaybeUninit")
                                                              []
                                                              [ Ty.path "u8" ],
                                                            "slice_assume_init_mut",
                                                            []
                                                          |),
                                                          [
                                                            M.call_closure (|
                                                              M.get_trait_method (|
                                                                "core::ops::index::IndexMut",
                                                                Ty.apply
                                                                  (Ty.path "slice")
                                                                  []
                                                                  [
                                                                    Ty.apply
                                                                      (Ty.path
                                                                        "core::mem::maybe_uninit::MaybeUninit")
                                                                      []
                                                                      [ Ty.path "u8" ]
                                                                  ],
                                                                [
                                                                  Ty.apply
                                                                    (Ty.path
                                                                      "core::ops::range::RangeTo")
                                                                    []
                                                                    [ Ty.path "usize" ]
                                                                ],
                                                                "index_mut",
                                                                []
                                                              |),
                                                              [
                                                                M.read (| buf |);
                                                                Value.StructRecord
                                                                  "core::ops::range::RangeTo"
                                                                  [ ("end_", M.read (| len |)) ]
                                                              ]
                                                            |)
                                                          ]
                                                        |)
                                                      ]
                                                    |)
                                                  |) in
                                                let γ0_0 :=
                                                  M.SubPointer.get_struct_tuple_field (|
                                                    γ,
                                                    "core::option::Option::Some",
                                                    0
                                                  |) in
                                                let c := M.copy (| γ0_0 |) in
                                                let~ _ :=
                                                  let β := exp in
                                                  M.write (|
                                                    β,
                                                    BinOp.Wrap.add (|
                                                      M.read (| β |),
                                                      Value.Integer IntegerKind.I16 1
                                                    |)
                                                  |) in
                                                M.match_operator (|
                                                  M.alloc (| Value.Tuple [] |),
                                                  [
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (let γ :=
                                                          M.use
                                                            (M.alloc (|
                                                              LogicalOp.and (|
                                                                BinOp.gt (|
                                                                  M.read (| exp |),
                                                                  M.read (| limit |)
                                                                |),
                                                                ltac:(M.monadic
                                                                  (BinOp.lt (|
                                                                    M.read (| len |),
                                                                    M.call_closure (|
                                                                      M.get_associated_function (|
                                                                        Ty.apply
                                                                          (Ty.path "slice")
                                                                          []
                                                                          [
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "core::mem::maybe_uninit::MaybeUninit")
                                                                              []
                                                                              [ Ty.path "u8" ]
                                                                          ],
                                                                        "len",
                                                                        []
                                                                      |),
                                                                      [ M.read (| buf |) ]
                                                                    |)
                                                                  |)))
                                                              |)
                                                            |)) in
                                                        let _ :=
                                                          M.is_constant_or_break_match (|
                                                            M.read (| γ |),
                                                            Value.Bool true
                                                          |) in
                                                        let~ _ :=
                                                          M.write (|
                                                            M.SubPointer.get_array_field (|
                                                              M.read (| buf |),
                                                              len
                                                            |),
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.apply
                                                                  (Ty.path
                                                                    "core::mem::maybe_uninit::MaybeUninit")
                                                                  []
                                                                  [ Ty.path "u8" ],
                                                                "new",
                                                                []
                                                              |),
                                                              [ M.read (| c |) ]
                                                            |)
                                                          |) in
                                                        let~ _ :=
                                                          let β := len in
                                                          M.write (|
                                                            β,
                                                            BinOp.Wrap.add (|
                                                              M.read (| β |),
                                                              Value.Integer IntegerKind.Usize 1
                                                            |)
                                                          |) in
                                                        M.alloc (| Value.Tuple [] |)));
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (M.alloc (| Value.Tuple [] |)))
                                                  ]
                                                |)));
                                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                          ]
                                        |) in
                                      M.return_ (|
                                        Value.StructTuple
                                          "core::option::Option::Some"
                                          [
                                            Value.Tuple
                                              [
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply
                                                      (Ty.path
                                                        "core::mem::maybe_uninit::MaybeUninit")
                                                      []
                                                      [ Ty.path "u8" ],
                                                    "slice_assume_init_ref",
                                                    []
                                                  |),
                                                  [
                                                    M.call_closure (|
                                                      M.get_trait_method (|
                                                        "core::ops::index::Index",
                                                        Ty.apply
                                                          (Ty.path "slice")
                                                          []
                                                          [
                                                            Ty.apply
                                                              (Ty.path
                                                                "core::mem::maybe_uninit::MaybeUninit")
                                                              []
                                                              [ Ty.path "u8" ]
                                                          ],
                                                        [
                                                          Ty.apply
                                                            (Ty.path "core::ops::range::RangeTo")
                                                            []
                                                            [ Ty.path "usize" ]
                                                        ],
                                                        "index",
                                                        []
                                                      |),
                                                      [
                                                        M.read (| buf |);
                                                        Value.StructRecord
                                                          "core::ops::range::RangeTo"
                                                          [ ("end_", M.read (| len |)) ]
                                                      ]
                                                    |)
                                                  ]
                                                |);
                                                M.read (| exp |)
                                              ]
                                          ]
                                      |)
                                    |)
                                  |)
                                |)));
                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                          ]
                        |) in
                      M.alloc (| Value.StructTuple "core::option::Option::None" [] |)
                    |)))
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          Axiom Function_possibly_round :
            M.IsFunction
              "core::num::flt2dec::strategy::grisu::format_exact_opt::possibly_round"
              possibly_round.
        End format_exact_opt.
        
        (*
        pub fn format_exact<'a>(
            d: &Decoded,
            buf: &'a mut [MaybeUninit<u8>],
            limit: i16,
        ) -> (/*digits*/ &'a [u8], /*exp*/ i16) {
            use crate::num::flt2dec::strategy::dragon::format_exact as fallback;
            // SAFETY: The borrow checker is not smart enough to let us use `buf`
            // in the second branch, so we launder the lifetime here. But we only re-use
            // `buf` if `format_exact_opt` returned `None` so this is okay.
            match format_exact_opt(d, unsafe { &mut *(buf as *mut _) }, limit) {
                Some(ret) => ret,
                None => fallback(d, buf, limit),
            }
        }
        *)
        Definition format_exact (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ d; buf; limit ] =>
            ltac:(M.monadic
              (let d := M.alloc (| d |) in
              let buf := M.alloc (| buf |) in
              let limit := M.alloc (| limit |) in
              M.read (|
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::num::flt2dec::strategy::grisu::format_exact_opt",
                        []
                      |),
                      [
                        M.read (| d |);
                        M.read (| M.use (M.alloc (| M.read (| buf |) |)) |);
                        M.read (| limit |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::option::Option::Some",
                            0
                          |) in
                        let ret := M.copy (| γ0_0 |) in
                        ret));
                    fun γ =>
                      ltac:(M.monadic
                        (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_function (|
                              "core::num::flt2dec::strategy::dragon::format_exact",
                              []
                            |),
                            [ M.read (| d |); M.read (| buf |); M.read (| limit |) ]
                          |)
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Function_format_exact :
          M.IsFunction "core::num::flt2dec::strategy::grisu::format_exact" format_exact.
      End grisu.
    End strategy.
  End flt2dec.
End num.
