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

Module num.
  Module flt2dec.
    Module strategy.
      Module dragon.
        Definition value_POW10 : Value.t :=
          M.run
            ltac:(M.monadic
              (M.alloc (|
                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
                    ]
                |)
              |))).
        
        Definition value_POW5TO16 : Value.t :=
          M.run
            ltac:(M.monadic
              (M.alloc (|
                M.alloc (|
                  Value.Array
                    [ Value.Integer IntegerKind.U32 2264035265; Value.Integer IntegerKind.U32 35 ]
                |)
              |))).
        
        Definition value_POW5TO32 : Value.t :=
          M.run
            ltac:(M.monadic
              (M.alloc (|
                M.alloc (|
                  Value.Array
                    [
                      Value.Integer IntegerKind.U32 2242703233;
                      Value.Integer IntegerKind.U32 762134875;
                      Value.Integer IntegerKind.U32 1262
                    ]
                |)
              |))).
        
        Definition value_POW5TO64 : Value.t :=
          M.run
            ltac:(M.monadic
              (M.alloc (|
                M.alloc (|
                  Value.Array
                    [
                      Value.Integer IntegerKind.U32 3211403009;
                      Value.Integer IntegerKind.U32 1849224548;
                      Value.Integer IntegerKind.U32 3668416493;
                      Value.Integer IntegerKind.U32 3913284084;
                      Value.Integer IntegerKind.U32 1593091
                    ]
                |)
              |))).
        
        Definition value_POW5TO128 : Value.t :=
          M.run
            ltac:(M.monadic
              (M.alloc (|
                M.alloc (|
                  Value.Array
                    [
                      Value.Integer IntegerKind.U32 781532673;
                      Value.Integer IntegerKind.U32 64985353;
                      Value.Integer IntegerKind.U32 253049085;
                      Value.Integer IntegerKind.U32 594863151;
                      Value.Integer IntegerKind.U32 3553621484;
                      Value.Integer IntegerKind.U32 3288652808;
                      Value.Integer IntegerKind.U32 3167596762;
                      Value.Integer IntegerKind.U32 2788392729;
                      Value.Integer IntegerKind.U32 3911132675;
                      Value.Integer IntegerKind.U32 590
                    ]
                |)
              |))).
        
        Definition value_POW5TO256 : Value.t :=
          M.run
            ltac:(M.monadic
              (M.alloc (|
                M.alloc (|
                  Value.Array
                    [
                      Value.Integer IntegerKind.U32 2553183233;
                      Value.Integer IntegerKind.U32 3201533787;
                      Value.Integer IntegerKind.U32 3638140786;
                      Value.Integer IntegerKind.U32 303378311;
                      Value.Integer IntegerKind.U32 1809731782;
                      Value.Integer IntegerKind.U32 3477761648;
                      Value.Integer IntegerKind.U32 3583367183;
                      Value.Integer IntegerKind.U32 649228654;
                      Value.Integer IntegerKind.U32 2915460784;
                      Value.Integer IntegerKind.U32 487929380;
                      Value.Integer IntegerKind.U32 1011012442;
                      Value.Integer IntegerKind.U32 1677677582;
                      Value.Integer IntegerKind.U32 3428152256;
                      Value.Integer IntegerKind.U32 1710878487;
                      Value.Integer IntegerKind.U32 1438394610;
                      Value.Integer IntegerKind.U32 2161952759;
                      Value.Integer IntegerKind.U32 4100910556;
                      Value.Integer IntegerKind.U32 1608314830;
                      Value.Integer IntegerKind.U32 349175
                    ]
                |)
              |))).
        
        (*
        pub fn mul_pow10(x: &mut Big, n: usize) -> &mut Big {
            debug_assert!(n < 512);
            // Save ourself the left shift for the smallest cases.
            if n < 8 {
                return x.mul_small(POW10[n & 7]);
            }
            // Multiply by the powers of 5 and shift the 2s in at the end.
            // This keeps the intermediate products smaller and faster.
            if n & 7 != 0 {
                x.mul_small(POW10[n & 7] >> (n & 7));
            }
            if n & 8 != 0 {
                x.mul_small(POW10[8] >> 8);
            }
            if n & 16 != 0 {
                x.mul_digits(&POW5TO16);
            }
            if n & 32 != 0 {
                x.mul_digits(&POW5TO32);
            }
            if n & 64 != 0 {
                x.mul_digits(&POW5TO64);
            }
            if n & 128 != 0 {
                x.mul_digits(&POW5TO128);
            }
            if n & 256 != 0 {
                x.mul_digits(&POW5TO256);
            }
            x.mul_pow2(n)
        }
        *)
        Definition mul_pow10 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ x; n ] =>
            ltac:(M.monadic
              (let x := M.alloc (| x |) in
              let n := M.alloc (| n |) 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 (| n |),
                                                  Value.Integer IntegerKind.Usize 512
                                                |)
                                              |)
                                            |)) 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: n < 512"
                                                |)
                                              ]
                                            |)
                                          |)
                                        |)));
                                    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.lt (| M.read (| n |), Value.Integer IntegerKind.Usize 8 |)
                                  |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              M.alloc (|
                                M.never_to_any (|
                                  M.read (|
                                    M.return_ (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "core::num::bignum::Big32x40",
                                          "mul_small",
                                          []
                                        |),
                                        [
                                          M.read (| x |);
                                          M.read (|
                                            M.SubPointer.get_array_field (|
                                              M.read (|
                                                M.get_constant (|
                                                  "core::num::flt2dec::strategy::dragon::POW10"
                                                |)
                                              |),
                                              M.alloc (|
                                                BinOp.bit_and
                                                  (M.read (| n |))
                                                  (Value.Integer IntegerKind.Usize 7)
                                              |)
                                            |)
                                          |)
                                        ]
                                      |)
                                    |)
                                  |)
                                |)
                              |)));
                          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.ne (|
                                      BinOp.bit_and
                                        (M.read (| n |))
                                        (Value.Integer IntegerKind.Usize 7),
                                      Value.Integer IntegerKind.Usize 0
                                    |)
                                  |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              let~ _ :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::num::bignum::Big32x40",
                                      "mul_small",
                                      []
                                    |),
                                    [
                                      M.read (| x |);
                                      BinOp.Wrap.shr (|
                                        M.read (|
                                          M.SubPointer.get_array_field (|
                                            M.read (|
                                              M.get_constant (|
                                                "core::num::flt2dec::strategy::dragon::POW10"
                                              |)
                                            |),
                                            M.alloc (|
                                              BinOp.bit_and
                                                (M.read (| n |))
                                                (Value.Integer IntegerKind.Usize 7)
                                            |)
                                          |)
                                        |),
                                        BinOp.bit_and
                                          (M.read (| n |))
                                          (Value.Integer IntegerKind.Usize 7)
                                      |)
                                    ]
                                  |)
                                |) 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.ne (|
                                      BinOp.bit_and
                                        (M.read (| n |))
                                        (Value.Integer IntegerKind.Usize 8),
                                      Value.Integer IntegerKind.Usize 0
                                    |)
                                  |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              let~ _ :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::num::bignum::Big32x40",
                                      "mul_small",
                                      []
                                    |),
                                    [
                                      M.read (| x |);
                                      BinOp.Wrap.shr (|
                                        M.read (|
                                          M.SubPointer.get_array_field (|
                                            M.read (|
                                              M.get_constant (|
                                                "core::num::flt2dec::strategy::dragon::POW10"
                                              |)
                                            |),
                                            M.alloc (| Value.Integer IntegerKind.Usize 8 |)
                                          |)
                                        |),
                                        Value.Integer IntegerKind.I32 8
                                      |)
                                    ]
                                  |)
                                |) 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.ne (|
                                      BinOp.bit_and
                                        (M.read (| n |))
                                        (Value.Integer IntegerKind.Usize 16),
                                      Value.Integer IntegerKind.Usize 0
                                    |)
                                  |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              let~ _ :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::num::bignum::Big32x40",
                                      "mul_digits",
                                      []
                                    |),
                                    [
                                      M.read (| x |);
                                      M.read (|
                                        M.get_constant (|
                                          "core::num::flt2dec::strategy::dragon::POW5TO16"
                                        |)
                                      |)
                                    ]
                                  |)
                                |) 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.ne (|
                                      BinOp.bit_and
                                        (M.read (| n |))
                                        (Value.Integer IntegerKind.Usize 32),
                                      Value.Integer IntegerKind.Usize 0
                                    |)
                                  |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              let~ _ :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::num::bignum::Big32x40",
                                      "mul_digits",
                                      []
                                    |),
                                    [
                                      M.read (| x |);
                                      M.read (|
                                        M.get_constant (|
                                          "core::num::flt2dec::strategy::dragon::POW5TO32"
                                        |)
                                      |)
                                    ]
                                  |)
                                |) 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.ne (|
                                      BinOp.bit_and
                                        (M.read (| n |))
                                        (Value.Integer IntegerKind.Usize 64),
                                      Value.Integer IntegerKind.Usize 0
                                    |)
                                  |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              let~ _ :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::num::bignum::Big32x40",
                                      "mul_digits",
                                      []
                                    |),
                                    [
                                      M.read (| x |);
                                      M.read (|
                                        M.get_constant (|
                                          "core::num::flt2dec::strategy::dragon::POW5TO64"
                                        |)
                                      |)
                                    ]
                                  |)
                                |) 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.ne (|
                                      BinOp.bit_and
                                        (M.read (| n |))
                                        (Value.Integer IntegerKind.Usize 128),
                                      Value.Integer IntegerKind.Usize 0
                                    |)
                                  |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              let~ _ :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::num::bignum::Big32x40",
                                      "mul_digits",
                                      []
                                    |),
                                    [
                                      M.read (| x |);
                                      M.read (|
                                        M.get_constant (|
                                          "core::num::flt2dec::strategy::dragon::POW5TO128"
                                        |)
                                      |)
                                    ]
                                  |)
                                |) 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.ne (|
                                      BinOp.bit_and
                                        (M.read (| n |))
                                        (Value.Integer IntegerKind.Usize 256),
                                      Value.Integer IntegerKind.Usize 0
                                    |)
                                  |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              let~ _ :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::num::bignum::Big32x40",
                                      "mul_digits",
                                      []
                                    |),
                                    [
                                      M.read (| x |);
                                      M.read (|
                                        M.get_constant (|
                                          "core::num::flt2dec::strategy::dragon::POW5TO256"
                                        |)
                                      |)
                                    ]
                                  |)
                                |) in
                              M.alloc (| Value.Tuple [] |)));
                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                        ]
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::num::bignum::Big32x40",
                          "mul_pow2",
                          []
                        |),
                        [ M.read (| x |); M.read (| n |) ]
                      |)
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Function_mul_pow10 :
          M.IsFunction "core::num::flt2dec::strategy::dragon::mul_pow10" mul_pow10.
        
        (*
        fn div_2pow10(x: &mut Big, mut n: usize) -> &mut Big {
            let largest = POW10.len() - 1;
            while n > largest {
                x.div_rem_small(POW10[largest]);
                n -= largest;
            }
            x.div_rem_small(POW10[n] << 1);
            x
        }
        *)
        Definition div_2pow10 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ x; n ] =>
            ltac:(M.monadic
              (let x := M.alloc (| x |) in
              let n := M.alloc (| n |) in
              M.read (|
                let~ largest :=
                  M.alloc (|
                    BinOp.Wrap.sub (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "slice") [] [ Ty.path "u32" ],
                          "len",
                          []
                        |),
                        [
                          M.read (|
                            M.get_constant (| "core::num::flt2dec::strategy::dragon::POW10" |)
                          |)
                        ]
                      |),
                      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.gt (| M.read (| n |), M.read (| largest |) |)
                                  |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              let~ _ :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::num::bignum::Big32x40",
                                      "div_rem_small",
                                      []
                                    |),
                                    [
                                      M.read (| x |);
                                      M.read (|
                                        M.SubPointer.get_array_field (|
                                          M.read (|
                                            M.get_constant (|
                                              "core::num::flt2dec::strategy::dragon::POW10"
                                            |)
                                          |),
                                          largest
                                        |)
                                      |)
                                    ]
                                  |)
                                |) in
                              let~ _ :=
                                let β := n in
                                M.write (|
                                  β,
                                  BinOp.Wrap.sub (| M.read (| β |), M.read (| largest |) |)
                                |) 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.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "core::num::bignum::Big32x40",
                        "div_rem_small",
                        []
                      |),
                      [
                        M.read (| x |);
                        BinOp.Wrap.shl (|
                          M.read (|
                            M.SubPointer.get_array_field (|
                              M.read (|
                                M.get_constant (| "core::num::flt2dec::strategy::dragon::POW10" |)
                              |),
                              n
                            |)
                          |),
                          Value.Integer IntegerKind.I32 1
                        |)
                      ]
                    |)
                  |) in
                M.alloc (| M.read (| x |) |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Function_div_2pow10 :
          M.IsFunction "core::num::flt2dec::strategy::dragon::div_2pow10" div_2pow10.
        
        (*
        fn div_rem_upto_16<'a>(
            x: &'a mut Big,
            scale: &Big,
            scale2: &Big,
            scale4: &Big,
            scale8: &Big,
        ) -> (u8, &'a mut Big) {
            let mut d = 0;
            if *x >= *scale8 {
                x.sub(scale8);
                d += 8;
            }
            if *x >= *scale4 {
                x.sub(scale4);
                d += 4;
            }
            if *x >= *scale2 {
                x.sub(scale2);
                d += 2;
            }
            if *x >= *scale {
                x.sub(scale);
                d += 1;
            }
            debug_assert!( *x < *scale);
            (d, x)
        }
        *)
        Definition div_rem_upto_16 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ x; scale; scale2; scale4; scale8 ] =>
            ltac:(M.monadic
              (let x := M.alloc (| x |) in
              let scale := M.alloc (| scale |) in
              let scale2 := M.alloc (| scale2 |) in
              let scale4 := M.alloc (| scale4 |) in
              let scale8 := M.alloc (| scale8 |) in
              M.read (|
                let~ d := M.alloc (| Value.Integer IntegerKind.U8 0 |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::cmp::PartialOrd",
                                    Ty.path "core::num::bignum::Big32x40",
                                    [ Ty.path "core::num::bignum::Big32x40" ],
                                    "ge",
                                    []
                                  |),
                                  [ M.read (| x |); M.read (| scale8 |) ]
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          let~ _ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::num::bignum::Big32x40",
                                  "sub",
                                  []
                                |),
                                [ M.read (| x |); M.read (| scale8 |) ]
                              |)
                            |) in
                          let~ _ :=
                            let β := d in
                            M.write (|
                              β,
                              BinOp.Wrap.add (| M.read (| β |), Value.Integer IntegerKind.U8 8 |)
                            |) 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 (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::cmp::PartialOrd",
                                    Ty.path "core::num::bignum::Big32x40",
                                    [ Ty.path "core::num::bignum::Big32x40" ],
                                    "ge",
                                    []
                                  |),
                                  [ M.read (| x |); M.read (| scale4 |) ]
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          let~ _ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::num::bignum::Big32x40",
                                  "sub",
                                  []
                                |),
                                [ M.read (| x |); M.read (| scale4 |) ]
                              |)
                            |) in
                          let~ _ :=
                            let β := d in
                            M.write (|
                              β,
                              BinOp.Wrap.add (| M.read (| β |), Value.Integer IntegerKind.U8 4 |)
                            |) 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 (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::cmp::PartialOrd",
                                    Ty.path "core::num::bignum::Big32x40",
                                    [ Ty.path "core::num::bignum::Big32x40" ],
                                    "ge",
                                    []
                                  |),
                                  [ M.read (| x |); M.read (| scale2 |) ]
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          let~ _ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::num::bignum::Big32x40",
                                  "sub",
                                  []
                                |),
                                [ M.read (| x |); M.read (| scale2 |) ]
                              |)
                            |) in
                          let~ _ :=
                            let β := d in
                            M.write (|
                              β,
                              BinOp.Wrap.add (| M.read (| β |), Value.Integer IntegerKind.U8 2 |)
                            |) 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 (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::cmp::PartialOrd",
                                    Ty.path "core::num::bignum::Big32x40",
                                    [ Ty.path "core::num::bignum::Big32x40" ],
                                    "ge",
                                    []
                                  |),
                                  [ M.read (| x |); M.read (| scale |) ]
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          let~ _ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::num::bignum::Big32x40",
                                  "sub",
                                  []
                                |),
                                [ M.read (| x |); M.read (| scale |) ]
                              |)
                            |) in
                          let~ _ :=
                            let β := d in
                            M.write (|
                              β,
                              BinOp.Wrap.add (| M.read (| β |), Value.Integer IntegerKind.U8 1 |)
                            |) in
                          M.alloc (| Value.Tuple [] |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.use (M.alloc (| Value.Bool true |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          let~ _ :=
                            M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          UnOp.not (|
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::cmp::PartialOrd",
                                                Ty.path "core::num::bignum::Big32x40",
                                                [ Ty.path "core::num::bignum::Big32x40" ],
                                                "lt",
                                                []
                                              |),
                                              [ M.read (| x |); M.read (| scale |) ]
                                            |)
                                          |)
                                        |)) 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 < *scale"
                                            |)
                                          ]
                                        |)
                                      |)
                                    |)));
                                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 (| d |); M.read (| x |) ] |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Function_div_rem_upto_16 :
          M.IsFunction "core::num::flt2dec::strategy::dragon::div_rem_upto_16" div_rem_upto_16.
        
        (*
        pub fn format_shortest<'a>(
            d: &Decoded,
            buf: &'a mut [MaybeUninit<u8>],
        ) -> (/*digits*/ &'a [u8], /*exp*/ i16) {
            // the number `v` to format is known to be:
            // - equal to `mant * 2^exp`;
            // - preceded by `(mant - 2 * minus) * 2^exp` in the original type; and
            // - followed by `(mant + 2 * plus) * 2^exp` in the original type.
            //
            // obviously, `minus` and `plus` cannot be zero. (for infinities, we use out-of-range values.)
            // also we assume that at least one digit is generated, i.e., `mant` cannot be zero too.
            //
            // this also means that any number between `low = (mant - minus) * 2^exp` and
            // `high = (mant + plus) * 2^exp` will map to this exact floating point number,
            // with bounds included when the original mantissa was even (i.e., `!mant_was_odd`).
        
            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);
        
            // `a.cmp(&b) < rounding` is `if d.inclusive {a <= b} else {a < b}`
            let rounding = if d.inclusive { Ordering::Greater } else { Ordering::Equal };
        
            // estimate `k_0` from original inputs satisfying `10^(k_0-1) < high <= 10^(k_0+1)`.
            // the tight bound `k` satisfying `10^(k-1) < high <= 10^k` is calculated later.
            let mut k = estimate_scaling_factor(d.mant + d.plus, d.exp);
        
            // convert `{mant, plus, minus} * 2^exp` into the fractional form so that:
            // - `v = mant / scale`
            // - `low = (mant - minus) / scale`
            // - `high = (mant + plus) / scale`
            let mut mant = Big::from_u64(d.mant);
            let mut minus = Big::from_u64(d.minus);
            let mut plus = Big::from_u64(d.plus);
            let mut scale = Big::from_small(1);
            if d.exp < 0 {
                scale.mul_pow2(-d.exp as usize);
            } else {
                mant.mul_pow2(d.exp as usize);
                minus.mul_pow2(d.exp as usize);
                plus.mul_pow2(d.exp as usize);
            }
        
            // divide `mant` by `10^k`. now `scale / 10 < mant + plus <= scale * 10`.
            if k >= 0 {
                mul_pow10(&mut scale, k as usize);
            } else {
                mul_pow10(&mut mant, -k as usize);
                mul_pow10(&mut minus, -k as usize);
                mul_pow10(&mut plus, -k as usize);
            }
        
            // fixup when `mant + plus > scale` (or `>=`).
            // we are not actually modifying `scale`, since we can skip the initial multiplication instead.
            // now `scale < mant + plus <= scale * 10` and we are ready to generate digits.
            //
            // note that `d[0]` *can* be zero, when `scale - plus < mant < scale`.
            // in this case rounding-up condition (`up` below) will be triggered immediately.
            if scale.cmp(mant.clone().add(&plus)) < rounding {
                // equivalent to scaling `scale` by 10
                k += 1;
            } else {
                mant.mul_small(10);
                minus.mul_small(10);
                plus.mul_small(10);
            }
        
            // cache `(2, 4, 8) * scale` for digit generation.
            let mut scale2 = scale.clone();
            scale2.mul_pow2(1);
            let mut scale4 = scale.clone();
            scale4.mul_pow2(2);
            let mut scale8 = scale.clone();
            scale8.mul_pow2(3);
        
            let mut down;
            let mut up;
            let mut i = 0;
            loop {
                // invariants, where `d[0..n-1]` are digits generated so far:
                // - `v = mant / scale * 10^(k-n-1) + d[0..n-1] * 10^(k-n)`
                // - `v - low = minus / scale * 10^(k-n-1)`
                // - `high - v = plus / scale * 10^(k-n-1)`
                // - `(mant + plus) / scale <= 10` (thus `mant / scale < 10`)
                // where `d[i..j]` is a shorthand for `d[i] * 10^(j-i) + ... + d[j-1] * 10 + d[j]`.
        
                // generate one digit: `d[n] = floor(mant / scale) < 10`.
                let (d, _) = div_rem_upto_16(&mut mant, &scale, &scale2, &scale4, &scale8);
                debug_assert!(d < 10);
                buf[i] = MaybeUninit::new(b'0' + d);
                i += 1;
        
                // this is a simplified description of the modified Dragon algorithm.
                // many intermediate derivations and completeness arguments are omitted for convenience.
                //
                // start with modified invariants, as we've updated `n`:
                // - `v = mant / scale * 10^(k-n) + d[0..n-1] * 10^(k-n)`
                // - `v - low = minus / scale * 10^(k-n)`
                // - `high - v = plus / scale * 10^(k-n)`
                //
                // assume that `d[0..n-1]` is the shortest representation between `low` and `high`,
                // i.e., `d[0..n-1]` satisfies both of the following but `d[0..n-2]` doesn't:
                // - `low < d[0..n-1] * 10^(k-n) < high` (bijectivity: digits round to `v`); and
                // - `abs(v / 10^(k-n) - d[0..n-1]) <= 1/2` (the last digit is correct).
                //
                // the second condition simplifies to `2 * mant <= scale`.
                // solving invariants in terms of `mant`, `low` and `high` yields
                // a simpler version of the first condition: `-plus < mant < minus`.
                // since `-plus < 0 <= mant`, we have the correct shortest representation
                // when `mant < minus` and `2 * mant <= scale`.
                // (the former becomes `mant <= minus` when the original mantissa is even.)
                //
                // when the second doesn't hold (`2 * mant > scale`), we need to increase the last digit.
                // this is enough for restoring that condition: we already know that
                // the digit generation guarantees `0 <= v / 10^(k-n) - d[0..n-1] < 1`.
                // in this case, the first condition becomes `-plus < mant - scale < minus`.
                // since `mant < scale` after the generation, we have `scale < mant + plus`.
                // (again, this becomes `scale <= mant + plus` when the original mantissa is even.)
                //
                // in short:
                // - stop and round `down` (keep digits as is) when `mant < minus` (or `<=`).
                // - stop and round `up` (increase the last digit) when `scale < mant + plus` (or `<=`).
                // - keep generating otherwise.
                down = mant.cmp(&minus) < rounding;
                up = scale.cmp(mant.clone().add(&plus)) < rounding;
                if down || up {
                    break;
                } // we have the shortest representation, proceed to the rounding
        
                // restore the invariants.
                // this makes the algorithm always terminating: `minus` and `plus` always increases,
                // but `mant` is clipped modulo `scale` and `scale` is fixed.
                mant.mul_small(10);
                minus.mul_small(10);
                plus.mul_small(10);
            }
        
            // rounding up happens when
            // i) only the rounding-up condition was triggered, or
            // ii) both conditions were triggered and tie breaking prefers rounding up.
            if up && (!down || *mant.mul_pow2(1) >= scale) {
                // if rounding up changes the length, the exponent should also change.
                // it seems that this condition is very hard to satisfy (possibly impossible),
                // but we are just being safe and consistent here.
                // SAFETY: we initialized that memory above.
                if let Some(c) = round_up(unsafe { MaybeUninit::slice_assume_init_mut(&mut buf[..i]) }) {
                    buf[i] = MaybeUninit::new(c);
                    i += 1;
                    k += 1;
                }
            }
        
            // SAFETY: we initialized that memory above.
            (unsafe { MaybeUninit::slice_assume_init_ref(&buf[..i]) }, k)
        }
        *)
        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 (|
                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~ rounding :=
                  M.copy (|
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.SubPointer.get_struct_record_field (|
                                  M.read (| d |),
                                  "core::num::flt2dec::decoder::Decoded",
                                  "inclusive"
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (| Value.StructTuple "core::cmp::Ordering::Greater" [] |)));
                        fun γ =>
                          ltac:(M.monadic
                            (M.alloc (| Value.StructTuple "core::cmp::Ordering::Equal" [] |)))
                      ]
                    |)
                  |) in
                let~ k :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::num::flt2dec::estimator::estimate_scaling_factor",
                        []
                      |),
                      [
                        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"
                            |)
                          |)
                        |);
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| d |),
                            "core::num::flt2dec::decoder::Decoded",
                            "exp"
                          |)
                        |)
                      ]
                    |)
                  |) in
                let~ mant :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "core::num::bignum::Big32x40",
                        "from_u64",
                        []
                      |),
                      [
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| d |),
                            "core::num::flt2dec::decoder::Decoded",
                            "mant"
                          |)
                        |)
                      ]
                    |)
                  |) in
                let~ minus :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "core::num::bignum::Big32x40",
                        "from_u64",
                        []
                      |),
                      [
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| d |),
                            "core::num::flt2dec::decoder::Decoded",
                            "minus"
                          |)
                        |)
                      ]
                    |)
                  |) in
                let~ plus :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "core::num::bignum::Big32x40",
                        "from_u64",
                        []
                      |),
                      [
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| d |),
                            "core::num::flt2dec::decoder::Decoded",
                            "plus"
                          |)
                        |)
                      ]
                    |)
                  |) in
                let~ scale :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "core::num::bignum::Big32x40",
                        "from_small",
                        []
                      |),
                      [ Value.Integer IntegerKind.U32 1 ]
                    |)
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.lt (|
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| d |),
                                      "core::num::flt2dec::decoder::Decoded",
                                      "exp"
                                    |)
                                  |),
                                  Value.Integer IntegerKind.I16 0
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          let~ _ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::num::bignum::Big32x40",
                                  "mul_pow2",
                                  []
                                |),
                                [
                                  scale;
                                  M.rust_cast
                                    (UnOp.neg (|
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| d |),
                                          "core::num::flt2dec::decoder::Decoded",
                                          "exp"
                                        |)
                                      |)
                                    |))
                                ]
                              |)
                            |) in
                          M.alloc (| Value.Tuple [] |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let~ _ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::num::bignum::Big32x40",
                                  "mul_pow2",
                                  []
                                |),
                                [
                                  mant;
                                  M.rust_cast
                                    (M.read (|
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| d |),
                                        "core::num::flt2dec::decoder::Decoded",
                                        "exp"
                                      |)
                                    |))
                                ]
                              |)
                            |) in
                          let~ _ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::num::bignum::Big32x40",
                                  "mul_pow2",
                                  []
                                |),
                                [
                                  minus;
                                  M.rust_cast
                                    (M.read (|
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| d |),
                                        "core::num::flt2dec::decoder::Decoded",
                                        "exp"
                                      |)
                                    |))
                                ]
                              |)
                            |) in
                          let~ _ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::num::bignum::Big32x40",
                                  "mul_pow2",
                                  []
                                |),
                                [
                                  plus;
                                  M.rust_cast
                                    (M.read (|
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| d |),
                                        "core::num::flt2dec::decoder::Decoded",
                                        "exp"
                                      |)
                                    |))
                                ]
                              |)
                            |) in
                          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 (| k |), Value.Integer IntegerKind.I16 0 |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          let~ _ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_function (|
                                  "core::num::flt2dec::strategy::dragon::mul_pow10",
                                  []
                                |),
                                [ scale; M.rust_cast (M.read (| k |)) ]
                              |)
                            |) in
                          M.alloc (| Value.Tuple [] |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let~ _ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_function (|
                                  "core::num::flt2dec::strategy::dragon::mul_pow10",
                                  []
                                |),
                                [ mant; M.rust_cast (UnOp.neg (| M.read (| k |) |)) ]
                              |)
                            |) in
                          let~ _ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_function (|
                                  "core::num::flt2dec::strategy::dragon::mul_pow10",
                                  []
                                |),
                                [ minus; M.rust_cast (UnOp.neg (| M.read (| k |) |)) ]
                              |)
                            |) in
                          let~ _ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_function (|
                                  "core::num::flt2dec::strategy::dragon::mul_pow10",
                                  []
                                |),
                                [ plus; M.rust_cast (UnOp.neg (| M.read (| k |) |)) ]
                              |)
                            |) in
                          M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::cmp::PartialOrd",
                                    Ty.path "core::cmp::Ordering",
                                    [ Ty.path "core::cmp::Ordering" ],
                                    "lt",
                                    []
                                  |),
                                  [
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::cmp::Ord",
                                          Ty.path "core::num::bignum::Big32x40",
                                          [],
                                          "cmp",
                                          []
                                        |),
                                        [
                                          scale;
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "core::num::bignum::Big32x40",
                                              "add",
                                              []
                                            |),
                                            [
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::clone::Clone",
                                                    Ty.path "core::num::bignum::Big32x40",
                                                    [],
                                                    "clone",
                                                    []
                                                  |),
                                                  [ mant ]
                                                |)
                                              |);
                                              plus
                                            ]
                                          |)
                                        ]
                                      |)
                                    |);
                                    rounding
                                  ]
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          let~ _ :=
                            let β := k in
                            M.write (|
                              β,
                              BinOp.Wrap.add (| M.read (| β |), Value.Integer IntegerKind.I16 1 |)
                            |) in
                          M.alloc (| Value.Tuple [] |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let~ _ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::num::bignum::Big32x40",
                                  "mul_small",
                                  []
                                |),
                                [ mant; Value.Integer IntegerKind.U32 10 ]
                              |)
                            |) in
                          let~ _ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::num::bignum::Big32x40",
                                  "mul_small",
                                  []
                                |),
                                [ minus; Value.Integer IntegerKind.U32 10 ]
                              |)
                            |) in
                          let~ _ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::num::bignum::Big32x40",
                                  "mul_small",
                                  []
                                |),
                                [ plus; Value.Integer IntegerKind.U32 10 ]
                              |)
                            |) in
                          M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ scale2 :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::clone::Clone",
                        Ty.path "core::num::bignum::Big32x40",
                        [],
                        "clone",
                        []
                      |),
                      [ scale ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "core::num::bignum::Big32x40",
                        "mul_pow2",
                        []
                      |),
                      [ scale2; Value.Integer IntegerKind.Usize 1 ]
                    |)
                  |) in
                let~ scale4 :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::clone::Clone",
                        Ty.path "core::num::bignum::Big32x40",
                        [],
                        "clone",
                        []
                      |),
                      [ scale ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "core::num::bignum::Big32x40",
                        "mul_pow2",
                        []
                      |),
                      [ scale4; Value.Integer IntegerKind.Usize 2 ]
                    |)
                  |) in
                let~ scale8 :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::clone::Clone",
                        Ty.path "core::num::bignum::Big32x40",
                        [],
                        "clone",
                        []
                      |),
                      [ scale ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "core::num::bignum::Big32x40",
                        "mul_pow2",
                        []
                      |),
                      [ scale8; Value.Integer IntegerKind.Usize 3 ]
                    |)
                  |) in
                let~ down := M.copy (| Value.DeclaredButUndefined |) in
                let~ up := M.copy (| Value.DeclaredButUndefined |) in
                let~ i := M.alloc (| Value.Integer IntegerKind.Usize 0 |) in
                let~ _ :=
                  M.loop (|
                    ltac:(M.monadic
                      (M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_function (|
                              "core::num::flt2dec::strategy::dragon::div_rem_upto_16",
                              []
                            |),
                            [ mant; scale; scale2; scale4; scale8 ]
                          |)
                        |),
                        [
                          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 d := M.copy (| γ0_0 |) in
                              let~ _ :=
                                M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ := M.use (M.alloc (| Value.Bool true |)) in
                                        let _ :=
                                          M.is_constant_or_break_match (|
                                            M.read (| γ |),
                                            Value.Bool true
                                          |) in
                                        let~ _ :=
                                          M.match_operator (|
                                            M.alloc (| Value.Tuple [] |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ :=
                                                    M.use
                                                      (M.alloc (|
                                                        UnOp.not (|
                                                          BinOp.lt (|
                                                            M.read (| d |),
                                                            Value.Integer IntegerKind.U8 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: d < 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.read (| d |)
                                      |)
                                    ]
                                  |)
                                |) in
                              let~ _ :=
                                let β := i in
                                M.write (|
                                  β,
                                  BinOp.Wrap.add (|
                                    M.read (| β |),
                                    Value.Integer IntegerKind.Usize 1
                                  |)
                                |) in
                              let~ _ :=
                                M.write (|
                                  down,
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::cmp::PartialOrd",
                                      Ty.path "core::cmp::Ordering",
                                      [ Ty.path "core::cmp::Ordering" ],
                                      "lt",
                                      []
                                    |),
                                    [
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::cmp::Ord",
                                            Ty.path "core::num::bignum::Big32x40",
                                            [],
                                            "cmp",
                                            []
                                          |),
                                          [ mant; minus ]
                                        |)
                                      |);
                                      rounding
                                    ]
                                  |)
                                |) in
                              let~ _ :=
                                M.write (|
                                  up,
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::cmp::PartialOrd",
                                      Ty.path "core::cmp::Ordering",
                                      [ Ty.path "core::cmp::Ordering" ],
                                      "lt",
                                      []
                                    |),
                                    [
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::cmp::Ord",
                                            Ty.path "core::num::bignum::Big32x40",
                                            [],
                                            "cmp",
                                            []
                                          |),
                                          [
                                            scale;
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.path "core::num::bignum::Big32x40",
                                                "add",
                                                []
                                              |),
                                              [
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_trait_method (|
                                                      "core::clone::Clone",
                                                      Ty.path "core::num::bignum::Big32x40",
                                                      [],
                                                      "clone",
                                                      []
                                                    |),
                                                    [ mant ]
                                                  |)
                                                |);
                                                plus
                                              ]
                                            |)
                                          ]
                                        |)
                                      |);
                                      rounding
                                    ]
                                  |)
                                |) in
                              let~ _ :=
                                M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ :=
                                          M.use
                                            (M.alloc (|
                                              LogicalOp.or (|
                                                M.read (| down |),
                                                ltac:(M.monadic (M.read (| up |)))
                                              |)
                                            |)) in
                                        let _ :=
                                          M.is_constant_or_break_match (|
                                            M.read (| γ |),
                                            Value.Bool true
                                          |) in
                                        M.alloc (|
                                          M.never_to_any (| M.read (| M.break (||) |) |)
                                        |)));
                                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                  ]
                                |) in
                              let~ _ :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::num::bignum::Big32x40",
                                      "mul_small",
                                      []
                                    |),
                                    [ mant; Value.Integer IntegerKind.U32 10 ]
                                  |)
                                |) in
                              let~ _ :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::num::bignum::Big32x40",
                                      "mul_small",
                                      []
                                    |),
                                    [ minus; Value.Integer IntegerKind.U32 10 ]
                                  |)
                                |) in
                              let~ _ :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::num::bignum::Big32x40",
                                      "mul_small",
                                      []
                                    |),
                                    [ plus; Value.Integer IntegerKind.U32 10 ]
                                  |)
                                |) 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 (|
                                  M.read (| up |),
                                  ltac:(M.monadic
                                    (LogicalOp.or (|
                                      UnOp.not (| M.read (| down |) |),
                                      ltac:(M.monadic
                                        (M.call_closure (|
                                          M.get_trait_method (|
                                            "core::cmp::PartialOrd",
                                            Ty.path "core::num::bignum::Big32x40",
                                            [ Ty.path "core::num::bignum::Big32x40" ],
                                            "ge",
                                            []
                                          |),
                                          [
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.path "core::num::bignum::Big32x40",
                                                "mul_pow2",
                                                []
                                              |),
                                              [ mant; Value.Integer IntegerKind.Usize 1 ]
                                            |);
                                            scale
                                          ]
                                        |)))
                                    |)))
                                |)
                              |)) 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.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 (| i |)) ]
                                                ]
                                              |)
                                            ]
                                          |)
                                        ]
                                      |)
                                    |) in
                                  let γ0_0 :=
                                    M.SubPointer.get_struct_tuple_field (|
                                      γ,
                                      "core::option::Option::Some",
                                      0
                                    |) in
                                  let c := M.copy (| γ0_0 |) 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",
                                          []
                                        |),
                                        [ M.read (| c |) ]
                                      |)
                                    |) in
                                  let~ _ :=
                                    let β := i in
                                    M.write (|
                                      β,
                                      BinOp.Wrap.add (|
                                        M.read (| β |),
                                        Value.Integer IntegerKind.Usize 1
                                      |)
                                    |) in
                                  let~ _ :=
                                    let β := k in
                                    M.write (|
                                      β,
                                      BinOp.Wrap.add (|
                                        M.read (| β |),
                                        Value.Integer IntegerKind.I16 1
                                      |)
                                    |) in
                                  M.alloc (| Value.Tuple [] |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                M.alloc (|
                  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 (| i |)) ]
                            ]
                          |)
                        ]
                      |);
                      M.read (| k |)
                    ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Function_format_shortest :
          M.IsFunction "core::num::flt2dec::strategy::dragon::format_shortest" format_shortest.
        
        (*
        pub fn format_exact<'a>(
            d: &Decoded,
            buf: &'a mut [MaybeUninit<u8>],
            limit: i16,
        ) -> (/*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());
        
            // estimate `k_0` from original inputs satisfying `10^(k_0-1) < v <= 10^(k_0+1)`.
            let mut k = estimate_scaling_factor(d.mant, d.exp);
        
            // `v = mant / scale`.
            let mut mant = Big::from_u64(d.mant);
            let mut scale = Big::from_small(1);
            if d.exp < 0 {
                scale.mul_pow2(-d.exp as usize);
            } else {
                mant.mul_pow2(d.exp as usize);
            }
        
            // divide `mant` by `10^k`. now `scale / 10 < mant <= scale * 10`.
            if k >= 0 {
                mul_pow10(&mut scale, k as usize);
            } else {
                mul_pow10(&mut mant, -k as usize);
            }
        
            // fixup when `mant + plus >= scale`, where `plus / scale = 10^-buf.len() / 2`.
            // in order to keep the fixed-size bignum, we actually use `mant + floor(plus) >= scale`.
            // we are not actually modifying `scale`, since we can skip the initial multiplication instead.
            // again with the shortest algorithm, `d[0]` can be zero but will be eventually rounded up.
            if *div_2pow10(&mut scale.clone(), buf.len()).add(&mant) >= scale {
                // equivalent to scaling `scale` by 10
                k += 1;
            } else {
                mant.mul_small(10);
            }
        
            // 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 mut len = if k < 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.
                // we return an empty buffer, with an exception of the later rounding-up case
                // which occurs when `k == limit` and has to produce exactly one digit.
                0
            } else if ((k as i32 - limit as i32) as usize) < buf.len() {
                (k - limit) as usize
            } else {
                buf.len()
            };
        
            if len > 0 {
                // cache `(2, 4, 8) * scale` for digit generation.
                // (this can be expensive, so do not calculate them when the buffer is empty.)
                let mut scale2 = scale.clone();
                scale2.mul_pow2(1);
                let mut scale4 = scale.clone();
                scale4.mul_pow2(2);
                let mut scale8 = scale.clone();
                scale8.mul_pow2(3);
        
                for i in 0..len {
                    if mant.is_zero() {
                        // following digits are all zeroes, we stop here
                        // do *not* try to perform rounding! rather, fill remaining digits.
                        for c in &mut buf[i..len] {
                            *c = MaybeUninit::new(b'0');
                        }
                        // SAFETY: we initialized that memory above.
                        return (unsafe { MaybeUninit::slice_assume_init_ref(&buf[..len]) }, k);
                    }
        
                    let mut d = 0;
                    if mant >= scale8 {
                        mant.sub(&scale8);
                        d += 8;
                    }
                    if mant >= scale4 {
                        mant.sub(&scale4);
                        d += 4;
                    }
                    if mant >= scale2 {
                        mant.sub(&scale2);
                        d += 2;
                    }
                    if mant >= scale {
                        mant.sub(&scale);
                        d += 1;
                    }
                    debug_assert!(mant < scale);
                    debug_assert!(d < 10);
                    buf[i] = MaybeUninit::new(b'0' + d);
                    mant.mul_small(10);
                }
            }
        
            // rounding up if we stop in the middle of digits
            // if the following digits are exactly 5000..., check the prior digit and try to
            // round to even (i.e., avoid rounding up when the prior digit is even).
            let order = mant.cmp(scale.mul_small(5));
            if order == Ordering::Greater
                || (order == Ordering::Equal
                    // SAFETY: `buf[len-1]` is initialized.
                    && len > 0 && unsafe { buf[len - 1].assume_init() } & 1 == 1)
            {
                // if rounding up changes the length, the exponent should also change.
                // but we've been requested a fixed number of digits, so do not alter the buffer...
                // SAFETY: we initialized that memory above.
                if let Some(c) = round_up(unsafe { MaybeUninit::slice_assume_init_mut(&mut buf[..len]) }) {
                    // ...unless we've been requested the fixed precision instead.
                    // we also need to check that, if the original buffer was empty,
                    // the additional digit can only be added when `k == limit` (edge case).
                    k += 1;
                    if k > limit && len < buf.len() {
                        buf[len] = MaybeUninit::new(c);
                        len += 1;
                    }
                }
            }
        
            // SAFETY: we initialized that memory above.
            (unsafe { MaybeUninit::slice_assume_init_ref(&buf[..len]) }, k)
        }
        *)
        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.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 (|
                                      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~ k :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_function (|
                            "core::num::flt2dec::estimator::estimate_scaling_factor",
                            []
                          |),
                          [
                            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",
                                "exp"
                              |)
                            |)
                          ]
                        |)
                      |) in
                    let~ mant :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::num::bignum::Big32x40",
                            "from_u64",
                            []
                          |),
                          [
                            M.read (|
                              M.SubPointer.get_struct_record_field (|
                                M.read (| d |),
                                "core::num::flt2dec::decoder::Decoded",
                                "mant"
                              |)
                            |)
                          ]
                        |)
                      |) in
                    let~ scale :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::num::bignum::Big32x40",
                            "from_small",
                            []
                          |),
                          [ Value.Integer IntegerKind.U32 1 ]
                        |)
                      |) in
                    let~ _ :=
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.use
                                  (M.alloc (|
                                    BinOp.lt (|
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| d |),
                                          "core::num::flt2dec::decoder::Decoded",
                                          "exp"
                                        |)
                                      |),
                                      Value.Integer IntegerKind.I16 0
                                    |)
                                  |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              let~ _ :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::num::bignum::Big32x40",
                                      "mul_pow2",
                                      []
                                    |),
                                    [
                                      scale;
                                      M.rust_cast
                                        (UnOp.neg (|
                                          M.read (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| d |),
                                              "core::num::flt2dec::decoder::Decoded",
                                              "exp"
                                            |)
                                          |)
                                        |))
                                    ]
                                  |)
                                |) in
                              M.alloc (| Value.Tuple [] |)));
                          fun γ =>
                            ltac:(M.monadic
                              (let~ _ :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::num::bignum::Big32x40",
                                      "mul_pow2",
                                      []
                                    |),
                                    [
                                      mant;
                                      M.rust_cast
                                        (M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| d |),
                                            "core::num::flt2dec::decoder::Decoded",
                                            "exp"
                                          |)
                                        |))
                                    ]
                                  |)
                                |) in
                              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 (| k |), Value.Integer IntegerKind.I16 0 |)
                                  |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              let~ _ :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_function (|
                                      "core::num::flt2dec::strategy::dragon::mul_pow10",
                                      []
                                    |),
                                    [ scale; M.rust_cast (M.read (| k |)) ]
                                  |)
                                |) in
                              M.alloc (| Value.Tuple [] |)));
                          fun γ =>
                            ltac:(M.monadic
                              (let~ _ :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_function (|
                                      "core::num::flt2dec::strategy::dragon::mul_pow10",
                                      []
                                    |),
                                    [ mant; M.rust_cast (UnOp.neg (| M.read (| k |) |)) ]
                                  |)
                                |) in
                              M.alloc (| Value.Tuple [] |)))
                        ]
                      |) in
                    let~ _ :=
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.use
                                  (M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::cmp::PartialOrd",
                                        Ty.path "core::num::bignum::Big32x40",
                                        [ Ty.path "core::num::bignum::Big32x40" ],
                                        "ge",
                                        []
                                      |),
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "core::num::bignum::Big32x40",
                                            "add",
                                            []
                                          |),
                                          [
                                            M.call_closure (|
                                              M.get_function (|
                                                "core::num::flt2dec::strategy::dragon::div_2pow10",
                                                []
                                              |),
                                              [
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_trait_method (|
                                                      "core::clone::Clone",
                                                      Ty.path "core::num::bignum::Big32x40",
                                                      [],
                                                      "clone",
                                                      []
                                                    |),
                                                    [ scale ]
                                                  |)
                                                |);
                                                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 |) ]
                                                |)
                                              ]
                                            |);
                                            mant
                                          ]
                                        |);
                                        scale
                                      ]
                                    |)
                                  |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              let~ _ :=
                                let β := k in
                                M.write (|
                                  β,
                                  BinOp.Wrap.add (|
                                    M.read (| β |),
                                    Value.Integer IntegerKind.I16 1
                                  |)
                                |) in
                              M.alloc (| Value.Tuple [] |)));
                          fun γ =>
                            ltac:(M.monadic
                              (let~ _ :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::num::bignum::Big32x40",
                                      "mul_small",
                                      []
                                    |),
                                    [ mant; Value.Integer IntegerKind.U32 10 ]
                                  |)
                                |) in
                              M.alloc (| Value.Tuple [] |)))
                        ]
                      |) in
                    let~ len :=
                      M.copy (|
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      BinOp.lt (| M.read (| k |), M.read (| limit |) |)
                                    |)) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                M.alloc (| Value.Integer IntegerKind.Usize 0 |)));
                            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 (| k |)),
                                                    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 (| k |),
                                              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 (|
                                    BinOp.gt (|
                                      M.read (| len |),
                                      Value.Integer IntegerKind.Usize 0
                                    |)
                                  |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              let~ scale2 :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::clone::Clone",
                                      Ty.path "core::num::bignum::Big32x40",
                                      [],
                                      "clone",
                                      []
                                    |),
                                    [ scale ]
                                  |)
                                |) in
                              let~ _ :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::num::bignum::Big32x40",
                                      "mul_pow2",
                                      []
                                    |),
                                    [ scale2; Value.Integer IntegerKind.Usize 1 ]
                                  |)
                                |) in
                              let~ scale4 :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::clone::Clone",
                                      Ty.path "core::num::bignum::Big32x40",
                                      [],
                                      "clone",
                                      []
                                    |),
                                    [ scale ]
                                  |)
                                |) in
                              let~ _ :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::num::bignum::Big32x40",
                                      "mul_pow2",
                                      []
                                    |),
                                    [ scale4; Value.Integer IntegerKind.Usize 2 ]
                                  |)
                                |) in
                              let~ scale8 :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::clone::Clone",
                                      Ty.path "core::num::bignum::Big32x40",
                                      [],
                                      "clone",
                                      []
                                    |),
                                    [ scale ]
                                  |)
                                |) in
                              let~ _ :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::num::bignum::Big32x40",
                                      "mul_pow2",
                                      []
                                    |),
                                    [ scale8; Value.Integer IntegerKind.Usize 3 ]
                                  |)
                                |) in
                              M.use
                                (M.match_operator (|
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::iter::traits::collect::IntoIterator",
                                        Ty.apply
                                          (Ty.path "core::ops::range::Range")
                                          []
                                          [ Ty.path "usize" ],
                                        [],
                                        "into_iter",
                                        []
                                      |),
                                      [
                                        Value.StructRecord
                                          "core::ops::range::Range"
                                          [
                                            ("start", Value.Integer IntegerKind.Usize 0);
                                            ("end_", M.read (| len |))
                                          ]
                                      ]
                                    |)
                                  |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let iter := M.copy (| γ |) in
                                        M.loop (|
                                          ltac:(M.monadic
                                            (let~ _ :=
                                              M.match_operator (|
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_trait_method (|
                                                      "core::iter::traits::iterator::Iterator",
                                                      Ty.apply
                                                        (Ty.path "core::ops::range::Range")
                                                        []
                                                        [ Ty.path "usize" ],
                                                      [],
                                                      "next",
                                                      []
                                                    |),
                                                    [ iter ]
                                                  |)
                                                |),
                                                [
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let _ :=
                                                        M.is_struct_tuple (|
                                                          γ,
                                                          "core::option::Option::None"
                                                        |) in
                                                      M.alloc (|
                                                        M.never_to_any (|
                                                          M.read (| M.break (||) |)
                                                        |)
                                                      |)));
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ0_0 :=
                                                        M.SubPointer.get_struct_tuple_field (|
                                                          γ,
                                                          "core::option::Option::Some",
                                                          0
                                                        |) in
                                                      let i := M.copy (| γ0_0 |) in
                                                      let~ _ :=
                                                        M.match_operator (|
                                                          M.alloc (| Value.Tuple [] |),
                                                          [
                                                            fun γ =>
                                                              ltac:(M.monadic
                                                                (let γ :=
                                                                  M.use
                                                                    (M.alloc (|
                                                                      M.call_closure (|
                                                                        M.get_associated_function (|
                                                                          Ty.path
                                                                            "core::num::bignum::Big32x40",
                                                                          "is_zero",
                                                                          []
                                                                        |),
                                                                        [ mant ]
                                                                      |)
                                                                    |)) in
                                                                let _ :=
                                                                  M.is_constant_or_break_match (|
                                                                    M.read (| γ |),
                                                                    Value.Bool true
                                                                  |) in
                                                                M.alloc (|
                                                                  M.never_to_any (|
                                                                    M.read (|
                                                                      let~ _ :=
                                                                        M.use
                                                                          (M.match_operator (|
                                                                            M.alloc (|
                                                                              M.call_closure (|
                                                                                M.get_trait_method (|
                                                                                  "core::iter::traits::collect::IntoIterator",
                                                                                  Ty.apply
                                                                                    (Ty.path "&mut")
                                                                                    []
                                                                                    [
                                                                                      Ty.apply
                                                                                        (Ty.path
                                                                                          "slice")
                                                                                        []
                                                                                        [
                                                                                          Ty.apply
                                                                                            (Ty.path
                                                                                              "core::mem::maybe_uninit::MaybeUninit")
                                                                                            []
                                                                                            [
                                                                                              Ty.path
                                                                                                "u8"
                                                                                            ]
                                                                                        ]
                                                                                    ],
                                                                                  [],
                                                                                  "into_iter",
                                                                                  []
                                                                                |),
                                                                                [
                                                                                  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::Range")
                                                                                          []
                                                                                          [
                                                                                            Ty.path
                                                                                              "usize"
                                                                                          ]
                                                                                      ],
                                                                                      "index_mut",
                                                                                      []
                                                                                    |),
                                                                                    [
                                                                                      M.read (|
                                                                                        buf
                                                                                      |);
                                                                                      Value.StructRecord
                                                                                        "core::ops::range::Range"
                                                                                        [
                                                                                          ("start",
                                                                                            M.read (|
                                                                                              i
                                                                                            |));
                                                                                          ("end_",
                                                                                            M.read (|
                                                                                              len
                                                                                            |))
                                                                                        ]
                                                                                    ]
                                                                                  |)
                                                                                ]
                                                                              |)
                                                                            |),
                                                                            [
                                                                              fun γ =>
                                                                                ltac:(M.monadic
                                                                                  (let iter :=
                                                                                    M.copy (|
                                                                                      γ
                                                                                    |) in
                                                                                  M.loop (|
                                                                                    ltac:(M.monadic
                                                                                      (let~ _ :=
                                                                                        M.match_operator (|
                                                                                          M.alloc (|
                                                                                            M.call_closure (|
                                                                                              M.get_trait_method (|
                                                                                                "core::iter::traits::iterator::Iterator",
                                                                                                Ty.apply
                                                                                                  (Ty.path
                                                                                                    "core::slice::iter::IterMut")
                                                                                                  []
                                                                                                  [
                                                                                                    Ty.apply
                                                                                                      (Ty.path
                                                                                                        "core::mem::maybe_uninit::MaybeUninit")
                                                                                                      []
                                                                                                      [
                                                                                                        Ty.path
                                                                                                          "u8"
                                                                                                      ]
                                                                                                  ],
                                                                                                [],
                                                                                                "next",
                                                                                                []
                                                                                              |),
                                                                                              [ iter
                                                                                              ]
                                                                                            |)
                                                                                          |),
                                                                                          [
                                                                                            fun γ =>
                                                                                              ltac:(M.monadic
                                                                                                (let
                                                                                                      _ :=
                                                                                                  M.is_struct_tuple (|
                                                                                                    γ,
                                                                                                    "core::option::Option::None"
                                                                                                  |) in
                                                                                                M.alloc (|
                                                                                                  M.never_to_any (|
                                                                                                    M.read (|
                                                                                                      M.break (||)
                                                                                                    |)
                                                                                                  |)
                                                                                                |)));
                                                                                            fun γ =>
                                                                                              ltac:(M.monadic
                                                                                                (let
                                                                                                      γ0_0 :=
                                                                                                  M.SubPointer.get_struct_tuple_field (|
                                                                                                    γ,
                                                                                                    "core::option::Option::Some",
                                                                                                    0
                                                                                                  |) in
                                                                                                let
                                                                                                      c :=
                                                                                                  M.copy (|
                                                                                                    γ0_0
                                                                                                  |) in
                                                                                                let~
                                                                                                      _ :=
                                                                                                  M.write (|
                                                                                                    M.read (|
                                                                                                      c
                                                                                                    |),
                                                                                                    M.call_closure (|
                                                                                                      M.get_associated_function (|
                                                                                                        Ty.apply
                                                                                                          (Ty.path
                                                                                                            "core::mem::maybe_uninit::MaybeUninit")
                                                                                                          []
                                                                                                          [
                                                                                                            Ty.path
                                                                                                              "u8"
                                                                                                          ],
                                                                                                        "new",
                                                                                                        []
                                                                                                      |),
                                                                                                      [
                                                                                                        M.read (|
                                                                                                          UnsupportedLiteral
                                                                                                        |)
                                                                                                      ]
                                                                                                    |)
                                                                                                  |) in
                                                                                                M.alloc (|
                                                                                                  Value.Tuple
                                                                                                    []
                                                                                                |)))
                                                                                          ]
                                                                                        |) in
                                                                                      M.alloc (|
                                                                                        Value.Tuple
                                                                                          []
                                                                                      |)))
                                                                                  |)))
                                                                            ]
                                                                          |)) in
                                                                      M.return_ (|
                                                                        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 (| k |)
                                                                          ]
                                                                      |)
                                                                    |)
                                                                  |)
                                                                |)));
                                                            fun γ =>
                                                              ltac:(M.monadic
                                                                (M.alloc (| Value.Tuple [] |)))
                                                          ]
                                                        |) in
                                                      let~ d :=
                                                        M.alloc (|
                                                          Value.Integer IntegerKind.U8 0
                                                        |) in
                                                      let~ _ :=
                                                        M.match_operator (|
                                                          M.alloc (| Value.Tuple [] |),
                                                          [
                                                            fun γ =>
                                                              ltac:(M.monadic
                                                                (let γ :=
                                                                  M.use
                                                                    (M.alloc (|
                                                                      M.call_closure (|
                                                                        M.get_trait_method (|
                                                                          "core::cmp::PartialOrd",
                                                                          Ty.path
                                                                            "core::num::bignum::Big32x40",
                                                                          [
                                                                            Ty.path
                                                                              "core::num::bignum::Big32x40"
                                                                          ],
                                                                          "ge",
                                                                          []
                                                                        |),
                                                                        [ mant; scale8 ]
                                                                      |)
                                                                    |)) in
                                                                let _ :=
                                                                  M.is_constant_or_break_match (|
                                                                    M.read (| γ |),
                                                                    Value.Bool true
                                                                  |) in
                                                                let~ _ :=
                                                                  M.alloc (|
                                                                    M.call_closure (|
                                                                      M.get_associated_function (|
                                                                        Ty.path
                                                                          "core::num::bignum::Big32x40",
                                                                        "sub",
                                                                        []
                                                                      |),
                                                                      [ mant; scale8 ]
                                                                    |)
                                                                  |) in
                                                                let~ _ :=
                                                                  let β := d in
                                                                  M.write (|
                                                                    β,
                                                                    BinOp.Wrap.add (|
                                                                      M.read (| β |),
                                                                      Value.Integer IntegerKind.U8 8
                                                                    |)
                                                                  |) 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 (|
                                                                      M.call_closure (|
                                                                        M.get_trait_method (|
                                                                          "core::cmp::PartialOrd",
                                                                          Ty.path
                                                                            "core::num::bignum::Big32x40",
                                                                          [
                                                                            Ty.path
                                                                              "core::num::bignum::Big32x40"
                                                                          ],
                                                                          "ge",
                                                                          []
                                                                        |),
                                                                        [ mant; scale4 ]
                                                                      |)
                                                                    |)) in
                                                                let _ :=
                                                                  M.is_constant_or_break_match (|
                                                                    M.read (| γ |),
                                                                    Value.Bool true
                                                                  |) in
                                                                let~ _ :=
                                                                  M.alloc (|
                                                                    M.call_closure (|
                                                                      M.get_associated_function (|
                                                                        Ty.path
                                                                          "core::num::bignum::Big32x40",
                                                                        "sub",
                                                                        []
                                                                      |),
                                                                      [ mant; scale4 ]
                                                                    |)
                                                                  |) in
                                                                let~ _ :=
                                                                  let β := d in
                                                                  M.write (|
                                                                    β,
                                                                    BinOp.Wrap.add (|
                                                                      M.read (| β |),
                                                                      Value.Integer IntegerKind.U8 4
                                                                    |)
                                                                  |) 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 (|
                                                                      M.call_closure (|
                                                                        M.get_trait_method (|
                                                                          "core::cmp::PartialOrd",
                                                                          Ty.path
                                                                            "core::num::bignum::Big32x40",
                                                                          [
                                                                            Ty.path
                                                                              "core::num::bignum::Big32x40"
                                                                          ],
                                                                          "ge",
                                                                          []
                                                                        |),
                                                                        [ mant; scale2 ]
                                                                      |)
                                                                    |)) in
                                                                let _ :=
                                                                  M.is_constant_or_break_match (|
                                                                    M.read (| γ |),
                                                                    Value.Bool true
                                                                  |) in
                                                                let~ _ :=
                                                                  M.alloc (|
                                                                    M.call_closure (|
                                                                      M.get_associated_function (|
                                                                        Ty.path
                                                                          "core::num::bignum::Big32x40",
                                                                        "sub",
                                                                        []
                                                                      |),
                                                                      [ mant; scale2 ]
                                                                    |)
                                                                  |) in
                                                                let~ _ :=
                                                                  let β := d in
                                                                  M.write (|
                                                                    β,
                                                                    BinOp.Wrap.add (|
                                                                      M.read (| β |),
                                                                      Value.Integer IntegerKind.U8 2
                                                                    |)
                                                                  |) 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 (|
                                                                      M.call_closure (|
                                                                        M.get_trait_method (|
                                                                          "core::cmp::PartialOrd",
                                                                          Ty.path
                                                                            "core::num::bignum::Big32x40",
                                                                          [
                                                                            Ty.path
                                                                              "core::num::bignum::Big32x40"
                                                                          ],
                                                                          "ge",
                                                                          []
                                                                        |),
                                                                        [ mant; scale ]
                                                                      |)
                                                                    |)) in
                                                                let _ :=
                                                                  M.is_constant_or_break_match (|
                                                                    M.read (| γ |),
                                                                    Value.Bool true
                                                                  |) in
                                                                let~ _ :=
                                                                  M.alloc (|
                                                                    M.call_closure (|
                                                                      M.get_associated_function (|
                                                                        Ty.path
                                                                          "core::num::bignum::Big32x40",
                                                                        "sub",
                                                                        []
                                                                      |),
                                                                      [ mant; scale ]
                                                                    |)
                                                                  |) in
                                                                let~ _ :=
                                                                  let β := d in
                                                                  M.write (|
                                                                    β,
                                                                    BinOp.Wrap.add (|
                                                                      M.read (| β |),
                                                                      Value.Integer IntegerKind.U8 1
                                                                    |)
                                                                  |) in
                                                                M.alloc (| Value.Tuple [] |)));
                                                            fun γ =>
                                                              ltac:(M.monadic
                                                                (M.alloc (| Value.Tuple [] |)))
                                                          ]
                                                        |) in
                                                      let~ _ :=
                                                        M.match_operator (|
                                                          M.alloc (| Value.Tuple [] |),
                                                          [
                                                            fun γ =>
                                                              ltac:(M.monadic
                                                                (let γ :=
                                                                  M.use
                                                                    (M.alloc (|
                                                                      Value.Bool true
                                                                    |)) in
                                                                let _ :=
                                                                  M.is_constant_or_break_match (|
                                                                    M.read (| γ |),
                                                                    Value.Bool true
                                                                  |) in
                                                                let~ _ :=
                                                                  M.match_operator (|
                                                                    M.alloc (| Value.Tuple [] |),
                                                                    [
                                                                      fun γ =>
                                                                        ltac:(M.monadic
                                                                          (let γ :=
                                                                            M.use
                                                                              (M.alloc (|
                                                                                UnOp.not (|
                                                                                  M.call_closure (|
                                                                                    M.get_trait_method (|
                                                                                      "core::cmp::PartialOrd",
                                                                                      Ty.path
                                                                                        "core::num::bignum::Big32x40",
                                                                                      [
                                                                                        Ty.path
                                                                                          "core::num::bignum::Big32x40"
                                                                                      ],
                                                                                      "lt",
                                                                                      []
                                                                                    |),
                                                                                    [ mant; scale ]
                                                                                  |)
                                                                                |)
                                                                              |)) 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: mant < scale"
                                                                                  |)
                                                                                ]
                                                                              |)
                                                                            |)
                                                                          |)));
                                                                      fun γ =>
                                                                        ltac:(M.monadic
                                                                          (M.alloc (|
                                                                            Value.Tuple []
                                                                          |)))
                                                                    ]
                                                                  |) in
                                                                M.alloc (| Value.Tuple [] |)));
                                                            fun γ =>
                                                              ltac:(M.monadic
                                                                (M.alloc (| Value.Tuple [] |)))
                                                          ]
                                                        |) in
                                                      let~ _ :=
                                                        M.match_operator (|
                                                          M.alloc (| Value.Tuple [] |),
                                                          [
                                                            fun γ =>
                                                              ltac:(M.monadic
                                                                (let γ :=
                                                                  M.use
                                                                    (M.alloc (|
                                                                      Value.Bool true
                                                                    |)) in
                                                                let _ :=
                                                                  M.is_constant_or_break_match (|
                                                                    M.read (| γ |),
                                                                    Value.Bool true
                                                                  |) in
                                                                let~ _ :=
                                                                  M.match_operator (|
                                                                    M.alloc (| Value.Tuple [] |),
                                                                    [
                                                                      fun γ =>
                                                                        ltac:(M.monadic
                                                                          (let γ :=
                                                                            M.use
                                                                              (M.alloc (|
                                                                                UnOp.not (|
                                                                                  BinOp.lt (|
                                                                                    M.read (| d |),
                                                                                    Value.Integer
                                                                                      IntegerKind.U8
                                                                                      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: d < 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.read (| d |)
                                                              |)
                                                            ]
                                                          |)
                                                        |) in
                                                      let~ _ :=
                                                        M.alloc (|
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.path "core::num::bignum::Big32x40",
                                                              "mul_small",
                                                              []
                                                            |),
                                                            [ mant; Value.Integer IntegerKind.U32 10
                                                            ]
                                                          |)
                                                        |) in
                                                      M.alloc (| Value.Tuple [] |)))
                                                ]
                                              |) in
                                            M.alloc (| Value.Tuple [] |)))
                                        |)))
                                  ]
                                |))));
                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                        ]
                      |) in
                    let~ order :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::cmp::Ord",
                            Ty.path "core::num::bignum::Big32x40",
                            [],
                            "cmp",
                            []
                          |),
                          [
                            mant;
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::num::bignum::Big32x40",
                                "mul_small",
                                []
                              |),
                              [ scale; Value.Integer IntegerKind.U32 5 ]
                            |)
                          ]
                        |)
                      |) in
                    let~ _ :=
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.use
                                  (M.alloc (|
                                    LogicalOp.or (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::cmp::PartialEq",
                                          Ty.path "core::cmp::Ordering",
                                          [ Ty.path "core::cmp::Ordering" ],
                                          "eq",
                                          []
                                        |),
                                        [
                                          order;
                                          M.alloc (|
                                            Value.StructTuple "core::cmp::Ordering::Greater" []
                                          |)
                                        ]
                                      |),
                                      ltac:(M.monadic
                                        (LogicalOp.and (|
                                          LogicalOp.and (|
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::cmp::PartialEq",
                                                Ty.path "core::cmp::Ordering",
                                                [ Ty.path "core::cmp::Ordering" ],
                                                "eq",
                                                []
                                              |),
                                              [
                                                order;
                                                M.alloc (|
                                                  Value.StructTuple "core::cmp::Ordering::Equal" []
                                                |)
                                              ]
                                            |),
                                            ltac:(M.monadic
                                              (BinOp.gt (|
                                                M.read (| len |),
                                                Value.Integer IntegerKind.Usize 0
                                              |)))
                                          |),
                                          ltac:(M.monadic
                                            (BinOp.eq (|
                                              BinOp.bit_and
                                                (M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply
                                                      (Ty.path
                                                        "core::mem::maybe_uninit::MaybeUninit")
                                                      []
                                                      [ Ty.path "u8" ],
                                                    "assume_init",
                                                    []
                                                  |),
                                                  [
                                                    M.read (|
                                                      M.SubPointer.get_array_field (|
                                                        M.read (| buf |),
                                                        M.alloc (|
                                                          BinOp.Wrap.sub (|
                                                            M.read (| len |),
                                                            Value.Integer IntegerKind.Usize 1
                                                          |)
                                                        |)
                                                      |)
                                                    |)
                                                  ]
                                                |))
                                                (Value.Integer IntegerKind.U8 1),
                                              Value.Integer IntegerKind.U8 1
                                            |)))
                                        |)))
                                    |)
                                  |)) 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.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 β := k 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 (| k |),
                                                        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 [] |)))
                                ]
                              |)));
                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                        ]
                      |) in
                    M.alloc (|
                      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 (| k |)
                        ]
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Function_format_exact :
          M.IsFunction "core::num::flt2dec::strategy::dragon::format_exact" format_exact.
      End dragon.
    End strategy.
  End flt2dec.
End num.
