Talos · verification report
← all projects

rust_u64_tests verified

rust: rust/rust_u64_tests · lean: lean/Project/RustU64Tests · repo @ ee45cadd9455 · leanprover/lean4:v4.32.0
0 / 0 exports have a proven spec
Exports
0
Specs
22
Verifications
22
Diagnostics
44

Formal specs

Project.RustU64Tests.Spec.AddChainSpec lean/Project/RustU64Tests/Spec.lean:63
1 proof

Informal spec

No informal description provided.

Formal statement

AddChainSpec : Prop := ∀ (a b c : UInt64),

Proofs

↗ Project.RustU64Tests.Spec.add_chain_correct

Rust binding

No @[spec_of "rust-exported" …] reference. Cannot link to a Rust export.

References

  • rust-exported rust_u64_tests::add_chain
Project.RustU64Tests.Spec.AddThenMulSpec lean/Project/RustU64Tests/Spec.lean:90
1 proof

Informal spec

No informal description provided.

Formal statement

AddThenMulSpec : Prop := ∀ (a b c : UInt64),

Proofs

↗ Project.RustU64Tests.Spec.add_then_mul_correct

Rust binding

No @[spec_of "rust-exported" …] reference. Cannot link to a Rust export.

References

  • rust-exported rust_u64_tests::add_then_mul
Project.RustU64Tests.Spec.SubChainSpec lean/Project/RustU64Tests/Spec.lean:118
1 proof

Informal spec

No informal description provided.

Formal statement

SubChainSpec : Prop := ∀ (a b c : UInt64),

Proofs

↗ Project.RustU64Tests.Spec.sub_chain_correct

Rust binding

No @[spec_of "rust-exported" …] reference. Cannot link to a Rust export.

References

  • rust-exported rust_u64_tests::sub_chain
Project.RustU64Tests.Spec.SubThenAddSpec lean/Project/RustU64Tests/Spec.lean:145
1 proof

Informal spec

No informal description provided.

Formal statement

SubThenAddSpec : Prop := ∀ (a b c : UInt64),

Proofs

↗ Project.RustU64Tests.Spec.sub_then_add_correct

Rust binding

No @[spec_of "rust-exported" …] reference. Cannot link to a Rust export.

References

  • rust-exported rust_u64_tests::sub_then_add
Project.RustU64Tests.Spec.MulChainSpec lean/Project/RustU64Tests/Spec.lean:173
1 proof

Informal spec

No informal description provided.

Formal statement

MulChainSpec : Prop := ∀ (a b c : UInt64),

Proofs

↗ Project.RustU64Tests.Spec.mul_chain_correct

Rust binding

No @[spec_of "rust-exported" …] reference. Cannot link to a Rust export.

References

  • rust-exported rust_u64_tests::mul_chain
Project.RustU64Tests.Spec.MulThenAddSpec lean/Project/RustU64Tests/Spec.lean:200
1 proof

Informal spec

No informal description provided.

Formal statement

MulThenAddSpec : Prop := ∀ (a b c : UInt64),

Proofs

↗ Project.RustU64Tests.Spec.mul_then_add_correct

Rust binding

No @[spec_of "rust-exported" …] reference. Cannot link to a Rust export.

References

  • rust-exported rust_u64_tests::mul_then_add
Project.RustU64Tests.Spec.AndChainSpec lean/Project/RustU64Tests/Spec.lean:228
1 proof

Informal spec

No informal description provided.

Formal statement

AndChainSpec : Prop := ∀ (a b c : UInt64),

Proofs

↗ Project.RustU64Tests.Spec.and_chain_correct

Rust binding

No @[spec_of "rust-exported" …] reference. Cannot link to a Rust export.

References

  • rust-exported rust_u64_tests::and_chain
Project.RustU64Tests.Spec.AndThenOrSpec lean/Project/RustU64Tests/Spec.lean:255
1 proof

Informal spec

No informal description provided.

Formal statement

AndThenOrSpec : Prop := ∀ (a b c : UInt64),

Proofs

↗ Project.RustU64Tests.Spec.and_then_or_correct

Rust binding

No @[spec_of "rust-exported" …] reference. Cannot link to a Rust export.

References

  • rust-exported rust_u64_tests::and_then_or
Project.RustU64Tests.Spec.OrChainSpec lean/Project/RustU64Tests/Spec.lean:283
1 proof

Informal spec

No informal description provided.

Formal statement

OrChainSpec : Prop := ∀ (a b c : UInt64),

Proofs

↗ Project.RustU64Tests.Spec.or_chain_correct

Rust binding

No @[spec_of "rust-exported" …] reference. Cannot link to a Rust export.

References

  • rust-exported rust_u64_tests::or_chain
Project.RustU64Tests.Spec.OrThenXorSpec lean/Project/RustU64Tests/Spec.lean:310
1 proof

Informal spec

No informal description provided.

Formal statement

OrThenXorSpec : Prop := ∀ (a b c : UInt64),

Proofs

↗ Project.RustU64Tests.Spec.or_then_xor_correct

Rust binding

No @[spec_of "rust-exported" …] reference. Cannot link to a Rust export.

References

  • rust-exported rust_u64_tests::or_then_xor
Project.RustU64Tests.Spec.XorChainSpec lean/Project/RustU64Tests/Spec.lean:338
1 proof

Informal spec

No informal description provided.

Formal statement

XorChainSpec : Prop := ∀ (a b c : UInt64),

Proofs

↗ Project.RustU64Tests.Spec.xor_chain_correct

Rust binding

No @[spec_of "rust-exported" …] reference. Cannot link to a Rust export.

References

  • rust-exported rust_u64_tests::xor_chain
Project.RustU64Tests.Spec.XorThenAndSpec lean/Project/RustU64Tests/Spec.lean:365
1 proof

Informal spec

No informal description provided.

Formal statement

XorThenAndSpec : Prop := ∀ (a b c : UInt64),

Proofs

↗ Project.RustU64Tests.Spec.xor_then_and_correct

Rust binding

No @[spec_of "rust-exported" …] reference. Cannot link to a Rust export.

References

  • rust-exported rust_u64_tests::xor_then_and
Project.RustU64Tests.Spec.NotTwiceSpec lean/Project/RustU64Tests/Spec.lean:393
1 proof

Informal spec

No informal description provided.

Formal statement

NotTwiceSpec : Prop := ∀ (a : UInt64),

Proofs

↗ Project.RustU64Tests.Spec.not_twice_correct

Rust binding

No @[spec_of "rust-exported" …] reference. Cannot link to a Rust export.

References

  • rust-exported rust_u64_tests::not_twice
Project.RustU64Tests.Spec.NotThenXorSpec lean/Project/RustU64Tests/Spec.lean:423
1 proof

Informal spec

No informal description provided.

Formal statement

NotThenXorSpec : Prop := ∀ (a b : UInt64),

Proofs

↗ Project.RustU64Tests.Spec.not_then_xor_correct

Rust binding

No @[spec_of "rust-exported" …] reference. Cannot link to a Rust export.

References

  • rust-exported rust_u64_tests::not_then_xor
Project.RustU64Tests.Spec.DivThenAddSpec lean/Project/RustU64Tests/Spec.lean:452
1 proof

Informal spec

No informal description provided.

Formal statement

DivThenAddSpec : Prop := ∀ (a b c : UInt64), b ≠ 0 →

Proofs

↗ Project.RustU64Tests.Spec.div_then_add_correct

Rust binding

No @[spec_of "rust-exported" …] reference. Cannot link to a Rust export.

References

  • rust-exported rust_u64_tests::div_then_add
Project.RustU64Tests.Spec.DivThenMulSpec lean/Project/RustU64Tests/Spec.lean:494
1 proof

Informal spec

No informal description provided.

Formal statement

DivThenMulSpec : Prop := ∀ (a b c : UInt64), b ≠ 0 →

Proofs

↗ Project.RustU64Tests.Spec.div_then_mul_correct

Rust binding

No @[spec_of "rust-exported" …] reference. Cannot link to a Rust export.

References

  • rust-exported rust_u64_tests::div_then_mul
Project.RustU64Tests.Spec.RemThenAddSpec lean/Project/RustU64Tests/Spec.lean:537
1 proof

Informal spec

No informal description provided.

Formal statement

RemThenAddSpec : Prop := ∀ (a b c : UInt64), b ≠ 0 →

Proofs

↗ Project.RustU64Tests.Spec.rem_then_add_correct

Rust binding

No @[spec_of "rust-exported" …] reference. Cannot link to a Rust export.

References

  • rust-exported rust_u64_tests::rem_then_add
Project.RustU64Tests.Spec.RemThenMulSpec lean/Project/RustU64Tests/Spec.lean:579
1 proof

Informal spec

No informal description provided.

Formal statement

RemThenMulSpec : Prop := ∀ (a b c : UInt64), b ≠ 0 →

Proofs

↗ Project.RustU64Tests.Spec.rem_then_mul_correct

Rust binding

No @[spec_of "rust-exported" …] reference. Cannot link to a Rust export.

References

  • rust-exported rust_u64_tests::rem_then_mul
Project.RustU64Tests.Spec.ShlThenAddSpec lean/Project/RustU64Tests/Spec.lean:622
1 proof

Informal spec

No informal description provided.

Formal statement

ShlThenAddSpec : Prop := ∀ (a : UInt64) (n : UInt32) (b : UInt64),

Proofs

↗ Project.RustU64Tests.Spec.shl_then_add_correct

Rust binding

No @[spec_of "rust-exported" …] reference. Cannot link to a Rust export.

References

  • rust-exported rust_u64_tests::shl_then_add
Project.RustU64Tests.Spec.ShlTwiceSpec lean/Project/RustU64Tests/Spec.lean:657
1 proof

Informal spec

No informal description provided.

Formal statement

ShlTwiceSpec : Prop := ∀ (a : UInt64) (n m : UInt32),

Proofs

↗ Project.RustU64Tests.Spec.shl_twice_correct

Rust binding

No @[spec_of "rust-exported" …] reference. Cannot link to a Rust export.

References

  • rust-exported rust_u64_tests::shl_twice
Project.RustU64Tests.Spec.ShrThenSubSpec lean/Project/RustU64Tests/Spec.lean:701
1 proof

Informal spec

No informal description provided.

Formal statement

ShrThenSubSpec : Prop := ∀ (a : UInt64) (n : UInt32) (b : UInt64),

Proofs

↗ Project.RustU64Tests.Spec.shr_then_sub_correct

Rust binding

No @[spec_of "rust-exported" …] reference. Cannot link to a Rust export.

References

  • rust-exported rust_u64_tests::shr_then_sub
Project.RustU64Tests.Spec.ShrTwiceSpec lean/Project/RustU64Tests/Spec.lean:736
1 proof

Informal spec

No informal description provided.

Formal statement

ShrTwiceSpec : Prop := ∀ (a : UInt64) (n m : UInt32),

Proofs

↗ Project.RustU64Tests.Spec.shr_twice_correct

Rust binding

No @[spec_of "rust-exported" …] reference. Cannot link to a Rust export.

References

  • rust-exported rust_u64_tests::shr_twice

Exported functions

No #[no_mangle] extern "C" exports were discovered by the extractor.

Program (Lean)

