Talos · verification report
← all projects

swap_elements verified

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

Formal specs

Project.SwapElements.Spec.SwapElementsSpec lean/Project/SwapElements/Spec.lean:323
1 proof

Informal spec

The exported swap_elements swaps two elements of a [u64] slice in place.

Given indices i, j both in bounds (< len); an array region [ptr, ptr + 8 * len) that is addressable (ptr.toNat + 8 * len.toNat ≤ pages * 65536), sits at or above the shadow-stack base (1048576 ≤ ptr, so the callee scratch frames cannot alias it), and does not wrap (pages ≤ 65536, the wasm32 limit); and the shadow-stack pointer at its initial value (global 0 = 1048576): the export terminates leaving no result and

  • the element at index i now holds the previous element at index j;
  • the element at index j now holds the previous element at index i;
  • every other in-bounds element k (k ≠ i, k ≠ j) is unchanged.

See the module docstring for why the last two hypotheses are required — without them the statement is not merely unprovable but false.

Formal statement

SwapElementsSpec : Prop :=

Proofs

↗ Project.SwapElements.Spec.swap_elements_correct

Rust binding

↗swap_elements
Wasm-exported entry point for `swap_elements`. Thin `extern "C"` wrapper around the pure [`crate::swap_elements`]. The project convention reserves this file for the wasm ABI surface, so the export table matches exactly what the verifier reasons about. Receives the array as a `(pointer, length)` pair plus the two indices to swap. On wasm32 both `usize` and the pointer are 32-bit. The caller must guarantee `i < data_length` and `j < data_length` and that `[array_ptr, array_ptr + data_length)` is a valid, aligned `u64` region.
fn swap_elements(array_ptr: *mut u64, data_length: usize, i: usize, j: usize)

References

  • rust-exported swap_elements::swap_elements

Exported functions

swap_elements rust/swap_elements/src/exports.rs:1
Wasm-exported entry point for `swap_elements`. Thin `extern "C"` wrapper around the pure [`crate::swap_elements`]. The project convention reserves this file for the wasm ABI surface, so the export table matches exactly what the verifier reasons about. Receives the array as a `(pointer, length)` pair plus the two indices to swap. On wasm32 both `usize` and the pointer are 32-bit. The caller must guarantee `i < data_length` and `j < data_length` and that `[array_ptr, array_ptr + data_length)` is a valid, aligned `u64` region.
fn swap_elements(array_ptr: *mut u64, data_length: usize, i: usize, j: usize)

Program (Lean)

Project.SwapElements.module lean/Project/SwapElements/Program.lean:7058 
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,
    func55Def,
    func56Def,
    func57Def,
    func58Def,
    func59Def,
    func60Def,
    func61Def
  ],
  exports := [
    { name := "swap_elements", funcIdx := 4 }
  ],
  memory := some { pagesMin := (17 : UInt32), pagesMax := none, data := [
    { offset := some (1048576 : UInt32), bytes := [(115 : UInt8), (119 : UInt8), (97 : UInt8), (112 : UInt8), (95 : UInt8), (101 : UInt8), (108 : UInt8), (101 : UInt8), (109 : UInt8), (101 : UInt8), (110 : UInt8), (116 : UInt8), (115 : UInt8), (47 : UInt8), (115 : UInt8), (114 : UInt8), (99 : UInt8), (47 : UInt8), (108 : UInt8), (105 : UInt8), (98 : UInt8), (46 : UInt8), (114 : UInt8), (115 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (16 : UInt8), (0 : UInt8), (24 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (9 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (9 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (115 : UInt8), (119 : UInt8), (97 : UInt8), (112 : UInt8), (95 : UInt8), (101 : UInt8), (108 : UInt8), (101 : UInt8), (109 : UInt8), (101 : UInt8), (110 : UInt8), (116 : UInt8), (115 : 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), (0 : UInt8), (0 : UInt8), (44 : UInt8), (0 : UInt8), (16 : UInt8), (0 : UInt8), (28 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (13 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (24 : 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), (204 : 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), (204 : 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), (152 : 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), (32 : UInt8), (105 : UInt8), (110 : UInt8), (100 : UInt8), (101 : UInt8), (120 : UInt8), (32 : UInt8), (111 : UInt8), (117 : UInt8), (116 : UInt8), (32 : UInt8), (111 : UInt8), (102 : UInt8), (32 : UInt8), (98 : UInt8), (111 : UInt8), (117 : UInt8), (110 : UInt8), (100 : UInt8), (115 : UInt8), (58 : UInt8), (32 : UInt8), (116 : UInt8), (104 : UInt8), (101 : UInt8), (32 : UInt8), (108 : UInt8), (101 : UInt8), (110 : UInt8), (32 : UInt8), (105 : UInt8), (115 : UInt8), (32 : UInt8), (192 : UInt8), (18 : UInt8), (32 : UInt8), (98 : UInt8), (117 : UInt8), (116 : UInt8), (32 : UInt8), (116 : UInt8), (104 : UInt8), (101 : UInt8), (32 : UInt8), (105 : UInt8), (110 : UInt8), (100 : UInt8), (101 : UInt8), (120 : UInt8), (32 : UInt8), (105 : UInt8), (115 : UInt8), (32 : UInt8), (192 : UInt8), (0 : UInt8), (48 : UInt8), (48 : UInt8), (48 : UInt8), (49 : UInt8), (48 : UInt8), (50 : UInt8), (48 : UInt8), (51 : UInt8), (48 : UInt8), (52 : UInt8), (48 : UInt8), (53 : UInt8), (48 : UInt8), (54 : UInt8), (48 : UInt8), (55 : UInt8), (48 : UInt8), (56 : UInt8), (48 : UInt8), (57 : UInt8), (49 : UInt8), (48 : UInt8), (49 : UInt8), (49 : UInt8), (49 : UInt8), (50 : UInt8), (49 : UInt8), (51 : UInt8), (49 : UInt8), (52 : UInt8), (49 : UInt8), (53 : UInt8), (49 : UInt8), (54 : UInt8), (49 : UInt8), (55 : UInt8), (49 : UInt8), (56 : UInt8), (49 : UInt8), (57 : UInt8), (50 : UInt8), (48 : UInt8), (50 : UInt8), (49 : UInt8), (50 : UInt8), (50 : UInt8), (50 : UInt8), (51 : UInt8), (50 : UInt8), (52 : UInt8), (50 : UInt8), (53 : UInt8), (50 : UInt8), (54 : UInt8), (50 : UInt8), (55 : UInt8), (50 : UInt8), (56 : UInt8), (50 : UInt8), (57 : UInt8), (51 : UInt8), (48 : UInt8), (51 : UInt8), (49 : UInt8), (51 : UInt8), (50 : UInt8), (51 : UInt8), (51 : UInt8), (51 : UInt8), (52 : UInt8), (51 : UInt8), (53 : UInt8), (51 : UInt8), (54 : UInt8), (51 : UInt8), (55 : UInt8), (51 : UInt8), (56 : UInt8), (51 : UInt8), (57 : UInt8), (52 : UInt8), (48 : UInt8), (52 : UInt8), (49 : UInt8), (52 : UInt8), (50 : UInt8), (52 : UInt8), (51 : UInt8), (52 : UInt8), (52 : UInt8), (52 : UInt8), (53 : UInt8), (52 : UInt8), (54 : UInt8), (52 : UInt8), (55 : UInt8), (52 : UInt8), (56 : UInt8), (52 : UInt8), (57 : UInt8), (53 : UInt8), (48 : UInt8), (53 : UInt8), (49 : UInt8), (53 : UInt8), (50 : UInt8), (53 : UInt8), (51 : UInt8), (53 : UInt8), (52 : UInt8), (53 : UInt8), (53 : UInt8), (53 : UInt8), (54 : UInt8), (53 : UInt8), (55 : UInt8), (53 : UInt8), (56 : UInt8), (53 : UInt8), (57 : UInt8), (54 : UInt8), (48 : UInt8), (54 : UInt8), (49 : UInt8), (54 : UInt8), (50 : UInt8), (54 : UInt8), (51 : UInt8), (54 : UInt8), (52 : UInt8), (54 : UInt8), (53 : UInt8), (54 : UInt8), (54 : UInt8), (54 : UInt8), (55 : UInt8), (54 : UInt8), (56 : UInt8), (54 : UInt8), (57 : UInt8), (55 : UInt8), (48 : UInt8), (55 : UInt8), (49 : UInt8), (55 : UInt8), (50 : UInt8), (55 : UInt8), (51 : UInt8), (55 : UInt8), (52 : UInt8), (55 : UInt8), (53 : UInt8), (55 : UInt8), (54 : UInt8), (55 : UInt8), (55 : UInt8), (55 : UInt8), (56 : UInt8), (55 : UInt8), (57 : UInt8), (56 : UInt8), (48 : UInt8), (56 : UInt8), (49 : UInt8), (56 : UInt8), (50 : UInt8), (56 : UInt8), (51 : UInt8), (56 : UInt8), (52 : UInt8), (56 : UInt8), (53 : UInt8), (56 : UInt8), (54 : UInt8), (56 : UInt8), (55 : UInt8), (56 : UInt8), (56 : UInt8), (56 : UInt8), (57 : UInt8), (57 : UInt8), (48 : UInt8), (57 : UInt8), (49 : UInt8), (57 : UInt8), (50 : UInt8), (57 : UInt8), (51 : UInt8), (57 : UInt8), (52 : UInt8), (57 : UInt8), (53 : UInt8), (57 : UInt8), (54 : UInt8), (57 : UInt8), (55 : UInt8), (57 : UInt8), (56 : UInt8), (57 : UInt8), (57 : UInt8)] }
  ] },
  globals := [
    { init := .i32 (1048576 : UInt32) },
    { init := .i32 (1049837 : UInt32) },
    { init := .i32 (1049840 : UInt32) }
  ],
  types := [
    { params := [.i32, .i32], results := [] },
    { params := [.i32, .i32, .i32], results := [.i32] },
    { params := [.i32, .i32], results := [.i32] },
    { params := [.i32, .i32, .i32, .i32], results := [] },
    { params := [.i32, .i32, .i32, .i32, .i32], results := [] },
    { params := [.i32, .i32, .i32], results := [] },
    { params := [.i32, .i32, .i32, .i32], results := [.i32] },
    { params := [], results := [] },
    { params := [.i32], results := [] },
    { params := [.i32, .i32, .i32, .i32, .i32, .i32], results := [] },
    { params := [.i32], results := [.i32] },
    { params := [.i32, .i32, .i32, .i32, .i32, .i32], results := [.i32] },
    { params := [.i32, .i32, .i32, .i32, .i32], results := [.i32] }
  ],
  tables := [
    { min := 18, max := some 18, elemType := .funcref }
  ],
  elements := [
    { tableIdx := some 0, offset := some 1, funcs := [some 20, some 12, some 44, some 43, some 48, some 42, some 41, some 39, some 40, some 13, some 38, some 46, some 45, some 47, some 37, some 36, some 61] }
  ]
}

Diagnostics

missing_informal_spec info
lean/Project/SwapElements/Spec.lean:323
spec `Project.SwapElements.Spec.SwapElementsSpec` has no `Informal spec:` block

Source files (appendix)

Lean (2)

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

import CodeLib

set_option maxRecDepth 1048576

namespace Project.SwapElements

open Wasm

def func0 : Wasm.Program :=
  [
  .localGet 0,
  .localGet 1,
  .localGet 2,
  .localGet 3,
  .const (1048604 : UInt32),
  .call 1,
  .ret
]

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

def func1 : Wasm.Program :=
  [
  .block 0 0 [
    .block 0 0 [
      .block 0 0 [
        .localGet 2,
        .localGet 1,
        .ltU,
        .const (1 : UInt32),
        .and,
        .eqz,
        .br_if 0,
        .localGet 0,
        .localGet 2,
        .const (3 : UInt32),
        .shl,
        .add,
        .localSet 5,
        .localGet 3,
        .localGet 1,
        .ltU,
        .const (1 : UInt32),
        .and,
        .br_if 1,
        .br 2
      ],
      .localGet 2,
      .localGet 1,
      .localGet 4,
      .call 56,
      .unreachable
    ],
    .localGet 5,
    .localGet 0,
    .localGet 3,
    .const (3 : UInt32),
    .shl,
    .add,
    .call 2,
    .ret
  ],
  .localGet 3,
  .localGet 1,
  .localGet 4,
  .call 56,
  .unreachable
]

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

def func2 : Wasm.Program :=
  [
  .globalGet 0,
  .const (16 : UInt32),
  .sub,
  .localSet 2,
  .localGet 2,
  .localGet 0,
  .load64 (0 : UInt32),
  .store64 (8 : UInt32),
  .localGet 0,
  .localGet 1,
  .load64 (0 : UInt32),
  .store64 (0 : UInt32),
  .localGet 1,
  .localGet 2,
  .load64 (8 : UInt32),
  .store64 (0 : UInt32),
  .ret
]

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

def func3 : Wasm.Program :=
  [
  .localGet 0,
  .localGet 2,
  .store32 (4 : UInt32),
  .localGet 0,
  .localGet 1,
  .store32 (0 : UInt32),
  .ret
]

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

/-- export: swap_elements -/
def func4 : Wasm.Program :=
  [
  .globalGet 0,
  .const (16 : UInt32),
  .sub,
  .localSet 4,
  .localGet 4,
  .globalSet 0,
  .const (1048652 : UInt32),
  .localSet 5,
  .localGet 4,
  .const (8 : UInt32),
  .add,
  .localGet 0,
  .localGet 1,
  .localGet 5,
  .call 3,
  .localGet 4,
  .load32 (12 : UInt32),
  .localSet 6,
  .localGet 4,
  .load32 (8 : UInt32),
  .localGet 6,
  .localGet 2,
  .localGet 3,
  .call 0,
  .localGet 4,
  .const (16 : UInt32),
  .add,
  .globalSet 0,
  .ret
]

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

def func5 : Wasm.Program :=
  [
  .localGet 0,
  .localGet 1,
  .call 22,
  .ret
]

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

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

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

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

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

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

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

def func9 : Wasm.Program :=
  [
  .call 25,
  .unreachable
]

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

def func10 : 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 50,
    .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 18,
  .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 50,
    .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 func10Def : Wasm.Function :=
  { params := [.i32, .i32, .i32, .i32, .i32], locals := [.i32], body := func10, results := [] }

def func11 : 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 6
  ]
]

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

def func12 : 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 6
  ]
]

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

def func13 : 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 6
  ]
]

