Talos · verification report
← all projects

float_trunc verified

rust: rust/float_trunc · lean: lean/Project/FloatTrunc · repo @ 52f92e873252 · leanprover/lean4:v4.32.0
1 / 3 exports have a proven spec
Exports
3
Specs
1
Verifications
1
Diagnostics
1

Formal specs

Project.FloatTrunc.Spec.FloatTruncSpec lean/Project/FloatTrunc/Spec.lean:152
1 proof

Informal spec

No informal description provided.

Formal statement

FloatTruncSpec : Prop :=

Proofs

Project.FloatTrunc.Spec.check_correct

Rust binding

check
fn check(x: f32)

References

  • rust-exported float_trunc::check

Exported functions

fn naive_trunc(x: f32) -> i32
fn sat_trunc(x: f32) -> i32

Program (Lean)

def «module» : Wasm.Module :=
{
  imports := [],
  funcs := [
    func0Def,
    func1Def,
    func2Def,
    func3Def,
    func4Def,
    func5Def,
    func6Def,
    func7Def,
    func8Def,
    func9Def,
    func10Def,
    func11Def,
    func12Def,
    func13Def,
    func14Def,
    func15Def,
    func16Def,
    func17Def,
    func18Def,
    func19Def,
    func20Def,
    func21Def,
    func22Def,
    func23Def,
    func24Def,
    func25Def,
    func26Def,
    func27Def,
    func28Def,
    func29Def,
    func30Def,
    func31Def,
    func32Def,
    func33Def,
    func34Def,
    func35Def,
    func36Def,
    func37Def,
    func38Def,
    func39Def,
    func40Def,
    func41Def,
    func42Def,
    func43Def,
    func44Def,
    func45Def,
    func46Def,
    func47Def,
    func48Def,
    func49Def,
    func50Def,
    func51Def,
    func52Def,
    func53Def,
    func54Def
  ],
  exports := [
    { name := "check", funcIdx := 2 }
  ],
  memory := some { pagesMin := (17 : UInt32), pagesMax := none, data := [
    { offset := some (1048576 : UInt32), bytes := [(105 : UInt8), (110 : UInt8), (116 : UInt8), (101 : UInt8), (114 : UInt8), (110 : UInt8), (97 : UInt8), (108 : UInt8), (32 : UInt8), (101 : UInt8), (114 : UInt8), (114 : UInt8), (111 : UInt8), (114 : UInt8), (58 : UInt8), (32 : UInt8), (101 : UInt8), (110 : UInt8), (116 : UInt8), (101 : UInt8), (114 : UInt8), (101 : UInt8), (100 : UInt8), (32 : UInt8), (117 : UInt8), (110 : UInt8), (114 : UInt8), (101 : UInt8), (97 : UInt8), (99 : UInt8), (104 : UInt8), (97 : UInt8), (98 : UInt8), (108 : UInt8), (101 : UInt8), (32 : UInt8), (99 : UInt8), (111 : UInt8), (100 : UInt8), (101 : UInt8), (102 : UInt8), (108 : UInt8), (111 : UInt8), (97 : UInt8), (116 : UInt8), (95 : UInt8), (116 : UInt8), (114 : UInt8), (117 : UInt8), (110 : UInt8), (99 : UInt8), (47 : UInt8), (115 : UInt8), (114 : UInt8), (99 : UInt8), (47 : UInt8), (101 : UInt8), (120 : UInt8), (112 : UInt8), (111 : UInt8), (114 : UInt8), (116 : UInt8), (115 : UInt8), (46 : UInt8), (114 : UInt8), (115 : UInt8), (0 : UInt8), (0 : UInt8), (40 : UInt8), (0 : UInt8), (16 : UInt8), (0 : UInt8), (26 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (20 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (9 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (2 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (12 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (4 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (3 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (4 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (5 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (8 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (4 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (6 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (7 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (8 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (9 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (10 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (16 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (4 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (11 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (12 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (13 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (14 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (109 : UInt8), (93 : UInt8), (203 : UInt8), (214 : UInt8), (44 : UInt8), (80 : UInt8), (235 : UInt8), (99 : UInt8), (120 : UInt8), (65 : UInt8), (166 : UInt8), (87 : UInt8), (113 : UInt8), (27 : UInt8), (139 : UInt8), (185 : UInt8), (21 : UInt8), (162 : UInt8), (92 : UInt8), (85 : UInt8), (52 : UInt8), (85 : UInt8), (7 : UInt8), (212 : UInt8), (83 : UInt8), (120 : UInt8), (173 : UInt8), (129 : UInt8), (81 : UInt8), (240 : UInt8), (163 : UInt8), (247 : UInt8), (47 : UInt8), (114 : UInt8), (117 : UInt8), (115 : UInt8), (116 : UInt8), (47 : UInt8), (100 : UInt8), (101 : UInt8), (112 : UInt8), (115 : UInt8), (47 : UInt8), (100 : UInt8), (108 : UInt8), (109 : UInt8), (97 : UInt8), (108 : UInt8), (108 : UInt8), (111 : UInt8), (99 : UInt8), (45 : UInt8), (48 : UInt8), (46 : UInt8), (50 : UInt8), (46 : UInt8), (49 : UInt8), (49 : UInt8), (47 : UInt8), (115 : UInt8), (114 : UInt8), (99 : UInt8), (47 : UInt8), (100 : UInt8), (108 : UInt8), (109 : UInt8), (97 : UInt8), (108 : UInt8), (108 : UInt8), (111 : UInt8), (99 : UInt8), (46 : UInt8), (114 : UInt8), (115 : UInt8), (0 : UInt8), (97 : UInt8), (115 : UInt8), (115 : UInt8), (101 : UInt8), (114 : UInt8), (116 : UInt8), (105 : UInt8), (111 : UInt8), (110 : UInt8), (32 : UInt8), (102 : UInt8), (97 : UInt8), (105 : UInt8), (108 : UInt8), (101 : UInt8), (100 : UInt8), (58 : UInt8), (32 : UInt8), (112 : UInt8), (115 : UInt8), (105 : UInt8), (122 : UInt8), (101 : UInt8), (32 : UInt8), (62 : UInt8), (61 : UInt8), (32 : UInt8), (115 : UInt8), (105 : UInt8), (122 : UInt8), (101 : UInt8), (32 : UInt8), (43 : UInt8), (32 : UInt8), (109 : UInt8), (105 : UInt8), (110 : UInt8), (95 : UInt8), (111 : UInt8), (118 : UInt8), (101 : UInt8), (114 : UInt8), (104 : UInt8), (101 : UInt8), (97 : UInt8), (100 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (196 : UInt8), (0 : UInt8), (16 : UInt8), (0 : UInt8), (42 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (177 : UInt8), (4 : UInt8), (0 : UInt8), (0 : UInt8), (9 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (97 : UInt8), (115 : UInt8), (115 : UInt8), (101 : UInt8), (114 : UInt8), (116 : UInt8), (105 : UInt8), (111 : UInt8), (110 : UInt8), (32 : UInt8), (102 : UInt8), (97 : UInt8), (105 : UInt8), (108 : UInt8), (101 : UInt8), (100 : UInt8), (58 : UInt8), (32 : UInt8), (112 : UInt8), (115 : UInt8), (105 : UInt8), (122 : UInt8), (101 : UInt8), (32 : UInt8), (60 : UInt8), (61 : UInt8), (32 : UInt8), (115 : UInt8), (105 : UInt8), (122 : UInt8), (101 : UInt8), (32 : UInt8), (43 : UInt8), (32 : UInt8), (109 : UInt8), (97 : UInt8), (120 : UInt8), (95 : UInt8), (111 : UInt8), (118 : UInt8), (101 : UInt8), (114 : UInt8), (104 : UInt8), (101 : UInt8), (97 : UInt8), (100 : UInt8), (0 : UInt8), (0 : UInt8), (196 : UInt8), (0 : UInt8), (16 : UInt8), (0 : UInt8), (42 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (183 : UInt8), (4 : UInt8), (0 : UInt8), (0 : UInt8), (13 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (8 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (4 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (15 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (2 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (12 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (4 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (16 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (47 : UInt8), (114 : UInt8), (117 : UInt8), (115 : UInt8), (116 : UInt8), (99 : UInt8), (47 : UInt8), (53 : UInt8), (57 : UInt8), (56 : UInt8), (48 : UInt8), (55 : UInt8), (54 : UInt8), (49 : UInt8), (54 : UInt8), (101 : UInt8), (49 : UInt8), (102 : UInt8), (97 : UInt8), (50 : UInt8), (53 : UInt8), (52 : UInt8), (48 : UInt8), (55 : UInt8), (50 : UInt8), (52 : UInt8), (98 : UInt8), (102 : UInt8), (98 : UInt8), (97 : UInt8), (99 : UInt8), (49 : UInt8), (52 : UInt8), (100 : UInt8), (55 : UInt8), (57 : UInt8), (55 : UInt8), (54 : UInt8), (100 : UInt8), (55 : UInt8), (101 : UInt8), (52 : UInt8), (97 : UInt8), (51 : UInt8), (56 : UInt8), (54 : UInt8), (48 : UInt8), (47 : UInt8), (108 : UInt8), (105 : UInt8), (98 : UInt8), (114 : UInt8), (97 : UInt8), (114 : UInt8), (121 : UInt8), (47 : UInt8), (97 : UInt8), (108 : UInt8), (108 : UInt8), (111 : UInt8), (99 : UInt8), (47 : UInt8), (115 : UInt8), (114 : UInt8), (99 : UInt8), (47 : UInt8), (114 : UInt8), (97 : UInt8), (119 : UInt8), (95 : UInt8), (118 : UInt8), (101 : UInt8), (99 : UInt8), (47 : UInt8), (109 : UInt8), (111 : UInt8), (100 : UInt8), (46 : UInt8), (114 : UInt8), (115 : UInt8), (0 : UInt8), (99 : UInt8), (97 : UInt8), (112 : UInt8), (97 : UInt8), (99 : UInt8), (105 : UInt8), (116 : UInt8), (121 : UInt8), (32 : UInt8), (111 : UInt8), (118 : UInt8), (101 : UInt8), (114 : UInt8), (102 : UInt8), (108 : UInt8), (111 : UInt8), (119 : UInt8), (0 : UInt8), (0 : UInt8), (144 : UInt8), (1 : UInt8), (16 : UInt8), (0 : UInt8), (80 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (28 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (5 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8)] }
  ] },
  globals := [
    { init := .i32 (1048576 : UInt32) },
    { init := .i32 (1049573 : UInt32) },
    { init := .i32 (1049584 : UInt32) }
  ],
  types := [
    { params := [.i32, .i32], results := [] },
    { params := [.i32, .i32, .i32], results := [.i32] },
    { params := [.i32, .i32], results := [.i32] },
    { params := [.f32], results := [.i32] },
    { params := [.f32], results := [] },
    { params := [.i32, .i32, .i32], results := [] },
    { params := [.i32, .i32, .i32, .i32], results := [.i32] },
    { params := [], results := [] },
    { params := [.i32, .i32, .i32, .i32, .i32], results := [] },
    { params := [.i32], results := [] },
    { params := [.i32, .i32, .i32, .i32, .i32, .i32], results := [] },
    { params := [.i32], results := [.i32] }
  ],
  tables := [
    { min := 17, max := some 17, elemType := .funcref }
  ],
  elements := [
    { tableIdx := some 0, offset := some 1, funcs := [some 18, some 10, some 42, some 41, some 46, some 40, some 39, some 37, some 38, some 11, some 36, some 44, some 43, some 45, some 35, some 34] }
  ]
}

Diagnostics

missing_docstring info
lean/Project/FloatTrunc/Spec.lean:152
spec `Project.FloatTrunc.Spec.FloatTruncSpec` has no `/-- … -/` docstring

Source files (appendix)

Lean (2)

lean/Project/FloatTrunc/Program.lean lean · 5970 lines
/-
  AUTO-GENERATED by `verifier emit`. Do not edit by hand.
-/

import CodeLib

set_option maxRecDepth 1048576

namespace Project.FloatTrunc

open Wasm

def func0 : Wasm.Program :=
  [
  .globalGet 0,
  .const (16 : UInt32),
  .sub,
  .localSet 1,
  .block 0 0 [
    .block 0 0 [
      .block 0 0 [
        .block 0 0 [
          .block 0 0 [
            .block 0 0 [
              .localGet 0,
              .localGet 0,
              .f32Ne,
              .const (1 : UInt32),
              .and,
              .br_if 0,
              .localGet 0,
              .f32Const (1325400064 : UInt32),
              .f32Ge,
              .const (1 : UInt32),
              .and,
              .br_if 2,
              .br 1
            ],
            .localGet 1,
            .const (0 : UInt32),
            .store32 (12 : UInt32),
            .br 4
          ],
          .localGet 0,
          .f32Const (3472883712 : UInt32),
          .f32Lt,
          .const (1 : UInt32),
          .and,
          .br_if 2,
          .br 1
        ],
        .localGet 1,
        .const (2147483647 : UInt32),
        .store32 (12 : UInt32),
        .br 2
      ],
      .localGet 1,
      .localGet 0,
      .i32TruncSatF32S,
      .store32 (12 : UInt32),
      .br 1
    ],
    .localGet 1,
    .const (2147483648 : UInt32),
    .store32 (12 : UInt32)
  ],
  .localGet 1,
  .load32 (12 : UInt32),
  .ret
]

def func0Def : Wasm.Function :=
  { params := [.f32], locals := [.i32], body := func0, results := [.i32] }

def func1 : Wasm.Program :=
  [
  .localGet 0,
  .i32TruncSatF32S,
  .ret
]

def func1Def : Wasm.Function :=
  { params := [.f32], locals := [], body := func1, results := [.i32] }

/-- export: check -/
def func2 : Wasm.Program :=
  [
  .block 0 0 [
    .localGet 0,
    .call 0,
    .localGet 0,
    .call 1,
    .ne,
    .const (1 : UInt32),
    .and,
    .br_if 0,
    .ret
  ],
  .const (1048576 : UInt32),
  .const (40 : UInt32),
  .const (1048644 : UInt32),
  .call 51,
  .unreachable
]

def func2Def : Wasm.Function :=
  { params := [.f32], locals := [], body := func2, results := [] }

def func3 : Wasm.Program :=
  [
  .localGet 0,
  .localGet 1,
  .call 20,
  .ret
]

def func3Def : Wasm.Function :=
  { params := [.i32, .i32], locals := [], body := func3, results := [.i32] }

def func4 : Wasm.Program :=
  [
  .localGet 0,
  .localGet 1,
  .localGet 2,
  .call 24,
  .ret
]

def func4Def : Wasm.Function :=
  { params := [.i32, .i32, .i32], locals := [], body := func4, results := [] }

def func5 : Wasm.Program :=
  [
  .localGet 0,
  .localGet 1,
  .localGet 2,
  .localGet 3,
  .call 26,
  .ret
]

def func5Def : Wasm.Function :=
  { params := [.i32, .i32, .i32, .i32], locals := [], body := func5, results := [.i32] }

def func6 : Wasm.Program :=
  [
  .ret
]

def func6Def : Wasm.Function :=
  { params := [], locals := [], body := func6, results := [] }

def func7 : Wasm.Program :=
  [
  .call 23,
  .unreachable
]

def func7Def : Wasm.Function :=
  { params := [.i32, .i32], locals := [], body := func7, results := [.i32] }

def func8 : Wasm.Program :=
  [
  .globalGet 0,
  .const (16 : UInt32),
  .sub,
  .localSet 5,
  .localGet 5,
  .globalSet 0,
  .block 0 0 [
    .localGet 2,
    .localGet 1,
    .add,
    .localSet 1,
    .localGet 1,
    .localGet 2,
    .geU,
    .br_if 0,
    .const (0 : UInt32),
    .const (0 : UInt32),
    .call 48,
    .unreachable
  ],
  .localGet 5,
  .const (4 : UInt32),
  .add,
  .localGet 0,
  .load32 (0 : UInt32),
  .localSet 2,
  .localGet 2,
  .localGet 0,
  .load32 (4 : UInt32),
  .localGet 1,
  .localGet 2,
  .const (1 : UInt32),
  .shl,
  .localSet 2,
  .localGet 2,
  .localGet 1,
  .localGet 2,
  .gtU,
  .select,
  .localSet 2,
  .localGet 2,
  .const (8 : UInt32),
  .const (4 : UInt32),
  .localGet 4,
  .const (1 : UInt32),
  .eq,
  .select,
  .localSet 1,
  .localGet 1,
  .localGet 2,
  .localGet 1,
  .gtU,
  .select,
  .localSet 2,
  .localGet 2,
  .localGet 3,
  .localGet 4,
  .call 16,
  .block 0 0 [
    .localGet 5,
    .load32 (4 : UInt32),
    .const (1 : UInt32),
    .ne,
    .br_if 0,
    .localGet 5,
    .load32 (8 : UInt32),
    .localGet 5,
    .load32 (12 : UInt32),
    .call 48,
    .unreachable
  ],
  .localGet 5,
  .load32 (8 : UInt32),
  .localSet 4,
  .localGet 0,
  .localGet 2,
  .store32 (0 : UInt32),
  .localGet 0,
  .localGet 4,
  .store32 (4 : UInt32),
  .localGet 5,
  .const (16 : UInt32),
  .add,
  .globalSet 0
]

def func8Def : Wasm.Function :=
  { params := [.i32, .i32, .i32, .i32, .i32], locals := [.i32], body := func8, results := [] }

def func9 : Wasm.Program :=
  [
  .block 0 0 [
    .localGet 0,
    .const (2147483648 : UInt32),
    .or,
    .const (2147483648 : UInt32),
    .eq,
    .br_if 0,
    .localGet 1,
    .localGet 0,
    .const (1 : UInt32),
    .call 4
  ]
]

def func9Def : Wasm.Function :=
  { params := [.i32, .i32], locals := [], body := func9, results := [] }

def func10 : Wasm.Program :=
  [
  .block 0 0 [
    .localGet 0,
    .load32 (0 : UInt32),
    .localSet 1,
    .localGet 1,
    .eqz,
    .br_if 0,
    .localGet 0,
    .load32 (4 : UInt32),
    .localGet 1,
    .const (1 : UInt32),
    .call 4
  ]
]

def func10Def : Wasm.Function :=
  { params := [.i32], locals := [.i32], body := func10, results := [] }

def func11 : Wasm.Program :=
  [
  .block 0 0 [
    .localGet 0,
    .load32 (0 : UInt32),
    .localSet 1,
    .localGet 1,
    .const (1 : UInt32),
    .ltS,
    .br_if 0,
    .localGet 0,
    .load32 (4 : UInt32),
    .localGet 1,
    .const (1 : UInt32),
    .call 4
  ]
]

def func11Def : Wasm.Function :=
  { params := [.i32], locals := [.i32], body := func11, results := [] }

def func12 : Wasm.Program :=
  [
  .localGet 0,
  .call 13,
  .unreachable
]

def func12Def : Wasm.Function :=
  { params := [.i32], locals := [], body := func12, results := [] }

def func13 : Wasm.Program :=
  [
  .localGet 0,
  .load32 (0 : UInt32),
  .localGet 0,
  .load32 (4 : UInt32),
  .const (0 : UInt32),
  .load32 (1049100 : UInt32),
  .localSet 0,
  .localGet 0,
  .const (1 : UInt32),
  .localGet 0,
  .select,
  .callIndirect 0 0,
  .unreachable
]

def func13Def : Wasm.Function :=
  { params := [.i32], locals := [], body := func13, results := [] }

def func14 : Wasm.Program :=
  [
  .localGet 0,
  .call 15,
  .unreachable
]

def func14Def : Wasm.Function :=
  { params := [.i32], locals := [], body := func14, results := [] }

def func15 : Wasm.Program :=
  [
  .globalGet 0,
  .const (16 : UInt32),
  .sub,
  .localSet 1,
  .localGet 1,
  .globalSet 0,
  .block 0 0 [
    .localGet 0,
    .load32 (0 : UInt32),
    .localSet 2,
    .localGet 2,
    .load32 (4 : UInt32),
    .localSet 3,
    .localGet 3,
    .const (1 : UInt32),
    .and,
    .eqz,
    .br_if 0,
    .localGet 2,
    .load32 (0 : UInt32),
    .localSet 2,
    .localGet 1,
    .localGet 3,
    .const (1 : UInt32),
    .shrU,
    .store32 (4 : UInt32),
    .localGet 1,
    .localGet 2,
    .store32 (0 : UInt32),
    .localGet 1,
    .const (1048684 : UInt32),
    .localGet 0,
    .load32 (4 : UInt32),
    .localGet 0,
    .load32 (8 : UInt32),
    .localSet 0,
    .localGet 0,
    .load8U (8 : UInt32),
    .localGet 0,
    .load8U (9 : UInt32),
    .call 17,
    .unreachable
  ],
  .localGet 1,
  .const (2147483648 : UInt32),
  .store32 (0 : UInt32),
  .localGet 1,
  .localGet 0,
  .store32 (12 : UInt32),
  .localGet 1,
  .const (1048712 : UInt32),
  .localGet 0,
  .load32 (4 : UInt32),
  .localGet 0,
  .load32 (8 : UInt32),
  .localSet 0,
  .localGet 0,
  .load8U (8 : UInt32),
  .localGet 0,
  .load8U (9 : UInt32),
  .call 17,
  .unreachable
]

def func15Def : Wasm.Function :=
  { params := [.i32], locals := [.i32, .i32, .i32], body := func15, results := [] }

def func16 : Wasm.Program :=
  [
  .const (1 : UInt32),
  .localSet 6,
  .const (4 : UInt32),
  .localSet 7,
  .block 0 0 [
    .block 0 0 [
      .localGet 5,
      .extendUI32,
      .localGet 3,
      .extendUI32,
      .mulI64,
      .localSet 8,
      .localGet 8,
      .constI64 (32 : UInt64),
      .shrUI64,
      .wrapI64,
      .eqz,
      .br_if 0,
      .const (0 : UInt32),
      .localSet 3,
      .br 1
    ],
    .block 0 0 [
      .localGet 8,
      .wrapI64,
      .localSet 3,
      .localGet 3,
      .const (2147483648 : UInt32),
      .localGet 4,
      .sub,
      .leU,
      .br_if 0,
      .const (0 : UInt32),
      .localSet 3,
      .br 1
    ],
    .block 0 0 [
      .block 0 0 [
        .block 0 0 [
          .block 0 0 [
            .localGet 1,
            .eqz,
            .br_if 0,
            .localGet 2,
            .localGet 5,
            .localGet 1,
            .mul,
            .localGet 4,
            .localGet 3,
            .call 5,
            .localSet 7,
            .br 1
          ],
          .block 0 0 [
            .localGet 3,
            .br_if 0,
            .localGet 4,
            .localSet 7,
            .br 2
          ],
          .call 6,
          .localGet 3,
          .localGet 4,
          .call 3,
          .localSet 7
        ],
        .localGet 7,
        .br_if 0,
        .localGet 0,
        .localGet 4,
        .store32 (4 : UInt32),
        .br 1
      ],
      .localGet 0,
      .localGet 7,
      .store32 (4 : UInt32),
      .const (0 : UInt32),
      .localSet 6
    ],
    .const (8 : UInt32),
    .localSet 7
  ],
  .localGet 0,
  .localGet 7,
  .add,
  .localGet 3,
  .store32 (0 : UInt32),
  .localGet 0,
  .localGet 6,
  .store32 (0 : UInt32)
]

def func16Def : Wasm.Function :=
  { params := [.i32, .i32, .i32, .i32, .i32, .i32], locals := [.i32, .i32, .i64], body := func16, results := [] }

def func17 : Wasm.Program :=
  [
  .globalGet 0,
  .const (32 : UInt32),
  .sub,
  .localSet 5,
  .localGet 5,
  .globalSet 0,
  .block 0 0 [
    .block 0 0 [
      .block 0 0 [
        .block 0 0 [
          .block 0 0 [
            .const (1 : UInt32),
            .call 33,
            .const (255 : UInt32),
            .and,
            .brTable [4, 1, 0] 1
          ],
          .const (0 : UInt32),
          .load32 (1049104 : UInt32),
          .localSet 6,
          .localGet 6,
          .const (4294967295 : UInt32),
          .leS,
          .br_if 3,
          .const (0 : UInt32),
          .localGet 6,
          .const (1 : UInt32),
          .add,
          .store32 (1049104 : UInt32),
          .const (0 : UInt32),
          .load32 (1049108 : UInt32),
          .eqz,
          .br_if 1,
          .localGet 5,
          .const (8 : UInt32),
          .add,
          .localGet 0,
          .localGet 1,
          .load32 (20 : UInt32),
          .callIndirect 0 0,
          .localGet 5,
          .localGet 4,
          .store8 (29 : UInt32),
          .localGet 5,
          .localGet 3,
          .store8 (28 : UInt32),
          .localGet 5,
          .localGet 2,
          .store32 (24 : UInt32),
          .localGet 5,
          .localGet 5,
          .load64 (8 : UInt32),
          .store64 (16 : UInt32),
          .const (0 : UInt32),
          .load32 (1049108 : UInt32),
          .localGet 5,
          .const (16 : UInt32),
          .add,
          .const (0 : UInt32),
          .load32 (1049112 : UInt32),
          .load32 (20 : UInt32),
          .callIndirect 0 0,
          .br 2
        ],
        .localGet 5,
        .localGet 0,
        .localGet 1,
        .load32 (24 : UInt32),
        .callIndirect 0 0,
        .br 2
      ],
      .const (2147483648 : UInt32),
      .localGet 5,
      .call 9
    ],
    .const (0 : UInt32),
    .const (0 : UInt32),
    .load32 (1049104 : UInt32),
    .const (4294967295 : UInt32),
    .add,
    .store32 (1049104 : UInt32),
    .const (0 : UInt32),
    .const (0 : UInt32),
    .store8 (1049096 : UInt32),
    .localGet 3,
    .eqz,
    .br_if 0,
    .localGet 0,
    .localGet 1,
    .call 19,
    .unreachable
  ],
  .unreachable
]

def func17Def : Wasm.Function :=
  { params := [.i32, .i32, .i32, .i32, .i32], locals := [.i32, .i32], body := func17, results := [] }

def func18 : Wasm.Program :=
  [
  .const (0 : UInt32),
  .const (1 : UInt32),
  .store8 (1049572 : UInt32)
]

def func18Def : Wasm.Function :=
  { params := [.i32, .i32], locals := [], body := func18, results := [] }

def func19 : Wasm.Program :=
  [
  .localGet 0,
  .localGet 1,
  .call 7,
  .drop,
  .unreachable
]

def func19Def : Wasm.Function :=
  { params := [.i32, .i32], locals := [], body := func19, results := [] }

def func20 : Wasm.Program :=
  [
  .block 0 0 [
    .localGet 1,
    .const (9 : UInt32),
    .ltU,
    .br_if 0,
    .localGet 1,
    .localGet 0,
    .call 21,
    .ret
  ],
  .localGet 0,
  .call 22
]

def func20Def : Wasm.Function :=
  { params := [.i32, .i32], locals := [], body := func20, results := [.i32] }

def func21 : Wasm.Program :=
  [
  .const (0 : UInt32),
  .localSet 2,
  .block 0 0 [
    .localGet 1,
    .const (4294901709 : UInt32),
    .localGet 0,
    .const (16 : UInt32),
    .localGet 0,
    .const (16 : UInt32),
    .gtU,
    .select,
    .localSet 0,
    .localGet 0,
    .sub,
    .geU,
    .br_if 0,
    .localGet 0,
    .const (16 : UInt32),
    .localGet 1,
    .const (11 : UInt32),
    .add,
    .const (4294967288 : UInt32),
    .and,
    .localGet 1,
    .const (11 : UInt32),
    .ltU,
    .select,
    .localSet 3,
    .localGet 3,
    .add,
    .const (12 : UInt32),
    .add,
    .call 22,
    .localSet 1,
    .localGet 1,
    .eqz,
    .br_if 0,
    .localGet 1,
    .const (4294967288 : UInt32),
    .add,
    .localSet 2,
    .block 0 0 [
      .block 0 0 [
        .localGet 0,
        .const (4294967295 : UInt32),
        .add,
        .localSet 4,
        .localGet 4,
        .localGet 1,
        .and,
        .br_if 0,
        .localGet 2,
        .localSet 0,
        .br 1
      ],
      .localGet 1,
      .const (4294967292 : UInt32),
      .add,
      .localSet 5,
      .localGet 5,
      .load32 (0 : UInt32),
      .localSet 6,
      .localGet 6,
      .const (4294967288 : UInt32),
      .and,
      .localGet 4,
      .localGet 1,
      .add,
      .const (0 : UInt32),
      .localGet 0,
      .sub,
      .and,
      .const (4294967288 : UInt32),
      .add,
      .localSet 1,
      .localGet 1,
      .const (0 : UInt32),
      .localGet 0,
      .localGet 1,
      .localGet 2,
      .sub,
      .const (16 : UInt32),
      .gtU,
      .select,
      .add,
      .localSet 0,
      .localGet 0,
      .localGet 2,
      .sub,
      .localSet 1,
      .localGet 1,
      .sub,
      .localSet 4,
      .block 0 0 [
        .localGet 6,
        .const (3 : UInt32),
        .and,
        .eqz,
        .br_if 0,
        .localGet 0,
        .localGet 4,
        .localGet 0,
        .load32 (4 : UInt32),
        .const (1 : UInt32),
        .and,
        .or,
        .const (2 : UInt32),
        .or,
        .store32 (4 : UInt32),
        .localGet 0,
        .localGet 4,
        .add,
        .localSet 4,
        .localGet 4,
        .localGet 4,
        .load32 (4 : UInt32),
        .const (1 : UInt32),
        .or,
        .store32 (4 : UInt32),
        .localGet 5,
        .localGet 1,
        .localGet 5,
        .load32 (0 : UInt32),
        .const (1 : UInt32),
        .and,
        .or,
        .const (2 : UInt32),
        .or,
        .store32 (0 : UInt32),
        .localGet 2,
        .localGet 1,
        .add,
        .localSet 4,
        .localGet 4,
        .localGet 4,
        .load32 (4 : UInt32),
        .const (1 : UInt32),
        .or,
        .store32 (4 : UInt32),
        .localGet 2,
        .localGet 1,
        .call 28,
        .br 1
      ],
      .localGet 2,
      .load32 (0 : UInt32),
      .localSet 2,
      .localGet 0,
      .localGet 4,
      .store32 (4 : UInt32),
      .localGet 0,
      .localGet 2,
      .localGet 1,
      .add,
      .store32 (0 : UInt32)
    ],
    .block 0 0 [
      .localGet 0,
      .load32 (4 : UInt32),
      .localSet 1,
      .localGet 1,
      .const (3 : UInt32),
      .and,
      .eqz,
      .br_if 0,
      .localGet 1,
      .const (4294967288 : UInt32),
      .and,
      .localSet 2,
      .localGet 2,
      .localGet 3,
      .const (16 : UInt32),
      .add,
      .leU,
      .br_if 0,
      .localGet 0,
      .localGet 3,
      .localGet 1,
      .const (1 : UInt32),
      .and,
      .or,
      .const (2 : UInt32),
      .or,
      .store32 (4 : UInt32),
      .localGet 0,
      .localGet 3,
      .add,
      .localSet 1,
      .localGet 1,
      .localGet 2,
      .localGet 3,
      .sub,
      .localSet 3,
      .localGet 3,
      .const (3 : UInt32),
      .or,
      .store32 (4 : UInt32),
      .localGet 0,
      .localGet 2,
      .add,
      .localSet 2,
      .localGet 2,
      .localGet 2,
      .load32 (4 : UInt32),
      .const (1 : UInt32),
      .or,
      .store32 (4 : UInt32),
      .localGet 1,
      .localGet 3,
      .call 28
    ],
    .localGet 0,
    .const (8 : UInt32),
    .add,
    .localSet 2
  ],
  .localGet 2
]

def func21Def : Wasm.Function :=
  { params := [.i32, .i32], locals := [.i32, .i32, .i32, .i32, .i32], body := func21, results := [.i32] }

def func22 : Wasm.Program :=
  [
  .globalGet 0,
  .const (16 : UInt32),
  .sub,
  .localSet 1,
  .localGet 1,
  .globalSet 0,
  .block 0 0 [
    .block 0 0 [
      .block 0 0 [
        .block 0 0 [
          .localGet 0,
          .const (245 : UInt32),
          .ltU,
          .br_if 0,
          .block 0 0 [
            .localGet 0,
            .const (4294901708 : UInt32),
            .leU,
            .br_if 0,
            .const (0 : UInt32),
            .localSet 0,
            .br 4
          ],
          .localGet 0,
          .const (11 : UInt32),
          .add,
          .localSet 2,
          .localGet 2,
          .const (4294967288 : UInt32),
          .and,
          .localSet 3,
          .const (0 : UInt32),
          .load32 (1049532 : UInt32),
          .localSet 4,
          .localGet 4,
          .eqz,
          .br_if 2,
          .const (31 : UInt32),
          .localSet 5,
          .localGet 0,
          .const (16777205 : UInt32),
          .geU,
          .br_if 1,
          .localGet 3,
          .const (38 : UInt32),
          .localGet 2,
          .const (8 : UInt32),
          .shrU,
          .clz,
          .localSet 0,
          .localGet 0,
          .sub,
          .shrU,
          .const (1 : UInt32),
          .and,
          .localGet 0,
          .const (1 : UInt32),
          .shl,
          .sub,
          .const (62 : UInt32),
          .add,
          .localSet 5,
          .br 1
        ],
        .block 0 0 [
          .block 0 0 [
            .block 0 0 [
              .block 0 0 [
                .block 0 0 [
                  .block 0 0 [
                    .const (0 : UInt32),
                    .load32 (1049528 : UInt32),
                    .localSet 6,
                    .localGet 6,
                    .const (16 : UInt32),
                    .localGet 0,
                    .const (11 : UInt32),
                    .add,
                    .const (504 : UInt32),
                    .and,
                    .localGet 0,
                    .const (11 : UInt32),
                    .ltU,
                    .select,
                    .localSet 3,
                    .localGet 3,
                    .const (3 : UInt32),
                    .shrU,
                    .localSet 2,
                    .localGet 2,
                    .shrU,
                    .localSet 0,
                    .localGet 0,
                    .const (3 : UInt32),
                    .and,
                    .eqz,
                    .br_if 0,
                    .localGet 0,
                    .const (4294967295 : UInt32),
                    .xor,
                    .const (1 : UInt32),
                    .and,
                    .localGet 2,
                    .add,
                    .localSet 7,
                    .localGet 7,
                    .const (3 : UInt32),
                    .shl,
                    .localSet 3,
                    .localGet 3,
                    .const (1049264 : UInt32),
                    .add,
                    .localSet 0,
                    .localGet 0,
                    .localGet 3,
                    .const (1049272 : UInt32),
                    .add,
                    .load32 (0 : UInt32),
                    .localSet 2,
                    .localGet 2,
                    .load32 (8 : UInt32),
                    .localSet 8,
                    .localGet 8,
                    .eq,
                    .br_if 1,
                    .localGet 8,
                    .localGet 0,
                    .store32 (12 : UInt32),
                    .localGet 0,
                    .localGet 8,
                    .store32 (8 : UInt32),
                    .br 2
                  ],
                  .localGet 3,
                  .const (0 : UInt32),
                  .load32 (1049536 : UInt32),
                  .leU,
                  .br_if 6,
                  .localGet 0,
                  .br_if 2,
                  .const (0 : UInt32),
                  .load32 (1049532 : UInt32),
                  .localSet 0,
                  .localGet 0,
                  .eqz,
                  .br_if 6,
                  .localGet 0,
                  .ctz,
                  .const (2 : UInt32),
                  .shl,
                  .const (1049120 : UInt32),
                  .add,
                  .load32 (0 : UInt32),
                  .localSet 8,
                  .localGet 8,
                  .load32 (4 : UInt32),
                  .const (4294967288 : UInt32),
                  .and,
                  .localGet 3,
                  .sub,
                  .localSet 2,
                  .localGet 8,
                  .localSet 6,
                  .loop 0 0 [
                    .block 0 0 [
                      .localGet 8,
                      .load32 (16 : UInt32),
                      .localSet 0,
                      .localGet 0,
                      .br_if 0,
                      .localGet 8,
                      .load32 (20 : UInt32),
                      .localSet 0,
                      .localGet 0,
                      .br_if 0,
                      .localGet 6,
                      .load32 (24 : UInt32),
                      .localSet 5,
                      .block 0 0 [
                        .block 0 0 [
                          .block 0 0 [
                            .localGet 6,
                            .load32 (12 : UInt32),
                            .localSet 0,
                            .localGet 0,
                            .localGet 6,
                            .ne,
                            .br_if 0,
                            .localGet 6,
                            .const (20 : UInt32),
                            .const (16 : UInt32),
                            .localGet 6,
                            .load32 (20 : UInt32),
                            .localSet 0,
                            .localGet 0,
                            .select,
                            .add,
                            .load32 (0 : UInt32),
                            .localSet 8,
                            .localGet 8,
                            .br_if 1,
                            .const (0 : UInt32),
                            .localSet 0,
                            .br 2
                          ],
                          .localGet 6,
                          .load32 (8 : UInt32),
                          .localSet 8,
                          .localGet 8,
                          .localGet 0,
                          .store32 (12 : UInt32),
                          .localGet 0,
                          .localGet 8,
                          .store32 (8 : UInt32),
                          .br 1
                        ],
                        .localGet 6,
                        .const (20 : UInt32),
                        .add,
                        .localGet 6,
                        .const (16 : UInt32),
                        .add,
                        .localGet 0,
                        .select,
                        .localSet 7,
                        .loop 0 0 [
                          .localGet 7,
                          .localSet 9,
                          .localGet 8,
                          .localSet 0,
                          .localGet 0,
                          .const (20 : UInt32),
                          .add,
                          .localGet 0,
                          .const (16 : UInt32),
                          .add,
                          .localGet 0,
                          .load32 (20 : UInt32),
                          .localSet 8,
                          .localGet 8,
                          .select,
                          .localSet 7,
                          .localGet 0,
                          .const (20 : UInt32),
                          .const (16 : UInt32),
                          .localGet 8,
                          .select,
                          .add,
                          .load32 (0 : UInt32),
                          .localSet 8,
                          .localGet 8,
                          .br_if 0
                        ],
                        .localGet 9,
                        .const (0 : UInt32),
                        .store32 (0 : UInt32)
                      ],
                      .localGet 5,
                      .eqz,
                      .br_if 6,
                      .block 0 0 [
                        .block 0 0 [
                          .localGet 6,
                          .localGet 6,
                          .load32 (28 : UInt32),
                          .const (2 : UInt32),
                          .shl,
                          .const (1049120 : UInt32),
                          .add,
                          .localSet 8,
                          .localGet 8,
                          .load32 (0 : UInt32),
                          .eq,
                          .br_if 0,
                          .block 0 0 [
                            .localGet 5,
                            .load32 (16 : UInt32),
                            .localGet 6,
                            .eq,
                            .br_if 0,
                            .localGet 5,
                            .localGet 0,
                            .store32 (20 : UInt32),
                            .localGet 0,
                            .br_if 2,
                            .br 9
                          ],
                          .localGet 5,
                          .localGet 0,
                          .store32 (16 : UInt32),
                          .localGet 0,
                          .br_if 1,
                          .br 8
                        ],
                        .localGet 8,
                        .localGet 0,
                        .store32 (0 : UInt32),
                        .localGet 0,
                        .eqz,
                        .br_if 6
                      ],
                      .localGet 0,
                      .localGet 5,
                      .store32 (24 : UInt32),
                      .block 0 0 [
                        .localGet 6,
                        .load32 (16 : UInt32),
                        .localSet 8,
                        .localGet 8,
                        .eqz,
                        .br_if 0,
                        .localGet 0,
                        .localGet 8,
                        .store32 (16 : UInt32),
                        .localGet 8,
                        .localGet 0,
                        .store32 (24 : UInt32)
                      ],
                      .localGet 6,
                      .load32 (20 : UInt32),
                      .localSet 8,
                      .localGet 8,
                      .eqz,
                      .br_if 6,
                      .localGet 0,
                      .localGet 8,
                      .store32 (20 : UInt32),
                      .localGet 8,
                      .localGet 0,
                      .store32 (24 : UInt32),
                      .br 6
                    ],
                    .localGet 0,
                    .load32 (4 : UInt32),
                    .const (4294967288 : UInt32),
                    .and,
                    .localGet 3,
                    .sub,
                    .localSet 8,
                    .localGet 8,
                    .localGet 2,
                    .localGet 8,
                    .localGet 2,
                    .ltU,
                    .localSet 8,
                    .localGet 8,
                    .select,
                    .localSet 2,
                    .localGet 0,
                    .localGet 6,
                    .localGet 8,
                    .select,
                    .localSet 6,
                    .localGet 0,
                    .localSet 8,
                    .br 0
                  ]
                ],
                .const (0 : UInt32),
                .localGet 6,
                .const (4294967294 : UInt32),
                .localGet 7,
                .rotl,
                .and,
                .store32 (1049528 : UInt32)
              ],
              .localGet 2,
              .const (8 : UInt32),
              .add,
              .localSet 0,
              .localGet 2,
              .localGet 3,
              .const (3 : UInt32),
              .or,
              .store32 (4 : UInt32),
              .localGet 2,
              .localGet 3,
              .add,
              .localSet 3,
              .localGet 3,
              .localGet 3,
              .load32 (4 : UInt32),
              .const (1 : UInt32),
              .or,
              .store32 (4 : UInt32),
              .br 5
            ],
            .block 0 0 [
              .block 0 0 [
                .localGet 0,
                .localGet 2,
                .shl,
                .const (2 : UInt32),
                .localGet 2,
                .shl,
                .localSet 0,
                .localGet 0,
                .const (0 : UInt32),
                .localGet 0,
                .sub,
                .or,
                .and,
                .ctz,
                .localSet 9,
                .localGet 9,
                .const (3 : UInt32),
                .shl,
                .localSet 2,
                .localGet 2,
                .const (1049264 : UInt32),
                .add,
                .localSet 8,
                .localGet 8,
                .localGet 2,
                .const (1049272 : UInt32),
                .add,
                .load32 (0 : UInt32),
                .localSet 0,
                .localGet 0,
                .load32 (8 : UInt32),
                .localSet 7,
                .localGet 7,
                .eq,
                .br_if 0,
                .localGet 7,
                .localGet 8,
                .store32 (12 : UInt32),
                .localGet 8,
                .localGet 7,
                .store32 (8 : UInt32),
                .br 1
              ],
              .const (0 : UInt32),
              .localGet 6,
              .const (4294967294 : UInt32),
              .localGet 9,
              .rotl,
              .and,
              .store32 (1049528 : UInt32)
            ],
            .localGet 0,
            .localGet 3,
            .const (3 : UInt32),
            .or,
            .store32 (4 : UInt32),
            .localGet 0,
            .localGet 3,
            .add,
            .localSet 6,
            .localGet 6,
            .localGet 2,
            .localGet 3,
            .sub,
            .localSet 8,
            .localGet 8,
            .const (1 : UInt32),
            .or,
            .store32 (4 : UInt32),
            .localGet 0,
            .localGet 2,
            .add,
            .localGet 8,
            .store32 (0 : UInt32),
            .block 0 0 [
              .const (0 : UInt32),
              .load32 (1049536 : UInt32),
              .localSet 2,
              .localGet 2,
              .eqz,
              .br_if 0,
              .const (0 : UInt32),
              .load32 (1049544 : UInt32),
              .localSet 3,
              .block 0 0 [
                .block 0 0 [
                  .const (0 : UInt32),
                  .load32 (1049528 : UInt32),
                  .localSet 7,
                  .localGet 7,
                  .const (1 : UInt32),
                  .localGet 2,
                  .const (3 : UInt32),
                  .shrU,
                  .shl,
                  .localSet 9,
                  .localGet 9,
                  .and,
                  .br_if 0,
                  .const (0 : UInt32),
                  .localGet 7,
                  .localGet 9,
                  .or,
                  .store32 (1049528 : UInt32),
                  .localGet 2,
                  .const (4294967288 : UInt32),
                  .and,
                  .const (1049264 : UInt32),
                  .add,
                  .localSet 2,
                  .localGet 2,
                  .localSet 7,
                  .br 1
                ],
                .localGet 2,
                .const (4294967288 : UInt32),
                .and,
                .localSet 2,
                .localGet 2,
                .const (1049264 : UInt32),
                .add,
                .localSet 7,
                .localGet 2,
                .const (1049272 : UInt32),
                .add,
                .load32 (0 : UInt32),
                .localSet 2
              ],
              .localGet 7,
              .localGet 3,
              .store32 (8 : UInt32),
              .localGet 2,
              .localGet 3,
              .store32 (12 : UInt32),
              .localGet 3,
              .localGet 7,
              .store32 (12 : UInt32),
              .localGet 3,
              .localGet 2,
              .store32 (8 : UInt32)
            ],
            .localGet 0,
            .const (8 : UInt32),
            .add,
            .localSet 0,
            .const (0 : UInt32),
            .localGet 6,
            .store32 (1049544 : UInt32),
            .const (0 : UInt32),
            .localGet 8,
            .store32 (1049536 : UInt32),
            .br 4
          ],
          .const (0 : UInt32),
          .const (0 : UInt32),
          .load32 (1049532 : UInt32),
          .const (4294967294 : UInt32),
          .localGet 6,
          .load32 (28 : UInt32),
          .rotl,
          .and,
          .store32 (1049532 : UInt32)
        ],
        .block 0 0 [
          .block 0 0 [
            .block 0 0 [
              .localGet 2,
              .const (16 : UInt32),
              .ltU,
              .br_if 0,
              .localGet 6,
              .localGet 3,
              .const (3 : UInt32),
              .or,
              .store32 (4 : UInt32),
              .localGet 6,
              .localGet 3,
              .add,
              .localSet 8,
              .localGet 8,
              .localGet 2,
              .const (1 : UInt32),
              .or,
              .store32 (4 : UInt32),
              .localGet 8,
              .localGet 2,
              .add,
              .localGet 2,
              .store32 (0 : UInt32),
              .const (0 : UInt32),
              .load32 (1049536 : UInt32),
              .localSet 7,
              .localGet 7,
              .eqz,
              .br_if 1,
              .const (0 : UInt32),
              .load32 (1049544 : UInt32),
              .localSet 0,
              .block 0 0 [
                .block 0 0 [
                  .const (0 : UInt32),
                  .load32 (1049528 : UInt32),
                  .localSet 9,
                  .localGet 9,
                  .const (1 : UInt32),
                  .localGet 7,
                  .const (3 : UInt32),
                  .shrU,
                  .shl,
                  .localSet 5,
                  .localGet 5,
                  .and,
                  .br_if 0,
                  .const (0 : UInt32),
                  .localGet 9,
                  .localGet 5,
                  .or,
                  .store32 (1049528 : UInt32),
                  .localGet 7,
                  .const (4294967288 : UInt32),
                  .and,
                  .const (1049264 : UInt32),
                  .add,
                  .localSet 7,
                  .localGet 7,
                  .localSet 9,
                  .br 1
                ],
                .localGet 7,
                .const (4294967288 : UInt32),
                .and,
                .localSet 7,
                .localGet 7,
                .const (1049264 : UInt32),
                .add,
                .localSet 9,
                .localGet 7,
                .const (1049272 : UInt32),
                .add,
                .load32 (0 : UInt32),
                .localSet 7
              ],
              .localGet 9,
              .localGet 0,
              .store32 (8 : UInt32),
              .localGet 7,
              .localGet 0,
              .store32 (12 : UInt32),
              .localGet 0,
              .localGet 9,
              .store32 (12 : UInt32),
              .localGet 0,
              .localGet 7,
              .store32 (8 : UInt32),
              .br 1
            ],
            .localGet 6,
            .localGet 2,
            .localGet 3,
            .add,
            .localSet 0,
            .localGet 0,
            .const (3 : UInt32),
            .or,
            .store32 (4 : UInt32),
            .localGet 6,
            .localGet 0,
            .add,
            .localSet 0,
            .localGet 0,
            .localGet 0,
            .load32 (4 : UInt32),
            .const (1 : UInt32),
            .or,
            .store32 (4 : UInt32),
            .br 1
          ],
          .const (0 : UInt32),
          .localGet 8,
          .store32 (1049544 : UInt32),
          .const (0 : UInt32),
          .localGet 2,
          .store32 (1049536 : UInt32)
        ],
        .localGet 6,
        .const (8 : UInt32),
        .add,
        .localSet 0,
        .localGet 0,
        .eqz,
        .br_if 1,
        .br 2
      ],
      .const (0 : UInt32),
      .localGet 3,
      .sub,
      .localSet 2,
      .block 0 0 [
        .block 0 0 [
          .block 0 0 [
            .block 0 0 [
              .localGet 5,
              .const (2 : UInt32),
              .shl,
              .const (1049120 : UInt32),
              .add,
              .load32 (0 : UInt32),
              .localSet 6,
              .localGet 6,
              .br_if 0,
              .const (0 : UInt32),
              .localSet 8,
              .const (0 : UInt32),
              .localSet 0,
              .br 1
            ],
            .const (0 : UInt32),
            .localSet 8,
            .localGet 3,
            .const (0 : UInt32),
            .const (25 : UInt32),
            .localGet 5,
            .const (1 : UInt32),
            .shrU,
            .sub,
            .localGet 5,
            .const (31 : UInt32),
            .eq,
            .select,
            .shl,
            .localSet 7,
            .const (0 : UInt32),
            .localSet 0,
            .loop 0 0 [
              .block 0 0 [
                .localGet 6,
                .localSet 6,
                .localGet 6,
                .load32 (4 : UInt32),
                .const (4294967288 : UInt32),
                .and,
                .localSet 9,
                .localGet 9,
                .localGet 3,
                .ltU,
                .br_if 0,
                .localGet 9,
                .localGet 3,
                .sub,
                .localSet 9,
                .localGet 9,
                .localGet 2,
                .geU,
                .br_if 0,
                .localGet 6,
                .localSet 8,
                .localGet 9,
                .localSet 2,
                .localGet 9,
                .br_if 0,
                .const (0 : UInt32),
                .localSet 2,
                .localGet 6,
                .localSet 0,
                .localGet 6,
                .localSet 8,
                .br 3
              ],
              .localGet 6,
              .load32 (20 : UInt32),
              .localSet 9,
              .localGet 9,
              .localGet 0,
              .localGet 9,
              .localGet 6,
              .localGet 7,
              .const (29 : UInt32),
              .shrU,
              .const (4 : UInt32),
              .and,
              .add,
              .load32 (16 : UInt32),
              .localSet 6,
              .localGet 6,
              .ne,
              .select,
              .localGet 0,
              .localGet 9,
              .select,
              .localSet 0,
              .localGet 7,
              .const (1 : UInt32),
              .shl,
              .localSet 7,
              .localGet 6,
              .br_if 0
            ]
          ],
          .block 0 0 [
            .localGet 0,
            .localGet 8,
            .or,
            .br_if 0,
            .const (0 : UInt32),
            .localSet 8,
            .const (2 : UInt32),
            .localGet 5,
            .shl,
            .localSet 0,
            .localGet 0,
            .const (0 : UInt32),
            .localGet 0,
            .sub,
            .or,
            .localGet 4,
            .and,
            .localSet 0,
            .localGet 0,
            .eqz,
            .br_if 3,
            .localGet 0,
            .ctz,
            .const (2 : UInt32),
            .shl,
            .const (1049120 : UInt32),
            .add,
            .load32 (0 : UInt32),
            .localSet 0
          ],
          .localGet 0,
          .eqz,
          .br_if 1
        ],
        .loop 0 0 [
          .localGet 0,
          .load32 (4 : UInt32),
          .const (4294967288 : UInt32),
          .and,
          .localSet 6,
          .localGet 6,
          .localGet 3,
          .sub,
          .localSet 7,
          .localGet 7,
          .localGet 2,
          .localGet 7,
          .localGet 2,
          .ltU,
          .localSet 9,
          .localGet 9,
          .select,
          .localSet 5,
          .localGet 6,
          .localGet 3,
          .ltU,
          .localSet 7,
          .localGet 0,
          .localGet 8,
          .localGet 9,
          .select,
          .localSet 9,
          .block 0 0 [
            .localGet 0,
            .load32 (16 : UInt32),
            .localSet 6,
            .localGet 6,
            .br_if 0,
            .localGet 0,
            .load32 (20 : UInt32),
            .localSet 6
          ],
          .localGet 2,
          .localGet 5,
          .localGet 7,
          .select,
          .localSet 2,
          .localGet 8,
          .localGet 9,
          .localGet 7,
          .select,
          .localSet 8,
          .localGet 6,
          .localSet 0,
          .localGet 6,
          .br_if 0
        ]
      ],
      .localGet 8,
      .eqz,
      .br_if 0,
      .block 0 0 [
        .const (0 : UInt32),
        .load32 (1049536 : UInt32),
        .localSet 0,
        .localGet 0,
        .localGet 3,
        .ltU,
        .br_if 0,
        .localGet 2,
        .localGet 0,
        .localGet 3,
        .sub,
        .geU,
        .br_if 1
      ],
      .localGet 8,
      .load32 (24 : UInt32),
      .localSet 5,
      .block 0 0 [
        .block 0 0 [
          .block 0 0 [
            .localGet 8,
            .load32 (12 : UInt32),
            .localSet 0,
            .localGet 0,
            .localGet 8,
            .ne,
            .br_if 0,
            .localGet 8,
            .const (20 : UInt32),
            .const (16 : UInt32),
            .localGet 8,
            .load32 (20 : UInt32),
            .localSet 0,
            .localGet 0,
            .select,
            .add,
            .load32 (0 : UInt32),
            .localSet 6,
            .localGet 6,
            .br_if 1,
            .const (0 : UInt32),
            .localSet 0,
            .br 2
          ],
          .localGet 8,
          .load32 (8 : UInt32),
          .localSet 6,
          .localGet 6,
          .localGet 0,
          .store32 (12 : UInt32),
          .localGet 0,
          .localGet 6,
          .store32 (8 : UInt32),
          .br 1
        ],
        .localGet 8,
        .const (20 : UInt32),
        .add,
        .localGet 8,
        .const (16 : UInt32),
        .add,
        .localGet 0,
        .select,
        .localSet 7,
        .loop 0 0 [
          .localGet 7,
          .localSet 9,
          .localGet 6,
          .localSet 0,
          .localGet 0,
          .const (20 : UInt32),
          .add,
          .localGet 0,
          .const (16 : UInt32),
          .add,
          .localGet 0,
          .load32 (20 : UInt32),
          .localSet 6,
          .localGet 6,
          .select,
          .localSet 7,
          .localGet 0,
          .const (20 : UInt32),
          .const (16 : UInt32),
          .localGet 6,
          .select,
          .add,
          .load32 (0 : UInt32),
          .localSet 6,
          .localGet 6,
          .br_if 0
        ],
        .localGet 9,
        .const (0 : UInt32),
        .store32 (0 : UInt32)
      ],
      .block 0 0 [
        .localGet 5,
        .eqz,
        .br_if 0,
        .block 0 0 [
          .block 0 0 [
            .block 0 0 [
              .localGet 8,
              .localGet 8,
              .load32 (28 : UInt32),
              .const (2 : UInt32),
              .shl,
              .const (1049120 : UInt32),
              .add,
              .localSet 6,
              .localGet 6,
              .load32 (0 : UInt32),
              .eq,
              .br_if 0,
              .block 0 0 [
                .localGet 5,
                .load32 (16 : UInt32),
                .localGet 8,
                .eq,
                .br_if 0,
                .localGet 5,
                .localGet 0,
                .store32 (20 : UInt32),
                .localGet 0,
                .br_if 2,
                .br 4
              ],
              .localGet 5,
              .localGet 0,
              .store32 (16 : UInt32),
              .localGet 0,
              .br_if 1,
              .br 3
            ],
            .localGet 6,
            .localGet 0,
            .store32 (0 : UInt32),
            .localGet 0,
            .eqz,
            .br_if 1
          ],
          .localGet 0,
          .localGet 5,
          .store32 (24 : UInt32),
          .block 0 0 [
            .localGet 8,
            .load32 (16 : UInt32),
            .localSet 6,
            .localGet 6,
            .eqz,
            .br_if 0,
            .localGet 0,
            .localGet 6,
            .store32 (16 : UInt32),
            .localGet 6,
            .localGet 0,
            .store32 (24 : UInt32)
          ],
          .localGet 8,
          .load32 (20 : UInt32),
          .localSet 6,
          .localGet 6,
          .eqz,
          .br_if 1,
          .localGet 0,
          .localGet 6,
          .store32 (20 : UInt32),
          .localGet 6,
          .localGet 0,
          .store32 (24 : UInt32),
          .br 1
        ],
        .const (0 : UInt32),
        .const (0 : UInt32),
        .load32 (1049532 : UInt32),
        .const (4294967294 : UInt32),
        .localGet 8,
        .load32 (28 : UInt32),
        .rotl,
        .and,
        .store32 (1049532 : UInt32)
      ],
      .block 0 0 [
        .block 0 0 [
          .localGet 2,
          .const (16 : UInt32),
          .ltU,
          .br_if 0,
          .localGet 8,
          .localGet 3,
          .const (3 : UInt32),
          .or,
          .store32 (4 : UInt32),
          .localGet 8,
          .localGet 3,
          .add,
          .localSet 0,
          .localGet 0,
          .localGet 2,
          .const (1 : UInt32),
          .or,
          .store32 (4 : UInt32),
          .localGet 0,
          .localGet 2,
          .add,
          .localGet 2,
          .store32 (0 : UInt32),
          .block 0 0 [
            .localGet 2,
            .const (256 : UInt32),
            .ltU,
            .br_if 0,
            .localGet 0,
            .localGet 2,
            .call 32,
            .br 2
          ],
          .block 0 0 [
            .block 0 0 [
              .const (0 : UInt32),
              .load32 (1049528 : UInt32),
              .localSet 6,
              .localGet 6,
              .const (1 : UInt32),
              .localGet 2,
              .const (3 : UInt32),
              .shrU,
              .shl,
              .localSet 7,
              .localGet 7,
              .and,
              .br_if 0,
              .const (0 : UInt32),
              .localGet 6,
              .localGet 7,
              .or,
              .store32 (1049528 : UInt32),
              .localGet 2,
              .const (248 : UInt32),
              .and,
              .const (1049264 : UInt32),
              .add,
              .localSet 2,
              .localGet 2,
              .localSet 6,
              .br 1
            ],
            .localGet 2,
            .const (248 : UInt32),
            .and,
            .localSet 2,
            .localGet 2,
            .const (1049264 : UInt32),
            .add,
            .localSet 6,
            .localGet 2,
            .const (1049272 : UInt32),
            .add,
            .load32 (0 : UInt32),
            .localSet 2
          ],
          .localGet 6,
          .localGet 0,
          .store32 (8 : UInt32),
          .localGet 2,
          .localGet 0,
          .store32 (12 : UInt32),
          .localGet 0,
          .localGet 6,
          .store32 (12 : UInt32),
          .localGet 0,
          .localGet 2,
          .store32 (8 : UInt32),
          .br 1
        ],
        .localGet 8,
        .localGet 2,
        .localGet 3,
        .add,
        .localSet 0,
        .localGet 0,
        .const (3 : UInt32),
        .or,
        .store32 (4 : UInt32),
        .localGet 8,
        .localGet 0,
        .add,
        .localSet 0,
        .localGet 0,
        .localGet 0,
        .load32 (4 : UInt32),
        .const (1 : UInt32),
        .or,
        .store32 (4 : UInt32)
      ],
      .localGet 8,
      .const (8 : UInt32),
      .add,
      .localSet 0,
      .localGet 0,
      .br_if 1
    ],
    .block 0 0 [
      .block 0 0 [
        .block 0 0 [
          .block 0 0 [
            .block 0 0 [
              .block 0 0 [
                .const (0 : UInt32),
                .load32 (1049536 : UInt32),
                .localSet 0,
                .localGet 0,
                .localGet 3,
                .geU,
                .br_if 0,
                .block 0 0 [
                  .const (0 : UInt32),
                  .load32 (1049540 : UInt32),
                  .localSet 0,
                  .localGet 0,
                  .localGet 3,
                  .gtU,
                  .br_if 0,
                  .localGet 1,
                  .const (4 : UInt32),
                  .add,
                  .const (1049572 : UInt32),
                  .localGet 3,
                  .const (65583 : UInt32),
                  .add,
                  .const (4294901760 : UInt32),
                  .and,
                  .call 47,
                  .block 0 0 [
                    .localGet 1,
                    .load32 (4 : UInt32),
                    .localSet 6,
                    .localGet 6,
                    .br_if 0,
                    .const (0 : UInt32),
                    .localSet 0,
                    .br 8
                  ],
                  .localGet 1,
                  .load32 (12 : UInt32),
                  .localSet 5,
                  .const (0 : UInt32),
                  .const (0 : UInt32),
                  .load32 (1049552 : UInt32),
                  .localGet 1,
                  .load32 (8 : UInt32),
                  .localSet 9,
                  .localGet 9,
                  .add,
                  .localSet 0,
                  .localGet 0,
                  .store32 (1049552 : UInt32),
                  .const (0 : UInt32),
                  .localGet 0,
                  .const (0 : UInt32),
                  .load32 (1049556 : UInt32),
                  .localSet 2,
                  .localGet 2,
                  .localGet 0,
                  .localGet 2,
                  .gtU,
                  .select,
                  .store32 (1049556 : UInt32),
                  .block 0 0 [
                    .block 0 0 [
                      .block 0 0 [
                        .const (0 : UInt32),
                        .load32 (1049548 : UInt32),
                        .localSet 2,
                        .localGet 2,
                        .eqz,
                        .br_if 0,
                        .const (1049248 : UInt32),
                        .localSet 0,
                        .loop 0 0 [
                          .localGet 6,
                          .localGet 0,
                          .load32 (0 : UInt32),
                          .localSet 8,
                          .localGet 8,
                          .localGet 0,
                          .load32 (4 : UInt32),
                          .localSet 7,
                          .localGet 7,
                          .add,
                          .eq,
                          .br_if 2,
                          .localGet 0,
                          .load32 (8 : UInt32),
                          .localSet 0,
                          .localGet 0,
                          .br_if 0,
                          .br 3
                        ]
                      ],
                      .block 0 0 [
                        .block 0 0 [
                          .const (0 : UInt32),
                          .load32 (1049564 : UInt32),
                          .localSet 0,
                          .localGet 0,
                          .eqz,
                          .br_if 0,
                          .localGet 6,
                          .localGet 0,
                          .geU,
                          .br_if 1
                        ],
                        .const (0 : UInt32),
                        .localGet 6,
                        .store32 (1049564 : UInt32)
                      ],
                      .const (0 : UInt32),
                      .const (4095 : UInt32),
                      .store32 (1049568 : UInt32),
                      .const (0 : UInt32),
                      .localGet 5,
                      .store32 (1049260 : UInt32),
                      .const (0 : UInt32),
                      .localGet 9,
                      .store32 (1049252 : UInt32),
                      .const (0 : UInt32),
                      .localGet 6,
                      .store32 (1049248 : UInt32),
                      .const (0 : UInt32),
                      .const (1049264 : UInt32),
                      .store32 (1049276 : UInt32),
                      .const (0 : UInt32),
                      .const (1049272 : UInt32),
                      .store32 (1049284 : UInt32),
                      .const (0 : UInt32),
                      .const (1049264 : UInt32),
                      .store32 (1049272 : UInt32),
                      .const (0 : UInt32),
                      .const (1049280 : UInt32),
                      .store32 (1049292 : UInt32),
                      .const (0 : UInt32),
                      .const (1049272 : UInt32),
                      .store32 (1049280 : UInt32),
                      .const (0 : UInt32),
                      .const (1049288 : UInt32),
                      .store32 (1049300 : UInt32),
                      .const (0 : UInt32),
                      .const (1049280 : UInt32),
                      .store32 (1049288 : UInt32),
                      .const (0 : UInt32),
                      .const (1049296 : UInt32),
                      .store32 (1049308 : UInt32),
                      .const (0 : UInt32),
                      .const (1049288 : UInt32),
                      .store32 (1049296 : UInt32),
                      .const (0 : UInt32),
                      .const (1049304 : UInt32),
                      .store32 (1049316 : UInt32),
                      .const (0 : UInt32),
                      .const (1049296 : UInt32),
                      .store32 (1049304 : UInt32),
                      .const (0 : UInt32),
                      .const (1049312 : UInt32),
                      .store32 (1049324 : UInt32),
                      .const (0 : UInt32),
                      .const (1049304 : UInt32),
                      .store32 (1049312 : UInt32),
                      .const (0 : UInt32),
                      .const (1049320 : UInt32),
                      .store32 (1049332 : UInt32),
                      .const (0 : UInt32),
                      .const (1049312 : UInt32),
                      .store32 (1049320 : UInt32),
                      .const (0 : UInt32),
                      .const (1049328 : UInt32),
                      .store32 (1049340 : UInt32),
                      .const (0 : UInt32),
                      .const (1049320 : UInt32),
                      .store32 (1049328 : UInt32),
                      .const (0 : UInt32),
                      .const (1049328 : UInt32),
                      .store32 (1049336 : UInt32),
                      .const (0 : UInt32),
                      .const (1049336 : UInt32),
                      .store32 (1049348 : UInt32),
                      .const (0 : UInt32),
                      .const (1049336 : UInt32),
                      .store32 (1049344 : UInt32),
                      .const (0 : UInt32),
                      .const (1049344 : UInt32),
                      .store32 (1049356 : UInt32),
                      .const (0 : UInt32),
                      .const (1049344 : UInt32),
                      .store32 (1049352 : UInt32),
                      .const (0 : UInt32),
                      .const (1049352 : UInt32),
                      .store32 (1049364 : UInt32),
                      .const (0 : UInt32),
                      .const (1049352 : UInt32),
                      .store32 (1049360 : UInt32),
                      .const (0 : UInt32),
                      .const (1049360 : UInt32),
                      .store32 (1049372 : UInt32),
                      .const (0 : UInt32),
                      .const (1049360 : UInt32),
                      .store32 (1049368 : UInt32),
                      .const (0 : UInt32),
                      .const (1049368 : UInt32),
                      .store32 (1049380 : UInt32),
                      .const (0 : UInt32),
                      .const (1049368 : UInt32),
                      .store32 (1049376 : UInt32),
                      .const (0 : UInt32),
                      .const (1049376 : UInt32),
                      .store32 (1049388 : UInt32),
                      .const (0 : UInt32),
                      .const (1049376 : UInt32),
                      .store32 (1049384 : UInt32),
                      .const (0 : UInt32),
                      .const (1049384 : UInt32),
                      .store32 (1049396 : UInt32),
                      .const (0 : UInt32),
                      .const (1049384 : UInt32),
                      .store32 (1049392 : UInt32),
                      .const (0 : UInt32),
                      .const (1049392 : UInt32),
                      .store32 (1049404 : UInt32),
                      .const (0 : UInt32),
                      .const (1049400 : UInt32),
                      .store32 (1049412 : UInt32),
                      .const (0 : UInt32),
                      .const (1049392 : UInt32),
                      .store32 (1049400 : UInt32),
                      .const (0 : UInt32),
                      .const (1049408 : UInt32),
                      .store32 (1049420 : UInt32),
                      .const (0 : UInt32),
                      .const (1049400 : UInt32),
                      .store32 (1049408 : UInt32),
                      .const (0 : UInt32),
                      .const (1049416 : UInt32),
                      .store32 (1049428 : UInt32),
                      .const (0 : UInt32),
                      .const (1049408 : UInt32),
                      .store32 (1049416 : UInt32),
                      .const (0 : UInt32),
                      .const (1049424 : UInt32),
                      .store32 (1049436 : UInt32),
                      .const (0 : UInt32),
                      .const (1049416 : UInt32),
                      .store32 (1049424 : UInt32),
                      .const (0 : UInt32),
                      .const (1049432 : UInt32),
                      .store32 (1049444 : UInt32),
                      .const (0 : UInt32),
                      .const (1049424 : UInt32),
                      .store32 (1049432 : UInt32),
                      .const (0 : UInt32),
                      .const (1049440 : UInt32),
                      .store32 (1049452 : UInt32),
                      .const (0 : UInt32),
                      .const (1049432 : UInt32),
                      .store32 (1049440 : UInt32),
                      .const (0 : UInt32),
                      .const (1049448 : UInt32),
                      .store32 (1049460 : UInt32),
                      .const (0 : UInt32),
                      .const (1049440 : UInt32),
                      .store32 (1049448 : UInt32),
                      .const (0 : UInt32),
                      .const (1049456 : UInt32),
                      .store32 (1049468 : UInt32),
                      .const (0 : UInt32),
                      .const (1049448 : UInt32),
                      .store32 (1049456 : UInt32),
                      .const (0 : UInt32),
                      .const (1049464 : UInt32),
                      .store32 (1049476 : UInt32),
                      .const (0 : UInt32),
                      .const (1049456 : UInt32),
                      .store32 (1049464 : UInt32),
                      .const (0 : UInt32),
                      .const (1049472 : UInt32),
                      .store32 (1049484 : UInt32),
                      .const (0 : UInt32),
                      .const (1049464 : UInt32),
                      .store32 (1049472 : UInt32),
                      .const (0 : UInt32),
                      .const (1049480 : UInt32),
                      .store32 (1049492 : UInt32),
                      .const (0 : UInt32),
                      .const (1049472 : UInt32),
                      .store32 (1049480 : UInt32),
                      .const (0 : UInt32),
                      .const (1049488 : UInt32),
                      .store32 (1049500 : UInt32),
                      .const (0 : UInt32),
                      .const (1049480 : UInt32),
                      .store32 (1049488 : UInt32),
                      .const (0 : UInt32),
                      .const (1049496 : UInt32),
                      .store32 (1049508 : UInt32),
                      .const (0 : UInt32),
                      .const (1049488 : UInt32),
                      .store32 (1049496 : UInt32),
                      .const (0 : UInt32),
                      .const (1049504 : UInt32),
                      .store32 (1049516 : UInt32),
                      .const (0 : UInt32),
                      .const (1049496 : UInt32),
                      .store32 (1049504 : UInt32),
                      .const (0 : UInt32),
                      .const (1049512 : UInt32),
                      .store32 (1049524 : UInt32),
                      .const (0 : UInt32),
                      .const (1049504 : UInt32),
                      .store32 (1049512 : UInt32),
                      .const (0 : UInt32),
                      .localGet 6,
                      .const (15 : UInt32),
                      .add,
                      .const (4294967288 : UInt32),
                      .and,
                      .localSet 0,
                      .localGet 0,
                      .const (4294967288 : UInt32),
                      .add,
                      .localSet 2,
                      .localGet 2,
                      .store32 (1049548 : UInt32),
                      .const (0 : UInt32),
                      .const (1049512 : UInt32),
                      .store32 (1049520 : UInt32),
                      .const (0 : UInt32),
                      .localGet 6,
                      .localGet 0,
                      .sub,
                      .localGet 9,
                      .const (4294967256 : UInt32),
                      .add,
                      .localSet 0,
                      .localGet 0,
                      .add,
                      .const (8 : UInt32),
                      .add,
                      .localSet 8,
                      .localGet 8,
                      .store32 (1049540 : UInt32),
                      .localGet 2,
                      .localGet 8,
                      .const (1 : UInt32),
                      .or,
                      .store32 (4 : UInt32),
                      .localGet 6,
                      .localGet 0,
                      .add,
                      .const (40 : UInt32),
                      .store32 (4 : UInt32),
                      .const (0 : UInt32),
                      .const (2097152 : UInt32),
                      .store32 (1049560 : UInt32),
                      .br 8
                    ],
                    .localGet 2,
                    .localGet 6,
                    .geU,
                    .br_if 0,
                    .localGet 8,
                    .localGet 2,
                    .gtU,
                    .br_if 0,
                    .localGet 0,
                    .load32 (12 : UInt32),
                    .localSet 8,
                    .localGet 8,
                    .const (1 : UInt32),
                    .and,
                    .br_if 0,
                    .localGet 8,
                    .const (1 : UInt32),
                    .shrU,
                    .localGet 5,
                    .eq,
                    .br_if 3
                  ],
                  .const (0 : UInt32),
                  .const (0 : UInt32),
                  .load32 (1049564 : UInt32),
                  .localSet 0,
                  .localGet 0,
                  .localGet 6,
                  .localGet 0,
                  .localGet 6,
                  .ltU,
                  .select,
                  .store32 (1049564 : UInt32),
                  .localGet 6,
                  .localGet 9,
                  .add,
                  .localSet 8,
                  .const (1049248 : UInt32),
                  .localSet 0,
                  .block 0 0 [
                    .block 0 0 [
                      .block 0 0 [
                        .loop 0 0 [
                          .localGet 0,
                          .load32 (0 : UInt32),
                          .localSet 7,
                          .localGet 7,
                          .localGet 8,
                          .eq,
                          .br_if 1,
                          .localGet 0,
                          .load32 (8 : UInt32),
                          .localSet 0,
                          .localGet 0,
                          .br_if 0,
                          .br 2
                        ]
                      ],
                      .localGet 0,
                      .load32 (12 : UInt32),
                      .localSet 8,
                      .localGet 8,
                      .const (1 : UInt32),
                      .and,
                      .br_if 0,
                      .localGet 8,
                      .const (1 : UInt32),
                      .shrU,
                      .localGet 5,
                      .eq,
                      .br_if 1
                    ],
                    .const (1049248 : UInt32),
                    .localSet 0,
                    .block 0 0 [
                      .loop 0 0 [
                        .block 0 0 [
                          .localGet 0,
                          .load32 (0 : UInt32),
                          .localSet 8,
                          .localGet 8,
                          .localGet 2,
                          .gtU,
                          .br_if 0,
                          .localGet 2,
                          .localGet 8,
                          .localGet 0,
                          .load32 (4 : UInt32),
                          .add,
                          .localSet 8,
                          .localGet 8,
                          .ltU,
                          .br_if 2
                        ],
                        .localGet 0,
                        .load32 (8 : UInt32),
                        .localSet 0,
                        .br 0
                      ]
                    ],
                    .const (0 : UInt32),
                    .localGet 6,
                    .const (15 : UInt32),
                    .add,
                    .const (4294967288 : UInt32),
                    .and,
                    .localSet 0,
                    .localGet 0,
                    .const (4294967288 : UInt32),
                    .add,
                    .localSet 7,
                    .localGet 7,
                    .store32 (1049548 : UInt32),
                    .const (0 : UInt32),
                    .localGet 6,
                    .localGet 0,
                    .sub,
                    .localGet 9,
                    .const (4294967256 : UInt32),
                    .add,
                    .localSet 0,
                    .localGet 0,
                    .add,
                    .const (8 : UInt32),
                    .add,
                    .localSet 4,
                    .localGet 4,
                    .store32 (1049540 : UInt32),
                    .localGet 7,
                    .localGet 4,
                    .const (1 : UInt32),
                    .or,
                    .store32 (4 : UInt32),
                    .localGet 6,
                    .localGet 0,
                    .add,
                    .const (40 : UInt32),
                    .store32 (4 : UInt32),
                    .const (0 : UInt32),
                    .const (2097152 : UInt32),
                    .store32 (1049560 : UInt32),
                    .localGet 2,
                    .localGet 8,
                    .const (4294967264 : UInt32),
                    .add,
                    .const (4294967288 : UInt32),
                    .and,
                    .const (4294967288 : UInt32),
                    .add,
                    .localSet 0,
                    .localGet 0,
                    .localGet 0,
                    .localGet 2,
                    .const (16 : UInt32),
                    .add,
                    .ltU,
                    .select,
                    .localSet 7,
                    .localGet 7,
                    .const (27 : UInt32),
                    .store32 (4 : UInt32),
                    .const (0 : UInt32),
                    .load64 (1049248 : UInt32),
                    .localSet 10,
                    .localGet 7,
                    .const (16 : UInt32),
                    .add,
                    .const (0 : UInt32),
                    .load64 (1049256 : UInt32),
                    .store64 (0 : UInt32),
                    .localGet 7,
                    .const (8 : UInt32),
                    .add,
                    .localSet 0,
                    .localGet 0,
                    .localGet 10,
                    .store64 (0 : UInt32),
                    .const (0 : UInt32),
                    .localGet 5,
                    .store32 (1049260 : UInt32),
                    .const (0 : UInt32),
                    .localGet 9,
                    .store32 (1049252 : UInt32),
                    .const (0 : UInt32),
                    .localGet 6,
                    .store32 (1049248 : UInt32),
                    .const (0 : UInt32),
                    .localGet 0,
                    .store32 (1049256 : UInt32),
                    .localGet 7,
                    .const (28 : UInt32),
                    .add,
                    .localSet 0,
                    .loop 0 0 [
                      .localGet 0,
                      .const (7 : UInt32),
                      .store32 (0 : UInt32),
                      .localGet 0,
                      .const (4 : UInt32),
                      .add,
                      .localSet 0,
                      .localGet 0,
                      .localGet 8,
                      .ltU,
                      .br_if 0
                    ],
                    .localGet 7,
                    .localGet 2,
                    .eq,
                    .br_if 7,
                    .localGet 7,
                    .localGet 7,
                    .load32 (4 : UInt32),
                    .const (4294967294 : UInt32),
                    .and,
                    .store32 (4 : UInt32),
                    .localGet 2,
                    .localGet 7,
                    .localGet 2,
                    .sub,
                    .localSet 0,
                    .localGet 0,
                    .const (1 : UInt32),
                    .or,
                    .store32 (4 : UInt32),
                    .localGet 7,
                    .localGet 0,
                    .store32 (0 : UInt32),
                    .block 0 0 [
                      .localGet 0,
                      .const (256 : UInt32),
                      .ltU,
                      .br_if 0,
                      .localGet 2,
                      .localGet 0,
                      .call 32,
                      .br 8
                    ],
                    .block 0 0 [
                      .block 0 0 [
                        .const (0 : UInt32),
                        .load32 (1049528 : UInt32),
                        .localSet 8,
                        .localGet 8,
                        .const (1 : UInt32),
                        .localGet 0,
                        .const (3 : UInt32),
                        .shrU,
                        .shl,
                        .localSet 6,
                        .localGet 6,
                        .and,
                        .br_if 0,
                        .const (0 : UInt32),
                        .localGet 8,
                        .localGet 6,
                        .or,
                        .store32 (1049528 : UInt32),
                        .localGet 0,
                        .const (248 : UInt32),
                        .and,
                        .const (1049264 : UInt32),
                        .add,
                        .localSet 0,
                        .localGet 0,
                        .localSet 8,
                        .br 1
                      ],
                      .localGet 0,
                      .const (248 : UInt32),
                      .and,
                      .localSet 0,
                      .localGet 0,
                      .const (1049264 : UInt32),
                      .add,
                      .localSet 8,
                      .localGet 0,
                      .const (1049272 : UInt32),
                      .add,
                      .load32 (0 : UInt32),
                      .localSet 0
                    ],
                    .localGet 8,
                    .localGet 2,
                    .store32 (8 : UInt32),
                    .localGet 0,
                    .localGet 2,
                    .store32 (12 : UInt32),
                    .localGet 2,
                    .localGet 8,
                    .store32 (12 : UInt32),
                    .localGet 2,
                    .localGet 0,
                    .store32 (8 : UInt32),
                    .br 7
                  ],
                  .localGet 0,
                  .localGet 6,
                  .store32 (0 : UInt32),
                  .localGet 0,
                  .localGet 0,
                  .load32 (4 : UInt32),
                  .localGet 9,
                  .add,
                  .store32 (4 : UInt32),
                  .localGet 6,
                  .const (15 : UInt32),
                  .add,
                  .const (4294967288 : UInt32),
                  .and,
                  .const (4294967288 : UInt32),
                  .add,
                  .localSet 8,
                  .localGet 8,
                  .localGet 3,
                  .const (3 : UInt32),
                  .or,
                  .store32 (4 : UInt32),
                  .localGet 7,
                  .const (15 : UInt32),
                  .add,
                  .const (4294967288 : UInt32),
                  .and,
                  .const (4294967288 : UInt32),
                  .add,
                  .localSet 2,
                  .localGet 2,
                  .localGet 8,
                  .localGet 3,
                  .add,
                  .localSet 0,
                  .localGet 0,
                  .sub,
                  .localSet 3,
                  .localGet 2,
                  .const (0 : UInt32),
                  .load32 (1049548 : UInt32),
                  .eq,
                  .br_if 3,
                  .localGet 2,
                  .const (0 : UInt32),
                  .load32 (1049544 : UInt32),
                  .eq,
                  .br_if 4,
                  .block 0 0 [
                    .localGet 2,
                    .load32 (4 : UInt32),
                    .localSet 6,
                    .localGet 6,
                    .const (3 : UInt32),
                    .and,
                    .const (1 : UInt32),
                    .ne,
                    .br_if 0,
                    .localGet 2,
                    .localGet 6,
                    .const (4294967288 : UInt32),
                    .and,
                    .localSet 6,
                    .localGet 6,
                    .call 27,
                    .localGet 6,
                    .localGet 3,
                    .add,
                    .localSet 3,
                    .localGet 2,
                    .localGet 6,
                    .add,
                    .localSet 2,
                    .localGet 2,
                    .load32 (4 : UInt32),
                    .localSet 6
                  ],
                  .localGet 2,
                  .localGet 6,
                  .const (4294967294 : UInt32),
                  .and,
                  .store32 (4 : UInt32),
                  .localGet 0,
                  .localGet 3,
                  .const (1 : UInt32),
                  .or,
                  .store32 (4 : UInt32),
                  .localGet 0,
                  .localGet 3,
                  .add,
                  .localGet 3,
                  .store32 (0 : UInt32),
                  .block 0 0 [
                    .localGet 3,
                    .const (256 : UInt32),
                    .ltU,
                    .br_if 0,
                    .localGet 0,
                    .localGet 3,
                    .call 32,
                    .br 6
                  ],
                  .block 0 0 [
                    .block 0 0 [
                      .const (0 : UInt32),
                      .load32 (1049528 : UInt32),
                      .localSet 2,
                      .localGet 2,
                      .const (1 : UInt32),
                      .localGet 3,
                      .const (3 : UInt32),
                      .shrU,
                      .shl,
                      .localSet 6,
                      .localGet 6,
                      .and,
                      .br_if 0,
                      .const (0 : UInt32),
                      .localGet 2,
                      .localGet 6,
                      .or,
                      .store32 (1049528 : UInt32),
                      .localGet 3,
                      .const (248 : UInt32),
                      .and,
                      .const (1049264 : UInt32),
                      .add,
                      .localSet 3,
                      .localGet 3,
                      .localSet 2,
                      .br 1
                    ],
                    .localGet 3,
                    .const (248 : UInt32),
                    .and,
                    .localSet 3,
                    .localGet 3,
                    .const (1049264 : UInt32),
                    .add,
                    .localSet 2,
                    .localGet 3,
                    .const (1049272 : UInt32),
                    .add,
                    .load32 (0 : UInt32),
                    .localSet 3
                  ],
                  .localGet 2,
                  .localGet 0,
                  .store32 (8 : UInt32),
                  .localGet 3,
                  .localGet 0,
                  .store32 (12 : UInt32),
                  .localGet 0,
                  .localGet 2,
                  .store32 (12 : UInt32),
                  .localGet 0,
                  .localGet 3,
                  .store32 (8 : UInt32),
                  .br 5
                ],
                .const (0 : UInt32),
                .localGet 0,
                .localGet 3,
                .sub,
                .localSet 2,
                .localGet 2,
                .store32 (1049540 : UInt32),
                .const (0 : UInt32),
                .const (0 : UInt32),
                .load32 (1049548 : UInt32),
                .localSet 0,
                .localGet 0,
                .localGet 3,
                .add,
                .localSet 8,
                .localGet 8,
                .store32 (1049548 : UInt32),
                .localGet 8,
                .localGet 2,
                .const (1 : UInt32),
                .or,
                .store32 (4 : UInt32),
                .localGet 0,
                .localGet 3,
                .const (3 : UInt32),
                .or,
                .store32 (4 : UInt32),
                .localGet 0,
                .const (8 : UInt32),
                .add,
                .localSet 0,
                .br 6
              ],
              .const (0 : UInt32),
              .load32 (1049544 : UInt32),
              .localSet 2,
              .block 0 0 [
                .block 0 0 [
                  .localGet 0,
                  .localGet 3,
                  .sub,
                  .localSet 8,
                  .localGet 8,
                  .const (15 : UInt32),
                  .gtU,
                  .br_if 0,
                  .const (0 : UInt32),
                  .const (0 : UInt32),
                  .store32 (1049544 : UInt32),
                  .const (0 : UInt32),
                  .const (0 : UInt32),
                  .store32 (1049536 : UInt32),
                  .localGet 2,
                  .localGet 0,
                  .const (3 : UInt32),
                  .or,
                  .store32 (4 : UInt32),
                  .localGet 2,
                  .localGet 0,
                  .add,
                  .localSet 0,
                  .localGet 0,
                  .localGet 0,
                  .load32 (4 : UInt32),
                  .const (1 : UInt32),
                  .or,
                  .store32 (4 : UInt32),
                  .br 1
                ],
                .const (0 : UInt32),
                .localGet 8,
                .store32 (1049536 : UInt32),
                .const (0 : UInt32),
                .localGet 2,
                .localGet 3,
                .add,
                .localSet 6,
                .localGet 6,
                .store32 (1049544 : UInt32),
                .localGet 6,
                .localGet 8,
                .const (1 : UInt32),
                .or,
                .store32 (4 : UInt32),
                .localGet 2,
                .localGet 0,
                .add,
                .localGet 8,
                .store32 (0 : UInt32),
                .localGet 2,
                .localGet 3,
                .const (3 : UInt32),
                .or,
                .store32 (4 : UInt32)
              ],
              .localGet 2,
              .const (8 : UInt32),
              .add,
              .localSet 0,
              .br 5
            ],
            .localGet 0,
            .localGet 7,
            .localGet 9,
            .add,
            .store32 (4 : UInt32),
            .const (0 : UInt32),
            .const (0 : UInt32),
            .load32 (1049548 : UInt32),
            .localSet 0,
            .localGet 0,
            .const (15 : UInt32),
            .add,
            .const (4294967288 : UInt32),
            .and,
            .localSet 2,
            .localGet 2,
            .const (4294967288 : UInt32),
            .add,
            .localSet 8,
            .localGet 8,
            .store32 (1049548 : UInt32),
            .const (0 : UInt32),
            .localGet 0,
            .localGet 2,
            .sub,
            .const (0 : UInt32),
            .load32 (1049540 : UInt32),
            .localGet 9,
            .add,
            .localSet 2,
            .localGet 2,
            .add,
            .const (8 : UInt32),
            .add,
            .localSet 6,
            .localGet 6,
            .store32 (1049540 : UInt32),
            .localGet 8,
            .localGet 6,
            .const (1 : UInt32),
            .or,
            .store32 (4 : UInt32),
            .localGet 0,
            .localGet 2,
            .add,
            .const (40 : UInt32),
            .store32 (4 : UInt32),
            .const (0 : UInt32),
            .const (2097152 : UInt32),
            .store32 (1049560 : UInt32),
            .br 3
          ],
          .const (0 : UInt32),
          .localGet 0,
          .store32 (1049548 : UInt32),
          .const (0 : UInt32),
          .const (0 : UInt32),
          .load32 (1049540 : UInt32),
          .localGet 3,
          .add,
          .localSet 3,
          .localGet 3,
          .store32 (1049540 : UInt32),
          .localGet 0,
          .localGet 3,
          .const (1 : UInt32),
          .or,
          .store32 (4 : UInt32),
          .br 1
        ],
        .const (0 : UInt32),
        .localGet 0,
        .store32 (1049544 : UInt32),
        .const (0 : UInt32),
        .const (0 : UInt32),
        .load32 (1049536 : UInt32),
        .localGet 3,
        .add,
        .localSet 3,
        .localGet 3,
        .store32 (1049536 : UInt32),
        .localGet 0,
        .localGet 3,
        .const (1 : UInt32),
        .or,
        .store32 (4 : UInt32),
        .localGet 0,
        .localGet 3,
        .add,
        .localGet 3,
        .store32 (0 : UInt32)
      ],
      .localGet 8,
      .const (8 : UInt32),
      .add,
      .localSet 0,
      .br 1
    ],
    .const (0 : UInt32),
    .localSet 0,
    .const (0 : UInt32),
    .load32 (1049540 : UInt32),
    .localSet 2,
    .localGet 2,
    .localGet 3,
    .leU,
    .br_if 0,
    .const (0 : UInt32),
    .localGet 2,
    .localGet 3,
    .sub,
    .localSet 2,
    .localGet 2,
    .store32 (1049540 : UInt32),
    .const (0 : UInt32),
    .const (0 : UInt32),
    .load32 (1049548 : UInt32),
    .localSet 0,
    .localGet 0,
    .localGet 3,
    .add,
    .localSet 8,
    .localGet 8,
    .store32 (1049548 : UInt32),
    .localGet 8,
    .localGet 2,
    .const (1 : UInt32),
    .or,
    .store32 (4 : UInt32),
    .localGet 0,
    .localGet 3,
    .const (3 : UInt32),
    .or,
    .store32 (4 : UInt32),
    .localGet 0,
    .const (8 : UInt32),
    .add,
    .localSet 0
  ],
  .localGet 1,
  .const (16 : UInt32),
  .add,
  .globalSet 0,
  .localGet 0
]

def func22Def : Wasm.Function :=
  { params := [.i32], locals := [.i32, .i32, .i32, .i32, .i32, .i32, .i32, .i32, .i32, .i64], body := func22, results := [.i32] }

def func23 : Wasm.Program :=
  [
  .unreachable
]

def func23Def : Wasm.Function :=
  { params := [], locals := [], body := func23, results := [] }

def func24 : Wasm.Program :=
  [
  .block 0 0 [
    .block 0 0 [
      .localGet 0,
      .const (4294967292 : UInt32),
      .add,
      .load32 (0 : UInt32),
      .localSet 3,
      .localGet 3,
      .const (4294967288 : UInt32),
      .and,
      .localSet 4,
      .localGet 4,
      .const (4 : UInt32),
      .const (8 : UInt32),
      .localGet 3,
      .const (3 : UInt32),
      .and,
      .localSet 3,
      .localGet 3,
      .select,
      .localGet 1,
      .add,
      .ltU,
      .br_if 0,
      .block 0 0 [
        .localGet 3,
        .eqz,
        .br_if 0,
        .localGet 4,
        .localGet 1,
        .const (39 : UInt32),
        .add,
        .gtU,
        .br_if 2
      ],
      .localGet 0,
      .call 25,
      .ret
    ],
    .const (1048815 : UInt32),
    .const (46 : UInt32),
    .const (1048864 : UInt32),
    .call 51,
    .unreachable
  ],
  .const (1048880 : UInt32),
  .const (46 : UInt32),
  .const (1048928 : UInt32),
  .call 51,
  .unreachable
]

def func24Def : Wasm.Function :=
  { params := [.i32, .i32, .i32], locals := [.i32, .i32], body := func24, results := [] }

def func25 : Wasm.Program :=
  [
  .localGet 0,
  .const (4294967288 : UInt32),
  .add,
  .localSet 1,
  .localGet 1,
  .localGet 0,
  .const (4294967292 : UInt32),
  .add,
  .load32 (0 : UInt32),
  .localSet 2,
  .localGet 2,
  .const (4294967288 : UInt32),
  .and,
  .localSet 0,
  .localGet 0,
  .add,
  .localSet 3,
  .block 0 0 [
    .block 0 0 [
      .localGet 2,
      .const (1 : UInt32),
      .and,
      .br_if 0,
      .localGet 2,
      .const (2 : UInt32),
      .and,
      .eqz,
      .br_if 1,
      .localGet 1,
      .load32 (0 : UInt32),
      .localSet 2,
      .localGet 2,
      .localGet 0,
      .add,
      .localSet 0,
      .block 0 0 [
        .localGet 1,
        .localGet 2,
        .sub,
        .localSet 1,
        .localGet 1,
        .const (0 : UInt32),
        .load32 (1049544 : UInt32),
        .ne,
        .br_if 0,
        .localGet 3,
        .load32 (4 : UInt32),
        .const (3 : UInt32),
        .and,
        .const (3 : UInt32),
        .ne,
        .br_if 1,
        .const (0 : UInt32),
        .localGet 0,
        .store32 (1049536 : UInt32),
        .localGet 3,
        .localGet 3,
        .load32 (4 : UInt32),
        .const (4294967294 : UInt32),
        .and,
        .store32 (4 : UInt32),
        .localGet 1,
        .localGet 0,
        .const (1 : UInt32),
        .or,
        .store32 (4 : UInt32),
        .localGet 3,
        .localGet 0,
        .store32 (0 : UInt32),
        .ret
      ],
      .localGet 1,
      .localGet 2,
      .call 27
    ],
    .block 0 0 [
      .block 0 0 [
        .block 0 0 [
          .block 0 0 [
            .block 0 0 [
              .block 0 0 [
                .block 0 0 [
                  .block 0 0 [
                    .localGet 3,
                    .load32 (4 : UInt32),
                    .localSet 2,
                    .localGet 2,
                    .const (2 : UInt32),
                    .and,
                    .br_if 0,
                    .localGet 3,
                    .const (0 : UInt32),
                    .load32 (1049548 : UInt32),
                    .eq,
                    .br_if 2,
                    .localGet 3,
                    .const (0 : UInt32),
                    .load32 (1049544 : UInt32),
                    .eq,
                    .br_if 3,
                    .localGet 3,
                    .localGet 2,
                    .const (4294967288 : UInt32),
                    .and,
                    .localSet 2,
                    .localGet 2,
                    .call 27,
                    .localGet 1,
                    .localGet 2,
                    .localGet 0,
                    .add,
                    .localSet 0,
                    .localGet 0,
                    .const (1 : UInt32),
                    .or,
                    .store32 (4 : UInt32),
                    .localGet 1,
                    .localGet 0,
                    .add,
                    .localGet 0,
                    .store32 (0 : UInt32),
                    .localGet 1,
                    .const (0 : UInt32),
                    .load32 (1049544 : UInt32),
                    .ne,
                    .br_if 1,
                    .const (0 : UInt32),
                    .localGet 0,
                    .store32 (1049536 : UInt32),
                    .ret
                  ],
                  .localGet 3,
                  .localGet 2,
                  .const (4294967294 : UInt32),
                  .and,
                  .store32 (4 : UInt32),
                  .localGet 1,
                  .localGet 0,
                  .const (1 : UInt32),
                  .or,
                  .store32 (4 : UInt32),
                  .localGet 1,
                  .localGet 0,
                  .add,
                  .localGet 0,
                  .store32 (0 : UInt32)
                ],
                .localGet 0,
                .const (256 : UInt32),
                .ltU,
                .br_if 4,
                .localGet 1,
                .localGet 0,
                .call 32,
                .const (0 : UInt32),
                .const (0 : UInt32),
                .load32 (1049568 : UInt32),
                .const (4294967295 : UInt32),
                .add,
                .localSet 1,
                .localGet 1,
                .store32 (1049568 : UInt32),
                .localGet 1,
                .br_if 6,
                .const (0 : UInt32),
                .load32 (1049256 : UInt32),
                .localSet 0,
                .localGet 0,
                .br_if 2,
                .const (4095 : UInt32),
                .localSet 1,
                .br 3
              ],
              .const (0 : UInt32),
              .localGet 1,
              .store32 (1049548 : UInt32),
              .const (0 : UInt32),
              .const (0 : UInt32),
              .load32 (1049540 : UInt32),
              .localGet 0,
              .add,
              .localSet 0,
              .localGet 0,
              .store32 (1049540 : UInt32),
              .localGet 1,
              .localGet 0,
              .const (1 : UInt32),
              .or,
              .store32 (4 : UInt32),
              .block 0 0 [
                .localGet 1,
                .const (0 : UInt32),
                .load32 (1049544 : UInt32),
                .ne,
                .br_if 0,
                .const (0 : UInt32),
                .const (0 : UInt32),
                .store32 (1049536 : UInt32),
                .const (0 : UInt32),
                .const (0 : UInt32),
                .store32 (1049544 : UInt32)
              ],
              .localGet 0,
              .const (0 : UInt32),
              .load32 (1049560 : UInt32),
              .localSet 2,
              .localGet 2,
              .leU,
              .br_if 5,
              .const (0 : UInt32),
              .load32 (1049548 : UInt32),
              .localSet 0,
              .localGet 0,
              .eqz,
              .br_if 5,
              .const (0 : UInt32),
              .load32 (1049540 : UInt32),
              .localSet 4,
              .localGet 4,
              .const (41 : UInt32),
              .ltU,
              .br_if 4,
              .const (1049248 : UInt32),
              .localSet 1,
              .loop 0 0 [
                .block 0 0 [
                  .localGet 1,
                  .load32 (0 : UInt32),
                  .localSet 3,
                  .localGet 3,
                  .localGet 0,
                  .gtU,
                  .br_if 0,
                  .localGet 0,
                  .localGet 3,
                  .localGet 1,
                  .load32 (4 : UInt32),
                  .add,
                  .ltU,
                  .br_if 6
                ],
                .localGet 1,
                .load32 (8 : UInt32),
                .localSet 1,
                .br 0
              ]
            ],
            .const (0 : UInt32),
            .localGet 1,
            .store32 (1049544 : UInt32),
            .const (0 : UInt32),
            .const (0 : UInt32),
            .load32 (1049536 : UInt32),
            .localGet 0,
            .add,
            .localSet 0,
            .localGet 0,
            .store32 (1049536 : UInt32),
            .localGet 1,
            .localGet 0,
            .const (1 : UInt32),
            .or,
            .store32 (4 : UInt32),
            .localGet 1,
            .localGet 0,
            .add,
            .localGet 0,
            .store32 (0 : UInt32),
            .ret
          ],
          .const (0 : UInt32),
          .localSet 1,
          .loop 0 0 [
            .localGet 1,
            .const (1 : UInt32),
            .add,
            .localSet 1,
            .localGet 0,
            .load32 (8 : UInt32),
            .localSet 0,
            .localGet 0,
            .br_if 0
          ],
          .localGet 1,
          .const (4095 : UInt32),
          .localGet 1,
          .const (4095 : UInt32),
          .gtU,
          .select,
          .localSet 1
        ],
        .const (0 : UInt32),
        .localGet 1,
        .store32 (1049568 : UInt32),
        .ret
      ],
      .block 0 0 [
        .block 0 0 [
          .const (0 : UInt32),
          .load32 (1049528 : UInt32),
          .localSet 3,
          .localGet 3,
          .const (1 : UInt32),
          .localGet 0,
          .const (3 : UInt32),
          .shrU,
          .shl,
          .localSet 2,
          .localGet 2,
          .and,
          .br_if 0,
          .const (0 : UInt32),
          .localGet 3,
          .localGet 2,
          .or,
          .store32 (1049528 : UInt32),
          .localGet 0,
          .const (248 : UInt32),
          .and,
          .const (1049264 : UInt32),
          .add,
          .localSet 0,
          .localGet 0,
          .localSet 3,
          .br 1
        ],
        .localGet 0,
        .const (248 : UInt32),
        .and,
        .localSet 0,
        .localGet 0,
        .const (1049264 : UInt32),
        .add,
        .localSet 3,
        .localGet 0,
        .const (1049272 : UInt32),
        .add,
        .load32 (0 : UInt32),
        .localSet 0
      ],
      .localGet 3,
      .localGet 1,
      .store32 (8 : UInt32),
      .localGet 0,
      .localGet 1,
      .store32 (12 : UInt32),
      .localGet 1,
      .localGet 3,
      .store32 (12 : UInt32),
      .localGet 1,
      .localGet 0,
      .store32 (8 : UInt32),
      .ret
    ],
    .block 0 0 [
      .block 0 0 [
        .const (0 : UInt32),
        .load32 (1049256 : UInt32),
        .localSet 0,
        .localGet 0,
        .br_if 0,
        .const (4095 : UInt32),
        .localSet 1,
        .br 1
      ],
      .const (0 : UInt32),
      .localSet 1,
      .loop 0 0 [
        .localGet 1,
        .const (1 : UInt32),
        .add,
        .localSet 1,
        .localGet 0,
        .load32 (8 : UInt32),
        .localSet 0,
        .localGet 0,
        .br_if 0
      ],
      .localGet 1,
      .const (4095 : UInt32),
      .localGet 1,
      .const (4095 : UInt32),
      .gtU,
      .select,
      .localSet 1
    ],
    .const (0 : UInt32),
    .localGet 1,
    .store32 (1049568 : UInt32),
    .localGet 4,
    .localGet 2,
    .leU,
    .br_if 0,
    .const (0 : UInt32),
    .const (4294967295 : UInt32),
    .store32 (1049560 : UInt32)
  ]
]

def func25Def : Wasm.Function :=
  { params := [.i32], locals := [.i32, .i32, .i32, .i32], body := func25, results := [] }

def func26 : Wasm.Program :=
  [
  .block 0 0 [
    .block 0 0 [
      .block 0 0 [
        .block 0 0 [
          .block 0 0 [
            .block 0 0 [
              .block 0 0 [
                .block 0 0 [
                  .localGet 0,
                  .const (4294967292 : UInt32),
                  .add,
                  .localSet 4,
                  .localGet 4,
                  .load32 (0 : UInt32),
                  .localSet 5,
                  .localGet 5,
                  .const (4294967288 : UInt32),
                  .and,
                  .localSet 6,
                  .localGet 6,
                  .const (4 : UInt32),
                  .const (8 : UInt32),
                  .localGet 5,
                  .const (3 : UInt32),
                  .and,
                  .localSet 7,
                  .localGet 7,
                  .select,
                  .localGet 1,
                  .add,
                  .ltU,
                  .br_if 0,
                  .localGet 1,
                  .const (39 : UInt32),
                  .add,
                  .localSet 8,
                  .block 0 0 [
                    .localGet 7,
                    .eqz,
                    .br_if 0,
                    .localGet 6,
                    .localGet 8,
                    .gtU,
                    .br_if 2
                  ],
                  .block 0 0 [
                    .block 0 0 [
                      .localGet 2,
                      .const (9 : UInt32),
                      .ltU,
                      .br_if 0,
                      .localGet 2,
                      .localGet 3,
                      .call 21,
                      .localSet 2,
                      .localGet 2,
                      .br_if 1,
                      .const (0 : UInt32),
                      .ret
                    ],
                    .const (0 : UInt32),
                    .localSet 2,
                    .localGet 3,
                    .const (4294901708 : UInt32),
                    .gtU,
                    .br_if 8,
                    .const (16 : UInt32),
                    .localGet 3,
                    .const (11 : UInt32),
                    .add,
                    .const (4294967288 : UInt32),
                    .and,
                    .localGet 3,
                    .const (11 : UInt32),
                    .ltU,
                    .select,
                    .localSet 1,
                    .localGet 0,
                    .const (4294967288 : UInt32),
                    .add,
                    .localSet 8,
                    .block 0 0 [
                      .localGet 7,
                      .br_if 0,
                      .localGet 1,
                      .const (256 : UInt32),
                      .ltU,
                      .br_if 7,
                      .localGet 8,
                      .eqz,
                      .br_if 7,
                      .localGet 6,
                      .localGet 1,
                      .leU,
                      .br_if 7,
                      .localGet 6,
                      .localGet 1,
                      .sub,
                      .const (131072 : UInt32),
                      .gtU,
                      .br_if 7,
                      .localGet 0,
                      .ret
                    ],
                    .localGet 8,
                    .localGet 6,
                    .add,
                    .localSet 7,
                    .block 0 0 [
                      .block 0 0 [
                        .localGet 6,
                        .localGet 1,
                        .geU,
                        .br_if 0,
                        .localGet 7,
                        .const (0 : UInt32),
                        .load32 (1049548 : UInt32),
                        .eq,
                        .br_if 1,
                        .block 0 0 [
                          .localGet 7,
                          .const (0 : UInt32),
                          .load32 (1049544 : UInt32),
                          .eq,
                          .br_if 0,
                          .localGet 7,
                          .load32 (4 : UInt32),
                          .localSet 5,
                          .localGet 5,
                          .const (2 : UInt32),
                          .and,
                          .br_if 9,
                          .localGet 5,
                          .const (4294967288 : UInt32),
                          .and,
                          .localSet 9,
                          .localGet 9,
                          .localGet 6,
                          .add,
                          .localSet 5,
                          .localGet 5,
                          .localGet 1,
                          .ltU,
                          .br_if 9,
                          .localGet 7,
                          .localGet 9,
                          .call 27,
                          .block 0 0 [
                            .localGet 5,
                            .localGet 1,
                            .sub,
                            .localSet 7,
                            .localGet 7,
                            .const (16 : UInt32),
                            .ltU,
                            .br_if 0,
                            .localGet 4,
                            .localGet 1,
                            .localGet 4,
                            .load32 (0 : UInt32),
                            .const (1 : UInt32),
                            .and,
                            .or,
                            .const (2 : UInt32),
                            .or,
                            .store32 (0 : UInt32),
                            .localGet 8,
                            .localGet 1,
                            .add,
                            .localSet 1,
                            .localGet 1,
                            .localGet 7,
                            .const (3 : UInt32),
                            .or,
                            .store32 (4 : UInt32),
                            .localGet 8,
                            .localGet 5,
                            .add,
                            .localSet 5,
                            .localGet 5,
                            .localGet 5,
                            .load32 (4 : UInt32),
                            .const (1 : UInt32),
                            .or,
                            .store32 (4 : UInt32),
                            .localGet 1,
                            .localGet 7,
                            .call 28,
                            .br 9
                          ],
                          .localGet 4,
                          .localGet 5,
                          .localGet 4,
                          .load32 (0 : UInt32),
                          .const (1 : UInt32),
                          .and,
                          .or,
                          .const (2 : UInt32),
                          .or,
                          .store32 (0 : UInt32),
                          .localGet 8,
                          .localGet 5,
                          .add,
                          .localSet 1,
                          .localGet 1,
                          .localGet 1,
                          .load32 (4 : UInt32),
                          .const (1 : UInt32),
                          .or,
                          .store32 (4 : UInt32),
                          .br 8
                        ],
                        .const (0 : UInt32),
                        .load32 (1049536 : UInt32),
                        .localGet 6,
                        .add,
                        .localSet 7,
                        .localGet 7,
                        .localGet 1,
                        .ltU,
                        .br_if 8,
                        .block 0 0 [
                          .block 0 0 [
                            .localGet 7,
                            .localGet 1,
                            .sub,
                            .localSet 6,
                            .localGet 6,
                            .const (15 : UInt32),
                            .gtU,
                            .br_if 0,
                            .localGet 4,
                            .localGet 5,
                            .const (1 : UInt32),
                            .and,
                            .localGet 7,
                            .or,
                            .const (2 : UInt32),
                            .or,
                            .store32 (0 : UInt32),
                            .localGet 8,
                            .localGet 7,
                            .add,
                            .localSet 1,
                            .localGet 1,
                            .localGet 1,
                            .load32 (4 : UInt32),
                            .const (1 : UInt32),
                            .or,
                            .store32 (4 : UInt32),
                            .const (0 : UInt32),
                            .localSet 6,
                            .const (0 : UInt32),
                            .localSet 1,
                            .br 1
                          ],
                          .localGet 4,
                          .localGet 1,
                          .localGet 5,
                          .const (1 : UInt32),
                          .and,
                          .or,
                          .const (2 : UInt32),
                          .or,
                          .store32 (0 : UInt32),
                          .localGet 8,
                          .localGet 1,
                          .add,
                          .localSet 1,
                          .localGet 1,
                          .localGet 6,
                          .const (1 : UInt32),
                          .or,
                          .store32 (4 : UInt32),
                          .localGet 8,
                          .localGet 7,
                          .add,
                          .localSet 7,
                          .localGet 7,
                          .localGet 6,
                          .store32 (0 : UInt32),
                          .localGet 7,
                          .localGet 7,
                          .load32 (4 : UInt32),
                          .const (4294967294 : UInt32),
                          .and,
                          .store32 (4 : UInt32)
                        ],
                        .const (0 : UInt32),
                        .localGet 1,
                        .store32 (1049544 : UInt32),
                        .const (0 : UInt32),
                        .localGet 6,
                        .store32 (1049536 : UInt32),
                        .br 7
                      ],
                      .localGet 6,
                      .localGet 1,
                      .sub,
                      .localSet 6,
                      .localGet 6,
                      .const (15 : UInt32),
                      .leU,
                      .br_if 6,
                      .localGet 4,
                      .localGet 1,
                      .localGet 5,
                      .const (1 : UInt32),
                      .and,
                      .or,
                      .const (2 : UInt32),
                      .or,
                      .store32 (0 : UInt32),
                      .localGet 8,
                      .localGet 1,
                      .add,
                      .localSet 1,
                      .localGet 1,
                      .localGet 6,
                      .const (3 : UInt32),
                      .or,
                      .store32 (4 : UInt32),
                      .localGet 7,
                      .localGet 7,
                      .load32 (4 : UInt32),
                      .const (1 : UInt32),
                      .or,
                      .store32 (4 : UInt32),
                      .localGet 1,
                      .localGet 6,
                      .call 28,
                      .br 6
                    ],
                    .const (0 : UInt32),
                    .load32 (1049540 : UInt32),
                    .localGet 6,
                    .add,
                    .localSet 7,
                    .localGet 7,
                    .localGet 1,
                    .gtU,
                    .br_if 4,
                    .br 6
                  ],
                  .block 0 0 [
                    .localGet 3,
                    .localGet 1,
                    .localGet 3,
                    .localGet 1,
                    .ltU,
                    .select,
                    .localSet 3,
                    .localGet 3,
                    .eqz,
                    .br_if 0,
                    .localGet 2,
                    .localGet 0,
                    .localGet 3,
                    .memoryCopy
                  ],
                  .localGet 4,
                  .load32 (0 : UInt32),
                  .localSet 3,
                  .localGet 3,
                  .const (4294967288 : UInt32),
                  .and,
                  .localSet 7,
                  .localGet 7,
                  .const (4 : UInt32),
                  .const (8 : UInt32),
                  .localGet 3,
                  .const (3 : UInt32),
                  .and,
                  .localSet 3,
                  .localGet 3,
                  .select,
                  .localGet 1,
                  .add,
                  .ltU,
                  .br_if 2,
                  .localGet 3,
                  .eqz,
                  .br_if 6,
                  .localGet 7,
                  .localGet 8,
                  .leU,
                  .br_if 6,
                  .const (1048880 : UInt32),
                  .const (46 : UInt32),
                  .const (1048928 : UInt32),
                  .call 51,
                  .unreachable
                ],
                .const (1048815 : UInt32),
                .const (46 : UInt32),
                .const (1048864 : UInt32),
                .call 51,
                .unreachable
              ],
              .const (1048880 : UInt32),
              .const (46 : UInt32),
              .const (1048928 : UInt32),
              .call 51,
              .unreachable
            ],
            .const (1048815 : UInt32),
            .const (46 : UInt32),
            .const (1048864 : UInt32),
            .call 51,
            .unreachable
          ],
          .localGet 4,
          .localGet 1,
          .localGet 5,
          .const (1 : UInt32),
          .and,
          .or,
          .const (2 : UInt32),
          .or,
          .store32 (0 : UInt32),
          .localGet 8,
          .localGet 1,
          .add,
          .localSet 5,
          .localGet 5,
          .localGet 7,
          .localGet 1,
          .sub,
          .localSet 1,
          .localGet 1,
          .const (1 : UInt32),
          .or,
          .store32 (4 : UInt32),
          .const (0 : UInt32),
          .localGet 1,
          .store32 (1049540 : UInt32),
          .const (0 : UInt32),
          .localGet 5,
          .store32 (1049548 : UInt32)
        ],
        .localGet 8,
        .eqz,
        .br_if 0,
        .localGet 0,
        .ret
      ],
      .localGet 3,
      .call 22,
      .localSet 1,
      .localGet 1,
      .eqz,
      .br_if 1,
      .block 0 0 [
        .localGet 3,
        .const (4294967292 : UInt32),
        .const (4294967288 : UInt32),
        .localGet 4,
        .load32 (0 : UInt32),
        .localSet 2,
        .localGet 2,
        .const (3 : UInt32),
        .and,
        .select,
        .localGet 2,
        .const (4294967288 : UInt32),
        .and,
        .add,
        .localSet 2,
        .localGet 2,
        .localGet 3,
        .localGet 2,
        .ltU,
        .select,
        .localSet 3,
        .localGet 3,
        .eqz,
        .br_if 0,
        .localGet 1,
        .localGet 0,
        .localGet 3,
        .memoryCopy
      ],
      .localGet 1,
      .localSet 2
    ],
    .localGet 0,
    .call 25
  ],
  .localGet 2
]

def func26Def : Wasm.Function :=
  { params := [.i32, .i32, .i32, .i32], locals := [.i32, .i32, .i32, .i32, .i32, .i32], body := func26, results := [.i32] }

def func27 : Wasm.Program :=
  [
  .localGet 0,
  .load32 (12 : UInt32),
  .localSet 2,
  .block 0 0 [
    .block 0 0 [
      .block 0 0 [
        .block 0 0 [
          .localGet 1,
          .const (256 : UInt32),
          .ltU,
          .br_if 0,
          .localGet 0,
          .load32 (24 : UInt32),
          .localSet 3,
          .block 0 0 [
            .block 0 0 [
              .block 0 0 [
                .localGet 2,
                .localGet 0,
                .ne,
                .br_if 0,
                .localGet 0,
                .const (20 : UInt32),
                .const (16 : UInt32),
                .localGet 0,
                .load32 (20 : UInt32),
                .localSet 2,
                .localGet 2,
                .select,
                .add,
                .load32 (0 : UInt32),
                .localSet 1,
                .localGet 1,
                .br_if 1,
                .const (0 : UInt32),
                .localSet 2,
                .br 2
              ],
              .localGet 0,
              .load32 (8 : UInt32),
              .localSet 1,
              .localGet 1,
              .localGet 2,
              .store32 (12 : UInt32),
              .localGet 2,
              .localGet 1,
              .store32 (8 : UInt32),
              .br 1
            ],
            .localGet 0,
            .const (20 : UInt32),
            .add,
            .localGet 0,
            .const (16 : UInt32),
            .add,
            .localGet 2,
            .select,
            .localSet 4,
            .loop 0 0 [
              .localGet 4,
              .localSet 5,
              .localGet 1,
              .localSet 2,
              .localGet 2,
              .const (20 : UInt32),
              .add,
              .localGet 2,
              .const (16 : UInt32),
              .add,
              .localGet 2,
              .load32 (20 : UInt32),
              .localSet 1,
              .localGet 1,
              .select,
              .localSet 4,
              .localGet 2,
              .const (20 : UInt32),
              .const (16 : UInt32),
              .localGet 1,
              .select,
              .add,
              .load32 (0 : UInt32),
              .localSet 1,
              .localGet 1,
              .br_if 0
            ],
            .localGet 5,
            .const (0 : UInt32),
            .store32 (0 : UInt32)
          ],
          .localGet 3,
          .eqz,
          .br_if 2,
          .block 0 0 [
            .block 0 0 [
              .localGet 0,
              .localGet 0,
              .load32 (28 : UInt32),
              .const (2 : UInt32),
              .shl,
              .const (1049120 : UInt32),
              .add,
              .localSet 1,
              .localGet 1,
              .load32 (0 : UInt32),
              .eq,
              .br_if 0,
              .localGet 3,
              .load32 (16 : UInt32),
              .localGet 0,
              .eq,
              .br_if 1,
              .localGet 3,
              .localGet 2,
              .store32 (20 : UInt32),
              .localGet 2,
              .br_if 3,
              .br 4
            ],
            .localGet 1,
            .localGet 2,
            .store32 (0 : UInt32),
            .localGet 2,
            .eqz,
            .br_if 4,
            .br 2
          ],
          .localGet 3,
          .localGet 2,
          .store32 (16 : UInt32),
          .localGet 2,
          .br_if 1,
          .br 2
        ],
        .block 0 0 [
          .localGet 2,
          .localGet 0,
          .load32 (8 : UInt32),
          .localSet 4,
          .localGet 4,
          .eq,
          .br_if 0,
          .localGet 4,
          .localGet 2,
          .store32 (12 : UInt32),
          .localGet 2,
          .localGet 4,
          .store32 (8 : UInt32),
          .ret
        ],
        .const (0 : UInt32),
        .const (0 : UInt32),
        .load32 (1049528 : UInt32),
        .const (4294967294 : UInt32),
        .localGet 1,
        .const (3 : UInt32),
        .shrU,
        .rotl,
        .and,
        .store32 (1049528 : UInt32),
        .ret
      ],
      .localGet 2,
      .localGet 3,
      .store32 (24 : UInt32),
      .block 0 0 [
        .localGet 0,
        .load32 (16 : UInt32),
        .localSet 1,
        .localGet 1,
        .eqz,
        .br_if 0,
        .localGet 2,
        .localGet 1,
        .store32 (16 : UInt32),
        .localGet 1,
        .localGet 2,
        .store32 (24 : UInt32)
      ],
      .localGet 0,
      .load32 (20 : UInt32),
      .localSet 1,
      .localGet 1,
      .eqz,
      .br_if 0,
      .localGet 2,
      .localGet 1,
      .store32 (20 : UInt32),
      .localGet 1,
      .localGet 2,
      .store32 (24 : UInt32),
      .ret
    ],
    .ret
  ],
  .const (0 : UInt32),
  .const (0 : UInt32),
  .load32 (1049532 : UInt32),
  .const (4294967294 : UInt32),
  .localGet 0,
  .load32 (28 : UInt32),
  .rotl,
  .and,
  .store32 (1049532 : UInt32)
]

def func27Def : Wasm.Function :=
  { params := [.i32, .i32], locals := [.i32, .i32, .i32, .i32], body := func27, results := [] }

def func28 : Wasm.Program :=
  [
  .localGet 0,
  .localGet 1,
  .add,
  .localSet 2,
  .block 0 0 [
    .block 0 0 [
      .localGet 0,
      .load32 (4 : UInt32),
      .localSet 3,
      .localGet 3,
      .const (1 : UInt32),
      .and,
      .br_if 0,
      .localGet 3,
      .const (2 : UInt32),
      .and,
      .eqz,
      .br_if 1,
      .localGet 0,
      .load32 (0 : UInt32),
      .localSet 3,
      .localGet 3,
      .localGet 1,
      .add,
      .localSet 1,
      .block 0 0 [
        .localGet 0,
        .localGet 3,
        .sub,
        .localSet 0,
        .localGet 0,
        .const (0 : UInt32),
        .load32 (1049544 : UInt32),
        .ne,
        .br_if 0,
        .localGet 2,
        .load32 (4 : UInt32),
        .const (3 : UInt32),
        .and,
        .const (3 : UInt32),
        .ne,
        .br_if 1,
        .const (0 : UInt32),
        .localGet 1,
        .store32 (1049536 : UInt32),
        .localGet 2,
        .localGet 2,
        .load32 (4 : UInt32),
        .const (4294967294 : UInt32),
        .and,
        .store32 (4 : UInt32),
        .localGet 0,
        .localGet 1,
        .const (1 : UInt32),
        .or,
        .store32 (4 : UInt32),
        .localGet 2,
        .localGet 1,
        .store32 (0 : UInt32),
        .br 2
      ],
      .localGet 0,
      .localGet 3,
      .call 27
    ],
    .block 0 0 [
      .block 0 0 [
        .block 0 0 [
          .block 0 0 [
            .localGet 2,
            .load32 (4 : UInt32),
            .localSet 3,
            .localGet 3,
            .const (2 : UInt32),
            .and,
            .br_if 0,
            .localGet 2,
            .const (0 : UInt32),
            .load32 (1049548 : UInt32),
            .eq,
            .br_if 2,
            .localGet 2,
            .const (0 : UInt32),
            .load32 (1049544 : UInt32),
            .eq,
            .br_if 3,
            .localGet 2,
            .localGet 3,
            .const (4294967288 : UInt32),
            .and,
            .localSet 3,
            .localGet 3,
            .call 27,
            .localGet 0,
            .localGet 3,
            .localGet 1,
            .add,
            .localSet 1,
            .localGet 1,
            .const (1 : UInt32),
            .or,
            .store32 (4 : UInt32),
            .localGet 0,
            .localGet 1,
            .add,
            .localGet 1,
            .store32 (0 : UInt32),
            .localGet 0,
            .const (0 : UInt32),
            .load32 (1049544 : UInt32),
            .ne,
            .br_if 1,
            .const (0 : UInt32),
            .localGet 1,
            .store32 (1049536 : UInt32),
            .ret
          ],
          .localGet 2,
          .localGet 3,
          .const (4294967294 : UInt32),
          .and,
          .store32 (4 : UInt32),
          .localGet 0,
          .localGet 1,
          .const (1 : UInt32),
          .or,
          .store32 (4 : UInt32),
          .localGet 0,
          .localGet 1,
          .add,
          .localGet 1,
          .store32 (0 : UInt32)
        ],
        .block 0 0 [
          .localGet 1,
          .const (256 : UInt32),
          .ltU,
          .br_if 0,
          .localGet 0,
          .localGet 1,
          .call 32,
          .ret
        ],
        .block 0 0 [
          .block 0 0 [
            .const (0 : UInt32),
            .load32 (1049528 : UInt32),
            .localSet 2,
            .localGet 2,
            .const (1 : UInt32),
            .localGet 1,
            .const (3 : UInt32),
            .shrU,
            .shl,
            .localSet 3,
            .localGet 3,
            .and,
            .br_if 0,
            .const (0 : UInt32),
            .localGet 2,
            .localGet 3,
            .or,
            .store32 (1049528 : UInt32),
            .localGet 1,
            .const (248 : UInt32),
            .and,
            .const (1049264 : UInt32),
            .add,
            .localSet 1,
            .localGet 1,
            .localSet 2,
            .br 1
          ],
          .localGet 1,
          .const (248 : UInt32),
          .and,
          .localSet 1,
          .localGet 1,
          .const (1049264 : UInt32),
          .add,
          .localSet 2,
          .localGet 1,
          .const (1049272 : UInt32),
          .add,
          .load32 (0 : UInt32),
          .localSet 1
        ],
        .localGet 2,
        .localGet 0,
        .store32 (8 : UInt32),
        .localGet 1,
        .localGet 0,
        .store32 (12 : UInt32),
        .localGet 0,
        .localGet 2,
        .store32 (12 : UInt32),
        .localGet 0,
        .localGet 1,
        .store32 (8 : UInt32),
        .ret
      ],
      .const (0 : UInt32),
      .localGet 0,
      .store32 (1049548 : UInt32),
      .const (0 : UInt32),
      .const (0 : UInt32),
      .load32 (1049540 : UInt32),
      .localGet 1,
      .add,
      .localSet 1,
      .localGet 1,
      .store32 (1049540 : UInt32),
      .localGet 0,
      .localGet 1,
      .const (1 : UInt32),
      .or,
      .store32 (4 : UInt32),
      .localGet 0,
      .const (0 : UInt32),
      .load32 (1049544 : UInt32),
      .ne,
      .br_if 1,
      .const (0 : UInt32),
      .const (0 : UInt32),
      .store32 (1049536 : UInt32),
      .const (0 : UInt32),
      .const (0 : UInt32),
      .store32 (1049544 : UInt32),
      .ret
    ],
    .const (0 : UInt32),
    .localGet 0,
    .store32 (1049544 : UInt32),
    .const (0 : UInt32),
    .const (0 : UInt32),
    .load32 (1049536 : UInt32),
    .localGet 1,
    .add,
    .localSet 1,
    .localGet 1,
    .store32 (1049536 : UInt32),
    .localGet 0,
    .localGet 1,
    .const (1 : UInt32),
    .or,
    .store32 (4 : UInt32),
    .localGet 0,
    .localGet 1,
    .add,
    .localGet 1,
    .store32 (0 : UInt32),
    .ret
  ]
]

def func28Def : Wasm.Function :=
  { params := [.i32, .i32], locals := [.i32, .i32], body := func28, results := [] }

def func29 : Wasm.Program :=
  [
  .globalGet 0,
  .const (16 : UInt32),
  .sub,
  .localSet 1,
  .localGet 1,
  .globalSet 0,
  .localGet 0,
  .load64 (0 : UInt32),
  .localSet 2,
  .localGet 1,
  .localGet 0,
  .store32 (12 : UInt32),
  .localGet 1,
  .localGet 2,
  .store64 (4 : UInt32),
  .localGet 1,
  .const (4 : UInt32),
  .add,
  .call 14,
  .unreachable
]

def func29Def : Wasm.Function :=
  { params := [.i32], locals := [.i32, .i64], body := func29, results := [] }

def func30 : Wasm.Program :=
  [
  .localGet 1,
  .localGet 0,
  .call 31,
  .unreachable
]

def func30Def : Wasm.Function :=
  { params := [.i32, .i32], locals := [], body := func30, results := [] }

def func31 : Wasm.Program :=
  [
  .globalGet 0,
  .const (16 : UInt32),
  .sub,
  .localSet 2,
  .localGet 2,
  .globalSet 0,
  .localGet 2,
  .localGet 1,
  .store32 (12 : UInt32),
  .localGet 2,
  .localGet 0,
  .store32 (8 : UInt32),
  .localGet 2,
  .const (8 : UInt32),
  .add,
  .call 12,
  .unreachable
]

def func31Def : Wasm.Function :=
  { params := [.i32, .i32], locals := [.i32], body := func31, results := [] }

def func32 : Wasm.Program :=
  [
  .const (0 : UInt32),
  .localSet 2,
  .block 0 0 [
    .localGet 1,
    .const (8 : UInt32),
    .shrU,
    .localSet 3,
    .localGet 3,
    .eqz,
    .br_if 0,
    .const (31 : UInt32),
    .localSet 2,
    .localGet 1,
    .const (16777216 : UInt32),
    .geU,
    .br_if 0,
    .localGet 1,
    .const (38 : UInt32),
    .localGet 3,
    .clz,
    .localSet 2,
    .localGet 2,
    .sub,
    .shrU,
    .const (1 : UInt32),
    .and,
    .localGet 2,
    .const (1 : UInt32),
    .shl,
    .or,
    .const (62 : UInt32),
    .xor,
    .localSet 2
  ],
  .localGet 0,
  .constI64 (0 : UInt64),
  .store64 (16 : UInt32),
  .localGet 0,
  .localGet 2,
  .store32 (28 : UInt32),
  .localGet 2,
  .const (2 : UInt32),
  .shl,
  .const (1049120 : UInt32),
  .add,
  .localSet 3,
  .block 0 0 [
    .const (0 : UInt32),
    .load32 (1049532 : UInt32),
    .const (1 : UInt32),
    .localGet 2,
    .shl,
    .localSet 4,
    .localGet 4,
    .and,
    .br_if 0,
    .localGet 3,
    .localGet 0,
    .store32 (0 : UInt32),
    .localGet 0,
    .localGet 3,
    .store32 (24 : UInt32),
    .localGet 0,
    .localGet 0,
    .store32 (12 : UInt32),
    .localGet 0,
    .localGet 0,
    .store32 (8 : UInt32),
    .const (0 : UInt32),
    .const (0 : UInt32),
    .load32 (1049532 : UInt32),
    .localGet 4,
    .or,
    .store32 (1049532 : UInt32),
    .ret
  ],
  .block 0 0 [
    .block 0 0 [
      .block 0 0 [
        .localGet 3,
        .load32 (0 : UInt32),
        .localSet 4,
        .localGet 4,
        .load32 (4 : UInt32),
        .const (4294967288 : UInt32),
        .and,
        .localGet 1,
        .ne,
        .br_if 0,
        .localGet 4,
        .localSet 2,
        .br 1
      ],
      .localGet 1,
      .const (0 : UInt32),
      .const (25 : UInt32),
      .localGet 2,
      .const (1 : UInt32),
      .shrU,
      .sub,
      .localGet 2,
      .const (31 : UInt32),
      .eq,
      .select,
      .shl,
      .localSet 3,
      .loop 0 0 [
        .localGet 4,
        .localGet 3,
        .const (29 : UInt32),
        .shrU,
        .const (4 : UInt32),
        .and,
        .add,
        .localSet 5,
        .localGet 5,
        .load32 (16 : UInt32),
        .localSet 2,
        .localGet 2,
        .eqz,
        .br_if 2,
        .localGet 3,
        .const (1 : UInt32),
        .shl,
        .localSet 3,
        .localGet 2,
        .localSet 4,
        .localGet 2,
        .load32 (4 : UInt32),
        .const (4294967288 : UInt32),
        .and,
        .localGet 1,
        .ne,
        .br_if 0
      ]
    ],
    .localGet 2,
    .load32 (8 : UInt32),
    .localSet 3,
    .localGet 3,
    .localGet 0,
    .store32 (12 : UInt32),
    .localGet 2,
    .localGet 0,
    .store32 (8 : UInt32),
    .localGet 0,
    .const (0 : UInt32),
    .store32 (24 : UInt32),
    .localGet 0,
    .localGet 2,
    .store32 (12 : UInt32),
    .localGet 0,
    .localGet 3,
    .store32 (8 : UInt32),
    .ret
  ],
  .localGet 5,
  .const (16 : UInt32),
  .add,
  .localGet 0,
  .store32 (0 : UInt32),
  .localGet 0,
  .localGet 4,
  .store32 (24 : UInt32),
  .localGet 0,
  .localGet 0,
  .store32 (12 : UInt32),
  .localGet 0,
  .localGet 0,
  .store32 (8 : UInt32)
]

def func32Def : Wasm.Function :=
  { params := [.i32, .i32], locals := [.i32, .i32, .i32, .i32], body := func32, results := [] }

def func33 : Wasm.Program :=
  [
  .const (0 : UInt32),
  .localSet 1,
  .const (0 : UInt32),
  .const (0 : UInt32),
  .load32 (1049116 : UInt32),
  .localSet 2,
  .localGet 2,
  .const (1 : UInt32),
  .add,
  .store32 (1049116 : UInt32),
  .block 0 0 [
    .localGet 2,
    .const (0 : UInt32),
    .ltS,
    .br_if 0,
    .const (1 : UInt32),
    .localSet 1,
    .const (0 : UInt32),
    .load8U (1049096 : UInt32),
    .br_if 0,
    .const (0 : UInt32),
    .localGet 0,
    .store8 (1049096 : UInt32),
    .const (0 : UInt32),
    .const (0 : UInt32),
    .load32 (1049092 : UInt32),
    .const (1 : UInt32),
    .add,
    .store32 (1049092 : UInt32),
    .const (2 : UInt32),
    .localSet 1
  ],
  .localGet 1
]

def func33Def : Wasm.Function :=
  { params := [.i32], locals := [.i32, .i32], body := func33, results := [.i32] }

def func34 : Wasm.Program :=
  [
  .localGet 0,
  .const (0 : UInt32),
  .load64 (1048764 : UInt32),
  .store64 (8 : UInt32),
  .localGet 0,
  .const (0 : UInt32),
  .load64 (1048756 : UInt32),
  .store64 (0 : UInt32)
]

def func34Def : Wasm.Function :=
  { params := [.i32, .i32], locals := [], body := func34, results := [] }

def func35 : Wasm.Program :=
  [
  .localGet 0,
  .const (0 : UInt32),
  .load64 (1048748 : UInt32),
  .store64 (8 : UInt32),
  .localGet 0,
  .const (0 : UInt32),
  .load64 (1048740 : UInt32),
  .store64 (0 : UInt32)
]

def func35Def : Wasm.Function :=
  { params := [.i32, .i32], locals := [], body := func35, results := [] }

def func36 : Wasm.Program :=
  [
  .block 0 0 [
    .localGet 0,
    .load32 (0 : UInt32),
    .const (2147483648 : UInt32),
    .eq,
    .br_if 0,
    .localGet 1,
    .localGet 0,
    .load32 (4 : UInt32),
    .localGet 0,
    .load32 (8 : UInt32),
    .call 54,
    .ret
  ],
  .localGet 1,
  .load32 (0 : UInt32),
  .localGet 1,
  .load32 (4 : UInt32),
  .localGet 0,
  .load32 (12 : UInt32),
  .load32 (0 : UInt32),
  .localSet 0,
  .localGet 0,
  .load32 (0 : UInt32),
  .localGet 0,
  .load32 (4 : UInt32),
  .call 53
]

def func36Def : Wasm.Function :=
  { params := [.i32, .i32], locals := [], body := func36, results := [.i32] }

def func37 : Wasm.Program :=
  [
  .localGet 0,
  .const (1048944 : UInt32),
  .store32 (4 : UInt32),
  .localGet 0,
  .localGet 1,
  .store32 (0 : UInt32)
]

def func37Def : Wasm.Function :=
  { params := [.i32, .i32], locals := [], body := func37, results := [] }

def func38 : Wasm.Program :=
  [
  .localGet 0,
  .localGet 1,
  .load64 (0 : UInt32),
  .store64 (0 : UInt32)
]

def func38Def : Wasm.Function :=
  { params := [.i32, .i32], locals := [], body := func38, results := [] }

def func39 : Wasm.Program :=
  [
  .localGet 1,
  .load32 (4 : UInt32),
  .localSet 2,
  .localGet 1,
  .load32 (0 : UInt32),
  .localSet 3,
  .call 6,
  .block 0 0 [
    .const (8 : UInt32),
    .const (4 : UInt32),
    .call 3,
    .localSet 1,
    .localGet 1,
    .br_if 0,
    .const (4 : UInt32),
    .const (8 : UInt32),
    .call 49,
    .unreachable
  ],
  .localGet 1,
  .localGet 2,
  .store32 (4 : UInt32),
  .localGet 1,
  .localGet 3,
  .store32 (0 : UInt32),
  .localGet 0,
  .const (1048944 : UInt32),
  .store32 (4 : UInt32),
  .localGet 0,
  .localGet 1,
  .store32 (0 : UInt32)
]

def func39Def : Wasm.Function :=
  { params := [.i32, .i32], locals := [.i32, .i32], body := func39, results := [] }

def func40 : Wasm.Program :=
  [
  .localGet 1,
  .localGet 0,
  .load32 (0 : UInt32),
  .localGet 0,
  .load32 (4 : UInt32),
  .call 54
]

def func40Def : Wasm.Function :=
  { params := [.i32, .i32], locals := [], body := func40, results := [.i32] }

def func41 : Wasm.Program :=
  [
  .localGet 0,
  .load32 (8 : UInt32),
  .localSet 2,
  .block 0 0 [
    .block 0 0 [
      .localGet 1,
      .const (128 : UInt32),
      .geU,
      .br_if 0,
      .const (1 : UInt32),
      .localSet 3,
      .br 1
    ],
    .block 0 0 [
      .localGet 1,
      .const (2048 : UInt32),
      .geU,
      .br_if 0,
      .const (2 : UInt32),
      .localSet 3,
      .br 1
    ],
    .const (3 : UInt32),
    .const (4 : UInt32),
    .localGet 1,
    .const (65536 : UInt32),
    .ltU,
    .select,
    .localSet 3
  ],
  .localGet 2,
  .localSet 4,
  .block 0 0 [
    .localGet 3,
    .localGet 0,
    .load32 (0 : UInt32),
    .localGet 2,
    .sub,
    .leU,
    .br_if 0,
    .localGet 0,
    .localGet 2,
    .localGet 3,
    .const (1 : UInt32),
    .const (1 : UInt32),
    .call 8,
    .localGet 0,
    .load32 (8 : UInt32),
    .localSet 4
  ],
  .localGet 0,
  .load32 (4 : UInt32),
  .localGet 4,
  .add,
  .localSet 4,
  .block 0 0 [
    .block 0 0 [
      .localGet 1,
      .const (128 : UInt32),
      .ltU,
      .br_if 0,
      .localGet 1,
      .const (63 : UInt32),
      .and,
      .const (4294967168 : UInt32),
      .or,
      .localSet 5,
      .localGet 1,
      .const (6 : UInt32),
      .shrU,
      .localSet 6,
      .block 0 0 [
        .localGet 1,
        .const (2048 : UInt32),
        .geU,
        .br_if 0,
        .localGet 4,
        .localGet 5,
        .store8 (1 : UInt32),
        .localGet 4,
        .localGet 6,
        .const (192 : UInt32),
        .or,
        .store8 (0 : UInt32),
        .br 2
      ],
      .localGet 1,
      .const (12 : UInt32),
      .shrU,
      .localSet 7,
      .localGet 6,
      .const (63 : UInt32),
      .and,
      .const (4294967168 : UInt32),
      .or,
      .localSet 6,
      .block 0 0 [
        .localGet 1,
        .const (65535 : UInt32),
        .gtU,
        .br_if 0,
        .localGet 4,
        .localGet 5,
        .store8 (2 : UInt32),
        .localGet 4,
        .localGet 6,
        .store8 (1 : UInt32),
        .localGet 4,
        .localGet 7,
        .const (224 : UInt32),
        .or,
        .store8 (0 : UInt32),
        .br 2
      ],
      .localGet 4,
      .localGet 5,
      .store8 (3 : UInt32),
      .localGet 4,
      .localGet 6,
      .store8 (2 : UInt32),
      .localGet 4,
      .localGet 7,
      .const (63 : UInt32),
      .and,
      .const (4294967168 : UInt32),
      .or,
      .store8 (1 : UInt32),
      .localGet 4,
      .localGet 1,
      .const (18 : UInt32),
      .shrU,
      .const (4294967280 : UInt32),
      .or,
      .store8 (0 : UInt32),
      .br 1
    ],
    .localGet 4,
    .localGet 1,
    .store8 (0 : UInt32)
  ],
  .localGet 0,
  .localGet 3,
  .localGet 2,
  .add,
  .store32 (8 : UInt32),
  .const (0 : UInt32)
]

def func41Def : Wasm.Function :=
  { params := [.i32, .i32], locals := [.i32, .i32, .i32, .i32, .i32, .i32], body := func41, results := [.i32] }

def func42 : Wasm.Program :=
  [
  .block 0 0 [
    .block 0 0 [
      .block 0 0 [
        .localGet 2,
        .localGet 0,
        .load32 (0 : UInt32),
        .localGet 0,
        .load32 (8 : UInt32),
        .localSet 3,
        .localGet 3,
        .sub,
        .leU,
        .br_if 0,
        .localGet 0,
        .localGet 3,
        .localGet 2,
        .const (1 : UInt32),
        .const (1 : UInt32),
        .call 8,
        .localGet 0,
        .load32 (8 : UInt32),
        .localSet 3,
        .br 1
      ],
      .localGet 2,
      .eqz,
      .br_if 1
    ],
    .localGet 2,
    .eqz,
    .br_if 0,
    .localGet 0,
    .load32 (4 : UInt32),
    .localGet 3,
    .add,
    .localGet 1,
    .localGet 2,
    .memoryCopy
  ],
  .localGet 0,
  .localGet 3,
  .localGet 2,
  .add,
  .store32 (8 : UInt32),
  .const (0 : UInt32)
]

def func42Def : Wasm.Function :=
  { params := [.i32, .i32, .i32], locals := [.i32], body := func42, results := [.i32] }

def func43 : Wasm.Program :=
  [
  .globalGet 0,
  .const (32 : UInt32),
  .sub,
  .localSet 2,
  .localGet 2,
  .globalSet 0,
  .block 0 0 [
    .localGet 1,
    .load32 (0 : UInt32),
    .const (2147483648 : UInt32),
    .ne,
    .br_if 0,
    .localGet 1,
    .load32 (12 : UInt32),
    .localSet 3,
    .localGet 2,
    .const (0 : UInt32),
    .store32 (28 : UInt32),
    .localGet 2,
    .constI64 (4294967296 : UInt64),
    .store64 (20 : UInt32),
    .localGet 2,
    .const (20 : UInt32),
    .add,
    .const (1048660 : UInt32),
    .localGet 3,
    .load32 (0 : UInt32),
    .localSet 3,
    .localGet 3,
    .load32 (0 : UInt32),
    .localGet 3,
    .load32 (4 : UInt32),
    .call 53,
    .drop,
    .localGet 2,
    .localGet 2,
    .load32 (28 : UInt32),
    .localSet 3,
    .localGet 3,
    .store32 (16 : UInt32),
    .localGet 2,
    .localGet 2,
    .load64 (20 : UInt32),
    .localSet 4,
    .localGet 4,
    .store64 (8 : UInt32),
    .localGet 1,
    .localGet 3,
    .store32 (8 : UInt32),
    .localGet 1,
    .localGet 4,
    .store64 (0 : UInt32)
  ],
  .localGet 0,
  .const (1048960 : UInt32),
  .store32 (4 : UInt32),
  .localGet 0,
  .localGet 1,
  .store32 (0 : UInt32),
  .localGet 2,
  .const (32 : UInt32),
  .add,
  .globalSet 0
]

def func43Def : Wasm.Function :=
  { params := [.i32, .i32], locals := [.i32, .i32, .i64], body := func43, results := [] }

def func44 : Wasm.Program :=
  [
  .globalGet 0,
  .const (48 : UInt32),
  .sub,
  .localSet 2,
  .localGet 2,
  .globalSet 0,
  .block 0 0 [
    .localGet 1,
    .load32 (0 : UInt32),
    .const (2147483648 : UInt32),
    .ne,
    .br_if 0,
    .localGet 1,
    .load32 (12 : UInt32),
    .localSet 3,
    .localGet 2,
    .const (0 : UInt32),
    .store32 (44 : UInt32),
    .localGet 2,
    .constI64 (4294967296 : UInt64),
    .store64 (36 : UInt32),
    .localGet 2,
    .const (36 : UInt32),
    .add,
    .const (1048660 : UInt32),
    .localGet 3,
    .load32 (0 : UInt32),
    .localSet 3,
    .localGet 3,
    .load32 (0 : UInt32),
    .localGet 3,
    .load32 (4 : UInt32),
    .call 53,
    .drop,
    .localGet 2,
    .localGet 2,
    .load32 (44 : UInt32),
    .localSet 3,
    .localGet 3,
    .store32 (32 : UInt32),
    .localGet 2,
    .localGet 2,
    .load64 (36 : UInt32),
    .localSet 4,
    .localGet 4,
    .store64 (24 : UInt32),
    .localGet 1,
    .localGet 3,
    .store32 (8 : UInt32),
    .localGet 1,
    .localGet 4,
    .store64 (0 : UInt32)
  ],
  .localGet 1,
  .load32 (8 : UInt32),
  .localSet 3,
  .localGet 1,
  .const (0 : UInt32),
  .store32 (8 : UInt32),
  .localGet 1,
  .load64 (0 : UInt32),
  .localSet 4,
  .localGet 1,
  .constI64 (4294967296 : UInt64),
  .store64 (0 : UInt32),
  .localGet 2,
  .localGet 3,
  .store32 (16 : UInt32),
  .localGet 2,
  .localGet 4,
  .store64 (8 : UInt32),
  .call 6,
  .block 0 0 [
    .const (12 : UInt32),
    .const (4 : UInt32),
    .call 3,
    .localSet 1,
    .localGet 1,
    .br_if 0,
    .const (4 : UInt32),
    .const (12 : UInt32),
    .call 49,
    .unreachable
  ],
  .localGet 1,
  .localGet 2,
  .load32 (16 : UInt32),
  .store32 (8 : UInt32),
  .localGet 1,
  .localGet 2,
  .load64 (8 : UInt32),
  .store64 (0 : UInt32),
  .localGet 0,
  .const (1048960 : UInt32),
  .store32 (4 : UInt32),
  .localGet 0,
  .localGet 1,
  .store32 (0 : UInt32),
  .localGet 2,
  .const (48 : UInt32),
  .add,
  .globalSet 0
]

def func44Def : Wasm.Function :=
  { params := [.i32, .i32], locals := [.i32, .i32, .i64], body := func44, results := [] }

def func45 : Wasm.Program :=
  [
  .localGet 0,
  .const (0 : UInt32),
  .store32 (0 : UInt32)
]

def func45Def : Wasm.Function :=
  { params := [.i32, .i32], locals := [], body := func45, results := [] }

def func46 : Wasm.Program :=
  [
  .localGet 0,
  .const (1048660 : UInt32),
  .localGet 1,
  .localGet 2,
  .call 53
]

def func46Def : Wasm.Function :=
  { params := [.i32, .i32, .i32], locals := [], body := func46, results := [.i32] }

def func47 : Wasm.Program :=
  [
  .block 0 0 [
    .block 0 0 [
      .localGet 2,
      .const (16 : UInt32),
      .shrU,
      .localGet 2,
      .const (65535 : UInt32),
      .and,
      .const (0 : UInt32),
      .ne,
      .add,
      .localSet 2,
      .localGet 2,
      .memoryGrow,
      .localSet 3,
      .localGet 3,
      .const (4294967295 : UInt32),
      .ne,
      .br_if 0,
      .const (0 : UInt32),
      .localSet 2,
      .const (0 : UInt32),
      .localSet 4,
      .br 1
    ],
    .localGet 2,
    .const (16 : UInt32),
    .shl,
    .localSet 4,
    .localGet 4,
    .const (4294967280 : UInt32),
    .add,
    .localGet 4,
    .localGet 3,
    .const (16 : UInt32),
    .shl,
    .localSet 2,
    .localGet 2,
    .const (0 : UInt32),
    .localGet 4,
    .sub,
    .eq,
    .select,
    .localSet 4
  ],
  .localGet 0,
  .const (0 : UInt32),
  .store32 (8 : UInt32),
  .localGet 0,
  .localGet 4,
  .store32 (4 : UInt32),
  .localGet 0,
  .localGet 2,
  .store32 (0 : UInt32)
]

def func47Def : Wasm.Function :=
  { params := [.i32, .i32, .i32], locals := [.i32, .i32], body := func47, results := [] }

def func48 : Wasm.Program :=
  [
  .block 0 0 [
    .localGet 0,
    .eqz,
    .br_if 0,
    .localGet 0,
    .localGet 1,
    .call 49,
    .unreachable
  ],
  .call 50,
  .unreachable
]

def func48Def : Wasm.Function :=
  { params := [.i32, .i32], locals := [], body := func48, results := [] }

def func49 : Wasm.Program :=
  [
  .localGet 1,
  .localGet 0,
  .call 30,
  .unreachable
]

def func49Def : Wasm.Function :=
  { params := [.i32, .i32], locals := [], body := func49, results := [] }

def func50 : Wasm.Program :=
  [
  .const (1049057 : UInt32),
  .const (35 : UInt32),
  .const (1049076 : UInt32),
  .call 52,
  .unreachable
]

def func50Def : Wasm.Function :=
  { params := [], locals := [], body := func50, results := [] }

def func51 : Wasm.Program :=
  [
  .localGet 0,
  .localGet 1,
  .const (1 : UInt32),
  .shl,
  .const (1 : UInt32),
  .or,
  .localGet 2,
  .call 52,
  .unreachable
]

def func51Def : Wasm.Function :=
  { params := [.i32, .i32, .i32], locals := [], body := func51, results := [] }

def func52 : Wasm.Program :=
  [
  .globalGet 0,
  .const (32 : UInt32),
  .sub,
  .localSet 3,
  .localGet 3,
  .globalSet 0,
  .localGet 3,
  .localGet 1,
  .store32 (16 : UInt32),
  .localGet 3,
  .localGet 0,
  .store32 (12 : UInt32),
  .localGet 3,
  .const (1 : UInt32),
  .store16 (28 : UInt32),
  .localGet 3,
  .localGet 2,
  .store32 (24 : UInt32),
  .localGet 3,
  .localGet 3,
  .const (12 : UInt32),
  .add,
  .store32 (20 : UInt32),
  .localGet 3,
  .const (20 : UInt32),
  .add,
  .call 29,
  .unreachable
]

def func52Def : Wasm.Function :=
  { params := [.i32, .i32, .i32], locals := [.i32], body := func52, results := [] }

def func53 : Wasm.Program :=
  [
  .globalGet 0,
  .const (16 : UInt32),
  .sub,
  .localSet 4,
  .localGet 4,
  .globalSet 0,
  .block 0 0 [
    .block 0 0 [
      .block 0 0 [
        .localGet 3,
        .const (1 : UInt32),
        .and,
        .br_if 0,
        .localGet 2,
        .load8U (0 : UInt32),
        .localSet 5,
        .localGet 5,
        .br_if 1,
        .const (0 : UInt32),
        .localSet 5,
        .br 2
      ],
      .localGet 0,
      .localGet 2,
      .localGet 3,
      .const (1 : UInt32),
      .shrU,
      .localGet 1,
      .load32 (12 : UInt32),
      .callIndirect 1 0,
      .localSet 5,
      .br 1
    ],
    .localGet 1,
    .load32 (12 : UInt32),
    .localSet 6,
    .const (0 : UInt32),
    .localSet 7,
    .loop 0 0 [
      .localGet 2,
      .const (1 : UInt32),
      .add,
      .localSet 8,
      .block 0 0 [
        .block 0 0 [
          .block 0 0 [
            .block 0 0 [
              .block 0 0 [
                .localGet 5,
                .extend8S,
                .const (4294967295 : UInt32),
                .gtS,
                .br_if 0,
                .localGet 5,
                .const (255 : UInt32),
                .and,
                .localSet 9,
                .localGet 9,
                .const (128 : UInt32),
                .eq,
                .br_if 1,
                .localGet 9,
                .const (192 : UInt32),
                .ne,
                .br_if 3,
                .localGet 4,
                .localGet 1,
                .store32 (4 : UInt32),
                .localGet 4,
                .localGet 0,
                .store32 (0 : UInt32),
                .localGet 4,
                .constI64 (1610612768 : UInt64),
                .store64 (8 : UInt32),
                .localGet 3,
                .localGet 7,
                .const (3 : UInt32),
                .shl,
                .add,
                .localSet 5,
                .localGet 5,
                .load32 (0 : UInt32),
                .localGet 4,
                .localGet 5,
                .load32 (4 : UInt32),
                .callIndirect 2 0,
                .eqz,
                .br_if 2,
                .const (1 : UInt32),
                .localSet 5,
                .br 6
              ],
              .block 0 0 [
                .localGet 0,
                .localGet 8,
                .localGet 5,
                .const (255 : UInt32),
                .and,
                .localSet 5,
                .localGet 5,
                .localGet 6,
                .callIndirect 1 0,
                .br_if 0,
                .localGet 8,
                .localGet 5,
                .add,
                .localSet 2,
                .br 4
              ],
              .const (1 : UInt32),
              .localSet 5,
              .br 5
            ],
            .block 0 0 [
              .localGet 0,
              .localGet 2,
              .const (3 : UInt32),
              .add,
              .localSet 5,
              .localGet 5,
              .localGet 2,
              .load16U (1 : UInt32),
              .localSet 2,
              .localGet 2,
              .localGet 6,
              .callIndirect 1 0,
              .br_if 0,
              .localGet 5,
              .localGet 2,
              .add,
              .localSet 2,
              .br 3
            ],
            .const (1 : UInt32),
            .localSet 5,
            .br 4
          ],
          .localGet 7,
          .const (1 : UInt32),
          .add,
          .localSet 7,
          .localGet 8,
          .localSet 2,
          .br 1
        ],
        .const (1610612768 : UInt32),
        .localSet 10,
        .block 0 0 [
          .localGet 5,
          .const (1 : UInt32),
          .and,
          .eqz,
          .br_if 0,
          .localGet 2,
          .const (5 : UInt32),
          .add,
          .localSet 8,
          .localGet 2,
          .load32 (1 : UInt32),
          .localSet 10
        ],
        .const (0 : UInt32),
        .localSet 9,
        .block 0 0 [
          .block 0 0 [
            .localGet 5,
            .const (2 : UInt32),
            .and,
            .br_if 0,
            .const (0 : UInt32),
            .localSet 11,
            .localGet 8,
            .localSet 2,
            .br 1
          ],
          .localGet 8,
          .const (2 : UInt32),
          .add,
          .localSet 2,
          .localGet 8,
          .load16U (0 : UInt32),
          .localSet 11
        ],
        .block 0 0 [
          .block 0 0 [
            .localGet 5,
            .const (4 : UInt32),
            .and,
            .br_if 0,
            .localGet 2,
            .localSet 8,
            .br 1
          ],
          .localGet 2,
          .const (2 : UInt32),
          .add,
          .localSet 8,
          .localGet 2,
          .load16U (0 : UInt32),
          .localSet 9
        ],
        .block 0 0 [
          .block 0 0 [
            .localGet 5,
            .const (8 : UInt32),
            .and,
            .br_if 0,
            .localGet 8,
            .localSet 2,
            .br 1
          ],
          .localGet 8,
          .const (2 : UInt32),
          .add,
          .localSet 2,
          .localGet 8,
          .load16U (0 : UInt32),
          .localSet 7
        ],
        .block 0 0 [
          .localGet 5,
          .const (16 : UInt32),
          .and,
          .eqz,
          .br_if 0,
          .localGet 3,
          .localGet 11,
          .const (65535 : UInt32),
          .and,
          .const (3 : UInt32),
          .shl,
          .add,
          .load16U (4 : UInt32),
          .localSet 11
        ],
        .block 0 0 [
          .localGet 5,
          .const (32 : UInt32),
          .and,
          .eqz,
          .br_if 0,
          .localGet 3,
          .localGet 9,
          .const (65535 : UInt32),
          .and,
          .const (3 : UInt32),
          .shl,
          .add,
          .load16U (4 : UInt32),
          .localSet 9
        ],
        .localGet 4,
        .localGet 9,
        .store16 (14 : UInt32),
        .localGet 4,
        .localGet 11,
        .store16 (12 : UInt32),
        .localGet 4,
        .localGet 10,
        .store32 (8 : UInt32),
        .localGet 4,
        .localGet 1,
        .store32 (4 : UInt32),
        .localGet 4,
        .localGet 0,
        .store32 (0 : UInt32),
        .block 0 0 [
          .localGet 3,
          .localGet 7,
          .const (3 : UInt32),
          .shl,
          .add,
          .localSet 5,
          .localGet 5,
          .load32 (0 : UInt32),
          .localGet 4,
          .localGet 5,
          .load32 (4 : UInt32),
          .callIndirect 2 0,
          .eqz,
          .br_if 0,
          .const (1 : UInt32),
          .localSet 5,
          .br 3
        ],
        .localGet 7,
        .const (1 : UInt32),
        .add,
        .localSet 7
      ],
      .localGet 2,
      .load8U (0 : UInt32),
      .localSet 5,
      .localGet 5,
      .br_if 0
    ],
    .const (0 : UInt32),
    .localSet 5
  ],
  .localGet 4,
  .const (16 : UInt32),
  .add,
  .globalSet 0,
  .localGet 5
]

def func53Def : Wasm.Function :=
  { params := [.i32, .i32, .i32, .i32], locals := [.i32, .i32, .i32, .i32, .i32, .i32, .i32, .i32], body := func53, results := [.i32] }

def func54 : Wasm.Program :=
  [
  .localGet 0,
  .load32 (0 : UInt32),
  .localGet 1,
  .localGet 2,
  .localGet 0,
  .load32 (4 : UInt32),
  .load32 (12 : UInt32),
  .callIndirect 1 0
]

def func54Def : Wasm.Function :=
  { params := [.i32, .i32, .i32], locals := [], body := func54, results := [.i32] }

def «module» : Wasm.Module :=
{
  imports := [],
  funcs := [
    func0Def,
    func1Def,
    func2Def,
    func3Def,
    func4Def,
    func5Def,
    func6Def,
    func7Def,
    func8Def,
    func9Def,
    func10Def,
    func11Def,
    func12Def,
    func13Def,
    func14Def,
    func15Def,
    func16Def,
    func17Def,
    func18Def,
    func19Def,
    func20Def,
    func21Def,
    func22Def,
    func23Def,
    func24Def,
    func25Def,
    func26Def,
    func27Def,
    func28Def,
    func29Def,
    func30Def,
    func31Def,
    func32Def,
    func33Def,
    func34Def,
    func35Def,
    func36Def,
    func37Def,
    func38Def,
    func39Def,
    func40Def,
    func41Def,
    func42Def,
    func43Def,
    func44Def,
    func45Def,
    func46Def,
    func47Def,
    func48Def,
    func49Def,
    func50Def,
    func51Def,
    func52Def,
    func53Def,
    func54Def
  ],
  exports := [
    { name := "check", funcIdx := 2 }
  ],
  memory := some { pagesMin := (17 : UInt32), pagesMax := none, data := [
    { offset := some (1048576 : UInt32), bytes := [(105 : UInt8), (110 : UInt8), (116 : UInt8), (101 : UInt8), (114 : UInt8), (110 : UInt8), (97 : UInt8), (108 : UInt8), (32 : UInt8), (101 : UInt8), (114 : UInt8), (114 : UInt8), (111 : UInt8), (114 : UInt8), (58 : UInt8), (32 : UInt8), (101 : UInt8), (110 : UInt8), (116 : UInt8), (101 : UInt8), (114 : UInt8), (101 : UInt8), (100 : UInt8), (32 : UInt8), (117 : UInt8), (110 : UInt8), (114 : UInt8), (101 : UInt8), (97 : UInt8), (99 : UInt8), (104 : UInt8), (97 : UInt8), (98 : UInt8), (108 : UInt8), (101 : UInt8), (32 : UInt8), (99 : UInt8), (111 : UInt8), (100 : UInt8), (101 : UInt8), (102 : UInt8), (108 : UInt8), (111 : UInt8), (97 : UInt8), (116 : UInt8), (95 : UInt8), (116 : UInt8), (114 : UInt8), (117 : UInt8), (110 : UInt8), (99 : UInt8), (47 : UInt8), (115 : UInt8), (114 : UInt8), (99 : UInt8), (47 : UInt8), (101 : UInt8), (120 : UInt8), (112 : UInt8), (111 : UInt8), (114 : UInt8), (116 : UInt8), (115 : UInt8), (46 : UInt8), (114 : UInt8), (115 : UInt8), (0 : UInt8), (0 : UInt8), (40 : UInt8), (0 : UInt8), (16 : UInt8), (0 : UInt8), (26 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (20 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (9 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (2 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (12 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (4 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (3 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (4 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (5 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (8 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (4 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (6 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (7 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (8 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (9 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (10 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (16 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (4 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (11 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (12 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (13 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (14 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (109 : UInt8), (93 : UInt8), (203 : UInt8), (214 : UInt8), (44 : UInt8), (80 : UInt8), (235 : UInt8), (99 : UInt8), (120 : UInt8), (65 : UInt8), (166 : UInt8), (87 : UInt8), (113 : UInt8), (27 : UInt8), (139 : UInt8), (185 : UInt8), (21 : UInt8), (162 : UInt8), (92 : UInt8), (85 : UInt8), (52 : UInt8), (85 : UInt8), (7 : UInt8), (212 : UInt8), (83 : UInt8), (120 : UInt8), (173 : UInt8), (129 : UInt8), (81 : UInt8), (240 : UInt8), (163 : UInt8), (247 : UInt8), (47 : UInt8), (114 : UInt8), (117 : UInt8), (115 : UInt8), (116 : UInt8), (47 : UInt8), (100 : UInt8), (101 : UInt8), (112 : UInt8), (115 : UInt8), (47 : UInt8), (100 : UInt8), (108 : UInt8), (109 : UInt8), (97 : UInt8), (108 : UInt8), (108 : UInt8), (111 : UInt8), (99 : UInt8), (45 : UInt8), (48 : UInt8), (46 : UInt8), (50 : UInt8), (46 : UInt8), (49 : UInt8), (49 : UInt8), (47 : UInt8), (115 : UInt8), (114 : UInt8), (99 : UInt8), (47 : UInt8), (100 : UInt8), (108 : UInt8), (109 : UInt8), (97 : UInt8), (108 : UInt8), (108 : UInt8), (111 : UInt8), (99 : UInt8), (46 : UInt8), (114 : UInt8), (115 : UInt8), (0 : UInt8), (97 : UInt8), (115 : UInt8), (115 : UInt8), (101 : UInt8), (114 : UInt8), (116 : UInt8), (105 : UInt8), (111 : UInt8), (110 : UInt8), (32 : UInt8), (102 : UInt8), (97 : UInt8), (105 : UInt8), (108 : UInt8), (101 : UInt8), (100 : UInt8), (58 : UInt8), (32 : UInt8), (112 : UInt8), (115 : UInt8), (105 : UInt8), (122 : UInt8), (101 : UInt8), (32 : UInt8), (62 : UInt8), (61 : UInt8), (32 : UInt8), (115 : UInt8), (105 : UInt8), (122 : UInt8), (101 : UInt8), (32 : UInt8), (43 : UInt8), (32 : UInt8), (109 : UInt8), (105 : UInt8), (110 : UInt8), (95 : UInt8), (111 : UInt8), (118 : UInt8), (101 : UInt8), (114 : UInt8), (104 : UInt8), (101 : UInt8), (97 : UInt8), (100 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (196 : UInt8), (0 : UInt8), (16 : UInt8), (0 : UInt8), (42 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (177 : UInt8), (4 : UInt8), (0 : UInt8), (0 : UInt8), (9 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (97 : UInt8), (115 : UInt8), (115 : UInt8), (101 : UInt8), (114 : UInt8), (116 : UInt8), (105 : UInt8), (111 : UInt8), (110 : UInt8), (32 : UInt8), (102 : UInt8), (97 : UInt8), (105 : UInt8), (108 : UInt8), (101 : UInt8), (100 : UInt8), (58 : UInt8), (32 : UInt8), (112 : UInt8), (115 : UInt8), (105 : UInt8), (122 : UInt8), (101 : UInt8), (32 : UInt8), (60 : UInt8), (61 : UInt8), (32 : UInt8), (115 : UInt8), (105 : UInt8), (122 : UInt8), (101 : UInt8), (32 : UInt8), (43 : UInt8), (32 : UInt8), (109 : UInt8), (97 : UInt8), (120 : UInt8), (95 : UInt8), (111 : UInt8), (118 : UInt8), (101 : UInt8), (114 : UInt8), (104 : UInt8), (101 : UInt8), (97 : UInt8), (100 : UInt8), (0 : UInt8), (0 : UInt8), (196 : UInt8), (0 : UInt8), (16 : UInt8), (0 : UInt8), (42 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (183 : UInt8), (4 : UInt8), (0 : UInt8), (0 : UInt8), (13 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (8 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (4 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (15 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (2 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (12 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (4 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (16 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (47 : UInt8), (114 : UInt8), (117 : UInt8), (115 : UInt8), (116 : UInt8), (99 : UInt8), (47 : UInt8), (53 : UInt8), (57 : UInt8), (56 : UInt8), (48 : UInt8), (55 : UInt8), (54 : UInt8), (49 : UInt8), (54 : UInt8), (101 : UInt8), (49 : UInt8), (102 : UInt8), (97 : UInt8), (50 : UInt8), (53 : UInt8), (52 : UInt8), (48 : UInt8), (55 : UInt8), (50 : UInt8), (52 : UInt8), (98 : UInt8), (102 : UInt8), (98 : UInt8), (97 : UInt8), (99 : UInt8), (49 : UInt8), (52 : UInt8), (100 : UInt8), (55 : UInt8), (57 : UInt8), (55 : UInt8), (54 : UInt8), (100 : UInt8), (55 : UInt8), (101 : UInt8), (52 : UInt8), (97 : UInt8), (51 : UInt8), (56 : UInt8), (54 : UInt8), (48 : UInt8), (47 : UInt8), (108 : UInt8), (105 : UInt8), (98 : UInt8), (114 : UInt8), (97 : UInt8), (114 : UInt8), (121 : UInt8), (47 : UInt8), (97 : UInt8), (108 : UInt8), (108 : UInt8), (111 : UInt8), (99 : UInt8), (47 : UInt8), (115 : UInt8), (114 : UInt8), (99 : UInt8), (47 : UInt8), (114 : UInt8), (97 : UInt8), (119 : UInt8), (95 : UInt8), (118 : UInt8), (101 : UInt8), (99 : UInt8), (47 : UInt8), (109 : UInt8), (111 : UInt8), (100 : UInt8), (46 : UInt8), (114 : UInt8), (115 : UInt8), (0 : UInt8), (99 : UInt8), (97 : UInt8), (112 : UInt8), (97 : UInt8), (99 : UInt8), (105 : UInt8), (116 : UInt8), (121 : UInt8), (32 : UInt8), (111 : UInt8), (118 : UInt8), (101 : UInt8), (114 : UInt8), (102 : UInt8), (108 : UInt8), (111 : UInt8), (119 : UInt8), (0 : UInt8), (0 : UInt8), (144 : UInt8), (1 : UInt8), (16 : UInt8), (0 : UInt8), (80 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (28 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (5 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8)] }
  ] },
  globals := [
    { init := .i32 (1048576 : UInt32) },
    { init := .i32 (1049573 : UInt32) },
    { init := .i32 (1049584 : UInt32) }
  ],
  types := [
    { params := [.i32, .i32], results := [] },
    { params := [.i32, .i32, .i32], results := [.i32] },
    { params := [.i32, .i32], results := [.i32] },
    { params := [.f32], results := [.i32] },
    { params := [.f32], results := [] },
    { params := [.i32, .i32, .i32], results := [] },
    { params := [.i32, .i32, .i32, .i32], results := [.i32] },
    { params := [], results := [] },
    { params := [.i32, .i32, .i32, .i32, .i32], results := [] },
    { params := [.i32], results := [] },
    { params := [.i32, .i32, .i32, .i32, .i32, .i32], results := [] },
    { params := [.i32], results := [.i32] }
  ],
  tables := [
    { min := 17, max := some 17, elemType := .funcref }
  ],
  elements := [
    { tableIdx := some 0, offset := some 1, funcs := [some 18, some 10, some 42, some 41, some 46, some 40, some 39, some 37, some 38, some 11, some 36, some 44, some 43, some 45, some 35, some 34] }
  ]
}

end Project.FloatTrunc
lean/Project/FloatTrunc/Spec.lean lean · 175 lines
import Project.FloatTrunc.Program

/-!
# Specification for `float_trunc`

The exported `check` function asserts that `naive_trunc` (NaN/range checks + cast)
and `sat_trunc` (Rust's saturating `x as i32`) agree on every `f32` bit pattern.
The proof shows `check` always terminates normally with empty result.
-/

namespace Project.FloatTrunc.Spec

open Wasm

set_option maxRecDepth 1048576

/-! ## Efficient `∀ x : UInt32` decidability -/

/-- Countdown from n: true iff p holds for every UInt32 with toNat < n. -/
private def forallUInt32Aux (p : UInt32 → Bool) : Nat → Bool
  | 0     => true
  | n + 1 => if p (UInt32.ofNat n) then forallUInt32Aux p n else false

private theorem forallUInt32Aux_iff (p : UInt32 → Bool) (n : Nat) :
    forallUInt32Aux p n = true ↔ ∀ k : UInt32, k.toNat < n → p k = true := by
  induction n with
  | zero => simp [forallUInt32Aux]
  | succ n ih =>
    simp only [forallUInt32Aux]
    rcases Bool.eq_false_or_eq_true (p (UInt32.ofNat n)) with ht | hf
    · -- ht : p (UInt32.ofNat n) = true
      simp only [ht, ite_true, ih]
      constructor
      · intro hall k hk
        rcases (by omega : k.toNat < n ∨ k.toNat = n) with hlt | hkn
        · exact hall k hlt
        · have hke : k = UInt32.ofNat n := by
            have h0 := UInt32.ofNat_toNat (x := k)
            rw [hkn] at h0; exact h0.symm
          rw [hke]; exact ht
      · intro hall k hlt
        exact hall k (Nat.lt_succ_of_lt hlt)
    · -- hf : p (UInt32.ofNat n) = false
      simp only [hf, ite_false, Bool.false_eq_true, false_iff]
      intro hall
      have hlt : (UInt32.ofNat n).toNat < n + 1 := by
        have h1 : (UInt32.ofNat n).toNat = n % 2 ^ 32 := UInt32.toNat_ofNat'
        have h2 : n % 2 ^ 32 ≤ n := Nat.mod_le n _
        omega
      have hval := hall (UInt32.ofNat n) hlt
      simp [hf] at hval

/-- `native_decide` can decide `∀ x : UInt32, P x` via a 4B-iteration countdown. -/
private instance decidableForallUInt32 {P : UInt32 → Prop} [DecidablePred P] :
    Decidable (∀ x : UInt32, P x) :=
  let p := fun x => decide (P x)
  if h : forallUInt32Aux p UInt32.size then
    isTrue fun x =>
      of_decide_eq_true
        ((forallUInt32Aux_iff p UInt32.size).mp h x (UInt32.toNat_lt_size x))
  else
    isFalse fun hall =>
      h ((forallUInt32Aux_iff p UInt32.size).mpr fun k _ => decide_eq_true (hall k))

/-! ## Float math helpers -/

/-- Expose `private satI32S` body; provable by `rfl` since the kernel reduces it. -/
private theorem i32TruncSatF32S_expand (x : UInt32) :
    i32TruncSatF32S x =
    let f := (Float32.ofBits x).toFloat
    if f.isNaN then 0
    else let t := if f < 0.0 then f.ceil else f.floor
         if t ≤ (-2147483648.0 : Float) then 0x80000000
         else if t ≥ (2147483647.0 : Float) then 0x7FFFFFFF
         else t.toInt64.toUInt64.toUInt32 := rfl

/-- IEEE 754: `f32Ne x x = true` iff `x` encodes a NaN.
`f32Ne x x = !(f == f)` and `Float.isNaN f = !(f == f)` (both opaque externs);
checked for all 2^32 bit patterns by native evaluation. -/
private theorem f32Ne_self_iff_isNaN (x : UInt32) :
    f32Ne x x = (Float32.ofBits x).toFloat.isNaN :=
  IEEE32Exec.f32Ne_self_iff_isNaN x

private theorem i32TruncSatF32S_nan {x : UInt32}
    (h : (Float32.ofBits x).toFloat.isNaN) : i32TruncSatF32S x = 0 := by
  simp [i32TruncSatF32S_expand, h]

/-- `2^31` as a `Float32` bit pattern is `0x4F000000 = 1325400064`. When
`f ≥ 2^31`, `floor f ≥ 2^31 > 2147483647`, so `satI32S` saturates to `MAX`.
Checked for all 2^32 bit patterns by native evaluation. -/
private theorem i32TruncSatF32S_large_pos {x : UInt32}
    (hnan : f32Ne x x = false)
    (hge : f32Ge x 1325400064 = true) :
    i32TruncSatF32S x = 0x7FFFFFFF :=
  IEEE32Exec.i32TruncSatF32S_large_pos hnan hge

/-- `-2^31` as a `Float32` bit pattern is `0xCF000000 = 3472883712`. When
`f < -2^31`, `ceil f ≤ -2^31 ≤ -2147483648`, so `satI32S` saturates to `MIN`.
Checked for all 2^32 bit patterns by native evaluation. -/
private theorem i32TruncSatF32S_large_neg {x : UInt32}
    (hnan : f32Ne x x = false)
    (hlt : f32Lt x 3472883712 = true) :
    i32TruncSatF32S x = 0x80000000 :=
  IEEE32Exec.i32TruncSatF32S_large_neg hnan hlt

/-! ## Per-function termination -/

theorem func1_terminates (env : HostEnv Unit) (st : Store Unit) (x : UInt32)
    (tail : List Value) :
    TerminatesWith env «module» 1 st ([.f32 x] ++ tail)
      (fun _ rs => rs = [.i32 (i32TruncSatF32S x)] ++ tail) := by
  apply TerminatesWith.of_wp_entry_for (f := ⟨[.f32], [], func1, [.i32], none⟩) rfl
  unfold func1
  wp_run
  simp

set_option maxHeartbeats 800000 in
theorem func0_terminates (env : HostEnv Unit) (x : UInt32) :
    TerminatesWith env «module» 0 «module».initialStore [.f32 x]
      (fun _ rs => rs = [.i32 (i32TruncSatF32S x)]) := by
  have hg : («module».initialStore : Store Unit).globals.globals[0]? =
      some (.i32 1048576) := rfl
  have hp : («module».initialStore : Store Unit).mem.pages = 17 := rfl
  apply TerminatesWith.of_wp_entry_for (f := ⟨[.f32], [.i32], func0, [.i32], none⟩) rfl
  unfold func0; wp_run
  simp only [hg]
  apply wp_block_cons; apply wp_block_cons; apply wp_block_cons
  apply wp_block_cons; apply wp_block_cons; apply wp_block_cons
  wp_run
  -- Four-way case split: NaN, large-pos, large-neg, normal
  cases hnan : f32Ne x x
  · -- f32Ne x x = false → not NaN
    cases hge : f32Ge x 1325400064
    · -- not large pos
      cases hlt : f32Lt x 3472883712
      · -- normal case: func0 calls i32TruncSatF32S directly
        simp [hnan, hge, hlt, hp, Mem.write32_pages, Mem.read32_write32_same]
      · -- large neg: stores 0x80000000
        have heq := i32TruncSatF32S_large_neg hnan hlt
        simp [hnan, hge, hlt, hp, Mem.write32_pages, Mem.read32_write32_same, heq]
    · -- large pos: stores 0x7FFFFFFF
      have heq := i32TruncSatF32S_large_pos hnan hge
      simp [hnan, hge, hp, Mem.write32_pages, Mem.read32_write32_same, heq]
  · -- f32Ne x x = true → NaN: stores 0
    have hisNaN : (Float32.ofBits x).toFloat.isNaN = true :=
      (f32Ne_self_iff_isNaN x).symm.trans hnan
    have heq := i32TruncSatF32S_nan hisNaN
    simp [hnan, hp, Mem.write32_pages, Mem.read32_write32_same, heq]

/-! ## Top-level spec -/

@[spec_of "rust-exported" "float_trunc::check"]
def FloatTruncSpec : Prop :=
  ∀ (env : HostEnv Unit) (initial : Store Unit) (x : UInt32),
    initial = «module».initialStore →
    TerminatesWith env «module» 2 initial [.f32 x] (fun _ rs => rs = [])

@[proves Project.FloatTrunc.Spec.FloatTruncSpec]
theorem check_correct : FloatTruncSpec := by
  intro env initial x hinit
  subst hinit
  apply TerminatesWith.of_wp_entry_for (f := ⟨[.f32], [], func2, [], none⟩) rfl
  unfold func2
  apply wp_block_cons
  wp_run
  apply wp_call_tw (func0_terminates env x)
  rintro st0 vs0 rfl
  wp_run
  apply wp_call_tw (func1_terminates env st0 x [.i32 (i32TruncSatF32S x)])
  rintro st1 vs1 rfl
  wp_run
  simp [ne_eq]

end Project.FloatTrunc.Spec

Rust (2)

rust/float_trunc/src/exports.rs rust · 23 lines
fn naive_trunc(x: f32) -> i32 {
    if x != x {
        0
    } else if x >= 2147483648.0f32 {
        i32::MAX
    } else if x < -2147483648.0f32 {
        i32::MIN
    } else {
        x as i32
    }
}

fn sat_trunc(x: f32) -> i32 {
    x as i32
}

#[unsafe(no_mangle)]
pub extern "C" fn check(x: f32) {
    if naive_trunc(x) != sat_trunc(x) {
        unreachable!()
    }
}
rust/float_trunc/src/lib.rs rust · 2 lines
mod exports;

Other (1)

rust/float_trunc/Cargo.toml toml · 8 lines
[package]
name = "float_trunc"
version = "0.1.0"
edition = "2024"

[lib]
crate-type = ["cdylib", "rlib"]