Project.RustU64Tests.module lean/Project/RustU64Tests/Program.lean:6174 
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,
    func62Def,
    func63Def,
    func64Def,
    func65Def,
    func66Def,
    func67Def,
    func68Def,
    func69Def,
    func70Def,
    func71Def,
    func72Def,
    func73Def,
    func74Def,
    func75Def
  ],
  exports := [
    { name := "add_chain", funcIdx := 0 },
    { name := "add_then_mul", funcIdx := 1 },
    { name := "and_chain", funcIdx := 2 },
    { name := "and_then_or", funcIdx := 3 },
    { name := "div_then_add", funcIdx := 4 },
    { name := "div_then_mul", funcIdx := 5 },
    { name := "mul_chain", funcIdx := 6 },
    { name := "mul_then_add", funcIdx := 7 },
    { name := "not_then_xor", funcIdx := 8 },
    { name := "not_twice", funcIdx := 9 },
    { name := "or_chain", funcIdx := 10 },
    { name := "or_then_xor", funcIdx := 11 },
    { name := "rem_then_add", funcIdx := 12 },
    { name := "rem_then_mul", funcIdx := 13 },
    { name := "shl_then_add", funcIdx := 14 },
    { name := "shl_twice", funcIdx := 15 },
    { name := "shr_then_sub", funcIdx := 16 },
    { name := "shr_twice", funcIdx := 17 },
    { name := "sub_chain", funcIdx := 18 },
    { name := "sub_then_add", funcIdx := 19 },
    { name := "xor_chain", funcIdx := 20 },
    { name := "xor_then_and", funcIdx := 21 }
  ],
  memory := some { pagesMin := (17 : UInt32), pagesMax := none, data := [
    { offset := some (1048576 : UInt32), bytes := [(114 : UInt8), (117 : UInt8), (115 : UInt8), (116 : UInt8), (95 : UInt8), (117 : UInt8), (54 : UInt8), (52 : UInt8), (95 : UInt8), (116 : UInt8), (101 : UInt8), (115 : 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), (0 : UInt8), (16 : UInt8), (0 : UInt8), (29 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (47 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (86 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (16 : UInt8), (0 : UInt8), (29 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (48 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (86 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (16 : UInt8), (0 : UInt8), (29 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (51 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (86 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (16 : UInt8), (0 : UInt8), (29 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (52 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (86 : 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), (208 : 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), (208 : 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), (156 : 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), (97 : UInt8), (116 : UInt8), (116 : UInt8), (101 : UInt8), (109 : UInt8), (112 : UInt8), (116 : UInt8), (32 : UInt8), (116 : UInt8), (111 : UInt8), (32 : UInt8), (100 : UInt8), (105 : UInt8), (118 : UInt8), (105 : UInt8), (100 : UInt8), (101 : UInt8), (32 : UInt8), (98 : UInt8), (121 : UInt8), (32 : UInt8), (122 : UInt8), (101 : UInt8), (114 : UInt8), (111 : UInt8), (97 : UInt8), (116 : UInt8), (116 : UInt8), (101 : UInt8), (109 : UInt8), (112 : UInt8), (116 : UInt8), (32 : UInt8), (116 : UInt8), (111 : UInt8), (32 : UInt8), (99 : UInt8), (97 : UInt8), (108 : UInt8), (99 : UInt8), (117 : UInt8), (108 : UInt8), (97 : UInt8), (116 : UInt8), (101 : UInt8), (32 : UInt8), (116 : UInt8), (104 : UInt8), (101 : UInt8), (32 : UInt8), (114 : UInt8), (101 : UInt8), (109 : UInt8), (97 : UInt8), (105 : UInt8), (110 : UInt8), (100 : UInt8), (101 : UInt8), (114 : UInt8), (32 : UInt8), (119 : UInt8), (105 : UInt8), (116 : UInt8), (104 : UInt8), (32 : UInt8), (97 : UInt8), (32 : UInt8), (100 : UInt8), (105 : UInt8), (118 : UInt8), (105 : UInt8), (115 : UInt8), (111 : UInt8), (114 : UInt8), (32 : UInt8), (111 : UInt8), (102 : UInt8), (32 : UInt8), (122 : UInt8), (101 : UInt8), (114 : UInt8), (111 : UInt8)] }
  ] },
  globals := [
    { init := .i32 (1048576 : UInt32) },
    { init := .i32 (1049669 : UInt32) },
    { init := .i32 (1049680 : UInt32) }
  ],
  types := [
    { params := [.i32, .i32], results := [] },
    { params := [.i32, .i32, .i32], results := [.i32] },
    { params := [.i32, .i32], results := [.i32] },
    { params := [.i64, .i64, .i64], results := [.i64] },
    { params := [.i64, .i64], results := [.i64] },
    { params := [.i64], results := [.i64] },
    { params := [.i64, .i32, .i64], results := [.i64] },
    { params := [.i64, .i32, .i32], results := [.i64] },
    { params := [.i32, .i32, .i32], results := [] },
    { params := [.i32, .i32, .i32, .i32], results := [.i32] },
    { params := [], results := [] },
    { params := [.i32, .i32, .i32, .i32, .i32], results := [] },
    { params := [.i32], results := [] },
    { params := [.i32, .i32, .i32, .i32, .i32, .i32], results := [] },
    { params := [.i32], results := [.i32] }
  ],
  tables := [
    { min := 17, max := some 17, elemType := .funcref }
  ],
  elements := [
    { tableIdx := some 0, offset := some 1, funcs := [some 37, some 29, some 61, some 60, some 65, some 59, some 58, some 56, some 57, some 30, some 55, some 63, some 62, some 64, some 54, some 53] }
  ]
}

Diagnostics

unresolved_spec_of_target warn
lean/Project/RustU64Tests/Spec.lean:64
`rust_u64_tests::add_chain` does not resolve to any export of crate `rust_u64_tests`
missing_docstring info
lean/Project/RustU64Tests/Spec.lean:63
spec `Project.RustU64Tests.Spec.AddChainSpec` has no `/-- … -/` docstring
unresolved_spec_of_target warn
lean/Project/RustU64Tests/Spec.lean:91
`rust_u64_tests::add_then_mul` does not resolve to any export of crate `rust_u64_tests`
missing_docstring info
lean/Project/RustU64Tests/Spec.lean:90
spec `Project.RustU64Tests.Spec.AddThenMulSpec` has no `/-- … -/` docstring
unresolved_spec_of_target warn
lean/Project/RustU64Tests/Spec.lean:119
`rust_u64_tests::sub_chain` does not resolve to any export of crate `rust_u64_tests`
missing_docstring info
lean/Project/RustU64Tests/Spec.lean:118
spec `Project.RustU64Tests.Spec.SubChainSpec` has no `/-- … -/` docstring
unresolved_spec_of_target warn
lean/Project/RustU64Tests/Spec.lean:146
`rust_u64_tests::sub_then_add` does not resolve to any export of crate `rust_u64_tests`
missing_docstring info
lean/Project/RustU64Tests/Spec.lean:145
spec `Project.RustU64Tests.Spec.SubThenAddSpec` has no `/-- … -/` docstring
unresolved_spec_of_target warn
lean/Project/RustU64Tests/Spec.lean:174
`rust_u64_tests::mul_chain` does not resolve to any export of crate `rust_u64_tests`
missing_docstring info
lean/Project/RustU64Tests/Spec.lean:173
spec `Project.RustU64Tests.Spec.MulChainSpec` has no `/-- … -/` docstring
unresolved_spec_of_target warn
lean/Project/RustU64Tests/Spec.lean:201
`rust_u64_tests::mul_then_add` does not resolve to any export of crate `rust_u64_tests`
missing_docstring info
lean/Project/RustU64Tests/Spec.lean:200
spec `Project.RustU64Tests.Spec.MulThenAddSpec` has no `/-- … -/` docstring
unresolved_spec_of_target warn
lean/Project/RustU64Tests/Spec.lean:229
`rust_u64_tests::and_chain` does not resolve to any export of crate `rust_u64_tests`
missing_docstring info
lean/Project/RustU64Tests/Spec.lean:228
spec `Project.RustU64Tests.Spec.AndChainSpec` has no `/-- … -/` docstring
unresolved_spec_of_target warn
lean/Project/RustU64Tests/Spec.lean:256
`rust_u64_tests::and_then_or` does not resolve to any export of crate `rust_u64_tests`
missing_docstring info
lean/Project/RustU64Tests/Spec.lean:255
spec `Project.RustU64Tests.Spec.AndThenOrSpec` has no `/-- … -/` docstring
unresolved_spec_of_target warn
lean/Project/RustU64Tests/Spec.lean:284
`rust_u64_tests::or_chain` does not resolve to any export of crate `rust_u64_tests`
missing_docstring info
lean/Project/RustU64Tests/Spec.lean:283
spec `Project.RustU64Tests.Spec.OrChainSpec` has no `/-- … -/` docstring
unresolved_spec_of_target warn
lean/Project/RustU64Tests/Spec.lean:311
`rust_u64_tests::or_then_xor` does not resolve to any export of crate `rust_u64_tests`
missing_docstring info
lean/Project/RustU64Tests/Spec.lean:310
spec `Project.RustU64Tests.Spec.OrThenXorSpec` has no `/-- … -/` docstring
unresolved_spec_of_target warn
lean/Project/RustU64Tests/Spec.lean:339
`rust_u64_tests::xor_chain` does not resolve to any export of crate `rust_u64_tests`
missing_docstring info
lean/Project/RustU64Tests/Spec.lean:338
spec `Project.RustU64Tests.Spec.XorChainSpec` has no `/-- … -/` docstring
unresolved_spec_of_target warn
lean/Project/RustU64Tests/Spec.lean:366
`rust_u64_tests::xor_then_and` does not resolve to any export of crate `rust_u64_tests`
missing_docstring info
lean/Project/RustU64Tests/Spec.lean:365
spec `Project.RustU64Tests.Spec.XorThenAndSpec` has no `/-- … -/` docstring
unresolved_spec_of_target warn
lean/Project/RustU64Tests/Spec.lean:394
`rust_u64_tests::not_twice` does not resolve to any export of crate `rust_u64_tests`
missing_docstring info
lean/Project/RustU64Tests/Spec.lean:393
spec `Project.RustU64Tests.Spec.NotTwiceSpec` has no `/-- … -/` docstring
unresolved_spec_of_target warn
lean/Project/RustU64Tests/Spec.lean:424
`rust_u64_tests::not_then_xor` does not resolve to any export of crate `rust_u64_tests`
missing_docstring info
lean/Project/RustU64Tests/Spec.lean:423
spec `Project.RustU64Tests.Spec.NotThenXorSpec` has no `/-- … -/` docstring
unresolved_spec_of_target warn
lean/Project/RustU64Tests/Spec.lean:453
`rust_u64_tests::div_then_add` does not resolve to any export of crate `rust_u64_tests`
missing_docstring info
lean/Project/RustU64Tests/Spec.lean:452
spec `Project.RustU64Tests.Spec.DivThenAddSpec` has no `/-- … -/` docstring
unresolved_spec_of_target warn
lean/Project/RustU64Tests/Spec.lean:495
`rust_u64_tests::div_then_mul` does not resolve to any export of crate `rust_u64_tests`
missing_docstring info
lean/Project/RustU64Tests/Spec.lean:494
spec `Project.RustU64Tests.Spec.DivThenMulSpec` has no `/-- … -/` docstring
unresolved_spec_of_target warn
lean/Project/RustU64Tests/Spec.lean:538
`rust_u64_tests::rem_then_add` does not resolve to any export of crate `rust_u64_tests`
missing_docstring info
lean/Project/RustU64Tests/Spec.lean:537
spec `Project.RustU64Tests.Spec.RemThenAddSpec` has no `/-- … -/` docstring
unresolved_spec_of_target warn
lean/Project/RustU64Tests/Spec.lean:580
`rust_u64_tests::rem_then_mul` does not resolve to any export of crate `rust_u64_tests`
missing_docstring info
lean/Project/RustU64Tests/Spec.lean:579
spec `Project.RustU64Tests.Spec.RemThenMulSpec` has no `/-- … -/` docstring
unresolved_spec_of_target warn
lean/Project/RustU64Tests/Spec.lean:623
`rust_u64_tests::shl_then_add` does not resolve to any export of crate `rust_u64_tests`
missing_docstring info
lean/Project/RustU64Tests/Spec.lean:622
spec `Project.RustU64Tests.Spec.ShlThenAddSpec` has no `/-- … -/` docstring
unresolved_spec_of_target warn
lean/Project/RustU64Tests/Spec.lean:658
`rust_u64_tests::shl_twice` does not resolve to any export of crate `rust_u64_tests`
missing_docstring info
lean/Project/RustU64Tests/Spec.lean:657
spec `Project.RustU64Tests.Spec.ShlTwiceSpec` has no `/-- … -/` docstring
unresolved_spec_of_target warn
lean/Project/RustU64Tests/Spec.lean:702
`rust_u64_tests::shr_then_sub` does not resolve to any export of crate `rust_u64_tests`
missing_docstring info
lean/Project/RustU64Tests/Spec.lean:701
spec `Project.RustU64Tests.Spec.ShrThenSubSpec` has no `/-- … -/` docstring
unresolved_spec_of_target warn
lean/Project/RustU64Tests/Spec.lean:737
`rust_u64_tests::shr_twice` does not resolve to any export of crate `rust_u64_tests`
missing_docstring info
lean/Project/RustU64Tests/Spec.lean:736
spec `Project.RustU64Tests.Spec.ShrTwiceSpec` has no `/-- … -/` docstring

Source files (appendix)

Lean (2)

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

import CodeLib

set_option maxRecDepth 1048576

namespace Project.RustU64Tests

open Wasm

/-- export: add_chain -/
def func0 : Wasm.Program :=
  [
  .localGet 0,
  .localGet 1,
  .addI64,
  .localGet 2,
  .addI64,
  .ret
]

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

/-- export: add_then_mul -/
def func1 : Wasm.Program :=
  [
  .localGet 0,
  .localGet 1,
  .addI64,
  .localGet 2,
  .mulI64,
  .ret
]

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

/-- export: and_chain -/
def func2 : Wasm.Program :=
  [
  .localGet 0,
  .localGet 1,
  .andI64,
  .localGet 2,
  .andI64,
  .ret
]

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

/-- export: and_then_or -/
def func3 : Wasm.Program :=
  [
  .localGet 0,
  .localGet 1,
  .andI64,
  .localGet 2,
  .orI64,
  .ret
]

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

/-- export: div_then_add -/
def func4 : Wasm.Program :=
  [
  .block 0 0 [
    .localGet 1,
    .constI64 (0 : UInt64),
    .eqI64,
    .const (1 : UInt32),
    .and,
    .br_if 0,
    .localGet 0,
    .localGet 1,
    .divUI64,
    .localGet 2,
    .addI64,
    .ret
  ],
  .const (1048608 : UInt32),
  .call 74,
  .unreachable
]

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

/-- export: div_then_mul -/
def func5 : Wasm.Program :=
  [
  .block 0 0 [
    .localGet 1,
    .constI64 (0 : UInt64),
    .eqI64,
    .const (1 : UInt32),
    .and,
    .br_if 0,
    .localGet 0,
    .localGet 1,
    .divUI64,
    .localGet 2,
    .mulI64,
    .ret
  ],
  .const (1048624 : UInt32),
  .call 74,
  .unreachable
]

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

/-- export: mul_chain -/
def func6 : Wasm.Program :=
  [
  .localGet 0,
  .localGet 1,
  .mulI64,
  .localGet 2,
  .mulI64,
  .ret
]

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

/-- export: mul_then_add -/
def func7 : Wasm.Program :=
  [
  .localGet 0,
  .localGet 1,
  .mulI64,
  .localGet 2,
  .addI64,
  .ret
]

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

/-- export: not_then_xor -/
def func8 : Wasm.Program :=
  [
  .localGet 0,
  .constI64 (18446744073709551615 : UInt64),
  .xorI64,
  .localGet 1,
  .xorI64,
  .ret
]

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

/-- export: not_twice -/
def func9 : Wasm.Program :=
  [
  .localGet 0,
  .constI64 (18446744073709551615 : UInt64),
  .xorI64,
  .constI64 (18446744073709551615 : UInt64),
  .xorI64,
  .ret
]

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

/-- export: or_chain -/
def func10 : Wasm.Program :=
  [
  .localGet 0,
  .localGet 1,
  .orI64,
  .localGet 2,
  .orI64,
  .ret
]

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

/-- export: or_then_xor -/
def func11 : Wasm.Program :=
  [
  .localGet 0,
  .localGet 1,
  .orI64,
  .localGet 2,
  .xorI64,
  .ret
]

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

/-- export: rem_then_add -/
def func12 : Wasm.Program :=
  [
  .block 0 0 [
    .localGet 1,
    .constI64 (0 : UInt64),
    .eqI64,
    .const (1 : UInt32),
    .and,
    .br_if 0,
    .localGet 0,
    .localGet 1,
    .remUI64,
    .localGet 2,
    .addI64,
    .ret
  ],
  .const (1048640 : UInt32),
  .call 75,
  .unreachable
]

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

/-- export: rem_then_mul -/
def func13 : Wasm.Program :=
  [
  .block 0 0 [
    .localGet 1,
    .constI64 (0 : UInt64),
    .eqI64,
    .const (1 : UInt32),
    .and,
    .br_if 0,
    .localGet 0,
    .localGet 1,
    .remUI64,
    .localGet 2,
    .mulI64,
    .ret
  ],
  .const (1048656 : UInt32),
  .call 75,
  .unreachable
]

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

/-- export: shl_then_add -/
def func14 : Wasm.Program :=
  [
  .localGet 0,
  .localGet 1,
  .const (63 : UInt32),
  .and,
  .extendUI32,
  .shlI64,
  .localGet 2,
  .addI64,
  .ret
]

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

/-- export: shl_twice -/
def func15 : Wasm.Program :=
  [
  .localGet 0,
  .localGet 1,
  .const (63 : UInt32),
  .and,
  .extendUI32,
  .shlI64,
  .localGet 2,
  .const (63 : UInt32),
  .and,
  .extendUI32,
  .shlI64,
  .ret
]

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

/-- export: shr_then_sub -/
def func16 : Wasm.Program :=
  [
  .localGet 0,
  .localGet 1,
  .const (63 : UInt32),
  .and,
  .extendUI32,
  .shrUI64,
  .localGet 2,
  .subI64,
  .ret
]

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

/-- export: shr_twice -/
def func17 : Wasm.Program :=
  [
  .localGet 0,
  .localGet 1,
  .const (63 : UInt32),
  .and,
  .extendUI32,
  .shrUI64,
  .localGet 2,
  .const (63 : UInt32),
  .and,
  .extendUI32,
  .shrUI64,
  .ret
]

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

/-- export: sub_chain -/
def func18 : Wasm.Program :=
  [
  .localGet 0,
  .localGet 1,
  .subI64,
  .localGet 2,
  .subI64,
  .ret
]

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

/-- export: sub_then_add -/
def func19 : Wasm.Program :=
  [
  .localGet 0,
  .localGet 1,
  .subI64,
  .localGet 2,
  .addI64,
  .ret
]

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

/-- export: xor_chain -/
def func20 : Wasm.Program :=
  [
  .localGet 0,
  .localGet 1,
  .xorI64,
  .localGet 2,
  .xorI64,
  .ret
]

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

/-- export: xor_then_and -/
def func21 : Wasm.Program :=
  [
  .localGet 0,
  .localGet 1,
  .xorI64,
  .localGet 2,
  .andI64,
  .ret
]

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

def func22 : Wasm.Program :=
  [
  .localGet 0,
  .localGet 1,
  .call 39,
  .ret
]

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

def func23 : Wasm.Program :=
  [
  .localGet 0,
  .localGet 1,
  .localGet 2,
  .call 43,
  .ret
]

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

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

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

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

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

def func26 : Wasm.Program :=
  [
  .call 42,
  .unreachable
]

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

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

def func28 : 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 23
  ]
]

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

def func29 : 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 23
  ]
]

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

def func30 : 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 23
  ]
]

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

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

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

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

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

def func33 : Wasm.Program :=
  [
  .localGet 0,
  .call 34,
  .unreachable
]

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

def func34 : 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 (1048696 : UInt32),
    .localGet 0,
    .load32 (4 : UInt32),
    .localGet 0,
    .load32 (8 : UInt32),
    .localSet 0,
    .localGet 0,
    .load8U (8 : UInt32),
    .localGet 0,
    .load8U (9 : UInt32),
    .call 36,
    .unreachable
  ],
  .localGet 1,
  .const (2147483648 : UInt32),
  .store32 (0 : UInt32),
  .localGet 1,
  .localGet 0,
  .store32 (12 : UInt32),
  .localGet 1,
  .const (1048724 : UInt32),
  .localGet 0,
  .load32 (4 : UInt32),
  .localGet 0,
  .load32 (8 : UInt32),
  .localSet 0,
  .localGet 0,
  .load8U (8 : UInt32),
  .localGet 0,
  .load8U (9 : UInt32),
  .call 36,
  .unreachable
]

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

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

def func36 : 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 52,
            .const (255 : UInt32),
            .and,
            .brTable [4, 1, 0] 1
          ],
          .const (0 : UInt32),
          .load32 (1049200 : UInt32),
          .localSet 6,
          .localGet 6,
          .const (4294967295 : UInt32),
          .leS,
          .br_if 3,
          .const (0 : UInt32),
          .localGet 6,
          .const (1 : UInt32),
          .add,
          .store32 (1049200 : UInt32),
          .const (0 : UInt32),
          .load32 (1049204 : 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 (1049204 : UInt32),
          .localGet 5,
          .const (16 : UInt32),
          .add,
          .const (0 : UInt32),
          .load32 (1049208 : 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 28
    ],
    .const (0 : UInt32),
    .const (0 : UInt32),
    .load32 (1049200 : UInt32),
    .const (4294967295 : UInt32),
    .add,
    .store32 (1049200 : UInt32),
    .const (0 : UInt32),
    .const (0 : UInt32),
    .store8 (1049192 : UInt32),
    .localGet 3,
    .eqz,
    .br_if 0,
    .localGet 0,
    .localGet 1,
    .call 38,
    .unreachable
  ],
  .unreachable
]

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

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

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