def func13Def : Wasm.Function :=
  { params := [.i32], locals := [.i32], 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 :=
  [
  .localGet 0,
  .load32 (0 : UInt32),
  .localGet 0,
  .load32 (4 : UInt32),
  .const (0 : UInt32),
  .load32 (1049364 : UInt32),
  .localSet 0,
  .localGet 0,
  .const (1 : UInt32),
  .localGet 0,
  .select,
  .callIndirect 0 0,
  .unreachable
]

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

def func16 : Wasm.Program :=
  [
  .localGet 0,
  .call 17,
  .unreachable
]

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

def func17 : 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 (1048692 : UInt32),
    .localGet 0,
    .load32 (4 : UInt32),
    .localGet 0,
    .load32 (8 : UInt32),
    .localSet 0,
    .localGet 0,
    .load8U (8 : UInt32),
    .localGet 0,
    .load8U (9 : UInt32),
    .call 19,
    .unreachable
  ],
  .localGet 1,
  .const (2147483648 : UInt32),
  .store32 (0 : UInt32),
  .localGet 1,
  .localGet 0,
  .store32 (12 : UInt32),
  .localGet 1,
  .const (1048720 : UInt32),
  .localGet 0,
  .load32 (4 : UInt32),
  .localGet 0,
  .load32 (8 : UInt32),
  .localSet 0,
  .localGet 0,
  .load8U (8 : UInt32),
  .localGet 0,
  .load8U (9 : UInt32),
  .call 19,
  .unreachable
]

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

def func18 : 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 7,
            .localSet 7,
            .br 1
          ],
          .block 0 0 [
            .localGet 3,
            .br_if 0,
            .localGet 4,
            .localSet 7,
            .br 2
          ],
          .call 8,
          .localGet 3,
          .localGet 4,
          .call 5,
          .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 func18Def : Wasm.Function :=
  { params := [.i32, .i32, .i32, .i32, .i32, .i32], locals := [.i32, .i32, .i64], body := func18, results := [] }

def func19 : 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 35,
            .const (255 : UInt32),
            .and,
            .brTable [4, 1, 0] 1
          ],
          .const (0 : UInt32),
          .load32 (1049368 : UInt32),
          .localSet 6,
          .localGet 6,
          .const (4294967295 : UInt32),
          .leS,
          .br_if 3,
          .const (0 : UInt32),
          .localGet 6,
          .const (1 : UInt32),
          .add,
          .store32 (1049368 : UInt32),
          .const (0 : UInt32),
          .load32 (1049372 : 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 (1049372 : UInt32),
          .localGet 5,
          .const (16 : UInt32),
          .add,
          .const (0 : UInt32),
          .load32 (1049376 : 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 11
    ],
    .const (0 : UInt32),
    .const (0 : UInt32),
    .load32 (1049368 : UInt32),
    .const (4294967295 : UInt32),
    .add,
    .store32 (1049368 : UInt32),
    .const (0 : UInt32),
    .const (0 : UInt32),
    .store8 (1049360 : UInt32),
    .localGet 3,
    .eqz,
    .br_if 0,
    .localGet 0,
    .localGet 1,
    .call 21,
    .unreachable
  ],
  .unreachable
]

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

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

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

def func21 : Wasm.Program :=
  [
  .localGet 0,
  .localGet 1,
  .call 9,
  .drop,
  .unreachable
]

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

def func22 : Wasm.Program :=
  [
  .block 0 0 [
    .localGet 1,
    .const (9 : UInt32),
    .ltU,
    .br_if 0,
    .localGet 1,
    .localGet 0,
    .call 23,
    .ret
  ],
  .localGet 0,
  .call 24
]

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

def func23 : 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 24,
    .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 30,
        .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 30
    ],
    .localGet 0,
    .const (8 : UInt32),
    .add,
    .localSet 2
  ],
  .localGet 2
]

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