def func38 : Wasm.Program :=
  [
  .localGet 0,
  .localGet 1,
  .call 26,
  .drop,
  .unreachable
]

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

def func39 : Wasm.Program :=
  [
  .block 0 0 [
    .localGet 1,
    .const (9 : UInt32),
    .ltU,
    .br_if 0,
    .localGet 1,
    .localGet 0,
    .call 40,
    .ret
  ],
  .localGet 0,
  .call 41
]

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

def func40 : 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 41,
    .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 47,
        .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 47
    ],
    .localGet 0,
    .const (8 : UInt32),
    .add,
    .localSet 2
  ],
  .localGet 2
]

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

def func41 : 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 (1049628 : 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 (1049624 : 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 (1049360 : UInt32),
                    .add,
                    .localSet 0,
                    .localGet 0,
                    .localGet 3,
                    .const (1049368 : 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 (1049632 : UInt32),
                  .leU,
                  .br_if 6,
                  .localGet 0,
                  .br_if 2,
                  .const (0 : UInt32),
                  .load32 (1049628 : UInt32),
                  .localSet 0,
                  .localGet 0,
                  .eqz,
                  .br_if 6,
                  .localGet 0,
                  .ctz,
                  .const (2 : UInt32),
                  .shl,
                  .const (1049216 : 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 (1049216 : 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 (1049624 : 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 (1049360 : UInt32),
                .add,
                .localSet 8,
                .localGet 8,
                .localGet 2,
                .const (1049368 : 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 (1049624 : 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 (1049632 : UInt32),
              .localSet 2,
              .localGet 2,
              .eqz,
              .br_if 0,
              .const (0 : UInt32),
              .load32 (1049640 : UInt32),
              .localSet 3,
              .block 0 0 [
                .block 0 0 [
                  .const (0 : UInt32),
                  .load32 (1049624 : 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 (1049624 : UInt32),
                  .localGet 2,
                  .const (4294967288 : UInt32),
                  .and,
                  .const (1049360 : UInt32),
                  .add,
                  .localSet 2,
                  .localGet 2,
                  .localSet 7,
                  .br 1
                ],
                .localGet 2,
                .const (4294967288 : UInt32),
                .and,
                .localSet 2,
                .localGet 2,
                .const (1049360 : UInt32),
                .add,
                .localSet 7,
                .localGet 2,
                .const (1049368 : 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 (1049640 : UInt32),
            .const (0 : UInt32),
            .localGet 8,
            .store32 (1049632 : UInt32),
            .br 4
          ],
          .const (0 : UInt32),
          .const (0 : UInt32),
          .load32 (1049628 : UInt32),
          .const (4294967294 : UInt32),
          .localGet 6,
          .load32 (28 : UInt32),
          .rotl,
          .and,
          .store32 (1049628 : 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 (1049632 : UInt32),
              .localSet 7,
              .localGet 7,
              .eqz,
              .br_if 1,
              .const (0 : UInt32),
              .load32 (1049640 : UInt32),
              .localSet 0,
              .block 0 0 [
                .block 0 0 [
                  .const (0 : UInt32),
                  .load32 (1049624 : 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 (1049624 : UInt32),
                  .localGet 7,
                  .const (4294967288 : UInt32),
                  .and,
                  .const (1049360 : UInt32),
                  .add,
                  .localSet 7,
                  .localGet 7,
                  .localSet 9,
                  .br 1
                ],
                .localGet 7,
                .const (4294967288 : UInt32),
                .and,
                .localSet 7,
                .localGet 7,
                .const (1049360 : UInt32),
                .add,
                .localSet 9,
                .localGet 7,
                .const (1049368 : 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 (1049640 : UInt32),
          .const (0 : UInt32),
          .localGet 2,
          .store32 (1049632 : 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 (1049216 : 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 (1049216 : 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 (1049632 : 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 (1049216 : 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 (1049628 : UInt32),
        .const (4294967294 : UInt32),
        .localGet 8,
        .load32 (28 : UInt32),
        .rotl,
        .and,
        .store32 (1049628 : 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 51,
            .br 2
          ],
          .block 0 0 [
            .block 0 0 [
              .const (0 : UInt32),
              .load32 (1049624 : 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 (1049624 : UInt32),
              .localGet 2,
              .const (248 : UInt32),
              .and,
              .const (1049360 : UInt32),
              .add,
              .localSet 2,
              .localGet 2,
              .localSet 6,
              .br 1
            ],
            .localGet 2,
            .const (248 : UInt32),
            .and,
            .localSet 2,
            .localGet 2,
            .const (1049360 : UInt32),
            .add,
            .localSet 6,
            .localGet 2,
            .const (1049368 : 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 (1049632 : UInt32),
                .localSet 0,
                .localGet 0,
                .localGet 3,
                .geU,
                .br_if 0,
                .block 0 0 [
                  .const (0 : UInt32),
                  .load32 (1049636 : UInt32),
                  .localSet 0,
                  .localGet 0,
                  .localGet 3,
                  .gtU,
                  .br_if 0,
                  .localGet 1,
                  .const (4 : UInt32),
                  .add,
                  .const (1049668 : UInt32),
                  .localGet 3,
                  .const (65583 : UInt32),
                  .add,
                  .const (4294901760 : UInt32),
                  .and,
                  .call 66,
                  .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 (1049648 : UInt32),
                  .localGet 1,
                  .load32 (8 : UInt32),
                  .localSet 9,
                  .localGet 9,
                  .add,
                  .localSet 0,
                  .localGet 0,
                  .store32 (1049648 : UInt32),
                  .const (0 : UInt32),
                  .localGet 0,
                  .const (0 : UInt32),
                  .load32 (1049652 : UInt32),
                  .localSet 2,
                  .localGet 2,
                  .localGet 0,
                  .localGet 2,
                  .gtU,
                  .select,
                  .store32 (1049652 : UInt32),
                  .block 0 0 [
                    .block 0 0 [
                      .block 0 0 [
                        .const (0 : UInt32),
                        .load32 (1049644 : UInt32),
                        .localSet 2,
                        .localGet 2,
                        .eqz,
                        .br_if 0,
                        .const (1049344 : 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 (1049660 : UInt32),
                          .localSet 0,
                          .localGet 0,
                          .eqz,
                          .br_if 0,
                          .localGet 6,
                          .localGet 0,
                          .geU,
                          .br_if 1
                        ],
                        .const (0 : UInt32),
                        .localGet 6,
                        .store32 (1049660 : UInt32)
                      ],
                      .const (0 : UInt32),
                      .const (4095 : UInt32),
                      .store32 (1049664 : UInt32),
                      .const (0 : UInt32),
                      .localGet 5,
                      .store32 (1049356 : UInt32),
                      .const (0 : UInt32),
                      .localGet 9,
                      .store32 (1049348 : UInt32),
                      .const (0 : UInt32),
                      .localGet 6,
                      .store32 (1049344 : UInt32),
                      .const (0 : UInt32),
                      .const (1049360 : UInt32),
                      .store32 (1049372 : UInt32),
                      .const (0 : UInt32),
                      .const (1049368 : UInt32),
                      .store32 (1049380 : UInt32),
                      .const (0 : UInt32),
                      .const (1049360 : UInt32),
                      .store32 (1049368 : UInt32),
                      .const (0 : UInt32),
                      .const (1049376 : UInt32),
                      .store32 (1049388 : UInt32),
                      .const (0 : UInt32),
                      .const (1049368 : UInt32),
                      .store32 (1049376 : UInt32),
                      .const (0 : UInt32),
                      .const (1049384 : UInt32),
                      .store32 (1049396 : UInt32),
                      .const (0 : UInt32),
                      .const (1049376 : UInt32),
                      .store32 (1049384 : UInt32),
                      .const (0 : UInt32),
                      .const (1049392 : UInt32),
                      .store32 (1049404 : UInt32),
                      .const (0 : UInt32),
                      .const (1049384 : UInt32),
                      .store32 (1049392 : UInt32),
                      .const (0 : UInt32),
                      .const (1049400 : UInt32),
                      .store32 (1049412 : UInt32),
                      .const (0 : UInt32),
                      .const (1049392 : UInt32),
                      .store32 (1049400 : UInt32),
                      .const (0 : UInt32),
                      .const (1049408 : UInt32),
                      .store32 (1049420 : UInt32),
                      .const (0 : UInt32),
                      .const (1049400 : UInt32),
                      .store32 (1049408 : UInt32),
                      .const (0 : UInt32),
                      .const (1049416 : UInt32),
                      .store32 (1049428 : UInt32),
                      .const (0 : UInt32),
                      .const (1049408 : UInt32),
                      .store32 (1049416 : UInt32),
                      .const (0 : UInt32),
                      .const (1049424 : UInt32),
                      .store32 (1049436 : UInt32),
                      .const (0 : UInt32),
                      .const (1049416 : UInt32),
                      .store32 (1049424 : UInt32),
                      .const (0 : UInt32),
                      .const (1049424 : UInt32),
                      .store32 (1049432 : UInt32),
                      .const (0 : UInt32),
                      .const (1049432 : UInt32),
                      .store32 (1049444 : UInt32),
                      .const (0 : UInt32),
                      .const (1049432 : UInt32),
                      .store32 (1049440 : UInt32),
                      .const (0 : UInt32),
                      .const (1049440 : UInt32),
                      .store32 (1049452 : UInt32),
                      .const (0 : UInt32),
                      .const (1049440 : UInt32),
                      .store32 (1049448 : UInt32),
                      .const (0 : UInt32),
                      .const (1049448 : UInt32),
                      .store32 (1049460 : UInt32),
                      .const (0 : UInt32),
                      .const (1049448 : UInt32),
                      .store32 (1049456 : UInt32),
                      .const (0 : UInt32),
                      .const (1049456 : UInt32),
                      .store32 (1049468 : UInt32),
                      .const (0 : UInt32),
                      .const (1049456 : UInt32),
                      .store32 (1049464 : UInt32),
                      .const (0 : UInt32),
                      .const (1049464 : UInt32),
                      .store32 (1049476 : UInt32),
                      .const (0 : UInt32),
                      .const (1049464 : UInt32),
                      .store32 (1049472 : UInt32),
                      .const (0 : UInt32),
                      .const (1049472 : UInt32),
                      .store32 (1049484 : UInt32),
                      .const (0 : UInt32),
                      .const (1049472 : UInt32),
                      .store32 (1049480 : UInt32),
                      .const (0 : UInt32),
                      .const (1049480 : UInt32),
                      .store32 (1049492 : UInt32),
                      .const (0 : UInt32),
                      .const (1049480 : UInt32),
                      .store32 (1049488 : UInt32),
                      .const (0 : UInt32),
                      .const (1049488 : UInt32),
                      .store32 (1049500 : UInt32),
                      .const (0 : UInt32),
                      .const (1049496 : UInt32),
                      .store32 (1049508 : UInt32),
                      .const (0 : UInt32),
                      .const (1049488 : UInt32),
                      .store32 (1049496 : UInt32),
                      .const (0 : UInt32),
                      .const (1049504 : UInt32),
                      .store32 (1049516 : UInt32),
                      .const (0 : UInt32),
                      .const (1049496 : UInt32),
                      .store32 (1049504 : UInt32),
                      .const (0 : UInt32),
                      .const (1049512 : UInt32),
                      .store32 (1049524 : UInt32),
                      .const (0 : UInt32),
                      .const (1049504 : UInt32),
                      .store32 (1049512 : UInt32),
                      .const (0 : UInt32),
                      .const (1049520 : UInt32),
                      .store32 (1049532 : UInt32),
                      .const (0 : UInt32),
                      .const (1049512 : UInt32),
                      .store32 (1049520 : UInt32),
                      .const (0 : UInt32),
                      .const (1049528 : UInt32),
                      .store32 (1049540 : UInt32),
                      .const (0 : UInt32),
                      .const (1049520 : UInt32),
                      .store32 (1049528 : 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 (1049600 : UInt32),
                      .store32 (1049612 : UInt32),
                      .const (0 : UInt32),
                      .const (1049592 : UInt32),
                      .store32 (1049600 : UInt32),
                      .const (0 : UInt32),
                      .const (1049608 : UInt32),
                      .store32 (1049620 : UInt32),
                      .const (0 : UInt32),
                      .const (1049600 : UInt32),
                      .store32 (1049608 : 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 (1049644 : UInt32),
                      .const (0 : UInt32),
                      .const (1049608 : UInt32),
                      .store32 (1049616 : 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 (1049636 : 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 (1049656 : 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 (1049660 : UInt32),
                  .localSet 0,
                  .localGet 0,
                  .localGet 6,
                  .localGet 0,
                  .localGet 6,
                  .ltU,
                  .select,
                  .store32 (1049660 : UInt32),
                  .localGet 6,
                  .localGet 9,
                  .add,
                  .localSet 8,
                  .const (1049344 : 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 (1049344 : 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 (1049644 : 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 (1049636 : 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 (1049656 : 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 (1049344 : UInt32),
                    .localSet 10,
                    .localGet 7,
                    .const (16 : UInt32),
                    .add,
                    .const (0 : UInt32),
                    .load64 (1049352 : 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 (1049356 : UInt32),
                    .const (0 : UInt32),
                    .localGet 9,
                    .store32 (1049348 : UInt32),
                    .const (0 : UInt32),
                    .localGet 6,
                    .store32 (1049344 : UInt32),
                    .const (0 : UInt32),
                    .localGet 0,
                    .store32 (1049352 : 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 51,
                      .br 8
                    ],
                    .block 0 0 [
                      .block 0 0 [
                        .const (0 : UInt32),
                        .load32 (1049624 : 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 (1049624 : UInt32),
                        .localGet 0,
                        .const (248 : UInt32),
                        .and,
                        .const (1049360 : UInt32),
                        .add,
                        .localSet 0,
                        .localGet 0,
                        .localSet 8,
                        .br 1
                      ],
                      .localGet 0,
                      .const (248 : UInt32),
                      .and,
                      .localSet 0,
                      .localGet 0,
                      .const (1049360 : UInt32),
                      .add,
                      .localSet 8,
                      .localGet 0,
                      .const (1049368 : 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 (1049644 : UInt32),
                  .eq,
                  .br_if 3,
                  .localGet 2,
                  .const (0 : UInt32),
                  .load32 (1049640 : 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 46,
                    .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 51,
                    .br 6
                  ],
                  .block 0 0 [
                    .block 0 0 [
                      .const (0 : UInt32),
                      .load32 (1049624 : 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 (1049624 : UInt32),
                      .localGet 3,
                      .const (248 : UInt32),
                      .and,
                      .const (1049360 : UInt32),
                      .add,
                      .localSet 3,
                      .localGet 3,
                      .localSet 2,
                      .br 1
                    ],
                    .localGet 3,
                    .const (248 : UInt32),
                    .and,
                    .localSet 3,
                    .localGet 3,
                    .const (1049360 : UInt32),
                    .add,
                    .localSet 2,
                    .localGet 3,
                    .const (1049368 : 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 (1049636 : UInt32),
                .const (0 : UInt32),
                .const (0 : UInt32),
                .load32 (1049644 : UInt32),
                .localSet 0,
                .localGet 0,
                .localGet 3,
                .add,
                .localSet 8,
                .localGet 8,
                .store32 (1049644 : 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 (1049640 : 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 (1049640 : UInt32),
                  .const (0 : UInt32),
                  .const (0 : UInt32),
                  .store32 (1049632 : 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 (1049632 : UInt32),
                .const (0 : UInt32),
                .localGet 2,
                .localGet 3,
                .add,
                .localSet 6,
                .localGet 6,
                .store32 (1049640 : 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 (1049644 : 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 (1049644 : UInt32),
            .const (0 : UInt32),
            .localGet 0,
            .localGet 2,
            .sub,
            .const (0 : UInt32),
            .load32 (1049636 : UInt32),
            .localGet 9,
            .add,
            .localSet 2,
            .localGet 2,
            .add,
            .const (8 : UInt32),
            .add,
            .localSet 6,
            .localGet 6,
            .store32 (1049636 : 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 (1049656 : UInt32),
            .br 3
          ],
          .const (0 : UInt32),
          .localGet 0,
          .store32 (1049644 : UInt32),
          .const (0 : UInt32),
          .const (0 : UInt32),
          .load32 (1049636 : UInt32),
          .localGet 3,
          .add,
          .localSet 3,
          .localGet 3,
          .store32 (1049636 : UInt32),
          .localGet 0,
          .localGet 3,
          .const (1 : UInt32),
          .or,
          .store32 (4 : UInt32),
          .br 1
        ],
        .const (0 : UInt32),
        .localGet 0,
        .store32 (1049640 : UInt32),
        .const (0 : UInt32),
        .const (0 : UInt32),
        .load32 (1049632 : UInt32),
        .localGet 3,
        .add,
        .localSet 3,
        .localGet 3,
        .store32 (1049632 : 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 (1049636 : UInt32),
    .localSet 2,
    .localGet 2,
    .localGet 3,
    .leU,
    .br_if 0,
    .const (0 : UInt32),
    .localGet 2,
    .localGet 3,
    .sub,
    .localSet 2,
    .localGet 2,
    .store32 (1049636 : UInt32),
    .const (0 : UInt32),
    .const (0 : UInt32),
    .load32 (1049644 : UInt32),
    .localSet 0,
    .localGet 0,
    .localGet 3,
    .add,
    .localSet 8,
    .localGet 8,
    .store32 (1049644 : 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 func41Def : Wasm.Function :=
  { params := [.i32], locals := [.i32, .i32, .i32, .i32, .i32, .i32, .i32, .i32, .i32, .i64], body := func41, results := [.i32] }

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

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

def func43 : 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 44,
      .ret
    ],
    .const (1048827 : UInt32),
    .const (46 : UInt32),
    .const (1048876 : UInt32),
    .call 70,
    .unreachable
  ],
  .const (1048892 : UInt32),
  .const (46 : UInt32),
  .const (1048940 : UInt32),
  .call 70,
  .unreachable
]

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

def func44 : 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 (1049640 : 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 (1049632 : 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 46
    ],
    .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 (1049644 : UInt32),
                    .eq,
                    .br_if 2,
                    .localGet 3,
                    .const (0 : UInt32),
                    .load32 (1049640 : UInt32),
                    .eq,
                    .br_if 3,
                    .localGet 3,
                    .localGet 2,
                    .const (4294967288 : UInt32),
                    .and,
                    .localSet 2,
                    .localGet 2,
                    .call 46,
                    .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 (1049640 : UInt32),
                    .ne,
                    .br_if 1,
                    .const (0 : UInt32),
                    .localGet 0,
                    .store32 (1049632 : 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 51,
                .const (0 : UInt32),
                .const (0 : UInt32),
                .load32 (1049664 : UInt32),
                .const (4294967295 : UInt32),
                .add,
                .localSet 1,
                .localGet 1,
                .store32 (1049664 : UInt32),
                .localGet 1,
                .br_if 6,
                .const (0 : UInt32),
                .load32 (1049352 : UInt32),
                .localSet 0,
                .localGet 0,
                .br_if 2,
                .const (4095 : UInt32),
                .localSet 1,
                .br 3
              ],
              .const (0 : UInt32),
              .localGet 1,
              .store32 (1049644 : UInt32),
              .const (0 : UInt32),
              .const (0 : UInt32),
              .load32 (1049636 : UInt32),
              .localGet 0,
              .add,
              .localSet 0,
              .localGet 0,
              .store32 (1049636 : UInt32),
              .localGet 1,
              .localGet 0,
              .const (1 : UInt32),
              .or,
              .store32 (4 : UInt32),
              .block 0 0 [
                .localGet 1,
                .const (0 : UInt32),
                .load32 (1049640 : UInt32),
                .ne,
                .br_if 0,
                .const (0 : UInt32),
                .const (0 : UInt32),
                .store32 (1049632 : UInt32),
                .const (0 : UInt32),
                .const (0 : UInt32),
                .store32 (1049640 : UInt32)
              ],
              .localGet 0,
              .const (0 : UInt32),
              .load32 (1049656 : UInt32),
              .localSet 2,
              .localGet 2,
              .leU,
              .br_if 5,
              .const (0 : UInt32),
              .load32 (1049644 : UInt32),
              .localSet 0,
              .localGet 0,
              .eqz,
              .br_if 5,
              .const (0 : UInt32),
              .load32 (1049636 : UInt32),
              .localSet 4,
              .localGet 4,
              .const (41 : UInt32),
              .ltU,
              .br_if 4,
              .const (1049344 : 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 (1049640 : UInt32),
            .const (0 : UInt32),
            .const (0 : UInt32),
            .load32 (1049632 : UInt32),
            .localGet 0,
            .add,
            .localSet 0,
            .localGet 0,
            .store32 (1049632 : 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 (1049664 : UInt32),
        .ret
      ],
      .block 0 0 [
        .block 0 0 [
          .const (0 : UInt32),
          .load32 (1049624 : 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 (1049624 : UInt32),
          .localGet 0,
          .const (248 : UInt32),
          .and,
          .const (1049360 : UInt32),
          .add,
          .localSet 0,
          .localGet 0,
          .localSet 3,
          .br 1
        ],
        .localGet 0,
        .const (248 : UInt32),
        .and,
        .localSet 0,
        .localGet 0,
        .const (1049360 : UInt32),
        .add,
        .localSet 3,
        .localGet 0,
        .const (1049368 : 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 (1049352 : 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 (1049664 : UInt32),
    .localGet 4,
    .localGet 2,
    .leU,
    .br_if 0,
    .const (0 : UInt32),
    .const (4294967295 : UInt32),
    .store32 (1049656 : UInt32)
  ]
]

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

def func45 : 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 40,
                      .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 (1049644 : UInt32),
                        .eq,
                        .br_if 1,
                        .block 0 0 [
                          .localGet 7,
                          .const (0 : UInt32),
                          .load32 (1049640 : 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 46,
                          .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 47,
                            .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 (1049632 : 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 (1049640 : UInt32),
                        .const (0 : UInt32),
                        .localGet 6,
                        .store32 (1049632 : 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 47,
                      .br 6
                    ],
                    .const (0 : UInt32),
                    .load32 (1049636 : 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 (1048892 : UInt32),
                  .const (46 : UInt32),
                  .const (1048940 : UInt32),
                  .call 70,
                  .unreachable
                ],
                .const (1048827 : UInt32),
                .const (46 : UInt32),
                .const (1048876 : UInt32),
                .call 70,
                .unreachable
              ],
              .const (1048892 : UInt32),
              .const (46 : UInt32),
              .const (1048940 : UInt32),
              .call 70,
              .unreachable
            ],
            .const (1048827 : UInt32),
            .const (46 : UInt32),
            .const (1048876 : UInt32),
            .call 70,
            .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 (1049636 : UInt32),
          .const (0 : UInt32),
          .localGet 5,
          .store32 (1049644 : UInt32)
        ],
        .localGet 8,
        .eqz,
        .br_if 0,
        .localGet 0,
        .ret
      ],
      .localGet 3,
      .call 41,
      .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 44
  ],
  .localGet 2
]

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

def func46 : 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 (1049216 : 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 (1049624 : UInt32),
        .const (4294967294 : UInt32),
        .localGet 1,
        .const (3 : UInt32),
        .shrU,
        .rotl,
        .and,
        .store32 (1049624 : 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 (1049628 : UInt32),
  .const (4294967294 : UInt32),
  .localGet 0,
  .load32 (28 : UInt32),
  .rotl,
  .and,
  .store32 (1049628 : UInt32)
]

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

def func47 : 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 (1049640 : 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 (1049632 : 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 46
    ],
    .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 (1049644 : UInt32),
            .eq,
            .br_if 2,
            .localGet 2,
            .const (0 : UInt32),
            .load32 (1049640 : UInt32),
            .eq,
            .br_if 3,
            .localGet 2,
            .localGet 3,
            .const (4294967288 : UInt32),
            .and,
            .localSet 3,
            .localGet 3,
            .call 46,
            .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 (1049640 : UInt32),
            .ne,
            .br_if 1,
            .const (0 : UInt32),
            .localGet 1,
            .store32 (1049632 : 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 51,
          .ret
        ],
        .block 0 0 [
          .block 0 0 [
            .const (0 : UInt32),
            .load32 (1049624 : 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 (1049624 : UInt32),
            .localGet 1,
            .const (248 : UInt32),
            .and,
            .const (1049360 : UInt32),
            .add,
            .localSet 1,
            .localGet 1,
            .localSet 2,
            .br 1
          ],
          .localGet 1,
          .const (248 : UInt32),
          .and,
          .localSet 1,
          .localGet 1,
          .const (1049360 : UInt32),
          .add,
          .localSet 2,
          .localGet 1,
          .const (1049368 : 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 (1049644 : UInt32),
      .const (0 : UInt32),
      .const (0 : UInt32),
      .load32 (1049636 : UInt32),
      .localGet 1,
      .add,
      .localSet 1,
      .localGet 1,
      .store32 (1049636 : UInt32),
      .localGet 0,
      .localGet 1,
      .const (1 : UInt32),
      .or,
      .store32 (4 : UInt32),
      .localGet 0,
      .const (0 : UInt32),
      .load32 (1049640 : UInt32),
      .ne,
      .br_if 1,
      .const (0 : UInt32),
      .const (0 : UInt32),
      .store32 (1049632 : UInt32),
      .const (0 : UInt32),
      .const (0 : UInt32),
      .store32 (1049640 : UInt32),
      .ret
    ],
    .const (0 : UInt32),
    .localGet 0,
    .store32 (1049640 : UInt32),
    .const (0 : UInt32),
    .const (0 : UInt32),
    .load32 (1049632 : UInt32),
    .localGet 1,
    .add,
    .localSet 1,
    .localGet 1,
    .store32 (1049632 : UInt32),
    .localGet 0,
    .localGet 1,
    .const (1 : UInt32),
    .or,
    .store32 (4 : UInt32),
    .localGet 0,
    .localGet 1,
    .add,
    .localGet 1,
    .store32 (0 : UInt32),
    .ret
  ]
]

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

def func48 : 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 33,
  .unreachable
]

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

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

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

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

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

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

def func52 : Wasm.Program :=
  [
  .const (0 : UInt32),
  .localSet 1,
  .const (0 : UInt32),
  .const (0 : UInt32),
  .load32 (1049212 : UInt32),
  .localSet 2,
  .localGet 2,
  .const (1 : UInt32),
  .add,
  .store32 (1049212 : UInt32),
  .block 0 0 [
    .localGet 2,
    .const (0 : UInt32),
    .ltS,
    .br_if 0,
    .const (1 : UInt32),
    .localSet 1,
    .const (0 : UInt32),
    .load8U (1049192 : UInt32),
    .br_if 0,
    .const (0 : UInt32),
    .localGet 0,
    .store8 (1049192 : UInt32),
    .const (0 : UInt32),
    .const (0 : UInt32),
    .load32 (1049188 : UInt32),
    .const (1 : UInt32),
    .add,
    .store32 (1049188 : UInt32),
    .const (2 : UInt32),
    .localSet 1
  ],
  .localGet 1
]

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

def func53 : Wasm.Program :=
  [
  .localGet 0,
  .const (0 : UInt32),
  .load64 (1048776 : UInt32),
  .store64 (8 : UInt32),
  .localGet 0,
  .const (0 : UInt32),
  .load64 (1048768 : UInt32),
  .store64 (0 : UInt32)
]

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

def func54 : Wasm.Program :=
  [
  .localGet 0,
  .const (0 : UInt32),
  .load64 (1048760 : UInt32),
  .store64 (8 : UInt32),
  .localGet 0,
  .const (0 : UInt32),
  .load64 (1048752 : UInt32),
  .store64 (0 : UInt32)
]

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

def func55 : 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 73,
    .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 72
]

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

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

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

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

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

def func58 : Wasm.Program :=
  [
  .localGet 1,
  .load32 (4 : UInt32),
  .localSet 2,
  .localGet 1,
  .load32 (0 : UInt32),
  .localSet 3,
  .call 25,
  .block 0 0 [
    .const (8 : UInt32),
    .const (4 : UInt32),
    .call 22,
    .localSet 1,
    .localGet 1,
    .br_if 0,
    .const (4 : UInt32),
    .const (8 : UInt32),
    .call 68,
    .unreachable
  ],
  .localGet 1,
  .localGet 2,
  .store32 (4 : UInt32),
  .localGet 1,
  .localGet 3,
  .store32 (0 : UInt32),
  .localGet 0,
  .const (1048956 : UInt32),
  .store32 (4 : UInt32),
  .localGet 0,
  .localGet 1,
  .store32 (0 : UInt32)
]

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

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

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

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

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

def func62 : 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 (1048672 : UInt32),
    .localGet 3,
    .load32 (0 : UInt32),
    .localSet 3,
    .localGet 3,
    .load32 (0 : UInt32),
    .localGet 3,
    .load32 (4 : UInt32),
    .call 72,
    .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 (1048972 : UInt32),
  .store32 (4 : UInt32),
  .localGet 0,
  .localGet 1,
  .store32 (0 : UInt32),
  .localGet 2,
  .const (32 : UInt32),
  .add,
  .globalSet 0
]

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

def func63 : 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 (1048672 : UInt32),
    .localGet 3,
    .load32 (0 : UInt32),
    .localSet 3,
    .localGet 3,
    .load32 (0 : UInt32),
    .localGet 3,
    .load32 (4 : UInt32),
    .call 72,
    .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 25,
  .block 0 0 [
    .const (12 : UInt32),
    .const (4 : UInt32),
    .call 22,
    .localSet 1,
    .localGet 1,
    .br_if 0,
    .const (4 : UInt32),
    .const (12 : UInt32),
    .call 68,
    .unreachable
  ],
  .localGet 1,
  .localGet 2,
  .load32 (16 : UInt32),
  .store32 (8 : UInt32),
  .localGet 1,
  .localGet 2,
  .load64 (8 : UInt32),
  .store64 (0 : UInt32),
  .localGet 0,
  .const (1048972 : UInt32),
  .store32 (4 : UInt32),
  .localGet 0,
  .localGet 1,
  .store32 (0 : UInt32),
  .localGet 2,
  .const (48 : UInt32),
  .add,
  .globalSet 0
]

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

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

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

def func65 : Wasm.Program :=
  [
  .localGet 0,
  .const (1048672 : UInt32),
  .localGet 1,
  .localGet 2,
  .call 72
]

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

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

def func67 : Wasm.Program :=
  [
  .block 0 0 [
    .localGet 0,
    .eqz,
    .br_if 0,
    .localGet 0,
    .localGet 1,
    .call 68,
    .unreachable
  ],
  .call 69,
  .unreachable
]

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

def func68 : Wasm.Program :=
  [
  .localGet 1,
  .localGet 0,
  .call 49,
  .unreachable
]

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

def func69 : Wasm.Program :=
  [
  .const (1049069 : UInt32),
  .const (35 : UInt32),
  .const (1049088 : UInt32),
  .call 71,
  .unreachable
]

def func69Def : Wasm.Function :=
  { params := [], locals := [], body := func69, results := [] }

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

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

def func71 : 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 48,
  .unreachable
]

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

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

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

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

def func74 : Wasm.Program :=
  [
  .const (1049104 : UInt32),
  .const (51 : UInt32),
  .localGet 0,
  .call 71,
  .unreachable
]

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

def func75 : Wasm.Program :=
  [
  .const (1049129 : UInt32),
  .const (115 : UInt32),
  .localGet 0,
  .call 71,
  .unreachable
]

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

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,
    func62Def,
    func63Def,
    func64Def,
    func65Def,
    func66Def,
    func67Def,
    func68Def,
    func69Def,
    func70Def,
    func71Def,
    func72Def,
    func73Def,
    func74Def,
    func75Def
  ],
  exports := [
    { name := "add_chain", funcIdx := 0 },
    { name := "add_then_mul", funcIdx := 1 },
    { name := "and_chain", funcIdx := 2 },
    { name := "and_then_or", funcIdx := 3 },
    { name := "div_then_add", funcIdx := 4 },
    { name := "div_then_mul", funcIdx := 5 },
    { name := "mul_chain", funcIdx := 6 },
    { name := "mul_then_add", funcIdx := 7 },
    { name := "not_then_xor", funcIdx := 8 },
    { name := "not_twice", funcIdx := 9 },
    { name := "or_chain", funcIdx := 10 },
    { name := "or_then_xor", funcIdx := 11 },
    { name := "rem_then_add", funcIdx := 12 },
    { name := "rem_then_mul", funcIdx := 13 },
    { name := "shl_then_add", funcIdx := 14 },
    { name := "shl_twice", funcIdx := 15 },
    { name := "shr_then_sub", funcIdx := 16 },
    { name := "shr_twice", funcIdx := 17 },
    { name := "sub_chain", funcIdx := 18 },
    { name := "sub_then_add", funcIdx := 19 },
    { name := "xor_chain", funcIdx := 20 },
    { name := "xor_then_and", funcIdx := 21 }
  ],
  memory := some { pagesMin := (17 : UInt32), pagesMax := none, data := [
    { offset := some (1048576 : UInt32), bytes := [(114 : UInt8), (117 : UInt8), (115 : UInt8), (116 : UInt8), (95 : UInt8), (117 : UInt8), (54 : UInt8), (52 : UInt8), (95 : UInt8), (116 : UInt8), (101 : UInt8), (115 : 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), (0 : UInt8), (16 : UInt8), (0 : UInt8), (29 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (47 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (86 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (16 : UInt8), (0 : UInt8), (29 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (48 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (86 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (16 : UInt8), (0 : UInt8), (29 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (51 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (86 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (16 : UInt8), (0 : UInt8), (29 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (52 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (86 : 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), (208 : 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), (208 : 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), (156 : 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), (97 : UInt8), (116 : UInt8), (116 : UInt8), (101 : UInt8), (109 : UInt8), (112 : UInt8), (116 : UInt8), (32 : UInt8), (116 : UInt8), (111 : UInt8), (32 : UInt8), (100 : UInt8), (105 : UInt8), (118 : UInt8), (105 : UInt8), (100 : UInt8), (101 : UInt8), (32 : UInt8), (98 : UInt8), (121 : UInt8), (32 : UInt8), (122 : UInt8), (101 : UInt8), (114 : UInt8), (111 : UInt8), (97 : UInt8), (116 : UInt8), (116 : UInt8), (101 : UInt8), (109 : UInt8), (112 : UInt8), (116 : UInt8), (32 : UInt8), (116 : UInt8), (111 : UInt8), (32 : UInt8), (99 : UInt8), (97 : UInt8), (108 : UInt8), (99 : UInt8), (117 : UInt8), (108 : UInt8), (97 : UInt8), (116 : UInt8), (101 : UInt8), (32 : UInt8), (116 : UInt8), (104 : UInt8), (101 : UInt8), (32 : UInt8), (114 : UInt8), (101 : UInt8), (109 : UInt8), (97 : UInt8), (105 : UInt8), (110 : UInt8), (100 : UInt8), (101 : UInt8), (114 : UInt8), (32 : UInt8), (119 : UInt8), (105 : UInt8), (116 : UInt8), (104 : UInt8), (32 : UInt8), (97 : UInt8), (32 : UInt8), (100 : UInt8), (105 : UInt8), (118 : UInt8), (105 : UInt8), (115 : UInt8), (111 : UInt8), (114 : UInt8), (32 : UInt8), (111 : UInt8), (102 : UInt8), (32 : UInt8), (122 : UInt8), (101 : UInt8), (114 : UInt8), (111 : UInt8)] }
  ] },
  globals := [
    { init := .i32 (1048576 : UInt32) },
    { init := .i32 (1049669 : UInt32) },
    { init := .i32 (1049680 : UInt32) }
  ],
  types := [
    { params := [.i32, .i32], results := [] },
    { params := [.i32, .i32, .i32], results := [.i32] },
    { params := [.i32, .i32], results := [.i32] },
    { params := [.i64, .i64, .i64], results := [.i64] },
    { params := [.i64, .i64], results := [.i64] },
    { params := [.i64], results := [.i64] },
    { params := [.i64, .i32, .i64], results := [.i64] },
    { params := [.i64, .i32, .i32], results := [.i64] },
    { params := [.i32, .i32, .i32], results := [] },
    { params := [.i32, .i32, .i32, .i32], results := [.i32] },
    { params := [], results := [] },
    { params := [.i32, .i32, .i32, .i32, .i32], results := [] },
    { params := [.i32], results := [] },
    { params := [.i32, .i32, .i32, .i32, .i32, .i32], results := [] },
    { params := [.i32], results := [.i32] }
  ],
  tables := [
    { min := 17, max := some 17, elemType := .funcref }
  ],
  elements := [
    { tableIdx := some 0, offset := some 1, funcs := [some 37, some 29, some 61, some 60, some 65, some 59, some 58, some 56, some 57, some 30, some 55, some 63, some 62, some 64, some 54, some 53] }
  ]
}

end Project.RustU64Tests
lean/Project/RustU64Tests/Spec.lean lean · 781 lines 
import Project.RustU64Tests.Program

/-!
# Reuse tests for the `CodeLib/RustStd/U64` corpus

Two structurally-distinct functions per operator, each using the operator inline
the way real client code emits it (no shim and no `.call`). Every public spec is
now a small-step `PartiallyMeets` theorem proved through iris-lean. The guarded
div/rem functions follow their nonzero branch and return before the panic tail;
the shift functions prove the emitted mask/extend sequence normalizes counts
modulo 64.
-/

namespace Project.RustU64Tests.Spec

open Wasm Wasm.RustStd Wasm.RustStd.U64
open Iris Iris.ProgramLogic Language.Notation

private def ternaryConfig (body : Program)
    (a b c : UInt64) : SmallStep.Config Unit :=
  { expr := .running
      ⟨⟨[.i64 a, .i64 b, .i64 c], [], []⟩,
        body, 1, [], [], []⟩
    store :=
      { runtime := { module := «module», host := {} }
        wasm := «module».initialStore } }

private def binaryConfig (body : Program)
    (a b : UInt64) : SmallStep.Config Unit :=
  { expr := .running
      ⟨⟨[.i64 a, .i64 b], [], []⟩, body, 1, [], [], []⟩
    store :=
      { runtime := { module := «module», host := {} }
        wasm := «module».initialStore } }

private def unaryConfig (body : Program)
    (a : UInt64) : SmallStep.Config Unit :=
  { expr := .running
      ⟨⟨[.i64 a], [], []⟩, body, 1, [], [], []⟩
    store :=
      { runtime := { module := «module», host := {} }
        wasm := «module».initialStore } }

private def shiftValueConfig (body : Program)
    (a : UInt64) (n : UInt32) (b : UInt64) : SmallStep.Config Unit :=
  { expr := .running
      ⟨⟨[.i64 a, .i32 n, .i64 b], [], []⟩,
        body, 1, [], [], []⟩
    store :=
      { runtime := { module := «module», host := {} }
        wasm := «module».initialStore } }

private def shiftTwiceConfig (body : Program)
    (a : UInt64) (n m : UInt32) : SmallStep.Config Unit :=
  { expr := .running
      ⟨⟨[.i64 a, .i32 n, .i32 m], [], []⟩,
        body, 1, [], [], []⟩
    store :=
      { runtime := { module := «module», host := {} }
        wasm := «module».initialStore } }

/-! ## add -/
@[spec_of "rust-exported" "rust_u64_tests::add_chain"]
def AddChainSpec : Prop := ∀ (a b c : UInt64),
  SmallStep.PartiallyMeets (ternaryConfig func0 a b c)
    (fun rs _store => rs = [.i64 (a + b + c)])
set_option maxRecDepth 4096 in
@[proves Project.RustU64Tests.Spec.AddChainSpec]
theorem add_chain_correct : AddChainSpec := by
  intro a b c
  apply SmallStep.wasm_smallStep_partiallyMeets.{0} (α := Unit)
  intro gs
  simp only [ternaryConfig, func0]
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_addI64
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_addI64
  inext
  iapply SmallStep.wp_returnFromFunction
  inext
  iapply wp_value'
  ipureintro
  rfl

@[spec_of "rust-exported" "rust_u64_tests::add_then_mul"]
def AddThenMulSpec : Prop := ∀ (a b c : UInt64),
  SmallStep.PartiallyMeets (ternaryConfig func1 a b c)
    (fun rs _store => rs = [.i64 ((a + b) * c)])
set_option maxRecDepth 4096 in
@[proves Project.RustU64Tests.Spec.AddThenMulSpec]
theorem add_then_mul_correct : AddThenMulSpec := by
  intro a b c
  apply SmallStep.wasm_smallStep_partiallyMeets.{0} (α := Unit)
  intro gs
  simp only [ternaryConfig, func1]
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_addI64
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_mulI64
  inext
  iapply SmallStep.wp_returnFromFunction
  inext
  iapply wp_value'
  ipureintro
  rfl

/-! ## sub -/
@[spec_of "rust-exported" "rust_u64_tests::sub_chain"]
def SubChainSpec : Prop := ∀ (a b c : UInt64),
  SmallStep.PartiallyMeets (ternaryConfig func18 a b c)
    (fun rs _store => rs = [.i64 (a - b - c)])
set_option maxRecDepth 4096 in
@[proves Project.RustU64Tests.Spec.SubChainSpec]
theorem sub_chain_correct : SubChainSpec := by
  intro a b c
  apply SmallStep.wasm_smallStep_partiallyMeets.{0} (α := Unit)
  intro gs
  simp only [ternaryConfig, func18]
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_subI64
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_subI64
  inext
  iapply SmallStep.wp_returnFromFunction
  inext
  iapply wp_value'
  ipureintro
  rfl

@[spec_of "rust-exported" "rust_u64_tests::sub_then_add"]
def SubThenAddSpec : Prop := ∀ (a b c : UInt64),
  SmallStep.PartiallyMeets (ternaryConfig func19 a b c)
    (fun rs _store => rs = [.i64 ((a - b) + c)])
set_option maxRecDepth 4096 in
@[proves Project.RustU64Tests.Spec.SubThenAddSpec]
theorem sub_then_add_correct : SubThenAddSpec := by
  intro a b c
  apply SmallStep.wasm_smallStep_partiallyMeets.{0} (α := Unit)
  intro gs
  simp only [ternaryConfig, func19]
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_subI64
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_addI64
  inext
  iapply SmallStep.wp_returnFromFunction
  inext
  iapply wp_value'
  ipureintro
  rfl

/-! ## mul -/
@[spec_of "rust-exported" "rust_u64_tests::mul_chain"]
def MulChainSpec : Prop := ∀ (a b c : UInt64),
  SmallStep.PartiallyMeets (ternaryConfig func6 a b c)
    (fun rs _store => rs = [.i64 (a * b * c)])
set_option maxRecDepth 4096 in
@[proves Project.RustU64Tests.Spec.MulChainSpec]
theorem mul_chain_correct : MulChainSpec := by
  intro a b c
  apply SmallStep.wasm_smallStep_partiallyMeets.{0} (α := Unit)
  intro gs
  simp only [ternaryConfig, func6]
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_mulI64
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_mulI64
  inext
  iapply SmallStep.wp_returnFromFunction
  inext
  iapply wp_value'
  ipureintro
  rfl

@[spec_of "rust-exported" "rust_u64_tests::mul_then_add"]
def MulThenAddSpec : Prop := ∀ (a b c : UInt64),
  SmallStep.PartiallyMeets (ternaryConfig func7 a b c)
    (fun rs _store => rs = [.i64 (a * b + c)])
set_option maxRecDepth 4096 in
@[proves Project.RustU64Tests.Spec.MulThenAddSpec]
theorem mul_then_add_correct : MulThenAddSpec := by
  intro a b c
  apply SmallStep.wasm_smallStep_partiallyMeets.{0} (α := Unit)
  intro gs
  simp only [ternaryConfig, func7]
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_mulI64
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_addI64
  inext
  iapply SmallStep.wp_returnFromFunction
  inext
  iapply wp_value'
  ipureintro
  rfl

/-! ## bitand -/
@[spec_of "rust-exported" "rust_u64_tests::and_chain"]
def AndChainSpec : Prop := ∀ (a b c : UInt64),
  SmallStep.PartiallyMeets (ternaryConfig func2 a b c)
    (fun rs _store => rs = [.i64 (a &&& b &&& c)])
set_option maxRecDepth 4096 in
@[proves Project.RustU64Tests.Spec.AndChainSpec]
theorem and_chain_correct : AndChainSpec := by
  intro a b c
  apply SmallStep.wasm_smallStep_partiallyMeets.{0} (α := Unit)
  intro gs
  simp only [ternaryConfig, func2]
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_andI64
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_andI64
  inext
  iapply SmallStep.wp_returnFromFunction
  inext
  iapply wp_value'
  ipureintro
  rfl

@[spec_of "rust-exported" "rust_u64_tests::and_then_or"]
def AndThenOrSpec : Prop := ∀ (a b c : UInt64),
  SmallStep.PartiallyMeets (ternaryConfig func3 a b c)
    (fun rs _store => rs = [.i64 ((a &&& b) ||| c)])
set_option maxRecDepth 4096 in
@[proves Project.RustU64Tests.Spec.AndThenOrSpec]
theorem and_then_or_correct : AndThenOrSpec := by
  intro a b c
  apply SmallStep.wasm_smallStep_partiallyMeets.{0} (α := Unit)
  intro gs
  simp only [ternaryConfig, func3]
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_andI64
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_orI64
  inext
  iapply SmallStep.wp_returnFromFunction
  inext
  iapply wp_value'
  ipureintro
  rfl

/-! ## bitor -/
@[spec_of "rust-exported" "rust_u64_tests::or_chain"]
def OrChainSpec : Prop := ∀ (a b c : UInt64),
  SmallStep.PartiallyMeets (ternaryConfig func10 a b c)
    (fun rs _store => rs = [.i64 (a ||| b ||| c)])
set_option maxRecDepth 4096 in
@[proves Project.RustU64Tests.Spec.OrChainSpec]
theorem or_chain_correct : OrChainSpec := by
  intro a b c
  apply SmallStep.wasm_smallStep_partiallyMeets.{0} (α := Unit)
  intro gs
  simp only [ternaryConfig, func10]
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_orI64
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_orI64
  inext
  iapply SmallStep.wp_returnFromFunction
  inext
  iapply wp_value'
  ipureintro
  rfl

@[spec_of "rust-exported" "rust_u64_tests::or_then_xor"]
def OrThenXorSpec : Prop := ∀ (a b c : UInt64),
  SmallStep.PartiallyMeets (ternaryConfig func11 a b c)
    (fun rs _store => rs = [.i64 ((a ||| b) ^^^ c)])
set_option maxRecDepth 4096 in
@[proves Project.RustU64Tests.Spec.OrThenXorSpec]
theorem or_then_xor_correct : OrThenXorSpec := by
  intro a b c
  apply SmallStep.wasm_smallStep_partiallyMeets.{0} (α := Unit)
  intro gs
  simp only [ternaryConfig, func11]
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_orI64
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_xorI64
  inext
  iapply SmallStep.wp_returnFromFunction
  inext
  iapply wp_value'
  ipureintro
  rfl

/-! ## bitxor -/
@[spec_of "rust-exported" "rust_u64_tests::xor_chain"]
def XorChainSpec : Prop := ∀ (a b c : UInt64),
  SmallStep.PartiallyMeets (ternaryConfig func20 a b c)
    (fun rs _store => rs = [.i64 (a ^^^ b ^^^ c)])
set_option maxRecDepth 4096 in
@[proves Project.RustU64Tests.Spec.XorChainSpec]
theorem xor_chain_correct : XorChainSpec := by
  intro a b c
  apply SmallStep.wasm_smallStep_partiallyMeets.{0} (α := Unit)
  intro gs
  simp only [ternaryConfig, func20]
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_xorI64
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_xorI64
  inext
  iapply SmallStep.wp_returnFromFunction
  inext
  iapply wp_value'
  ipureintro
  rfl

@[spec_of "rust-exported" "rust_u64_tests::xor_then_and"]
def XorThenAndSpec : Prop := ∀ (a b c : UInt64),
  SmallStep.PartiallyMeets (ternaryConfig func21 a b c)
    (fun rs _store => rs = [.i64 ((a ^^^ b) &&& c)])
set_option maxRecDepth 4096 in
@[proves Project.RustU64Tests.Spec.XorThenAndSpec]
theorem xor_then_and_correct : XorThenAndSpec := by
  intro a b c
  apply SmallStep.wasm_smallStep_partiallyMeets.{0} (α := Unit)
  intro gs
  simp only [ternaryConfig, func21]
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_xorI64
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_andI64
  inext
  iapply SmallStep.wp_returnFromFunction
  inext
  iapply wp_value'
  ipureintro
  rfl

/-! ## not -/
@[spec_of "rust-exported" "rust_u64_tests::not_twice"]
def NotTwiceSpec : Prop := ∀ (a : UInt64),
  SmallStep.PartiallyMeets (unaryConfig func9 a)
    (fun rs _store => rs = [.i64 (~~~(~~~a))])
set_option maxRecDepth 4096 in
@[proves Project.RustU64Tests.Spec.NotTwiceSpec]
theorem not_twice_correct : NotTwiceSpec := by
  intro a
  apply SmallStep.wasm_smallStep_partiallyMeets.{0} (α := Unit)
  intro gs
  simp only [unaryConfig, func9]
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_constI64
  inext
  iapply SmallStep.wp_xorI64
  inext
  rw [show a ^^^ (18446744073709551615 : UInt64) = ~~~a by bv_decide]
  iapply SmallStep.wp_constI64
  inext
  iapply SmallStep.wp_xorI64
  inext
  rw [show (~~~a) ^^^ (18446744073709551615 : UInt64) = ~~~(~~~a) by
    bv_decide]
  iapply SmallStep.wp_returnFromFunction
  inext
  iapply wp_value'
  ipureintro
  rfl

@[spec_of "rust-exported" "rust_u64_tests::not_then_xor"]
def NotThenXorSpec : Prop := ∀ (a b : UInt64),
  SmallStep.PartiallyMeets (binaryConfig func8 a b)
    (fun rs _store => rs = [.i64 ((~~~a) ^^^ b)])
set_option maxRecDepth 4096 in
@[proves Project.RustU64Tests.Spec.NotThenXorSpec]
theorem not_then_xor_correct : NotThenXorSpec := by
  intro a b
  apply SmallStep.wasm_smallStep_partiallyMeets.{0} (α := Unit)
  intro gs
  simp only [binaryConfig, func8]
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_constI64
  inext
  iapply SmallStep.wp_xorI64
  inext
  rw [show a ^^^ (18446744073709551615 : UInt64) = ~~~a by bv_decide]
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_xorI64
  inext
  iapply SmallStep.wp_returnFromFunction
  inext
  iapply wp_value'
  ipureintro
  rfl

/-! ## div (divisor nonzero) -/
@[spec_of "rust-exported" "rust_u64_tests::div_then_add"]
def DivThenAddSpec : Prop := ∀ (a b c : UInt64), b ≠ 0 →
  SmallStep.PartiallyMeets (ternaryConfig func4 a b c)
    (fun rs _store => rs = [.i64 (a / b + c)])
set_option maxRecDepth 4096 in
@[proves Project.RustU64Tests.Spec.DivThenAddSpec]
theorem div_then_add_correct : DivThenAddSpec := by
  intro a b c hb
  apply SmallStep.wasm_smallStep_partiallyMeets.{0} (α := Unit)
  intro gs
  simp only [ternaryConfig, func4]
  iapply SmallStep.wp_block
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_constI64
  inext
  iapply SmallStep.wp_eqI64 (result := 0) (by simp [hb])
  inext
  iapply SmallStep.wp_const
  inext
  iapply SmallStep.wp_and
  inext
  rw [show (0 &&& 1 : UInt32) = 0 by decide]
  iapply SmallStep.wp_brIfZero
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_divUI64 hb
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_addI64
  inext
  iapply SmallStep.wp_returnFromFunction
  inext
  iapply wp_value'
  ipureintro
  rfl

@[spec_of "rust-exported" "rust_u64_tests::div_then_mul"]
def DivThenMulSpec : Prop := ∀ (a b c : UInt64), b ≠ 0 →
  SmallStep.PartiallyMeets (ternaryConfig func5 a b c)
    (fun rs _store => rs = [.i64 (a / b * c)])
set_option maxRecDepth 4096 in
@[proves Project.RustU64Tests.Spec.DivThenMulSpec]
theorem div_then_mul_correct : DivThenMulSpec := by
  intro a b c hb
  apply SmallStep.wasm_smallStep_partiallyMeets.{0} (α := Unit)
  intro gs
  simp only [ternaryConfig, func5]
  iapply SmallStep.wp_block
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_constI64
  inext
  iapply SmallStep.wp_eqI64 (result := 0) (by simp [hb])
  inext
  iapply SmallStep.wp_const
  inext
  iapply SmallStep.wp_and
  inext
  rw [show (0 &&& 1 : UInt32) = 0 by decide]
  iapply SmallStep.wp_brIfZero
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_divUI64 hb
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_mulI64
  inext
  iapply SmallStep.wp_returnFromFunction
  inext
  iapply wp_value'
  ipureintro
  rfl

/-! ## rem (divisor nonzero) -/
@[spec_of "rust-exported" "rust_u64_tests::rem_then_add"]
def RemThenAddSpec : Prop := ∀ (a b c : UInt64), b ≠ 0 →
  SmallStep.PartiallyMeets (ternaryConfig func12 a b c)
    (fun rs _store => rs = [.i64 (a % b + c)])
set_option maxRecDepth 4096 in
@[proves Project.RustU64Tests.Spec.RemThenAddSpec]
theorem rem_then_add_correct : RemThenAddSpec := by
  intro a b c hb
  apply SmallStep.wasm_smallStep_partiallyMeets.{0} (α := Unit)
  intro gs
  simp only [ternaryConfig, func12]
  iapply SmallStep.wp_block
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_constI64
  inext
  iapply SmallStep.wp_eqI64 (result := 0) (by simp [hb])
  inext
  iapply SmallStep.wp_const
  inext
  iapply SmallStep.wp_and
  inext
  rw [show (0 &&& 1 : UInt32) = 0 by decide]
  iapply SmallStep.wp_brIfZero
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_remUI64 hb
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_addI64
  inext
  iapply SmallStep.wp_returnFromFunction
  inext
  iapply wp_value'
  ipureintro
  rfl

@[spec_of "rust-exported" "rust_u64_tests::rem_then_mul"]
def RemThenMulSpec : Prop := ∀ (a b c : UInt64), b ≠ 0 →
  SmallStep.PartiallyMeets (ternaryConfig func13 a b c)
    (fun rs _store => rs = [.i64 (a % b * c)])
set_option maxRecDepth 4096 in
@[proves Project.RustU64Tests.Spec.RemThenMulSpec]
theorem rem_then_mul_correct : RemThenMulSpec := by
  intro a b c hb
  apply SmallStep.wasm_smallStep_partiallyMeets.{0} (α := Unit)
  intro gs
  simp only [ternaryConfig, func13]
  iapply SmallStep.wp_block
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_constI64
  inext
  iapply SmallStep.wp_eqI64 (result := 0) (by simp [hb])
  inext
  iapply SmallStep.wp_const
  inext
  iapply SmallStep.wp_and
  inext
  rw [show (0 &&& 1 : UInt32) = 0 by decide]
  iapply SmallStep.wp_brIfZero
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_remUI64 hb
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_mulI64
  inext
  iapply SmallStep.wp_returnFromFunction
  inext
  iapply wp_value'
  ipureintro
  rfl

/-! ## shl / shr — mask, extend, then shift -/
@[spec_of "rust-exported" "rust_u64_tests::shl_then_add"]
def ShlThenAddSpec : Prop := ∀ (a : UInt64) (n : UInt32) (b : UInt64),
  SmallStep.PartiallyMeets (shiftValueConfig func14 a n b)
    (fun rs _store => rs = [.i64 ((a <<< (n.toUInt64 % 64)) + b)])
set_option maxRecDepth 4096 in
@[proves Project.RustU64Tests.Spec.ShlThenAddSpec]
theorem shl_then_add_correct : ShlThenAddSpec := by
  intro a n b
  apply SmallStep.wasm_smallStep_partiallyMeets.{0} (α := Unit)
  intro gs
  simp only [shiftValueConfig, func14]
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_const
  inext
  iapply SmallStep.wp_and
  inext
  rw [UInt32.and_comm n 63]
  iapply SmallStep.wp_extendUI32
  inext
  iapply SmallStep.wp_shlI64
  inext
  rw [shiftAmount_norm]
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_addI64
  inext
  iapply SmallStep.wp_returnFromFunction
  inext
  iapply wp_value'
  ipureintro
  rfl

@[spec_of "rust-exported" "rust_u64_tests::shl_twice"]
def ShlTwiceSpec : Prop := ∀ (a : UInt64) (n m : UInt32),
  SmallStep.PartiallyMeets (shiftTwiceConfig func15 a n m)
    (fun rs _store =>
      rs = [.i64 ((a <<< (n.toUInt64 % 64)) <<< (m.toUInt64 % 64))])
set_option maxRecDepth 4096 in
@[proves Project.RustU64Tests.Spec.ShlTwiceSpec]
theorem shl_twice_correct : ShlTwiceSpec := by
  intro a n m
  apply SmallStep.wasm_smallStep_partiallyMeets.{0} (α := Unit)
  intro gs
  simp only [shiftTwiceConfig, func15]
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_const
  inext
  iapply SmallStep.wp_and
  inext
  rw [UInt32.and_comm n 63]
  iapply SmallStep.wp_extendUI32
  inext
  iapply SmallStep.wp_shlI64
  inext
  rw [shiftAmount_norm]
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_const
  inext
  iapply SmallStep.wp_and
  inext
  rw [UInt32.and_comm m 63]
  iapply SmallStep.wp_extendUI32
  inext
  iapply SmallStep.wp_shlI64
  inext
  rw [shiftAmount_norm]
  iapply SmallStep.wp_returnFromFunction
  inext
  iapply wp_value'
  ipureintro
  rfl

@[spec_of "rust-exported" "rust_u64_tests::shr_then_sub"]
def ShrThenSubSpec : Prop := ∀ (a : UInt64) (n : UInt32) (b : UInt64),
  SmallStep.PartiallyMeets (shiftValueConfig func16 a n b)
    (fun rs _store => rs = [.i64 ((a >>> (n.toUInt64 % 64)) - b)])
set_option maxRecDepth 4096 in
@[proves Project.RustU64Tests.Spec.ShrThenSubSpec]
theorem shr_then_sub_correct : ShrThenSubSpec := by
  intro a n b
  apply SmallStep.wasm_smallStep_partiallyMeets.{0} (α := Unit)
  intro gs
  simp only [shiftValueConfig, func16]
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_const
  inext
  iapply SmallStep.wp_and
  inext
  rw [UInt32.and_comm n 63]
  iapply SmallStep.wp_extendUI32
  inext
  iapply SmallStep.wp_shrUI64
  inext
  rw [shiftAmount_norm]
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_subI64
  inext
  iapply SmallStep.wp_returnFromFunction
  inext
  iapply wp_value'
  ipureintro
  rfl

@[spec_of "rust-exported" "rust_u64_tests::shr_twice"]
def ShrTwiceSpec : Prop := ∀ (a : UInt64) (n m : UInt32),
  SmallStep.PartiallyMeets (shiftTwiceConfig func17 a n m)
    (fun rs _store =>
      rs = [.i64 ((a >>> (n.toUInt64 % 64)) >>> (m.toUInt64 % 64))])
set_option maxRecDepth 4096 in
@[proves Project.RustU64Tests.Spec.ShrTwiceSpec]
theorem shr_twice_correct : ShrTwiceSpec := by
  intro a n m
  apply SmallStep.wasm_smallStep_partiallyMeets.{0} (α := Unit)
  intro gs
  simp only [shiftTwiceConfig, func17]
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_const
  inext
  iapply SmallStep.wp_and
  inext
  rw [UInt32.and_comm n 63]
  iapply SmallStep.wp_extendUI32
  inext
  iapply SmallStep.wp_shrUI64
  inext
  rw [shiftAmount_norm]
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_const
  inext
  iapply SmallStep.wp_and
  inext
  rw [UInt32.and_comm m 63]
  iapply SmallStep.wp_extendUI32
  inext
  iapply SmallStep.wp_shrUI64
  inext
  rw [shiftAmount_norm]
  iapply SmallStep.wp_returnFromFunction
  inext
  iapply wp_value'
  ipureintro
  rfl

end Project.RustU64Tests.Spec

Rust (2)

rust/rust_u64_tests/src/exports.rs rust · 53 lines 
//! Reuse tests for the `CodeLib/RustStd/U64` corpus.
//!
//! Each operator gets TWO structurally-distinct functions that use it INLINE
//! the way real client code emits it (no `#[no_mangle]` shim manufacturing a
//! call, no calling the op as a function). Their proofs in `Spec.lean`
//! discharge the inlined instruction chunks by reusing the CodeLib chunk
//! theorems — exactly what `opt-0`'s "same inlined sequence everywhere"
//! guarantees.

// ── add ─────────────────────────────────────────────────────────────────────
#[unsafe(no_mangle)] pub extern "C" fn add_chain(a: u64, b: u64, c: u64) -> u64 { a + b + c }
#[unsafe(no_mangle)] pub extern "C" fn add_then_mul(a: u64, b: u64, c: u64) -> u64 { (a + b) * c }

// ── sub ─────────────────────────────────────────────────────────────────────
#[unsafe(no_mangle)] pub extern "C" fn sub_chain(a: u64, b: u64, c: u64) -> u64 { a - b - c }
#[unsafe(no_mangle)] pub extern "C" fn sub_then_add(a: u64, b: u64, c: u64) -> u64 { (a - b) + c }

// ── mul ─────────────────────────────────────────────────────────────────────
#[unsafe(no_mangle)] pub extern "C" fn mul_chain(a: u64, b: u64, c: u64) -> u64 { a * b * c }
#[unsafe(no_mangle)] pub extern "C" fn mul_then_add(a: u64, b: u64, c: u64) -> u64 { a * b + c }

// ── bitand ──────────────────────────────────────────────────────────────────
#[unsafe(no_mangle)] pub extern "C" fn and_chain(a: u64, b: u64, c: u64) -> u64 { a & b & c }
#[unsafe(no_mangle)] pub extern "C" fn and_then_or(a: u64, b: u64, c: u64) -> u64 { (a & b) | c }

// ── bitor ───────────────────────────────────────────────────────────────────
#[unsafe(no_mangle)] pub extern "C" fn or_chain(a: u64, b: u64, c: u64) -> u64 { a | b | c }
#[unsafe(no_mangle)] pub extern "C" fn or_then_xor(a: u64, b: u64, c: u64) -> u64 { (a | b) ^ c }

// ── bitxor ──────────────────────────────────────────────────────────────────
#[unsafe(no_mangle)] pub extern "C" fn xor_chain(a: u64, b: u64, c: u64) -> u64 { a ^ b ^ c }
#[unsafe(no_mangle)] pub extern "C" fn xor_then_and(a: u64, b: u64, c: u64) -> u64 { (a ^ b) & c }

// ── not ─────────────────────────────────────────────────────────────────────
#[unsafe(no_mangle)] pub extern "C" fn not_twice(a: u64) -> u64 { !!a }
#[unsafe(no_mangle)] pub extern "C" fn not_then_xor(a: u64, b: u64) -> u64 { (!a) ^ b }

// ── shl ─────────────────────────────────────────────────────────────────────
#[unsafe(no_mangle)] pub extern "C" fn shl_then_add(a: u64, n: u32, b: u64) -> u64 { (a << n) + b }
#[unsafe(no_mangle)] pub extern "C" fn shl_twice(a: u64, n: u32, m: u32) -> u64 { (a << n) << m }

// ── shr ─────────────────────────────────────────────────────────────────────
#[unsafe(no_mangle)] pub extern "C" fn shr_then_sub(a: u64, n: u32, b: u64) -> u64 { (a >> n) - b }
#[unsafe(no_mangle)] pub extern "C" fn shr_twice(a: u64, n: u32, m: u32) -> u64 { (a >> n) >> m }

// ── div (divisors nonzero) ──────────────────────────────────────────────────
#[unsafe(no_mangle)] pub extern "C" fn div_then_add(a: u64, b: u64, c: u64) -> u64 { a / b + c }
#[unsafe(no_mangle)] pub extern "C" fn div_then_mul(a: u64, b: u64, c: u64) -> u64 { (a / b) * c }

// ── rem (divisors nonzero) ──────────────────────────────────────────────────
#[unsafe(no_mangle)] pub extern "C" fn rem_then_add(a: u64, b: u64, c: u64) -> u64 { a % b + c }
#[unsafe(no_mangle)] pub extern "C" fn rem_then_mul(a: u64, b: u64, c: u64) -> u64 { (a % b) * c }
rust/rust_u64_tests/src/lib.rs rust · 2 lines 
mod exports;

Other (1)

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

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

[dependencies]