def func24 : 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 (1049796 : 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 (1049792 : 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 (1049528 : UInt32),
                    .add,
                    .localSet 0,
                    .localGet 0,
                    .localGet 3,
                    .const (1049536 : 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 (1049800 : UInt32),
                  .leU,
                  .br_if 6,
                  .localGet 0,
                  .br_if 2,
                  .const (0 : UInt32),
                  .load32 (1049796 : UInt32),
                  .localSet 0,
                  .localGet 0,
                  .eqz,
                  .br_if 6,
                  .localGet 0,
                  .ctz,
                  .const (2 : UInt32),
                  .shl,
                  .const (1049384 : 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 (1049384 : 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 (1049792 : 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 (1049528 : UInt32),
                .add,
                .localSet 8,
                .localGet 8,
                .localGet 2,
                .const (1049536 : 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 (1049792 : 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 (1049800 : UInt32),
              .localSet 2,
              .localGet 2,
              .eqz,
              .br_if 0,
              .const (0 : UInt32),
              .load32 (1049808 : UInt32),
              .localSet 3,
              .block 0 0 [
                .block 0 0 [
                  .const (0 : UInt32),
                  .load32 (1049792 : 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 (1049792 : UInt32),
                  .localGet 2,
                  .const (4294967288 : UInt32),
                  .and,
                  .const (1049528 : UInt32),
                  .add,
                  .localSet 2,
                  .localGet 2,
                  .localSet 7,
                  .br 1
                ],
                .localGet 2,
                .const (4294967288 : UInt32),
                .and,
                .localSet 2,
                .localGet 2,
                .const (1049528 : UInt32),
                .add,
                .localSet 7,
                .localGet 2,
                .const (1049536 : 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 (1049808 : UInt32),
            .const (0 : UInt32),
            .localGet 8,
            .store32 (1049800 : UInt32),
            .br 4
          ],
          .const (0 : UInt32),
          .const (0 : UInt32),
          .load32 (1049796 : UInt32),
          .const (4294967294 : UInt32),
          .localGet 6,
          .load32 (28 : UInt32),
          .rotl,
          .and,
          .store32 (1049796 : 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 (1049800 : UInt32),
              .localSet 7,
              .localGet 7,
              .eqz,
              .br_if 1,
              .const (0 : UInt32),
              .load32 (1049808 : UInt32),
              .localSet 0,
              .block 0 0 [
                .block 0 0 [
                  .const (0 : UInt32),
                  .load32 (1049792 : 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 (1049792 : UInt32),
                  .localGet 7,
                  .const (4294967288 : UInt32),
                  .and,
                  .const (1049528 : UInt32),
                  .add,
                  .localSet 7,
                  .localGet 7,
                  .localSet 9,
                  .br 1
                ],
                .localGet 7,
                .const (4294967288 : UInt32),
                .and,
                .localSet 7,
                .localGet 7,
                .const (1049528 : UInt32),
                .add,
                .localSet 9,
                .localGet 7,
                .const (1049536 : 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 (1049808 : UInt32),
          .const (0 : UInt32),
          .localGet 2,
          .store32 (1049800 : 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 (1049384 : 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 (1049384 : 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 (1049800 : 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 (1049384 : 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 (1049796 : UInt32),
        .const (4294967294 : UInt32),
        .localGet 8,
        .load32 (28 : UInt32),
        .rotl,
        .and,
        .store32 (1049796 : 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 34,
            .br 2
          ],
          .block 0 0 [
            .block 0 0 [
              .const (0 : UInt32),
              .load32 (1049792 : 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 (1049792 : UInt32),
              .localGet 2,
              .const (248 : UInt32),
              .and,
              .const (1049528 : UInt32),
              .add,
              .localSet 2,
              .localGet 2,
              .localSet 6,
              .br 1
            ],
            .localGet 2,
            .const (248 : UInt32),
            .and,
            .localSet 2,
            .localGet 2,
            .const (1049528 : UInt32),
            .add,
            .localSet 6,
            .localGet 2,
            .const (1049536 : 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 (1049800 : UInt32),
                .localSet 0,
                .localGet 0,
                .localGet 3,
                .geU,
                .br_if 0,
                .block 0 0 [
                  .const (0 : UInt32),
                  .load32 (1049804 : UInt32),
                  .localSet 0,
                  .localGet 0,
                  .localGet 3,
                  .gtU,
                  .br_if 0,
                  .localGet 1,
                  .const (4 : UInt32),
                  .add,
                  .const (1049836 : UInt32),
                  .localGet 3,
                  .const (65583 : UInt32),
                  .add,
                  .const (4294901760 : UInt32),
                  .and,
                  .call 49,
                  .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 (1049816 : UInt32),
                  .localGet 1,
                  .load32 (8 : UInt32),
                  .localSet 9,
                  .localGet 9,
                  .add,
                  .localSet 0,
                  .localGet 0,
                  .store32 (1049816 : UInt32),
                  .const (0 : UInt32),
                  .localGet 0,
                  .const (0 : UInt32),
                  .load32 (1049820 : UInt32),
                  .localSet 2,
                  .localGet 2,
                  .localGet 0,
                  .localGet 2,
                  .gtU,
                  .select,
                  .store32 (1049820 : UInt32),
                  .block 0 0 [
                    .block 0 0 [
                      .block 0 0 [
                        .const (0 : UInt32),
                        .load32 (1049812 : UInt32),
                        .localSet 2,
                        .localGet 2,
                        .eqz,
                        .br_if 0,
                        .const (1049512 : 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 (1049828 : UInt32),
                          .localSet 0,
                          .localGet 0,
                          .eqz,
                          .br_if 0,
                          .localGet 6,
                          .localGet 0,
                          .geU,
                          .br_if 1
                        ],
                        .const (0 : UInt32),
                        .localGet 6,
                        .store32 (1049828 : UInt32)
                      ],
                      .const (0 : UInt32),
                      .const (4095 : UInt32),
                      .store32 (1049832 : UInt32),
                      .const (0 : UInt32),
                      .localGet 5,
                      .store32 (1049524 : UInt32),
                      .const (0 : UInt32),
                      .localGet 9,
                      .store32 (1049516 : UInt32),
                      .const (0 : UInt32),
                      .localGet 6,
                      .store32 (1049512 : UInt32),
                      .const (0 : UInt32),
                      .const (1049528 : UInt32),
                      .store32 (1049540 : UInt32),
                      .const (0 : UInt32),
                      .const (1049536 : UInt32),
                      .store32 (1049548 : UInt32),
                      .const (0 : UInt32),
                      .const (1049528 : UInt32),
                      .store32 (1049536 : UInt32),
                      .const (0 : UInt32),
                      .const (1049544 : UInt32),
                      .store32 (1049556 : UInt32),
                      .const (0 : UInt32),
                      .const (1049536 : UInt32),
                      .store32 (1049544 : UInt32),
                      .const (0 : UInt32),
                      .const (1049552 : UInt32),
                      .store32 (1049564 : UInt32),
                      .const (0 : UInt32),
                      .const (1049544 : UInt32),
                      .store32 (1049552 : UInt32),
                      .const (0 : UInt32),
                      .const (1049560 : UInt32),
                      .store32 (1049572 : UInt32),
                      .const (0 : UInt32),
                      .const (1049552 : UInt32),
                      .store32 (1049560 : UInt32),
                      .const (0 : UInt32),
                      .const (1049568 : UInt32),
                      .store32 (1049580 : UInt32),
                      .const (0 : UInt32),
                      .const (1049560 : UInt32),
                      .store32 (1049568 : UInt32),
                      .const (0 : UInt32),
                      .const (1049576 : UInt32),
                      .store32 (1049588 : UInt32),
                      .const (0 : UInt32),
                      .const (1049568 : UInt32),
                      .store32 (1049576 : UInt32),
                      .const (0 : UInt32),
                      .const (1049584 : UInt32),
                      .store32 (1049596 : UInt32),
                      .const (0 : UInt32),
                      .const (1049576 : UInt32),
                      .store32 (1049584 : UInt32),
                      .const (0 : UInt32),
                      .const (1049592 : UInt32),
                      .store32 (1049604 : UInt32),
                      .const (0 : UInt32),
                      .const (1049584 : UInt32),
                      .store32 (1049592 : UInt32),
                      .const (0 : UInt32),
                      .const (1049592 : UInt32),
                      .store32 (1049600 : UInt32),
                      .const (0 : UInt32),
                      .const (1049600 : UInt32),
                      .store32 (1049612 : UInt32),
                      .const (0 : UInt32),
                      .const (1049600 : UInt32),
                      .store32 (1049608 : UInt32),
                      .const (0 : UInt32),
                      .const (1049608 : UInt32),
                      .store32 (1049620 : UInt32),
                      .const (0 : UInt32),
                      .const (1049608 : UInt32),
                      .store32 (1049616 : UInt32),
                      .const (0 : UInt32),
                      .const (1049616 : UInt32),
                      .store32 (1049628 : UInt32),
                      .const (0 : UInt32),
                      .const (1049616 : UInt32),
                      .store32 (1049624 : UInt32),
                      .const (0 : UInt32),
                      .const (1049624 : UInt32),
                      .store32 (1049636 : UInt32),
                      .const (0 : UInt32),
                      .const (1049624 : UInt32),
                      .store32 (1049632 : UInt32),
                      .const (0 : UInt32),
                      .const (1049632 : UInt32),
                      .store32 (1049644 : UInt32),
                      .const (0 : UInt32),
                      .const (1049632 : UInt32),
                      .store32 (1049640 : UInt32),
                      .const (0 : UInt32),
                      .const (1049640 : UInt32),
                      .store32 (1049652 : UInt32),
                      .const (0 : UInt32),
                      .const (1049640 : UInt32),
                      .store32 (1049648 : UInt32),
                      .const (0 : UInt32),
                      .const (1049648 : UInt32),
                      .store32 (1049660 : UInt32),
                      .const (0 : UInt32),
                      .const (1049648 : UInt32),
                      .store32 (1049656 : UInt32),
                      .const (0 : UInt32),
                      .const (1049656 : UInt32),
                      .store32 (1049668 : UInt32),
                      .const (0 : UInt32),
                      .const (1049664 : UInt32),
                      .store32 (1049676 : UInt32),
                      .const (0 : UInt32),
                      .const (1049656 : UInt32),
                      .store32 (1049664 : UInt32),
                      .const (0 : UInt32),
                      .const (1049672 : UInt32),
                      .store32 (1049684 : UInt32),
                      .const (0 : UInt32),
                      .const (1049664 : UInt32),
                      .store32 (1049672 : UInt32),
                      .const (0 : UInt32),
                      .const (1049680 : UInt32),
                      .store32 (1049692 : UInt32),
                      .const (0 : UInt32),
                      .const (1049672 : UInt32),
                      .store32 (1049680 : UInt32),
                      .const (0 : UInt32),
                      .const (1049688 : UInt32),
                      .store32 (1049700 : UInt32),
                      .const (0 : UInt32),
                      .const (1049680 : UInt32),
                      .store32 (1049688 : UInt32),
                      .const (0 : UInt32),
                      .const (1049696 : UInt32),
                      .store32 (1049708 : UInt32),
                      .const (0 : UInt32),
                      .const (1049688 : UInt32),
                      .store32 (1049696 : UInt32),
                      .const (0 : UInt32),
                      .const (1049704 : UInt32),
                      .store32 (1049716 : UInt32),
                      .const (0 : UInt32),
                      .const (1049696 : UInt32),
                      .store32 (1049704 : UInt32),
                      .const (0 : UInt32),
                      .const (1049712 : UInt32),
                      .store32 (1049724 : UInt32),
                      .const (0 : UInt32),
                      .const (1049704 : UInt32),
                      .store32 (1049712 : UInt32),
                      .const (0 : UInt32),
                      .const (1049720 : UInt32),
                      .store32 (1049732 : UInt32),
                      .const (0 : UInt32),
                      .const (1049712 : UInt32),
                      .store32 (1049720 : UInt32),
                      .const (0 : UInt32),
                      .const (1049728 : UInt32),
                      .store32 (1049740 : UInt32),
                      .const (0 : UInt32),
                      .const (1049720 : UInt32),
                      .store32 (1049728 : UInt32),
                      .const (0 : UInt32),
                      .const (1049736 : UInt32),
                      .store32 (1049748 : UInt32),
                      .const (0 : UInt32),
                      .const (1049728 : UInt32),
                      .store32 (1049736 : UInt32),
                      .const (0 : UInt32),
                      .const (1049744 : UInt32),
                      .store32 (1049756 : UInt32),
                      .const (0 : UInt32),
                      .const (1049736 : UInt32),
                      .store32 (1049744 : UInt32),
                      .const (0 : UInt32),
                      .const (1049752 : UInt32),
                      .store32 (1049764 : UInt32),
                      .const (0 : UInt32),
                      .const (1049744 : UInt32),
                      .store32 (1049752 : UInt32),
                      .const (0 : UInt32),
                      .const (1049760 : UInt32),
                      .store32 (1049772 : UInt32),
                      .const (0 : UInt32),
                      .const (1049752 : UInt32),
                      .store32 (1049760 : UInt32),
                      .const (0 : UInt32),
                      .const (1049768 : UInt32),
                      .store32 (1049780 : UInt32),
                      .const (0 : UInt32),
                      .const (1049760 : UInt32),
                      .store32 (1049768 : UInt32),
                      .const (0 : UInt32),
                      .const (1049776 : UInt32),
                      .store32 (1049788 : UInt32),
                      .const (0 : UInt32),
                      .const (1049768 : UInt32),
                      .store32 (1049776 : 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 (1049812 : UInt32),
                      .const (0 : UInt32),
                      .const (1049776 : UInt32),
                      .store32 (1049784 : 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 (1049804 : 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 (1049824 : 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 (1049828 : UInt32),
                  .localSet 0,
                  .localGet 0,
                  .localGet 6,
                  .localGet 0,
                  .localGet 6,
                  .ltU,
                  .select,
                  .store32 (1049828 : UInt32),
                  .localGet 6,
                  .localGet 9,
                  .add,
                  .localSet 8,
                  .const (1049512 : 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 (1049512 : 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 (1049812 : 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 (1049804 : 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 (1049824 : 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 (1049512 : UInt32),
                    .localSet 10,
                    .localGet 7,
                    .const (16 : UInt32),
                    .add,
                    .const (0 : UInt32),
                    .load64 (1049520 : 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 (1049524 : UInt32),
                    .const (0 : UInt32),
                    .localGet 9,
                    .store32 (1049516 : UInt32),
                    .const (0 : UInt32),
                    .localGet 6,
                    .store32 (1049512 : UInt32),
                    .const (0 : UInt32),
                    .localGet 0,
                    .store32 (1049520 : 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 34,
                      .br 8
                    ],
                    .block 0 0 [
                      .block 0 0 [
                        .const (0 : UInt32),
                        .load32 (1049792 : 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 (1049792 : UInt32),
                        .localGet 0,
                        .const (248 : UInt32),
                        .and,
                        .const (1049528 : UInt32),
                        .add,
                        .localSet 0,
                        .localGet 0,
                        .localSet 8,
                        .br 1
                      ],
                      .localGet 0,
                      .const (248 : UInt32),
                      .and,
                      .localSet 0,
                      .localGet 0,
                      .const (1049528 : UInt32),
                      .add,
                      .localSet 8,
                      .localGet 0,
                      .const (1049536 : 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 (1049812 : UInt32),
                  .eq,
                  .br_if 3,
                  .localGet 2,
                  .const (0 : UInt32),
                  .load32 (1049808 : 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 29,
                    .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 34,
                    .br 6
                  ],
                  .block 0 0 [
                    .block 0 0 [
                      .const (0 : UInt32),
                      .load32 (1049792 : 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 (1049792 : UInt32),
                      .localGet 3,
                      .const (248 : UInt32),
                      .and,
                      .const (1049528 : UInt32),
                      .add,
                      .localSet 3,
                      .localGet 3,
                      .localSet 2,
                      .br 1
                    ],
                    .localGet 3,
                    .const (248 : UInt32),
                    .and,
                    .localSet 3,
                    .localGet 3,
                    .const (1049528 : UInt32),
                    .add,
                    .localSet 2,
                    .localGet 3,
                    .const (1049536 : 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 (1049804 : UInt32),
                .const (0 : UInt32),
                .const (0 : UInt32),
                .load32 (1049812 : UInt32),
                .localSet 0,
                .localGet 0,
                .localGet 3,
                .add,
                .localSet 8,
                .localGet 8,
                .store32 (1049812 : 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 (1049808 : 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 (1049808 : UInt32),
                  .const (0 : UInt32),
                  .const (0 : UInt32),
                  .store32 (1049800 : 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 (1049800 : UInt32),
                .const (0 : UInt32),
                .localGet 2,
                .localGet 3,
                .add,
                .localSet 6,
                .localGet 6,
                .store32 (1049808 : 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 (1049812 : 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 (1049812 : UInt32),
            .const (0 : UInt32),
            .localGet 0,
            .localGet 2,
            .sub,
            .const (0 : UInt32),
            .load32 (1049804 : UInt32),
            .localGet 9,
            .add,
            .localSet 2,
            .localGet 2,
            .add,
            .const (8 : UInt32),
            .add,
            .localSet 6,
            .localGet 6,
            .store32 (1049804 : 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 (1049824 : UInt32),
            .br 3
          ],
          .const (0 : UInt32),
          .localGet 0,
          .store32 (1049812 : UInt32),
          .const (0 : UInt32),
          .const (0 : UInt32),
          .load32 (1049804 : UInt32),
          .localGet 3,
          .add,
          .localSet 3,
          .localGet 3,
          .store32 (1049804 : UInt32),
          .localGet 0,
          .localGet 3,
          .const (1 : UInt32),
          .or,
          .store32 (4 : UInt32),
          .br 1
        ],
        .const (0 : UInt32),
        .localGet 0,
        .store32 (1049808 : UInt32),
        .const (0 : UInt32),
        .const (0 : UInt32),
        .load32 (1049800 : UInt32),
        .localGet 3,
        .add,
        .localSet 3,
        .localGet 3,
        .store32 (1049800 : 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 (1049804 : UInt32),
    .localSet 2,
    .localGet 2,
    .localGet 3,
    .leU,
    .br_if 0,
    .const (0 : UInt32),
    .localGet 2,
    .localGet 3,
    .sub,
    .localSet 2,
    .localGet 2,
    .store32 (1049804 : UInt32),
    .const (0 : UInt32),
    .const (0 : UInt32),
    .load32 (1049812 : UInt32),
    .localSet 0,
    .localGet 0,
    .localGet 3,
    .add,
    .localSet 8,
    .localGet 8,
    .store32 (1049812 : 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 func24Def : Wasm.Function :=
  { params := [.i32], locals := [.i32, .i32, .i32, .i32, .i32, .i32, .i32, .i32, .i32, .i64], body := func24, results := [.i32] }

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

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

def func26 : 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 27,
      .ret
    ],
    .const (1048823 : UInt32),
    .const (46 : UInt32),
    .const (1048872 : UInt32),
    .call 53,
    .unreachable
  ],
  .const (1048888 : UInt32),
  .const (46 : UInt32),
  .const (1048936 : UInt32),
  .call 53,
  .unreachable
]

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

def func27 : 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 (1049808 : 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 (1049800 : 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 29
    ],
    .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 (1049812 : UInt32),
                    .eq,
                    .br_if 2,
                    .localGet 3,
                    .const (0 : UInt32),
                    .load32 (1049808 : UInt32),
                    .eq,
                    .br_if 3,
                    .localGet 3,
                    .localGet 2,
                    .const (4294967288 : UInt32),
                    .and,
                    .localSet 2,
                    .localGet 2,
                    .call 29,
                    .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 (1049808 : UInt32),
                    .ne,
                    .br_if 1,
                    .const (0 : UInt32),
                    .localGet 0,
                    .store32 (1049800 : 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 34,
                .const (0 : UInt32),
                .const (0 : UInt32),
                .load32 (1049832 : UInt32),
                .const (4294967295 : UInt32),
                .add,
                .localSet 1,
                .localGet 1,
                .store32 (1049832 : UInt32),
                .localGet 1,
                .br_if 6,
                .const (0 : UInt32),
                .load32 (1049520 : UInt32),
                .localSet 0,
                .localGet 0,
                .br_if 2,
                .const (4095 : UInt32),
                .localSet 1,
                .br 3
              ],
              .const (0 : UInt32),
              .localGet 1,
              .store32 (1049812 : UInt32),
              .const (0 : UInt32),
              .const (0 : UInt32),
              .load32 (1049804 : UInt32),
              .localGet 0,
              .add,
              .localSet 0,
              .localGet 0,
              .store32 (1049804 : UInt32),
              .localGet 1,
              .localGet 0,
              .const (1 : UInt32),
              .or,
              .store32 (4 : UInt32),
              .block 0 0 [
                .localGet 1,
                .const (0 : UInt32),
                .load32 (1049808 : UInt32),
                .ne,
                .br_if 0,
                .const (0 : UInt32),
                .const (0 : UInt32),
                .store32 (1049800 : UInt32),
                .const (0 : UInt32),
                .const (0 : UInt32),
                .store32 (1049808 : UInt32)
              ],
              .localGet 0,
              .const (0 : UInt32),
              .load32 (1049824 : UInt32),
              .localSet 2,
              .localGet 2,
              .leU,
              .br_if 5,
              .const (0 : UInt32),
              .load32 (1049812 : UInt32),
              .localSet 0,
              .localGet 0,
              .eqz,
              .br_if 5,
              .const (0 : UInt32),
              .load32 (1049804 : UInt32),
              .localSet 4,
              .localGet 4,
              .const (41 : UInt32),
              .ltU,
              .br_if 4,
              .const (1049512 : 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 (1049808 : UInt32),
            .const (0 : UInt32),
            .const (0 : UInt32),
            .load32 (1049800 : UInt32),
            .localGet 0,
            .add,
            .localSet 0,
            .localGet 0,
            .store32 (1049800 : 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 (1049832 : UInt32),
        .ret
      ],
      .block 0 0 [
        .block 0 0 [
          .const (0 : UInt32),
          .load32 (1049792 : 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 (1049792 : UInt32),
          .localGet 0,
          .const (248 : UInt32),
          .and,
          .const (1049528 : UInt32),
          .add,
          .localSet 0,
          .localGet 0,
          .localSet 3,
          .br 1
        ],
        .localGet 0,
        .const (248 : UInt32),
        .and,
        .localSet 0,
        .localGet 0,
        .const (1049528 : UInt32),
        .add,
        .localSet 3,
        .localGet 0,
        .const (1049536 : 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 (1049520 : 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 (1049832 : UInt32),
    .localGet 4,
    .localGet 2,
    .leU,
    .br_if 0,
    .const (0 : UInt32),
    .const (4294967295 : UInt32),
    .store32 (1049824 : UInt32)
  ]
]

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

def func28 : 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 23,
                      .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 (1049812 : UInt32),
                        .eq,
                        .br_if 1,
                        .block 0 0 [
                          .localGet 7,
                          .const (0 : UInt32),
                          .load32 (1049808 : 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 29,
                          .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 30,
                            .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 (1049800 : 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 (1049808 : UInt32),
                        .const (0 : UInt32),
                        .localGet 6,
                        .store32 (1049800 : 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 30,
                      .br 6
                    ],
                    .const (0 : UInt32),
                    .load32 (1049804 : 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 (1048888 : UInt32),
                  .const (46 : UInt32),
                  .const (1048936 : UInt32),
                  .call 53,
                  .unreachable
                ],
                .const (1048823 : UInt32),
                .const (46 : UInt32),
                .const (1048872 : UInt32),
                .call 53,
                .unreachable
              ],
              .const (1048888 : UInt32),
              .const (46 : UInt32),
              .const (1048936 : UInt32),
              .call 53,
              .unreachable
            ],
            .const (1048823 : UInt32),
            .const (46 : UInt32),
            .const (1048872 : UInt32),
            .call 53,
            .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 (1049804 : UInt32),
          .const (0 : UInt32),
          .localGet 5,
          .store32 (1049812 : UInt32)
        ],
        .localGet 8,
        .eqz,
        .br_if 0,
        .localGet 0,
        .ret
      ],
      .localGet 3,
      .call 24,
      .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 27
  ],
  .localGet 2
]

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

def func29 : 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 (1049384 : 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 (1049792 : UInt32),
        .const (4294967294 : UInt32),
        .localGet 1,
        .const (3 : UInt32),
        .shrU,
        .rotl,
        .and,
        .store32 (1049792 : 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 (1049796 : UInt32),
  .const (4294967294 : UInt32),
  .localGet 0,
  .load32 (28 : UInt32),
  .rotl,
  .and,
  .store32 (1049796 : UInt32)
]

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

def func30 : 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 (1049808 : 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 (1049800 : 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 29
    ],
    .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 (1049812 : UInt32),
            .eq,
            .br_if 2,
            .localGet 2,
            .const (0 : UInt32),
            .load32 (1049808 : UInt32),
            .eq,
            .br_if 3,
            .localGet 2,
            .localGet 3,
            .const (4294967288 : UInt32),
            .and,
            .localSet 3,
            .localGet 3,
            .call 29,
            .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 (1049808 : UInt32),
            .ne,
            .br_if 1,
            .const (0 : UInt32),
            .localGet 1,
            .store32 (1049800 : 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 34,
          .ret
        ],
        .block 0 0 [
          .block 0 0 [
            .const (0 : UInt32),
            .load32 (1049792 : 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 (1049792 : UInt32),
            .localGet 1,
            .const (248 : UInt32),
            .and,
            .const (1049528 : UInt32),
            .add,
            .localSet 1,
            .localGet 1,
            .localSet 2,
            .br 1
          ],
          .localGet 1,
          .const (248 : UInt32),
          .and,
          .localSet 1,
          .localGet 1,
          .const (1049528 : UInt32),
          .add,
          .localSet 2,
          .localGet 1,
          .const (1049536 : 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 (1049812 : UInt32),
      .const (0 : UInt32),
      .const (0 : UInt32),
      .load32 (1049804 : UInt32),
      .localGet 1,
      .add,
      .localSet 1,
      .localGet 1,
      .store32 (1049804 : UInt32),
      .localGet 0,
      .localGet 1,
      .const (1 : UInt32),
      .or,
      .store32 (4 : UInt32),
      .localGet 0,
      .const (0 : UInt32),
      .load32 (1049808 : UInt32),
      .ne,
      .br_if 1,
      .const (0 : UInt32),
      .const (0 : UInt32),
      .store32 (1049800 : UInt32),
      .const (0 : UInt32),
      .const (0 : UInt32),
      .store32 (1049808 : UInt32),
      .ret
    ],
    .const (0 : UInt32),
    .localGet 0,
    .store32 (1049808 : UInt32),
    .const (0 : UInt32),
    .const (0 : UInt32),
    .load32 (1049800 : UInt32),
    .localGet 1,
    .add,
    .localSet 1,
    .localGet 1,
    .store32 (1049800 : UInt32),
    .localGet 0,
    .localGet 1,
    .const (1 : UInt32),
    .or,
    .store32 (4 : UInt32),
    .localGet 0,
    .localGet 1,
    .add,
    .localGet 1,
    .store32 (0 : UInt32),
    .ret
  ]
]

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

def func31 : 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 16,
  .unreachable
]

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

def func32 : Wasm.Program :=
  [
  .localGet 1,
  .localGet 0,
  .call 33,
  .unreachable
]

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

def func33 : 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 14,
  .unreachable
]

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

def func34 : 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 (1049384 : UInt32),
  .add,
  .localSet 3,
  .block 0 0 [
    .const (0 : UInt32),
    .load32 (1049796 : 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 (1049796 : UInt32),
    .localGet 4,
    .or,
    .store32 (1049796 : 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 func34Def : Wasm.Function :=
  { params := [.i32, .i32], locals := [.i32, .i32, .i32, .i32], body := func34, results := [] }

def func35 : Wasm.Program :=
  [
  .const (0 : UInt32),
  .localSet 1,
  .const (0 : UInt32),
  .const (0 : UInt32),
  .load32 (1049380 : UInt32),
  .localSet 2,
  .localGet 2,
  .const (1 : UInt32),
  .add,
  .store32 (1049380 : UInt32),
  .block 0 0 [
    .localGet 2,
    .const (0 : UInt32),
    .ltS,
    .br_if 0,
    .const (1 : UInt32),
    .localSet 1,
    .const (0 : UInt32),
    .load8U (1049360 : UInt32),
    .br_if 0,
    .const (0 : UInt32),
    .localGet 0,
    .store8 (1049360 : UInt32),
    .const (0 : UInt32),
    .const (0 : UInt32),
    .load32 (1049356 : UInt32),
    .const (1 : UInt32),
    .add,
    .store32 (1049356 : UInt32),
    .const (2 : UInt32),
    .localSet 1
  ],
  .localGet 1
]

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

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

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

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

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

def func38 : 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 60,
    .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 55
]

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

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

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

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

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

def func41 : Wasm.Program :=
  [
  .localGet 1,
  .load32 (4 : UInt32),
  .localSet 2,
  .localGet 1,
  .load32 (0 : UInt32),
  .localSet 3,
  .call 8,
  .block 0 0 [
    .const (8 : UInt32),
    .const (4 : UInt32),
    .call 5,
    .localSet 1,
    .localGet 1,
    .br_if 0,
    .const (4 : UInt32),
    .const (8 : UInt32),
    .call 51,
    .unreachable
  ],
  .localGet 1,
  .localGet 2,
  .store32 (4 : UInt32),
  .localGet 1,
  .localGet 3,
  .store32 (0 : UInt32),
  .localGet 0,
  .const (1048952 : UInt32),
  .store32 (4 : UInt32),
  .localGet 0,
  .localGet 1,
  .store32 (0 : UInt32)
]

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

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

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

def func43 : 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 10,
    .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 func43Def : Wasm.Function :=
  { params := [.i32, .i32], locals := [.i32, .i32, .i32, .i32, .i32, .i32], body := func43, results := [.i32] }

def func44 : 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 10,
        .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 func44Def : Wasm.Function :=
  { params := [.i32, .i32, .i32], locals := [.i32], body := func44, results := [.i32] }

def func45 : 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 (1048668 : UInt32),
    .localGet 3,
    .load32 (0 : UInt32),
    .localSet 3,
    .localGet 3,
    .load32 (0 : UInt32),
    .localGet 3,
    .load32 (4 : UInt32),
    .call 55,
    .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 (1048968 : UInt32),
  .store32 (4 : UInt32),
  .localGet 0,
  .localGet 1,
  .store32 (0 : UInt32),
  .localGet 2,
  .const (32 : UInt32),
  .add,
  .globalSet 0
]

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

def func46 : 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 (1048668 : UInt32),
    .localGet 3,
    .load32 (0 : UInt32),
    .localSet 3,
    .localGet 3,
    .load32 (0 : UInt32),
    .localGet 3,
    .load32 (4 : UInt32),
    .call 55,
    .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 8,
  .block 0 0 [
    .const (12 : UInt32),
    .const (4 : UInt32),
    .call 5,
    .localSet 1,
    .localGet 1,
    .br_if 0,
    .const (4 : UInt32),
    .const (12 : UInt32),
    .call 51,
    .unreachable
  ],
  .localGet 1,
  .localGet 2,
  .load32 (16 : UInt32),
  .store32 (8 : UInt32),
  .localGet 1,
  .localGet 2,
  .load64 (8 : UInt32),
  .store64 (0 : UInt32),
  .localGet 0,
  .const (1048968 : UInt32),
  .store32 (4 : UInt32),
  .localGet 0,
  .localGet 1,
  .store32 (0 : UInt32),
  .localGet 2,
  .const (48 : UInt32),
  .add,
  .globalSet 0
]

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

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

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

def func48 : Wasm.Program :=
  [
  .localGet 0,
  .const (1048668 : UInt32),
  .localGet 1,
  .localGet 2,
  .call 55
]

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

def func49 : 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 func49Def : Wasm.Function :=
  { params := [.i32, .i32, .i32], locals := [.i32, .i32], body := func49, results := [] }

def func50 : Wasm.Program :=
  [
  .block 0 0 [
    .localGet 0,
    .eqz,
    .br_if 0,
    .localGet 0,
    .localGet 1,
    .call 51,
    .unreachable
  ],
  .call 52,
  .unreachable
]

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

def func51 : Wasm.Program :=
  [
  .localGet 1,
  .localGet 0,
  .call 32,
  .unreachable
]

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

def func52 : Wasm.Program :=
  [
  .const (1049065 : UInt32),
  .const (35 : UInt32),
  .const (1049084 : UInt32),
  .call 54,
  .unreachable
]

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

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

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

def func54 : 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 31,
  .unreachable
]

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

def func55 : 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 func55Def : Wasm.Function :=
  { params := [.i32, .i32, .i32, .i32], locals := [.i32, .i32, .i32, .i32, .i32, .i32, .i32, .i32], body := func55, results := [.i32] }

def func56 : Wasm.Program :=
  [
  .globalGet 0,
  .const (32 : UInt32),
  .sub,
  .localSet 3,
  .localGet 3,
  .globalSet 0,
  .localGet 3,
  .localGet 1,
  .store32 (12 : UInt32),
  .localGet 3,
  .localGet 0,
  .store32 (8 : UInt32),
  .localGet 3,
  .const (17 : UInt32),
  .extendUI32,
  .constI64 (32 : UInt64),
  .shlI64,
  .localSet 4,
  .localGet 4,
  .localGet 3,
  .const (8 : UInt32),
  .add,
  .extendUI32,
  .orI64,
  .store64 (24 : UInt32),
  .localGet 3,
  .localGet 4,
  .localGet 3,
  .const (12 : UInt32),
  .add,
  .extendUI32,
  .orI64,
  .store64 (16 : UInt32),
  .const (1049100 : UInt32),
  .localGet 3,
  .const (16 : UInt32),
  .add,
  .localGet 2,
  .call 54,
  .unreachable
]

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

def func57 : Wasm.Program :=
  [
  .const (43 : UInt32),
  .const (1114112 : UInt32),
  .localGet 0,
  .load32 (8 : UInt32),
  .localSet 6,
  .localGet 6,
  .const (2097152 : UInt32),
  .and,
  .localSet 7,
  .localGet 7,
  .select,
  .localSet 8,
  .localGet 7,
  .const (21 : UInt32),
  .shrU,
  .const (1 : UInt32),
  .localGet 1,
  .select,
  .localGet 5,
  .add,
  .localSet 9,
  .block 0 0 [
    .block 0 0 [
      .localGet 6,
      .const (8388608 : UInt32),
      .and,
      .br_if 0,
      .const (0 : UInt32),
      .localSet 2,
      .br 1
    ],
    .block 0 0 [
      .block 0 0 [
        .localGet 3,
        .const (16 : UInt32),
        .ltU,
        .br_if 0,
        .localGet 2,
        .localGet 3,
        .call 58,
        .localSet 7,
        .br 1
      ],
      .block 0 0 [
        .localGet 3,
        .br_if 0,
        .const (0 : UInt32),
        .localSet 7,
        .br 1
      ],
      .localGet 3,
      .const (3 : UInt32),
      .and,
      .localSet 10,
      .const (0 : UInt32),
      .localSet 11,
      .const (0 : UInt32),
      .localSet 7,
      .block 0 0 [
        .localGet 3,
        .const (4 : UInt32),
        .ltU,
        .br_if 0,
        .localGet 3,
        .const (12 : UInt32),
        .and,
        .localSet 12,
        .const (0 : UInt32),
        .localSet 11,
        .const (0 : UInt32),
        .localSet 7,
        .loop 0 0 [
          .localGet 7,
          .localGet 2,
          .localGet 11,
          .add,
          .localSet 13,
          .localGet 13,
          .load8S (0 : UInt32),
          .const (4294967231 : UInt32),
          .gtS,
          .add,
          .localGet 13,
          .const (1 : UInt32),
          .add,
          .load8S (0 : UInt32),
          .const (4294967231 : UInt32),
          .gtS,
          .add,
          .localGet 13,
          .const (2 : UInt32),
          .add,
          .load8S (0 : UInt32),
          .const (4294967231 : UInt32),
          .gtS,
          .add,
          .localGet 13,
          .const (3 : UInt32),
          .add,
          .load8S (0 : UInt32),
          .const (4294967231 : UInt32),
          .gtS,
          .add,
          .localSet 7,
          .localGet 12,
          .localGet 11,
          .const (4 : UInt32),
          .add,
          .localSet 11,
          .localGet 11,
          .ne,
          .br_if 0
        ],
        .localGet 10,
        .eqz,
        .br_if 1
      ],
      .localGet 2,
      .localGet 11,
      .add,
      .localSet 13,
      .loop 0 0 [
        .localGet 7,
        .localGet 13,
        .load8S (0 : UInt32),
        .const (4294967231 : UInt32),
        .gtS,
        .add,
        .localSet 7,
        .localGet 13,
        .const (1 : UInt32),
        .add,
        .localSet 13,
        .localGet 10,
        .const (4294967295 : UInt32),
        .add,
        .localSet 10,
        .localGet 10,
        .br_if 0
      ]
    ],
    .localGet 7,
    .localGet 9,
    .add,
    .localSet 9
  ],
  .localGet 8,
  .const (45 : UInt32),
  .localGet 1,
  .select,
  .localSet 12,
  .block 0 0 [
    .block 0 0 [
      .localGet 9,
      .localGet 0,
      .load16U (12 : UInt32),
      .localSet 1,
      .localGet 1,
      .geU,
      .br_if 0,
      .block 0 0 [
        .block 0 0 [
          .block 0 0 [
            .localGet 6,
            .const (16777216 : UInt32),
            .and,
            .br_if 0,
            .localGet 1,
            .localGet 9,
            .sub,
            .localSet 8,
            .const (0 : UInt32),
            .localSet 7,
            .const (0 : UInt32),
            .localSet 1,
            .block 0 0 [
              .block 0 0 [
                .block 0 0 [
                  .localGet 6,
                  .const (29 : UInt32),
                  .shrU,
                  .const (3 : UInt32),
                  .and,
                  .brTable [2, 0, 1, 0] 2
                ],
                .localGet 8,
                .localSet 1,
                .br 1
              ],
              .localGet 8,
              .const (65534 : UInt32),
              .and,
              .const (1 : UInt32),
              .shrU,
              .localSet 1
            ],
            .localGet 6,
            .const (2097151 : UInt32),
            .and,
            .localSet 9,
            .localGet 0,
            .load32 (4 : UInt32),
            .localSet 11,
            .localGet 0,
            .load32 (0 : UInt32),
            .localSet 10,
            .loop 0 0 [
              .localGet 7,
              .const (65535 : UInt32),
              .and,
              .localGet 1,
              .const (65535 : UInt32),
              .and,
              .geU,
              .br_if 2,
              .const (1 : UInt32),
              .localSet 13,
              .localGet 7,
              .const (1 : UInt32),
              .add,
              .localSet 7,
              .localGet 10,
              .localGet 9,
              .localGet 11,
              .load32 (16 : UInt32),
              .callIndirect 2 0,
              .eqz,
              .br_if 0,
              .br 5
            ]
          ],
          .localGet 0,
          .localGet 0,
          .load64 (8 : UInt32),
          .localSet 14,
          .localGet 14,
          .wrapI64,
          .const (2682257408 : UInt32),
          .and,
          .const (536870960 : UInt32),
          .or,
          .store32 (8 : UInt32),
          .const (1 : UInt32),
          .localSet 13,
          .localGet 0,
          .load32 (0 : UInt32),
          .localSet 10,
          .localGet 10,
          .localGet 0,
          .load32 (4 : UInt32),
          .localSet 11,
          .localGet 11,
          .localGet 12,
          .localGet 2,
          .localGet 3,
          .call 59,
          .br_if 3,
          .const (0 : UInt32),
          .localSet 7,
          .localGet 1,
          .localGet 9,
          .sub,
          .const (65535 : UInt32),
          .and,
          .localSet 2,
          .loop 0 0 [
            .localGet 7,
            .const (65535 : UInt32),
            .and,
            .localGet 2,
            .geU,
            .br_if 2,
            .const (1 : UInt32),
            .localSet 13,
            .localGet 7,
            .const (1 : UInt32),
            .add,
            .localSet 7,
            .localGet 10,
            .const (48 : UInt32),
            .localGet 11,
            .load32 (16 : UInt32),
            .callIndirect 2 0,
            .eqz,
            .br_if 0,
            .br 4
          ]
        ],
        .const (1 : UInt32),
        .localSet 13,
        .localGet 10,
        .localGet 11,
        .localGet 12,
        .localGet 2,
        .localGet 3,
        .call 59,
        .br_if 2,
        .localGet 10,
        .localGet 4,
        .localGet 5,
        .localGet 11,
        .load32 (12 : UInt32),
        .callIndirect 1 0,
        .br_if 2,
        .const (0 : UInt32),
        .localSet 7,
        .localGet 8,
        .localGet 1,
        .sub,
        .const (65535 : UInt32),
        .and,
        .localSet 0,
        .loop 0 0 [
          .localGet 7,
          .const (65535 : UInt32),
          .and,
          .localSet 2,
          .localGet 2,
          .localGet 0,
          .ltU,
          .localSet 13,
          .localGet 2,
          .localGet 0,
          .geU,
          .br_if 3,
          .localGet 7,
          .const (1 : UInt32),
          .add,
          .localSet 7,
          .localGet 10,
          .localGet 9,
          .localGet 11,
          .load32 (16 : UInt32),
          .callIndirect 2 0,
          .eqz,
          .br_if 0,
          .br 3
        ]
      ],
      .const (1 : UInt32),
      .localSet 13,
      .localGet 10,
      .localGet 4,
      .localGet 5,
      .localGet 11,
      .load32 (12 : UInt32),
      .callIndirect 1 0,
      .br_if 1,
      .localGet 0,
      .localGet 14,
      .store64 (8 : UInt32),
      .const (0 : UInt32),
      .ret
    ],
    .const (1 : UInt32),
    .localSet 13,
    .localGet 0,
    .load32 (0 : UInt32),
    .localSet 7,
    .localGet 7,
    .localGet 0,
    .load32 (4 : UInt32),
    .localSet 10,
    .localGet 10,
    .localGet 12,
    .localGet 2,
    .localGet 3,
    .call 59,
    .br_if 0,
    .localGet 7,
    .localGet 4,
    .localGet 5,
    .localGet 10,
    .load32 (12 : UInt32),
    .callIndirect 1 0,
    .localSet 13
  ],
  .localGet 13
]

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

def func58 : Wasm.Program :=
  [
  .block 0 0 [
    .block 0 0 [
      .localGet 1,
      .localGet 0,
      .const (3 : UInt32),
      .add,
      .const (4294967292 : UInt32),
      .and,
      .localSet 2,
      .localGet 2,
      .localGet 0,
      .sub,
      .localSet 3,
      .localGet 3,
      .ltU,
      .br_if 0,
      .localGet 1,
      .localGet 3,
      .sub,
      .localSet 4,
      .localGet 4,
      .const (2 : UInt32),
      .shrU,
      .localSet 5,
      .localGet 5,
      .eqz,
      .br_if 0,
      .localGet 4,
      .const (3 : UInt32),
      .and,
      .localSet 6,
      .const (0 : UInt32),
      .localSet 7,
      .const (0 : UInt32),
      .localSet 1,
      .block 0 0 [
        .localGet 2,
        .localGet 0,
        .eq,
        .br_if 0,
        .const (0 : UInt32),
        .localSet 8,
        .const (0 : UInt32),
        .localSet 1,
        .block 0 0 [
          .localGet 0,
          .localGet 2,
          .sub,
          .localSet 9,
          .localGet 9,
          .const (4294967292 : UInt32),
          .gtU,
          .br_if 0,
          .const (0 : UInt32),
          .localSet 8,
          .const (0 : UInt32),
          .localSet 1,
          .loop 0 0 [
            .localGet 1,
            .localGet 0,
            .localGet 8,
            .add,
            .localSet 2,
            .localGet 2,
            .load8S (0 : UInt32),
            .const (4294967231 : UInt32),
            .gtS,
            .add,
            .localGet 2,
            .const (1 : UInt32),
            .add,
            .load8S (0 : UInt32),
            .const (4294967231 : UInt32),
            .gtS,
            .add,
            .localGet 2,
            .const (2 : UInt32),
            .add,
            .load8S (0 : UInt32),
            .const (4294967231 : UInt32),
            .gtS,
            .add,
            .localGet 2,
            .const (3 : UInt32),
            .add,
            .load8S (0 : UInt32),
            .const (4294967231 : UInt32),
            .gtS,
            .add,
            .localSet 1,
            .localGet 8,
            .const (4 : UInt32),
            .add,
            .localSet 8,
            .localGet 8,
            .br_if 0
          ]
        ],
        .localGet 0,
        .localGet 8,
        .add,
        .localSet 2,
        .loop 0 0 [
          .localGet 1,
          .localGet 2,
          .load8S (0 : UInt32),
          .const (4294967231 : UInt32),
          .gtS,
          .add,
          .localSet 1,
          .localGet 2,
          .const (1 : UInt32),
          .add,
          .localSet 2,
          .localGet 9,
          .const (1 : UInt32),
          .add,
          .localSet 9,
          .localGet 9,
          .br_if 0
        ]
      ],
      .localGet 0,
      .localGet 3,
      .add,
      .localSet 9,
      .block 0 0 [
        .localGet 6,
        .eqz,
        .br_if 0,
        .localGet 9,
        .localGet 4,
        .const (2147483644 : UInt32),
        .and,
        .add,
        .localSet 2,
        .localGet 2,
        .load8S (0 : UInt32),
        .const (4294967231 : UInt32),
        .gtS,
        .localSet 7,
        .localGet 6,
        .const (1 : UInt32),
        .eq,
        .br_if 0,
        .localGet 7,
        .localGet 2,
        .load8S (1 : UInt32),
        .const (4294967231 : UInt32),
        .gtS,
        .add,
        .localSet 7,
        .localGet 6,
        .const (2 : UInt32),
        .eq,
        .br_if 0,
        .localGet 7,
        .localGet 2,
        .load8S (2 : UInt32),
        .const (4294967231 : UInt32),
        .gtS,
        .add,
        .localSet 7
      ],
      .localGet 7,
      .localGet 1,
      .add,
      .localSet 8,
      .loop 0 0 [
        .localGet 9,
        .localSet 3,
        .localGet 5,
        .eqz,
        .br_if 2,
        .localGet 5,
        .const (192 : UInt32),
        .localGet 5,
        .const (192 : UInt32),
        .ltU,
        .select,
        .localSet 7,
        .localGet 7,
        .const (3 : UInt32),
        .and,
        .localSet 6,
        .block 0 0 [
          .block 0 0 [
            .localGet 7,
            .const (2 : UInt32),
            .shl,
            .localSet 4,
            .localGet 4,
            .const (1008 : UInt32),
            .and,
            .localSet 1,
            .localGet 1,
            .br_if 0,
            .const (0 : UInt32),
            .localSet 2,
            .br 1
          ],
          .localGet 3,
          .localGet 1,
          .add,
          .localSet 0,
          .const (0 : UInt32),
          .localSet 2,
          .localGet 3,
          .localSet 1,
          .loop 0 0 [
            .localGet 1,
            .const (12 : UInt32),
            .add,
            .load32 (0 : UInt32),
            .localSet 9,
            .localGet 9,
            .const (4294967295 : UInt32),
            .xor,
            .const (7 : UInt32),
            .shrU,
            .localGet 9,
            .const (6 : UInt32),
            .shrU,
            .or,
            .const (16843009 : UInt32),
            .and,
            .localGet 1,
            .const (8 : UInt32),
            .add,
            .load32 (0 : UInt32),
            .localSet 9,
            .localGet 9,
            .const (4294967295 : UInt32),
            .xor,
            .const (7 : UInt32),
            .shrU,
            .localGet 9,
            .const (6 : UInt32),
            .shrU,
            .or,
            .const (16843009 : UInt32),
            .and,
            .localGet 1,
            .const (4 : UInt32),
            .add,
            .load32 (0 : UInt32),
            .localSet 9,
            .localGet 9,
            .const (4294967295 : UInt32),
            .xor,
            .const (7 : UInt32),
            .shrU,
            .localGet 9,
            .const (6 : UInt32),
            .shrU,
            .or,
            .const (16843009 : UInt32),
            .and,
            .localGet 1,
            .load32 (0 : UInt32),
            .localSet 9,
            .localGet 9,
            .const (4294967295 : UInt32),
            .xor,
            .const (7 : UInt32),
            .shrU,
            .localGet 9,
            .const (6 : UInt32),
            .shrU,
            .or,
            .const (16843009 : UInt32),
            .and,
            .localGet 2,
            .add,
            .add,
            .add,
            .add,
            .localSet 2,
            .localGet 1,
            .const (16 : UInt32),
            .add,
            .localSet 1,
            .localGet 1,
            .localGet 0,
            .ne,
            .br_if 0
          ]
        ],
        .localGet 5,
        .localGet 7,
        .sub,
        .localSet 5,
        .localGet 3,
        .localGet 4,
        .add,
        .localSet 9,
        .localGet 2,
        .const (8 : UInt32),
        .shrU,
        .const (16711935 : UInt32),
        .and,
        .localGet 2,
        .const (16711935 : UInt32),
        .and,
        .add,
        .const (65537 : UInt32),
        .mul,
        .const (16 : UInt32),
        .shrU,
        .localGet 8,
        .add,
        .localSet 8,
        .localGet 6,
        .eqz,
        .br_if 0
      ],
      .localGet 3,
      .localGet 7,
      .const (252 : UInt32),
      .and,
      .const (2 : UInt32),
      .shl,
      .add,
      .localSet 2,
      .localGet 2,
      .load32 (0 : UInt32),
      .localSet 1,
      .localGet 1,
      .const (4294967295 : UInt32),
      .xor,
      .const (7 : UInt32),
      .shrU,
      .localGet 1,
      .const (6 : UInt32),
      .shrU,
      .or,
      .const (16843009 : UInt32),
      .and,
      .localSet 1,
      .block 0 0 [
        .localGet 6,
        .const (1 : UInt32),
        .eq,
        .br_if 0,
        .localGet 2,
        .load32 (4 : UInt32),
        .localSet 9,
        .localGet 9,
        .const (4294967295 : UInt32),
        .xor,
        .const (7 : UInt32),
        .shrU,
        .localGet 9,
        .const (6 : UInt32),
        .shrU,
        .or,
        .const (16843009 : UInt32),
        .and,
        .localGet 1,
        .add,
        .localSet 1,
        .localGet 6,
        .const (2 : UInt32),
        .eq,
        .br_if 0,
        .localGet 2,
        .load32 (8 : UInt32),
        .localSet 2,
        .localGet 2,
        .const (4294967295 : UInt32),
        .xor,
        .const (7 : UInt32),
        .shrU,
        .localGet 2,
        .const (6 : UInt32),
        .shrU,
        .or,
        .const (16843009 : UInt32),
        .and,
        .localGet 1,
        .add,
        .localSet 1
      ],
      .localGet 1,
      .const (8 : UInt32),
      .shrU,
      .const (459007 : UInt32),
      .and,
      .localGet 1,
      .const (16711935 : UInt32),
      .and,
      .add,
      .const (65537 : UInt32),
      .mul,
      .const (16 : UInt32),
      .shrU,
      .localGet 8,
      .add,
      .localSet 8,
      .br 1
    ],
    .block 0 0 [
      .localGet 1,
      .br_if 0,
      .const (0 : UInt32),
      .ret
    ],
    .localGet 1,
    .const (3 : UInt32),
    .and,
    .localSet 2,
    .const (0 : UInt32),
    .localSet 9,
    .const (0 : UInt32),
    .localSet 8,
    .block 0 0 [
      .localGet 1,
      .const (4 : UInt32),
      .ltU,
      .br_if 0,
      .localGet 1,
      .const (4294967292 : UInt32),
      .and,
      .localSet 5,
      .const (0 : UInt32),
      .localSet 8,
      .const (0 : UInt32),
      .localSet 9,
      .loop 0 0 [
        .localGet 8,
        .localGet 0,
        .localGet 9,
        .add,
        .localSet 1,
        .localGet 1,
        .load8S (0 : UInt32),
        .const (4294967231 : UInt32),
        .gtS,
        .add,
        .localGet 1,
        .const (1 : UInt32),
        .add,
        .load8S (0 : UInt32),
        .const (4294967231 : UInt32),
        .gtS,
        .add,
        .localGet 1,
        .const (2 : UInt32),
        .add,
        .load8S (0 : UInt32),
        .const (4294967231 : UInt32),
        .gtS,
        .add,
        .localGet 1,
        .const (3 : UInt32),
        .add,
        .load8S (0 : UInt32),
        .const (4294967231 : UInt32),
        .gtS,
        .add,
        .localSet 8,
        .localGet 5,
        .localGet 9,
        .const (4 : UInt32),
        .add,
        .localSet 9,
        .localGet 9,
        .ne,
        .br_if 0
      ],
      .localGet 2,
      .eqz,
      .br_if 1
    ],
    .localGet 0,
    .localGet 9,
    .add,
    .localSet 1,
    .loop 0 0 [
      .localGet 8,
      .localGet 1,
      .load8S (0 : UInt32),
      .const (4294967231 : UInt32),
      .gtS,
      .add,
      .localSet 8,
      .localGet 1,
      .const (1 : UInt32),
      .add,
      .localSet 1,
      .localGet 2,
      .const (4294967295 : UInt32),
      .add,
      .localSet 2,
      .localGet 2,
      .br_if 0
    ]
  ],
  .localGet 8
]

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

def func59 : Wasm.Program :=
  [
  .block 0 0 [
    .localGet 2,
    .const (1114112 : UInt32),
    .eq,
    .br_if 0,
    .localGet 0,
    .localGet 2,
    .localGet 1,
    .load32 (16 : UInt32),
    .callIndirect 2 0,
    .eqz,
    .br_if 0,
    .const (1 : UInt32),
    .ret
  ],
  .block 0 0 [
    .localGet 3,
    .br_if 0,
    .const (0 : UInt32),
    .ret
  ],
  .localGet 0,
  .localGet 3,
  .localGet 4,
  .localGet 1,
  .load32 (12 : UInt32),
  .callIndirect 1 0
]

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

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

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

def func61 : Wasm.Program :=
  [
  .globalGet 0,
  .const (16 : UInt32),
  .sub,
  .localSet 2,
  .localGet 2,
  .globalSet 0,
  .const (10 : UInt32),
  .localSet 3,
  .localGet 0,
  .load32 (0 : UInt32),
  .localSet 4,
  .localGet 4,
  .localSet 5,
  .block 0 0 [
    .localGet 4,
    .const (1000 : UInt32),
    .ltU,
    .br_if 0,
    .const (10 : UInt32),
    .localSet 3,
    .localGet 4,
    .localSet 5,
    .loop 0 0 [
      .localGet 2,
      .const (6 : UInt32),
      .add,
      .localGet 3,
      .add,
      .localSet 6,
      .localGet 6,
      .const (4294967292 : UInt32),
      .add,
      .localGet 5,
      .localSet 0,
      .localGet 0,
      .localGet 0,
      .const (10000 : UInt32),
      .divU,
      .localSet 5,
      .localGet 5,
      .const (10000 : UInt32),
      .mul,
      .sub,
      .localSet 7,
      .localGet 7,
      .const (65535 : UInt32),
      .and,
      .const (100 : UInt32),
      .divU,
      .localSet 8,
      .localGet 8,
      .const (1 : UInt32),
      .shl,
      .load16U (1049155 : UInt32),
      .store16 (0 : UInt32),
      .localGet 6,
      .const (4294967294 : UInt32),
      .add,
      .localGet 7,
      .localGet 8,
      .const (100 : UInt32),
      .mul,
      .sub,
      .const (65535 : UInt32),
      .and,
      .const (1 : UInt32),
      .shl,
      .load16U (1049155 : UInt32),
      .store16 (0 : UInt32),
      .localGet 3,
      .const (4294967292 : UInt32),
      .add,
      .localSet 3,
      .localGet 0,
      .const (9999999 : UInt32),
      .gtU,
      .br_if 0
    ]
  ],
  .block 0 0 [
    .block 0 0 [
      .localGet 5,
      .const (9 : UInt32),
      .gtU,
      .br_if 0,
      .localGet 5,
      .localSet 0,
      .br 1
    ],
    .localGet 2,
    .const (6 : UInt32),
    .add,
    .localGet 3,
    .const (4294967294 : UInt32),
    .add,
    .localSet 3,
    .localGet 3,
    .add,
    .localGet 5,
    .localGet 5,
    .const (65535 : UInt32),
    .and,
    .const (100 : UInt32),
    .divU,
    .localSet 0,
    .localGet 0,
    .const (100 : UInt32),
    .mul,
    .sub,
    .const (65535 : UInt32),
    .and,
    .const (1 : UInt32),
    .shl,
    .load16U (1049155 : UInt32),
    .store16 (0 : UInt32)
  ],
  .block 0 0 [
    .block 0 0 [
      .localGet 4,
      .eqz,
      .br_if 0,
      .localGet 0,
      .eqz,
      .br_if 1
    ],
    .localGet 2,
    .const (6 : UInt32),
    .add,
    .localGet 3,
    .const (4294967295 : UInt32),
    .add,
    .localSet 3,
    .localGet 3,
    .add,
    .localGet 0,
    .const (1 : UInt32),
    .shl,
    .load8U (1049156 : UInt32),
    .store8 (0 : UInt32)
  ],
  .localGet 1,
  .const (1 : UInt32),
  .const (1 : UInt32),
  .const (0 : UInt32),
  .localGet 2,
  .const (6 : UInt32),
  .add,
  .localGet 3,
  .add,
  .const (10 : UInt32),
  .localGet 3,
  .sub,
  .call 57,
  .localSet 3,
  .localGet 2,
  .const (16 : UInt32),
  .add,
  .globalSet 0,
  .localGet 3
]

def func61Def : Wasm.Function :=
  { params := [.i32, .i32], locals := [.i32, .i32, .i32, .i32, .i32, .i32, .i32], body := func61, 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,
    func55Def,
    func56Def,
    func57Def,
    func58Def,
    func59Def,
    func60Def,
    func61Def
  ],
  exports := [
    { name := "swap_elements", funcIdx := 4 }
  ],
  memory := some { pagesMin := (17 : UInt32), pagesMax := none, data := [
    { offset := some (1048576 : UInt32), bytes := [(115 : UInt8), (119 : UInt8), (97 : UInt8), (112 : UInt8), (95 : UInt8), (101 : UInt8), (108 : UInt8), (101 : UInt8), (109 : UInt8), (101 : UInt8), (110 : UInt8), (116 : UInt8), (115 : UInt8), (47 : UInt8), (115 : UInt8), (114 : UInt8), (99 : UInt8), (47 : UInt8), (108 : UInt8), (105 : UInt8), (98 : UInt8), (46 : UInt8), (114 : UInt8), (115 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (16 : UInt8), (0 : UInt8), (24 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (9 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (9 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (115 : UInt8), (119 : UInt8), (97 : UInt8), (112 : UInt8), (95 : UInt8), (101 : UInt8), (108 : UInt8), (101 : UInt8), (109 : UInt8), (101 : UInt8), (110 : UInt8), (116 : UInt8), (115 : 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), (0 : UInt8), (0 : UInt8), (44 : UInt8), (0 : UInt8), (16 : UInt8), (0 : UInt8), (28 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (13 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (24 : 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), (204 : 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), (204 : 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), (152 : 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), (32 : UInt8), (105 : UInt8), (110 : UInt8), (100 : UInt8), (101 : UInt8), (120 : UInt8), (32 : UInt8), (111 : UInt8), (117 : UInt8), (116 : UInt8), (32 : UInt8), (111 : UInt8), (102 : UInt8), (32 : UInt8), (98 : UInt8), (111 : UInt8), (117 : UInt8), (110 : UInt8), (100 : UInt8), (115 : UInt8), (58 : UInt8), (32 : UInt8), (116 : UInt8), (104 : UInt8), (101 : UInt8), (32 : UInt8), (108 : UInt8), (101 : UInt8), (110 : UInt8), (32 : UInt8), (105 : UInt8), (115 : UInt8), (32 : UInt8), (192 : UInt8), (18 : UInt8), (32 : UInt8), (98 : UInt8), (117 : UInt8), (116 : UInt8), (32 : UInt8), (116 : UInt8), (104 : UInt8), (101 : UInt8), (32 : UInt8), (105 : UInt8), (110 : UInt8), (100 : UInt8), (101 : UInt8), (120 : UInt8), (32 : UInt8), (105 : UInt8), (115 : UInt8), (32 : UInt8), (192 : UInt8), (0 : UInt8), (48 : UInt8), (48 : UInt8), (48 : UInt8), (49 : UInt8), (48 : UInt8), (50 : UInt8), (48 : UInt8), (51 : UInt8), (48 : UInt8), (52 : UInt8), (48 : UInt8), (53 : UInt8), (48 : UInt8), (54 : UInt8), (48 : UInt8), (55 : UInt8), (48 : UInt8), (56 : UInt8), (48 : UInt8), (57 : UInt8), (49 : UInt8), (48 : UInt8), (49 : UInt8), (49 : UInt8), (49 : UInt8), (50 : UInt8), (49 : UInt8), (51 : UInt8), (49 : UInt8), (52 : UInt8), (49 : UInt8), (53 : UInt8), (49 : UInt8), (54 : UInt8), (49 : UInt8), (55 : UInt8), (49 : UInt8), (56 : UInt8), (49 : UInt8), (57 : UInt8), (50 : UInt8), (48 : UInt8), (50 : UInt8), (49 : UInt8), (50 : UInt8), (50 : UInt8), (50 : UInt8), (51 : UInt8), (50 : UInt8), (52 : UInt8), (50 : UInt8), (53 : UInt8), (50 : UInt8), (54 : UInt8), (50 : UInt8), (55 : UInt8), (50 : UInt8), (56 : UInt8), (50 : UInt8), (57 : UInt8), (51 : UInt8), (48 : UInt8), (51 : UInt8), (49 : UInt8), (51 : UInt8), (50 : UInt8), (51 : UInt8), (51 : UInt8), (51 : UInt8), (52 : UInt8), (51 : UInt8), (53 : UInt8), (51 : UInt8), (54 : UInt8), (51 : UInt8), (55 : UInt8), (51 : UInt8), (56 : UInt8), (51 : UInt8), (57 : UInt8), (52 : UInt8), (48 : UInt8), (52 : UInt8), (49 : UInt8), (52 : UInt8), (50 : UInt8), (52 : UInt8), (51 : UInt8), (52 : UInt8), (52 : UInt8), (52 : UInt8), (53 : UInt8), (52 : UInt8), (54 : UInt8), (52 : UInt8), (55 : UInt8), (52 : UInt8), (56 : UInt8), (52 : UInt8), (57 : UInt8), (53 : UInt8), (48 : UInt8), (53 : UInt8), (49 : UInt8), (53 : UInt8), (50 : UInt8), (53 : UInt8), (51 : UInt8), (53 : UInt8), (52 : UInt8), (53 : UInt8), (53 : UInt8), (53 : UInt8), (54 : UInt8), (53 : UInt8), (55 : UInt8), (53 : UInt8), (56 : UInt8), (53 : UInt8), (57 : UInt8), (54 : UInt8), (48 : UInt8), (54 : UInt8), (49 : UInt8), (54 : UInt8), (50 : UInt8), (54 : UInt8), (51 : UInt8), (54 : UInt8), (52 : UInt8), (54 : UInt8), (53 : UInt8), (54 : UInt8), (54 : UInt8), (54 : UInt8), (55 : UInt8), (54 : UInt8), (56 : UInt8), (54 : UInt8), (57 : UInt8), (55 : UInt8), (48 : UInt8), (55 : UInt8), (49 : UInt8), (55 : UInt8), (50 : UInt8), (55 : UInt8), (51 : UInt8), (55 : UInt8), (52 : UInt8), (55 : UInt8), (53 : UInt8), (55 : UInt8), (54 : UInt8), (55 : UInt8), (55 : UInt8), (55 : UInt8), (56 : UInt8), (55 : UInt8), (57 : UInt8), (56 : UInt8), (48 : UInt8), (56 : UInt8), (49 : UInt8), (56 : UInt8), (50 : UInt8), (56 : UInt8), (51 : UInt8), (56 : UInt8), (52 : UInt8), (56 : UInt8), (53 : UInt8), (56 : UInt8), (54 : UInt8), (56 : UInt8), (55 : UInt8), (56 : UInt8), (56 : UInt8), (56 : UInt8), (57 : UInt8), (57 : UInt8), (48 : UInt8), (57 : UInt8), (49 : UInt8), (57 : UInt8), (50 : UInt8), (57 : UInt8), (51 : UInt8), (57 : UInt8), (52 : UInt8), (57 : UInt8), (53 : UInt8), (57 : UInt8), (54 : UInt8), (57 : UInt8), (55 : UInt8), (57 : UInt8), (56 : UInt8), (57 : UInt8), (57 : UInt8)] }
  ] },
  globals := [
    { init := .i32 (1048576 : UInt32) },
    { init := .i32 (1049837 : UInt32) },
    { init := .i32 (1049840 : UInt32) }
  ],
  types := [
    { params := [.i32, .i32], results := [] },
    { params := [.i32, .i32, .i32], results := [.i32] },
    { params := [.i32, .i32], results := [.i32] },
    { params := [.i32, .i32, .i32, .i32], results := [] },
    { params := [.i32, .i32, .i32, .i32, .i32], results := [] },
    { params := [.i32, .i32, .i32], results := [] },
    { params := [.i32, .i32, .i32, .i32], results := [.i32] },
    { params := [], results := [] },
    { params := [.i32], results := [] },
    { params := [.i32, .i32, .i32, .i32, .i32, .i32], results := [] },
    { params := [.i32], results := [.i32] },
    { params := [.i32, .i32, .i32, .i32, .i32, .i32], results := [.i32] },
    { params := [.i32, .i32, .i32, .i32, .i32], results := [.i32] }
  ],
  tables := [
    { min := 18, max := some 18, elemType := .funcref }
  ],
  elements := [
    { tableIdx := some 0, offset := some 1, funcs := [some 20, some 12, some 44, some 43, some 48, some 42, some 41, some 39, some 40, some 13, some 38, some 46, some 45, some 47, some 37, some 36, some 61] }
  ]
}

end Project.SwapElements
lean/Project/SwapElements/Spec.lean lean · 361 lines 
import Project.SwapElements.Program
import Interpreter.Wasm.Wp.Call
import Interpreter.Wasm.Wp.Tactic

/-!
# Specification and proof for `swap_elements`

The Rust source is

```rust
pub fn swap_elements(arr: &mut [u64], i: usize, j: usize) {
    arr.swap(i, j);
}
```

exposed across the wasm ABI as

```rust
pub extern "C" fn swap_elements(
    array_ptr: *mut u64, data_length: usize, i: usize, j: usize,
)
```

so the export receives four `i32` values `(array_ptr, data_length, i, j)`,
reconstitutes the slice `[array_ptr, array_ptr + 8 * data_length)` of 8-byte
`u64` elements, and swaps the elements at indices `i` and `j`.

The element at logical index `k` lives at byte address `array_ptr + 8 * k`
(elements are `u64`, eight bytes wide), read/written with `Mem.read64` /
`Mem.write64`.

Wasm's calling convention pushes arguments left-to-right, so the entry's value
stack (top first) is `[j, i, data_length, array_ptr]`, matching `localGet 0 =
array_ptr, … , localGet 3 = j`.

## Call graph (opt-level 0)

`func4` (the export) allocates a 16-byte shadow-stack frame, calls `func3` to
materialise the slice fat pointer `(ptr, len)` into that frame, reads it back,
and calls `func0`. `func0` forwards to `func1`, which bounds-checks `i, j < len`
(the two `panic` branches are unreachable under the precondition) and calls
`func2`, the leaf that performs the exchange through a scratch slot.

## Two preconditions beyond the informal contract

The `swap` is only well-defined once the shadow stack and address arithmetic
are pinned down; both facts hold for every store the module actually produces,
but neither is implied by the four informal preconditions, so they are stated
explicitly:

* **`st.globals.globals[0]? = some (.i32 1048576)`** — the shadow-stack pointer
  is at its module-initial value. `func4`/`func2` derive their scratch frames
  as `global 0 − 16` and `global 0 − 32`; without pinning `global 0` the callee
  frames could alias the array (or wrap), and the statement would be *false*.
* **`st.mem.pages ≤ 65536`** — the wasm32 architectural memory limit (the module
  itself declares `pagesMin = 17`). Together with the addressability bound this
  gives `ptr.toNat + 8*len.toNat ≤ 2^32`, so element addresses `ptr + 8*k` do
  not wrap `UInt32`; without it two distinct in-bounds indices could collide (or
  an element could alias the scratch slot) and, again, the statement would fail.

Both mirror the shadow-stack pin already used by e.g. `total_variation` and the
interpreter's own in-bounds model.
-/

namespace Project.SwapElements.Spec

open Wasm

/-- Byte address of the `k`-th `u64` element of an array based at `ptr`. -/
@[reducible] def elemAddr (ptr k : UInt32) : UInt32 := ptr + 8 * k

/-! ## Address arithmetic

`elemAddr ptr k` is definitionally `(MemRegion.slot64 ptr k).base`, so the
slot algebra from `CodeLib.RustStd.Region` applies directly; the local names
below just specialise it to the `elemAddr` spelling the spec uses. -/

/-- Address arithmetic the codegen emits: `(k <<< 3) + ptr = elemAddr ptr k`. -/
theorem elemAddr_of_shl (ptr k : UInt32) : k <<< (3 % 32 : UInt32) + ptr = elemAddr ptr k :=
  MemRegion.slot64_of_shl ptr k

/-- No address wraparound: for an element index whose byte offset stays below
`2^32`, the wasm address `ptr + 8*k` is the true integer `ptr.toNat + 8*k.toNat`. -/
theorem elemAddr_toNat (ptr k : UInt32) (h : ptr.toNat + 8 * k.toNat < 4294967296) :
    (elemAddr ptr k).toNat = ptr.toNat + 8 * k.toNat :=
  MemRegion.slot64_base_toNat ptr k h

/-- Two distinct in-bounds element addresses are 8-byte disjoint. -/
theorem elemAddr_disjoint (ptr k l : UInt32)
    (hk : ptr.toNat + 8 * k.toNat < 4294967296) (hl : ptr.toNat + 8 * l.toNat < 4294967296)
    (hkl : k ≠ l) :
    (elemAddr ptr k).toNat + 8 ≤ (elemAddr ptr l).toNat
      ∨ (elemAddr ptr l).toNat + 8 ≤ (elemAddr ptr k).toNat :=
  MemRegion.slot64_disjoint ptr k l hk hl hkl

/-! ## `func2`: the exchange leaf -/

/-- `func2` (index 2) swaps the two `u64` values at `pi` and `pj` using a
scratch slot at `1048552` (= `global0 − 16 + 8` with `global0 = 1048560`).
Stated with an explicit final-memory equation so callers can frame reads. -/
theorem func2_swap (env : HostEnv Unit) (st : Store Unit) (pi pj : UInt32)
    (rest : List Value)
    (hg : st.globals.globals[0]? = some (.i32 1048560))
    (hpiN : 1048576 ≤ pi.toNat) (hpiHi : pi.toNat + 8 ≤ st.mem.pages * 65536)
    (hpjN : 1048576 ≤ pj.toNat) (hpjHi : pj.toNat + 8 ≤ st.mem.pages * 65536) :
    TerminatesWith env «module» 2 st (.i32 pj :: .i32 pi :: rest)
      (fun st' vs => vs = rest ∧ st'.globals = st.globals ∧ st'.mem.pages = st.mem.pages
        ∧ st'.mem =
            ((st.mem.write64 1048552 (st.mem.read64 pi)).write64 pi
              (st.mem.read64 pj)).write64 pj (st.mem.read64 pi)) := by
  have c52 : (1048552 : UInt32).toNat = 1048552 := by decide
  have gpi : ¬ (st.mem.pages * 65536 < pi.toNat + 8) := by omega
  have gpj : ¬ (st.mem.pages * 65536 < pj.toNat + 8) := by omega
  have gscr : ¬ (st.mem.pages * 65536 < 1048560) := by omega
  have e1 : (st.mem.write64 1048552 (st.mem.read64 pi)).read64 pj = st.mem.read64 pj :=
    Mem.read64_write64_disjoint _ _ _ _ (Or.inr (by omega))
  have e2 : ((st.mem.write64 1048552 (st.mem.read64 pi)).write64 pi
              (st.mem.read64 pj)).read64 1048552 = st.mem.read64 pi := by
    rw [Mem.read64_write64_disjoint _ _ _ _ (Or.inl (by omega)), Mem.read64_write64_same]
  apply TerminatesWith.of_wp_entry_for (f := ⟨[.i32, .i32], [.i32], func2, [], none⟩) rfl
  unfold func2
  wp_run
  rw [hg]
  simp [gpi, gpj, gscr, e1, e2]

/-! ## `func1`: the bounds checks -/

/-- `func1` (index 1): bounds-checks `i, j < len` (both panic branches are
unreachable under the preconditions) and calls `func2` on `&arr[i]`, `&arr[j]`. -/
theorem func1_swap (env : HostEnv Unit) (st1 : Store Unit) (ptr len i j loc : UInt32)
    (rest : List Value)
    (hg : st1.globals.globals[0]? = some (.i32 1048560))
    (hi : i < len) (hj : j < len)
    (hptr : 1048576 ≤ ptr.toNat)
    (hbound : ptr.toNat + 8 * len.toNat ≤ st1.mem.pages * 65536)
    (hpages : st1.mem.pages ≤ 65536) :
    TerminatesWith env «module» 1 st1
      (.i32 loc :: .i32 j :: .i32 i :: .i32 len :: .i32 ptr :: rest)
      (fun st' vs => vs = rest ∧ st'.globals = st1.globals ∧ st'.mem.pages = st1.mem.pages
        ∧ st'.mem =
            ((st1.mem.write64 1048552 (st1.mem.read64 (elemAddr ptr i))).write64 (elemAddr ptr i)
              (st1.mem.read64 (elemAddr ptr j))).write64 (elemAddr ptr j)
              (st1.mem.read64 (elemAddr ptr i))) := by
  have hbnd : st1.mem.pages * 65536 ≤ 4294967296 := by
    have := Nat.mul_le_mul_right 65536 hpages; omega
  have hwi : ptr.toNat + 8 * i.toNat < 4294967296 := by
    have hli : i.toNat < len.toNat := hi; omega
  have hwj : ptr.toNat + 8 * j.toNat < 4294967296 := by
    have hlj : j.toNat < len.toNat := hj; omega
  have hpiN : 1048576 ≤ (elemAddr ptr i).toNat := by rw [elemAddr_toNat ptr i hwi]; omega
  have hpjN : 1048576 ≤ (elemAddr ptr j).toNat := by rw [elemAddr_toNat ptr j hwj]; omega
  have hpiHi : (elemAddr ptr i).toNat + 8 ≤ st1.mem.pages * 65536 := by
    rw [elemAddr_toNat ptr i hwi]
    have hli : i.toNat < len.toNat := hi; omega
  have hpjHi : (elemAddr ptr j).toNat + 8 ≤ st1.mem.pages * 65536 := by
    rw [elemAddr_toNat ptr j hwj]
    have hlj : j.toNat < len.toNat := hj; omega
  apply TerminatesWith.of_wp_entry_for
    (f := ⟨[.i32, .i32, .i32, .i32, .i32], [.i32], func1, [], none⟩) rfl
  unfold func1
  apply wp_block_cons
  apply wp_block_cons
  apply wp_block_cons
  simp only [wp_simp, Locals.get, Locals.set?, Function.toLocals,
    Function.numParams, List.take, List.drop, 
    List.length, List.map, ValueType.zero, 
    List.reverse_cons, List.reverse_nil, List.cons_append, List.nil_append, List.append_nil,
    
    List.getElem?_cons_zero, List.getElem?_cons_succ,
    List.set_cons_zero, List.set_cons_succ,
    Nat.reduceLT, Nat.reduceAdd, Nat.reduceSub, reduceIte,
    hi, hj, elemAddr_of_shl,
    show ((1 : UInt32) &&& 1) = 1 from rfl, show ((1 : UInt32) = 0) = False from by simp]
  apply wp_call_tw (func2_swap env st1 (elemAddr ptr i) (elemAddr ptr j) []
    hg hpiN hpiHi hpjN hpjHi)
  rintro st' vs ⟨rfl, hglob, hpg, hmem⟩
  wp_run
  exact ⟨trivial, hglob, hpg, hmem⟩

/-! ## `func0`: the forwarder -/

/-- `func0` (index 0): forwards `(ptr, len, i, j)` plus the panic-location
constant to `func1`. -/
theorem func0_swap (env : HostEnv Unit) (st0 : Store Unit) (ptr len i j : UInt32)
    (rest : List Value)
    (hg : st0.globals.globals[0]? = some (.i32 1048560))
    (hi : i < len) (hj : j < len)
    (hptr : 1048576 ≤ ptr.toNat)
    (hbound : ptr.toNat + 8 * len.toNat ≤ st0.mem.pages * 65536)
    (hpages : st0.mem.pages ≤ 65536) :
    TerminatesWith env «module» 0 st0
      (.i32 j :: .i32 i :: .i32 len :: .i32 ptr :: rest)
      (fun st' vs => vs = rest ∧ st'.globals = st0.globals ∧ st'.mem.pages = st0.mem.pages
        ∧ st'.mem =
            ((st0.mem.write64 1048552 (st0.mem.read64 (elemAddr ptr i))).write64 (elemAddr ptr i)
              (st0.mem.read64 (elemAddr ptr j))).write64 (elemAddr ptr j)
              (st0.mem.read64 (elemAddr ptr i))) := by
  apply TerminatesWith.of_wp_entry_for
    (f := ⟨[.i32, .i32, .i32, .i32], [], func0, [], none⟩) rfl
  unfold func0
  wp_run
  apply wp_call_tw (func1_swap env st0 ptr len i j 1048604 [] hg hi hj hptr hbound hpages)
  rintro st' vs ⟨rfl, hglob, hpg, hmem⟩
  wp_run
  exact ⟨by simp, hglob, hpg, hmem⟩

/-! ## `func3`: materialise the slice fat pointer -/

/-- `func3` (index 3): writes the slice fat pointer `(a, b)` to `[dest, dest+8)`
(`store32` of `b` at `dest+4`, then `a` at `dest`). -/
theorem func3_writes (env : HostEnv Unit) (st : Store Unit) (dest a b c : UInt32)
    (rest : List Value)
    (hdlt : dest.toNat + 8 ≤ st.mem.pages * 65536) :
    TerminatesWith env «module» 3 st (.i32 c :: .i32 b :: .i32 a :: .i32 dest :: rest)
      (fun st' vs => vs = rest ∧ st'.globals = st.globals ∧ st'.mem.pages = st.mem.pages
        ∧ st'.mem = (st.mem.write32 (dest + 4) b).write32 dest a) := by
  have g1 : ¬ (st.mem.pages * 65536 < dest.toNat + 4 + 4) := by omega
  have g2 : ¬ (st.mem.pages * 65536 < dest.toNat + 4) := by omega
  apply TerminatesWith.of_wp_entry_for
    (f := ⟨[.i32, .i32, .i32, .i32], [], func3, [], none⟩) rfl
  unfold func3
  wp_run
  simp [g1, g2]

/-! ## `func4`: the export -/

/-- Byte addresses of the fat-pointer frame slots. -/
private theorem tn68 : (1048568 : UInt32).toNat = 1048568 := by decide
private theorem tn72 : (1048572 : UInt32).toNat = 1048572 := by decide
private theorem tn52 : (1048552 : UInt32).toNat = 1048552 := by decide

/-- A `read64` at any array address (≥ 1048576) ignores `func3`'s two
`store32`s into the fat-pointer frame at `[1048568, 1048576)`. -/
private theorem frame_read64 (m : Mem) (len ptr x : UInt32) (hx : 1048576 ≤ x.toNat) :
    ((m.write32 1048572 len).write32 1048568 ptr).read64 x = m.read64 x := by
  rw [Mem.read64_write32_disjoint _ _ _ _ (Or.inl (by rw [tn68]; omega)),
      Mem.read64_write32_disjoint _ _ _ _ (Or.inl (by rw [tn72]; omega))]

/-- `func4` (index 4, the export): frame setup → `func3` → read the fat pointer
back → `func0` → frame teardown. Total-correctness swap over the array. -/
theorem func4_swap (env : HostEnv Unit) (st : Store Unit) (ptr len i j : UInt32)
    (hi : i < len) (hj : j < len)
    (hptr : 1048576 ≤ ptr.toNat)
    (hbound : ptr.toNat + 8 * len.toNat ≤ st.mem.pages * 65536)
    (hpages : st.mem.pages ≤ 65536)
    (hsp : st.globals.globals[0]? = some (.i32 1048576)) :
    TerminatesWith env «module» 4 st [.i32 j, .i32 i, .i32 len, .i32 ptr]
      (fun st' rs => rs = []
        ∧ st'.mem.read64 (elemAddr ptr i) = st.mem.read64 (elemAddr ptr j)
        ∧ st'.mem.read64 (elemAddr ptr j) = st.mem.read64 (elemAddr ptr i)
        ∧ ∀ k : UInt32, k < len → k ≠ i → k ≠ j →
            st'.mem.read64 (elemAddr ptr k) = st.mem.read64 (elemAddr ptr k)) := by
  have hbnd : st.mem.pages * 65536 ≤ 4294967296 := by
    have := Nat.mul_le_mul_right 65536 hpages; omega
  have hwi : ptr.toNat + 8 * i.toNat < 4294967296 := by
    have h : i.toNat < len.toNat := hi; omega
  have hwj : ptr.toNat + 8 * j.toNat < 4294967296 := by
    have h : j.toNat < len.toNat := hj; omega
  have hpiN : 1048576 ≤ (elemAddr ptr i).toNat := by rw [elemAddr_toNat ptr i hwi]; omega
  have hpjN : 1048576 ≤ (elemAddr ptr j).toNat := by rw [elemAddr_toNat ptr j hwj]; omega
  obtain ⟨hlen, -⟩ := List.getElem?_eq_some_iff.mp hsp
  apply TerminatesWith.of_wp_entry_for
    (f := ⟨[.i32, .i32, .i32, .i32], [.i32, .i32, .i32], func4, [], none⟩) rfl
  unfold func4
  wp_run
  rw [hsp]
  simp only [wp_simp, 
    
    List.length, 
    List.reverse_cons, List.reverse_nil, List.cons_append, List.nil_append, List.append_nil,
    List.length_cons, 
    List.getElem?_cons_zero, List.getElem?_cons_succ,
    List.set_cons_zero, List.set_cons_succ,
    UInt32.reduceSub, UInt32.reduceAdd, Nat.reduceAdd, Nat.reduceSub, Nat.reduceLT, reduceIte,
    ]
  apply wp_call_tw (func3_writes env _ 1048568 ptr len 1048652 []
    (by show (1048568 : UInt32).toNat + 8 ≤ st.mem.pages * 65536; rw [tn68]; omega))
  rintro sta vsa ⟨rfl, hga, hpa, hma⟩
  simp only [UInt32.reduceAdd] at hma
  have hpg_a : sta.mem.pages = st.mem.pages := by rw [hma]; simp
  have hglob0 : sta.globals.globals[0]? = some (.i32 1048560) := by
    rw [hga]; exact List.getElem?_set_self hlen
  have hrlen : sta.mem.read32 1048572 = len := by
    rw [hma, Mem.read32_write32_disjoint _ _ _ _ (by rw [tn68, tn72]; omega),
        Mem.read32_write32_same]
  have hrptr : sta.mem.read32 1048568 = ptr := by rw [hma, Mem.read32_write32_same]
  simp only [wp_simp, Locals.get, Locals.set?, 
    
    List.length, 
    
    
    List.getElem?_cons_zero, List.getElem?_cons_succ,
    List.set_cons_zero, List.set_cons_succ,
    UInt32.reduceToNat, UInt32.reduceAdd, Nat.reduceAdd, Nat.reduceSub, Nat.reduceLT, reduceIte,
    hrlen, hrptr,
    show ¬ (1048576 > sta.mem.pages * 65536) from by rw [hpg_a]; omega,
    show ¬ (1048572 > sta.mem.pages * 65536) from by rw [hpg_a]; omega]
  apply wp_call_tw (func0_swap env sta ptr len i j [] hglob0 hi hj hptr
    (by rw [hpg_a]; exact hbound) (by rw [hpg_a]; exact hpages))
  rintro stb vsb ⟨rfl, hgb, hpb, hmb⟩
  wp_run
  rw [hgb, hga, List.getElem?_set_self hlen]
  rw [hma] at hmb
  refine ⟨trivial, ?_, ?_, ?_⟩
  · rw [hmb]
    by_cases hij : i = j
    · subst hij; rw [Mem.read64_write64_same, frame_read64 _ _ _ _ hpiN]
    · rw [Mem.read64_write64_disjoint _ _ _ _ (elemAddr_disjoint ptr i j hwi hwj hij),
          Mem.read64_write64_same, frame_read64 _ _ _ _ hpjN]
  · rw [hmb, Mem.read64_write64_same, frame_read64 _ _ _ _ hpiN]
  · intro k hk hki hkj
    have hwk : ptr.toNat + 8 * k.toNat < 4294967296 := by
      have h : k.toNat < len.toNat := hk; omega
    have hpkN : 1048576 ≤ (elemAddr ptr k).toNat := by rw [elemAddr_toNat ptr k hwk]; omega
    rw [hmb,
        Mem.read64_write64_disjoint _ _ _ _ (elemAddr_disjoint ptr k j hwk hwj hkj),
        Mem.read64_write64_disjoint _ _ _ _ (elemAddr_disjoint ptr k i hwk hwi hki),
        Mem.read64_write64_disjoint _ _ _ _ (Or.inr (by rw [tn52]; omega)),
        frame_read64 _ _ _ _ hpkN]

/-! ## The registered spec -/

/-- The exported `swap_elements` swaps two elements of a `[u64]` slice in place.

Given indices `i, j` both in bounds (`< len`); an array region
`[ptr, ptr + 8 * len)` that is addressable (`ptr.toNat + 8 * len.toNat ≤
pages * 65536`), sits at or above the shadow-stack base (`1048576 ≤ ptr`, so the
callee scratch frames cannot alias it), and does not wrap (`pages ≤ 65536`, the
wasm32 limit); and the shadow-stack pointer at its initial value (`global 0 =
1048576`): the export terminates leaving no result and

* the element at index `i` now holds the previous element at index `j`;
* the element at index `j` now holds the previous element at index `i`;
* every other in-bounds element `k` (`k ≠ i`, `k ≠ j`) is unchanged.

See the module docstring for why the last two hypotheses are required — without
them the statement is not merely unprovable but false. -/
@[spec_of "rust-exported" "swap_elements::swap_elements"]
def SwapElementsSpec : Prop :=
  ∀ (env : HostEnv Unit) (st : Store Unit) (ptr len i j : UInt32),
    i < len → j < len →
    ptr.toNat + 8 * len.toNat ≤ st.mem.pages * 65536 →
    1048576 ≤ ptr.toNat →
    st.mem.pages ≤ 65536 →
    st.globals.globals[0]? = some (.i32 1048576) →
    TerminatesWith env «module» 4 st
      [.i32 j, .i32 i, .i32 len, .i32 ptr]
      (fun st' rs =>
        rs = []
        ∧ st'.mem.read64 (elemAddr ptr i) = st.mem.read64 (elemAddr ptr j)
        ∧ st'.mem.read64 (elemAddr ptr j) = st.mem.read64 (elemAddr ptr i)
        ∧ ∀ k : UInt32, k < len → k ≠ i → k ≠ j →
            st'.mem.read64 (elemAddr ptr k) = st.mem.read64 (elemAddr ptr k))

@[proves Project.SwapElements.Spec.SwapElementsSpec]
theorem swap_elements_correct : SwapElementsSpec := by
  intro env st ptr len i j hi hj hbound hptr hpages hsp
  exact func4_swap env st ptr len i j hi hj hptr hbound hpages hsp

end Project.SwapElements.Spec

Rust (2)

rust/swap_elements/src/exports.rs rust · 16 lines 
/// Wasm-exported entry point for `swap_elements`.
///
/// Thin `extern "C"` wrapper around the pure [`crate::swap_elements`]. The
/// project convention reserves this file for the wasm ABI surface, so the
/// export table matches exactly what the verifier reasons about.
///
/// Receives the array as a `(pointer, length)` pair plus the two indices to
/// swap. On wasm32 both `usize` and the pointer are 32-bit. The caller must
/// guarantee `i < data_length` and `j < data_length` and that
/// `[array_ptr, array_ptr + data_length)` is a valid, aligned `u64` region.
#[unsafe(no_mangle)]
pub extern "C" fn swap_elements(array_ptr: *mut u64, data_length: usize, i: usize, j: usize) {
    let arr = unsafe { core::slice::from_raw_parts_mut(array_ptr, data_length) };
    crate::swap_elements(arr, i, j);
}
rust/swap_elements/src/lib.rs rust · 11 lines 
mod exports;

/// Swap the elements at indices `i` and `j` of a mutable slice.
///
/// Pure logic kept here; the wasm ABI surface (raw pointer + length) lives in
/// `exports.rs`. Both `i` and `j` are assumed to be in bounds (`< arr.len()`),
/// matching the contract documented on the export.
pub fn swap_elements(arr: &mut [u64], i: usize, j: usize) {
    arr.swap(i, j);
}

Other (1)

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

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

[dependencies]