Talos · verification report
← all projects

rust_u64_tests verified

rust: rust/rust_u64_tests · lean: lean/Project/RustU64Tests · repo @ 52f92e873252 · 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:31
1 proof

Informal spec

No informal description provided.

Formal statement

AddChainSpec : Prop := ∀ (env : HostEnv Unit) (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:47
1 proof

Informal spec

No informal description provided.

Formal statement

AddThenMulSpec : Prop := ∀ (env : HostEnv Unit) (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:64
1 proof

Informal spec

No informal description provided.

Formal statement

SubChainSpec : Prop := ∀ (env : HostEnv Unit) (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:80
1 proof

Informal spec

No informal description provided.

Formal statement

SubThenAddSpec : Prop := ∀ (env : HostEnv Unit) (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:97
1 proof

Informal spec

No informal description provided.

Formal statement

MulChainSpec : Prop := ∀ (env : HostEnv Unit) (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:113
1 proof

Informal spec

No informal description provided.

Formal statement

MulThenAddSpec : Prop := ∀ (env : HostEnv Unit) (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:130
1 proof

Informal spec

No informal description provided.

Formal statement

AndChainSpec : Prop := ∀ (env : HostEnv Unit) (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:146
1 proof

Informal spec

No informal description provided.

Formal statement

AndThenOrSpec : Prop := ∀ (env : HostEnv Unit) (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:163
1 proof

Informal spec

No informal description provided.

Formal statement

OrChainSpec : Prop := ∀ (env : HostEnv Unit) (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:179
1 proof

Informal spec

No informal description provided.

Formal statement

OrThenXorSpec : Prop := ∀ (env : HostEnv Unit) (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:196
1 proof

Informal spec

No informal description provided.

Formal statement

XorChainSpec : Prop := ∀ (env : HostEnv Unit) (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:212
1 proof

Informal spec

No informal description provided.

Formal statement

XorThenAndSpec : Prop := ∀ (env : HostEnv Unit) (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:229
1 proof

Informal spec

No informal description provided.

Formal statement

NotTwiceSpec : Prop := ∀ (env : HostEnv Unit) (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:245
1 proof

Informal spec

No informal description provided.

Formal statement

NotThenXorSpec : Prop := ∀ (env : HostEnv Unit) (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:262
1 proof

Informal spec

No informal description provided.

Formal statement

DivThenAddSpec : Prop := ∀ (env : HostEnv Unit) (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:286
1 proof

Informal spec

No informal description provided.

Formal statement

DivThenMulSpec : Prop := ∀ (env : HostEnv Unit) (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:311
1 proof

Informal spec

No informal description provided.

Formal statement

RemThenAddSpec : Prop := ∀ (env : HostEnv Unit) (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:335
1 proof

Informal spec

No informal description provided.

Formal statement

RemThenMulSpec : Prop := ∀ (env : HostEnv Unit) (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:360
1 proof

Informal spec

No informal description provided.

Formal statement

ShlThenAddSpec : Prop := ∀ (env : HostEnv Unit) (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:376
1 proof

Informal spec

No informal description provided.

Formal statement

ShlTwiceSpec : Prop := ∀ (env : HostEnv Unit) (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:392
1 proof

Informal spec

No informal description provided.

Formal statement

ShrThenSubSpec : Prop := ∀ (env : HostEnv Unit) (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:408
1 proof

Informal spec

No informal description provided.

Formal statement

ShrTwiceSpec : Prop := ∀ (env : HostEnv Unit) (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:32
`rust_u64_tests::add_chain` does not resolve to any export of crate `rust_u64_tests`
missing_docstring info
lean/Project/RustU64Tests/Spec.lean:31
spec `Project.RustU64Tests.Spec.AddChainSpec` has no `/-- … -/` docstring
unresolved_spec_of_target warn
lean/Project/RustU64Tests/Spec.lean:48
`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:47
spec `Project.RustU64Tests.Spec.AddThenMulSpec` has no `/-- … -/` docstring
unresolved_spec_of_target warn
lean/Project/RustU64Tests/Spec.lean:65
`rust_u64_tests::sub_chain` does not resolve to any export of crate `rust_u64_tests`
missing_docstring info
lean/Project/RustU64Tests/Spec.lean:64
spec `Project.RustU64Tests.Spec.SubChainSpec` has no `/-- … -/` docstring
unresolved_spec_of_target warn
lean/Project/RustU64Tests/Spec.lean:81
`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:80
spec `Project.RustU64Tests.Spec.SubThenAddSpec` has no `/-- … -/` docstring
unresolved_spec_of_target warn
lean/Project/RustU64Tests/Spec.lean:98
`rust_u64_tests::mul_chain` does not resolve to any export of crate `rust_u64_tests`
missing_docstring info
lean/Project/RustU64Tests/Spec.lean:97
spec `Project.RustU64Tests.Spec.MulChainSpec` has no `/-- … -/` docstring
unresolved_spec_of_target warn
lean/Project/RustU64Tests/Spec.lean:114
`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:113
spec `Project.RustU64Tests.Spec.MulThenAddSpec` has no `/-- … -/` docstring
unresolved_spec_of_target warn
lean/Project/RustU64Tests/Spec.lean:131
`rust_u64_tests::and_chain` does not resolve to any export of crate `rust_u64_tests`
missing_docstring info
lean/Project/RustU64Tests/Spec.lean:130
spec `Project.RustU64Tests.Spec.AndChainSpec` has no `/-- … -/` docstring
unresolved_spec_of_target warn
lean/Project/RustU64Tests/Spec.lean:147
`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:146
spec `Project.RustU64Tests.Spec.AndThenOrSpec` has no `/-- … -/` docstring
unresolved_spec_of_target warn
lean/Project/RustU64Tests/Spec.lean:164
`rust_u64_tests::or_chain` does not resolve to any export of crate `rust_u64_tests`
missing_docstring info
lean/Project/RustU64Tests/Spec.lean:163
spec `Project.RustU64Tests.Spec.OrChainSpec` has no `/-- … -/` docstring
unresolved_spec_of_target warn
lean/Project/RustU64Tests/Spec.lean:180
`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:179
spec `Project.RustU64Tests.Spec.OrThenXorSpec` has no `/-- … -/` docstring
unresolved_spec_of_target warn
lean/Project/RustU64Tests/Spec.lean:197
`rust_u64_tests::xor_chain` does not resolve to any export of crate `rust_u64_tests`
missing_docstring info
lean/Project/RustU64Tests/Spec.lean:196
spec `Project.RustU64Tests.Spec.XorChainSpec` has no `/-- … -/` docstring
unresolved_spec_of_target warn
lean/Project/RustU64Tests/Spec.lean:213
`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:212
spec `Project.RustU64Tests.Spec.XorThenAndSpec` has no `/-- … -/` docstring
unresolved_spec_of_target warn
lean/Project/RustU64Tests/Spec.lean:230
`rust_u64_tests::not_twice` does not resolve to any export of crate `rust_u64_tests`
missing_docstring info
lean/Project/RustU64Tests/Spec.lean:229
spec `Project.RustU64Tests.Spec.NotTwiceSpec` has no `/-- … -/` docstring
unresolved_spec_of_target warn
lean/Project/RustU64Tests/Spec.lean:246
`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:245
spec `Project.RustU64Tests.Spec.NotThenXorSpec` has no `/-- … -/` docstring
unresolved_spec_of_target warn
lean/Project/RustU64Tests/Spec.lean:263
`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:262
spec `Project.RustU64Tests.Spec.DivThenAddSpec` has no `/-- … -/` docstring
unresolved_spec_of_target warn
lean/Project/RustU64Tests/Spec.lean:287
`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:286
spec `Project.RustU64Tests.Spec.DivThenMulSpec` has no `/-- … -/` docstring
unresolved_spec_of_target warn
lean/Project/RustU64Tests/Spec.lean:312
`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:311
spec `Project.RustU64Tests.Spec.RemThenAddSpec` has no `/-- … -/` docstring
unresolved_spec_of_target warn
lean/Project/RustU64Tests/Spec.lean:336
`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:335
spec `Project.RustU64Tests.Spec.RemThenMulSpec` has no `/-- … -/` docstring
unresolved_spec_of_target warn
lean/Project/RustU64Tests/Spec.lean:361
`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:360
spec `Project.RustU64Tests.Spec.ShlThenAddSpec` has no `/-- … -/` docstring
unresolved_spec_of_target warn
lean/Project/RustU64Tests/Spec.lean:377
`rust_u64_tests::shl_twice` does not resolve to any export of crate `rust_u64_tests`
missing_docstring info
lean/Project/RustU64Tests/Spec.lean:376
spec `Project.RustU64Tests.Spec.ShlTwiceSpec` has no `/-- … -/` docstring
unresolved_spec_of_target warn
lean/Project/RustU64Tests/Spec.lean:393
`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:392
spec `Project.RustU64Tests.Spec.ShrThenSubSpec` has no `/-- … -/` docstring
unresolved_spec_of_target warn
lean/Project/RustU64Tests/Spec.lean:409
`rust_u64_tests::shr_twice` does not resolve to any export of crate `rust_u64_tests`
missing_docstring info
lean/Project/RustU64Tests/Spec.lean:408
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 · 425 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, no `.call`). **Every** inlined op is
discharged by rewriting with that op's CodeLib chunk theorem — the op's own
atomic `wp_*` lemma is deliberately NOT in the `simp` set, so the reusable
CodeLib theorem is the only way through (confirm by dropping the chunk lemma: the
proof then fails). This is a CodeLib proof reused on *inlined* client code, which
is the whole point — the same theorem also serves the called export body.

- straight-line + `not`: `add_seq`/`sub_seq`/`mul_seq`/`bitand_seq`/`bitor_seq`/
  `bitxor_seq`/`not_seq`.
- `shl`/`shr`: `shl_seq`/`shr_seq` — the width-specific mask-extend-shift chunk
  (the `b % 64` normalisation is baked into the chunk, so no `bv_decide` here).
- `div`/`rem`: peel the `block` (`wp_block_cons`), reuse `nonzeroGuardSeq` for the
  zero-divisor guard (no hand-rolled guard simp), then reuse `div_seq`/`rem_seq`
  for the divide/remainder (`divUI64`/`remUI64` atomics excluded). The trailing
  `+ c` / `* c` reuses `add_seq` / `mul_seq` too.
-/

set_option linter.unusedSimpArgs false

namespace Project.RustU64Tests.Spec

open Wasm Wasm.RustStd Wasm.RustStd.U64

/-! ## add -/
@[spec_of "rust-exported" "rust_u64_tests::add_chain"]
def AddChainSpec : Prop := ∀ (env : HostEnv Unit) (a b c : UInt64),
  TerminatesWith env «module» 0 «module».initialStore [.i64 c, .i64 b, .i64 a]
    (fun _ rs => rs = [.i64 (a + b + c)])
set_option maxRecDepth 4096 in
@[proves Project.RustU64Tests.Spec.AddChainSpec]
theorem add_chain_correct : AddChainSpec := by
  intro env a b c
  apply TerminatesWith.of_wp_entry_for (f := func0Def) rfl
  unfold func0Def func0
  simp only [Function.toLocals, Function.numParams, List.take, List.reverse, List.reverseAux,
    List.map, ValueType.zero, wp_localGet_cons, Locals.get, List.length_cons, List.length_nil,
    List.getElem?_cons_zero, List.getElem?_cons_succ, Nat.reduceAdd, Nat.reduceLT, reduceIte,
    List.drop, add_seq, wp_ret_cons, Continuation.Return.injEq, List.cons.injEq, and_true,
    List.append_nil]

@[spec_of "rust-exported" "rust_u64_tests::add_then_mul"]
def AddThenMulSpec : Prop := ∀ (env : HostEnv Unit) (a b c : UInt64),
  TerminatesWith env «module» 1 «module».initialStore [.i64 c, .i64 b, .i64 a]
    (fun _ rs => rs = [.i64 ((a + b) * c)])
set_option maxRecDepth 4096 in
@[proves Project.RustU64Tests.Spec.AddThenMulSpec]
theorem add_then_mul_correct : AddThenMulSpec := by
  intro env a b c
  apply TerminatesWith.of_wp_entry_for (f := func1Def) rfl
  unfold func1Def func1
  simp only [Function.toLocals, Function.numParams, List.take, List.reverse, List.reverseAux,
    List.map, ValueType.zero, wp_localGet_cons, Locals.get, List.length_cons, List.length_nil,
    List.getElem?_cons_zero, List.getElem?_cons_succ, Nat.reduceAdd, Nat.reduceLT, reduceIte,
    List.drop, add_seq, mul_seq, wp_ret_cons, Continuation.Return.injEq, List.cons.injEq,
    and_true, List.append_nil]

/-! ## sub -/
@[spec_of "rust-exported" "rust_u64_tests::sub_chain"]
def SubChainSpec : Prop := ∀ (env : HostEnv Unit) (a b c : UInt64),
  TerminatesWith env «module» 18 «module».initialStore [.i64 c, .i64 b, .i64 a]
    (fun _ rs => rs = [.i64 (a - b - c)])
set_option maxRecDepth 4096 in
@[proves Project.RustU64Tests.Spec.SubChainSpec]
theorem sub_chain_correct : SubChainSpec := by
  intro env a b c
  apply TerminatesWith.of_wp_entry_for (f := func18Def) rfl
  unfold func18Def func18
  simp only [Function.toLocals, Function.numParams, List.take, List.reverse, List.reverseAux,
    List.map, ValueType.zero, wp_localGet_cons, Locals.get, List.length_cons, List.length_nil,
    List.getElem?_cons_zero, List.getElem?_cons_succ, Nat.reduceAdd, Nat.reduceLT, reduceIte,
    List.drop, sub_seq, wp_ret_cons, Continuation.Return.injEq, List.cons.injEq, and_true,
    List.append_nil]

@[spec_of "rust-exported" "rust_u64_tests::sub_then_add"]
def SubThenAddSpec : Prop := ∀ (env : HostEnv Unit) (a b c : UInt64),
  TerminatesWith env «module» 19 «module».initialStore [.i64 c, .i64 b, .i64 a]
    (fun _ rs => rs = [.i64 ((a - b) + c)])
set_option maxRecDepth 4096 in
@[proves Project.RustU64Tests.Spec.SubThenAddSpec]
theorem sub_then_add_correct : SubThenAddSpec := by
  intro env a b c
  apply TerminatesWith.of_wp_entry_for (f := func19Def) rfl
  unfold func19Def func19
  simp only [Function.toLocals, Function.numParams, List.take, List.reverse, List.reverseAux,
    List.map, ValueType.zero, wp_localGet_cons, Locals.get, List.length_cons, List.length_nil,
    List.getElem?_cons_zero, List.getElem?_cons_succ, Nat.reduceAdd, Nat.reduceLT, reduceIte,
    List.drop, sub_seq, add_seq, wp_ret_cons, Continuation.Return.injEq, List.cons.injEq,
    and_true, List.append_nil]

/-! ## mul -/
@[spec_of "rust-exported" "rust_u64_tests::mul_chain"]
def MulChainSpec : Prop := ∀ (env : HostEnv Unit) (a b c : UInt64),
  TerminatesWith env «module» 6 «module».initialStore [.i64 c, .i64 b, .i64 a]
    (fun _ rs => rs = [.i64 (a * b * c)])
set_option maxRecDepth 4096 in
@[proves Project.RustU64Tests.Spec.MulChainSpec]
theorem mul_chain_correct : MulChainSpec := by
  intro env a b c
  apply TerminatesWith.of_wp_entry_for (f := func6Def) rfl
  unfold func6Def func6
  simp only [Function.toLocals, Function.numParams, List.take, List.reverse, List.reverseAux,
    List.map, ValueType.zero, wp_localGet_cons, Locals.get, List.length_cons, List.length_nil,
    List.getElem?_cons_zero, List.getElem?_cons_succ, Nat.reduceAdd, Nat.reduceLT, reduceIte,
    List.drop, mul_seq, wp_ret_cons, Continuation.Return.injEq, List.cons.injEq, and_true,
    List.append_nil]

@[spec_of "rust-exported" "rust_u64_tests::mul_then_add"]
def MulThenAddSpec : Prop := ∀ (env : HostEnv Unit) (a b c : UInt64),
  TerminatesWith env «module» 7 «module».initialStore [.i64 c, .i64 b, .i64 a]
    (fun _ rs => rs = [.i64 (a * b + c)])
set_option maxRecDepth 4096 in
@[proves Project.RustU64Tests.Spec.MulThenAddSpec]
theorem mul_then_add_correct : MulThenAddSpec := by
  intro env a b c
  apply TerminatesWith.of_wp_entry_for (f := func7Def) rfl
  unfold func7Def func7
  simp only [Function.toLocals, Function.numParams, List.take, List.reverse, List.reverseAux,
    List.map, ValueType.zero, wp_localGet_cons, Locals.get, List.length_cons, List.length_nil,
    List.getElem?_cons_zero, List.getElem?_cons_succ, Nat.reduceAdd, Nat.reduceLT, reduceIte,
    List.drop, mul_seq, add_seq, wp_ret_cons, Continuation.Return.injEq, List.cons.injEq,
    and_true, List.append_nil]

/-! ## bitand -/
@[spec_of "rust-exported" "rust_u64_tests::and_chain"]
def AndChainSpec : Prop := ∀ (env : HostEnv Unit) (a b c : UInt64),
  TerminatesWith env «module» 2 «module».initialStore [.i64 c, .i64 b, .i64 a]
    (fun _ rs => rs = [.i64 (a &&& b &&& c)])
set_option maxRecDepth 4096 in
@[proves Project.RustU64Tests.Spec.AndChainSpec]
theorem and_chain_correct : AndChainSpec := by
  intro env a b c
  apply TerminatesWith.of_wp_entry_for (f := func2Def) rfl
  unfold func2Def func2
  simp only [Function.toLocals, Function.numParams, List.take, List.reverse, List.reverseAux,
    List.map, ValueType.zero, wp_localGet_cons, Locals.get, List.length_cons, List.length_nil,
    List.getElem?_cons_zero, List.getElem?_cons_succ, Nat.reduceAdd, Nat.reduceLT, reduceIte,
    List.drop, bitand_seq, wp_ret_cons, Continuation.Return.injEq, List.cons.injEq, and_true,
    List.append_nil]

@[spec_of "rust-exported" "rust_u64_tests::and_then_or"]
def AndThenOrSpec : Prop := ∀ (env : HostEnv Unit) (a b c : UInt64),
  TerminatesWith env «module» 3 «module».initialStore [.i64 c, .i64 b, .i64 a]
    (fun _ rs => rs = [.i64 ((a &&& b) ||| c)])
set_option maxRecDepth 4096 in
@[proves Project.RustU64Tests.Spec.AndThenOrSpec]
theorem and_then_or_correct : AndThenOrSpec := by
  intro env a b c
  apply TerminatesWith.of_wp_entry_for (f := func3Def) rfl
  unfold func3Def func3
  simp only [Function.toLocals, Function.numParams, List.take, List.reverse, List.reverseAux,
    List.map, ValueType.zero, wp_localGet_cons, Locals.get, List.length_cons, List.length_nil,
    List.getElem?_cons_zero, List.getElem?_cons_succ, Nat.reduceAdd, Nat.reduceLT, reduceIte,
    List.drop, bitand_seq, bitor_seq, wp_ret_cons, Continuation.Return.injEq, List.cons.injEq,
    and_true, List.append_nil]

/-! ## bitor -/
@[spec_of "rust-exported" "rust_u64_tests::or_chain"]
def OrChainSpec : Prop := ∀ (env : HostEnv Unit) (a b c : UInt64),
  TerminatesWith env «module» 10 «module».initialStore [.i64 c, .i64 b, .i64 a]
    (fun _ rs => rs = [.i64 (a ||| b ||| c)])
set_option maxRecDepth 4096 in
@[proves Project.RustU64Tests.Spec.OrChainSpec]
theorem or_chain_correct : OrChainSpec := by
  intro env a b c
  apply TerminatesWith.of_wp_entry_for (f := func10Def) rfl
  unfold func10Def func10
  simp only [Function.toLocals, Function.numParams, List.take, List.reverse, List.reverseAux,
    List.map, ValueType.zero, wp_localGet_cons, Locals.get, List.length_cons, List.length_nil,
    List.getElem?_cons_zero, List.getElem?_cons_succ, Nat.reduceAdd, Nat.reduceLT, reduceIte,
    List.drop, bitor_seq, wp_ret_cons, Continuation.Return.injEq, List.cons.injEq, and_true,
    List.append_nil]

@[spec_of "rust-exported" "rust_u64_tests::or_then_xor"]
def OrThenXorSpec : Prop := ∀ (env : HostEnv Unit) (a b c : UInt64),
  TerminatesWith env «module» 11 «module».initialStore [.i64 c, .i64 b, .i64 a]
    (fun _ rs => rs = [.i64 ((a ||| b) ^^^ c)])
set_option maxRecDepth 4096 in
@[proves Project.RustU64Tests.Spec.OrThenXorSpec]
theorem or_then_xor_correct : OrThenXorSpec := by
  intro env a b c
  apply TerminatesWith.of_wp_entry_for (f := func11Def) rfl
  unfold func11Def func11
  simp only [Function.toLocals, Function.numParams, List.take, List.reverse, List.reverseAux,
    List.map, ValueType.zero, wp_localGet_cons, Locals.get, List.length_cons, List.length_nil,
    List.getElem?_cons_zero, List.getElem?_cons_succ, Nat.reduceAdd, Nat.reduceLT, reduceIte,
    List.drop, bitor_seq, bitxor_seq, wp_ret_cons, Continuation.Return.injEq, List.cons.injEq,
    and_true, List.append_nil]

/-! ## bitxor -/
@[spec_of "rust-exported" "rust_u64_tests::xor_chain"]
def XorChainSpec : Prop := ∀ (env : HostEnv Unit) (a b c : UInt64),
  TerminatesWith env «module» 20 «module».initialStore [.i64 c, .i64 b, .i64 a]
    (fun _ rs => rs = [.i64 (a ^^^ b ^^^ c)])
set_option maxRecDepth 4096 in
@[proves Project.RustU64Tests.Spec.XorChainSpec]
theorem xor_chain_correct : XorChainSpec := by
  intro env a b c
  apply TerminatesWith.of_wp_entry_for (f := func20Def) rfl
  unfold func20Def func20
  simp only [Function.toLocals, Function.numParams, List.take, List.reverse, List.reverseAux,
    List.map, ValueType.zero, wp_localGet_cons, Locals.get, List.length_cons, List.length_nil,
    List.getElem?_cons_zero, List.getElem?_cons_succ, Nat.reduceAdd, Nat.reduceLT, reduceIte,
    List.drop, bitxor_seq, wp_ret_cons, Continuation.Return.injEq, List.cons.injEq, and_true,
    List.append_nil]

@[spec_of "rust-exported" "rust_u64_tests::xor_then_and"]
def XorThenAndSpec : Prop := ∀ (env : HostEnv Unit) (a b c : UInt64),
  TerminatesWith env «module» 21 «module».initialStore [.i64 c, .i64 b, .i64 a]
    (fun _ rs => rs = [.i64 ((a ^^^ b) &&& c)])
set_option maxRecDepth 4096 in
@[proves Project.RustU64Tests.Spec.XorThenAndSpec]
theorem xor_then_and_correct : XorThenAndSpec := by
  intro env a b c
  apply TerminatesWith.of_wp_entry_for (f := func21Def) rfl
  unfold func21Def func21
  simp only [Function.toLocals, Function.numParams, List.take, List.reverse, List.reverseAux,
    List.map, ValueType.zero, wp_localGet_cons, Locals.get, List.length_cons, List.length_nil,
    List.getElem?_cons_zero, List.getElem?_cons_succ, Nat.reduceAdd, Nat.reduceLT, reduceIte,
    List.drop, bitxor_seq, bitand_seq, wp_ret_cons, Continuation.Return.injEq, List.cons.injEq,
    and_true, List.append_nil]

/-! ## not -/
@[spec_of "rust-exported" "rust_u64_tests::not_twice"]
def NotTwiceSpec : Prop := ∀ (env : HostEnv Unit) (a : UInt64),
  TerminatesWith env «module» 9 «module».initialStore [.i64 a]
    (fun _ rs => rs = [.i64 (~~~(~~~a))])
set_option maxRecDepth 4096 in
@[proves Project.RustU64Tests.Spec.NotTwiceSpec]
theorem not_twice_correct : NotTwiceSpec := by
  intro env a
  apply TerminatesWith.of_wp_entry_for (f := func9Def) rfl
  unfold func9Def func9
  simp only [Function.toLocals, Function.numParams, List.take, List.reverse, List.reverseAux,
    List.map, ValueType.zero, wp_localGet_cons, Locals.get, List.length_cons, List.length_nil,
    List.getElem?_cons_zero, List.getElem?_cons_succ, Nat.reduceAdd, Nat.reduceLT, reduceIte,
    List.drop, not_seq, wp_ret_cons, Continuation.Return.injEq, List.cons.injEq, and_true,
    List.append_nil]

@[spec_of "rust-exported" "rust_u64_tests::not_then_xor"]
def NotThenXorSpec : Prop := ∀ (env : HostEnv Unit) (a b : UInt64),
  TerminatesWith env «module» 8 «module».initialStore [.i64 b, .i64 a]
    (fun _ rs => rs = [.i64 ((~~~a) ^^^ b)])
set_option maxRecDepth 4096 in
@[proves Project.RustU64Tests.Spec.NotThenXorSpec]
theorem not_then_xor_correct : NotThenXorSpec := by
  intro env a b
  apply TerminatesWith.of_wp_entry_for (f := func8Def) rfl
  unfold func8Def func8
  simp only [Function.toLocals, Function.numParams, List.take, List.reverse, List.reverseAux,
    List.map, ValueType.zero, wp_localGet_cons, Locals.get, List.length_cons, List.length_nil,
    List.getElem?_cons_zero, List.getElem?_cons_succ, Nat.reduceAdd, Nat.reduceLT, reduceIte,
    List.drop, not_seq, bitxor_seq, wp_ret_cons, Continuation.Return.injEq, List.cons.injEq,
    and_true, List.append_nil]

/-! ## div (divisor nonzero) — peel the guard, then reuse `div_seq` -/
@[spec_of "rust-exported" "rust_u64_tests::div_then_add"]
def DivThenAddSpec : Prop := ∀ (env : HostEnv Unit) (a b c : UInt64), b ≠ 0 →
  TerminatesWith env «module» 4 «module».initialStore [.i64 c, .i64 b, .i64 a]
    (fun _ rs => rs = [.i64 (a / b + c)])
set_option maxRecDepth 4096 in
@[proves Project.RustU64Tests.Spec.DivThenAddSpec]
theorem div_then_add_correct : DivThenAddSpec := by
  intro env a b c hb
  apply TerminatesWith.of_wp_entry_for (f := func4Def) rfl
  unfold func4Def func4
  simp only [Function.toLocals, Function.numParams, List.take, List.reverse, List.reverseAux,
    List.map, ValueType.zero, List.length_cons, List.length_nil]
  apply wp_block_cons
  have hget : (⟨[.i64 a, .i64 b, .i64 c], [], []⟩ : Locals).get 1 = some (.i64 b) := rfl
  rw [nonzeroGuardSeq 1 b [] hget hb]
  simp only [wp_localGet_cons, Locals.get, List.length_cons, List.length_nil,
    List.getElem?_cons_zero, List.getElem?_cons_succ, Nat.reduceAdd, Nat.reduceLT, reduceIte,
    List.drop]
  rw [div_seq a b _ hb]
  simp only [wp_localGet_cons, Locals.get, List.length_cons, List.length_nil,
    List.getElem?_cons_zero, List.getElem?_cons_succ, Nat.reduceAdd, Nat.reduceLT, reduceIte,
    List.drop, add_seq, wp_ret_cons]
  simp [List.take]

@[spec_of "rust-exported" "rust_u64_tests::div_then_mul"]
def DivThenMulSpec : Prop := ∀ (env : HostEnv Unit) (a b c : UInt64), b ≠ 0 →
  TerminatesWith env «module» 5 «module».initialStore [.i64 c, .i64 b, .i64 a]
    (fun _ rs => rs = [.i64 (a / b * c)])
set_option maxRecDepth 4096 in
@[proves Project.RustU64Tests.Spec.DivThenMulSpec]
theorem div_then_mul_correct : DivThenMulSpec := by
  intro env a b c hb
  apply TerminatesWith.of_wp_entry_for (f := func5Def) rfl
  unfold func5Def func5
  simp only [Function.toLocals, Function.numParams, List.take, List.reverse, List.reverseAux,
    List.map, ValueType.zero, List.length_cons, List.length_nil]
  apply wp_block_cons
  have hget : (⟨[.i64 a, .i64 b, .i64 c], [], []⟩ : Locals).get 1 = some (.i64 b) := rfl
  rw [nonzeroGuardSeq 1 b [] hget hb]
  simp only [wp_localGet_cons, Locals.get, List.length_cons, List.length_nil,
    List.getElem?_cons_zero, List.getElem?_cons_succ, Nat.reduceAdd, Nat.reduceLT, reduceIte,
    List.drop]
  rw [div_seq a b _ hb]
  simp only [wp_localGet_cons, Locals.get, List.length_cons, List.length_nil,
    List.getElem?_cons_zero, List.getElem?_cons_succ, Nat.reduceAdd, Nat.reduceLT, reduceIte,
    List.drop, mul_seq, wp_ret_cons]
  simp [List.take]

/-! ## rem (divisor nonzero) -/
@[spec_of "rust-exported" "rust_u64_tests::rem_then_add"]
def RemThenAddSpec : Prop := ∀ (env : HostEnv Unit) (a b c : UInt64), b ≠ 0 →
  TerminatesWith env «module» 12 «module».initialStore [.i64 c, .i64 b, .i64 a]
    (fun _ rs => rs = [.i64 (a % b + c)])
set_option maxRecDepth 4096 in
@[proves Project.RustU64Tests.Spec.RemThenAddSpec]
theorem rem_then_add_correct : RemThenAddSpec := by
  intro env a b c hb
  apply TerminatesWith.of_wp_entry_for (f := func12Def) rfl
  unfold func12Def func12
  simp only [Function.toLocals, Function.numParams, List.take, List.reverse, List.reverseAux,
    List.map, ValueType.zero, List.length_cons, List.length_nil]
  apply wp_block_cons
  have hget : (⟨[.i64 a, .i64 b, .i64 c], [], []⟩ : Locals).get 1 = some (.i64 b) := rfl
  rw [nonzeroGuardSeq 1 b [] hget hb]
  simp only [wp_localGet_cons, Locals.get, List.length_cons, List.length_nil,
    List.getElem?_cons_zero, List.getElem?_cons_succ, Nat.reduceAdd, Nat.reduceLT, reduceIte,
    List.drop]
  rw [rem_seq a b _ hb]
  simp only [wp_localGet_cons, Locals.get, List.length_cons, List.length_nil,
    List.getElem?_cons_zero, List.getElem?_cons_succ, Nat.reduceAdd, Nat.reduceLT, reduceIte,
    List.drop, add_seq, wp_ret_cons]
  simp [List.take]

@[spec_of "rust-exported" "rust_u64_tests::rem_then_mul"]
def RemThenMulSpec : Prop := ∀ (env : HostEnv Unit) (a b c : UInt64), b ≠ 0 →
  TerminatesWith env «module» 13 «module».initialStore [.i64 c, .i64 b, .i64 a]
    (fun _ rs => rs = [.i64 (a % b * c)])
set_option maxRecDepth 4096 in
@[proves Project.RustU64Tests.Spec.RemThenMulSpec]
theorem rem_then_mul_correct : RemThenMulSpec := by
  intro env a b c hb
  apply TerminatesWith.of_wp_entry_for (f := func13Def) rfl
  unfold func13Def func13
  simp only [Function.toLocals, Function.numParams, List.take, List.reverse, List.reverseAux,
    List.map, ValueType.zero, List.length_cons, List.length_nil]
  apply wp_block_cons
  have hget : (⟨[.i64 a, .i64 b, .i64 c], [], []⟩ : Locals).get 1 = some (.i64 b) := rfl
  rw [nonzeroGuardSeq 1 b [] hget hb]
  simp only [wp_localGet_cons, Locals.get, List.length_cons, List.length_nil,
    List.getElem?_cons_zero, List.getElem?_cons_succ, Nat.reduceAdd, Nat.reduceLT, reduceIte,
    List.drop]
  rw [rem_seq a b _ hb]
  simp only [wp_localGet_cons, Locals.get, List.length_cons, List.length_nil,
    List.getElem?_cons_zero, List.getElem?_cons_succ, Nat.reduceAdd, Nat.reduceLT, reduceIte,
    List.drop, mul_seq, wp_ret_cons]
  simp [List.take]

/-! ## shl / shr — width-specific mask-extend-shift (reusable theorem: `U64.shl_seq`) -/
@[spec_of "rust-exported" "rust_u64_tests::shl_then_add"]
def ShlThenAddSpec : Prop := ∀ (env : HostEnv Unit) (a : UInt64) (n : UInt32) (b : UInt64),
  TerminatesWith env «module» 14 «module».initialStore [.i64 b, .i32 n, .i64 a]
    (fun _ rs => 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 env a n b
  apply TerminatesWith.of_wp_entry_for (f := func14Def) rfl
  unfold func14Def func14
  simp only [Function.toLocals, Function.numParams, List.take, List.reverse, List.reverseAux,
    List.map, ValueType.zero, wp_localGet_cons, Locals.get, List.length_cons, List.length_nil,
    List.getElem?_cons_zero, List.getElem?_cons_succ, Nat.reduceAdd, Nat.reduceLT, reduceIte,
    List.drop, shiftAmountFrag, shiftMask, shl_seq, add_seq, wp_ret_cons,
    Continuation.Return.injEq, List.cons.injEq, and_true, List.append_nil]

@[spec_of "rust-exported" "rust_u64_tests::shl_twice"]
def ShlTwiceSpec : Prop := ∀ (env : HostEnv Unit) (a : UInt64) (n m : UInt32),
  TerminatesWith env «module» 15 «module».initialStore [.i32 m, .i32 n, .i64 a]
    (fun _ rs => 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 env a n m
  apply TerminatesWith.of_wp_entry_for (f := func15Def) rfl
  unfold func15Def func15
  simp only [Function.toLocals, Function.numParams, List.take, List.reverse, List.reverseAux,
    List.map, ValueType.zero, wp_localGet_cons, Locals.get, List.length_cons, List.length_nil,
    List.getElem?_cons_zero, List.getElem?_cons_succ, Nat.reduceAdd, Nat.reduceLT, reduceIte,
    List.drop, shiftAmountFrag, shiftMask, shl_seq, wp_ret_cons, Continuation.Return.injEq,
    List.cons.injEq, and_true, List.append_nil]

@[spec_of "rust-exported" "rust_u64_tests::shr_then_sub"]
def ShrThenSubSpec : Prop := ∀ (env : HostEnv Unit) (a : UInt64) (n : UInt32) (b : UInt64),
  TerminatesWith env «module» 16 «module».initialStore [.i64 b, .i32 n, .i64 a]
    (fun _ rs => 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 env a n b
  apply TerminatesWith.of_wp_entry_for (f := func16Def) rfl
  unfold func16Def func16
  simp only [Function.toLocals, Function.numParams, List.take, List.reverse, List.reverseAux,
    List.map, ValueType.zero, wp_localGet_cons, Locals.get, List.length_cons, List.length_nil,
    List.getElem?_cons_zero, List.getElem?_cons_succ, Nat.reduceAdd, Nat.reduceLT, reduceIte,
    List.drop, shiftAmountFrag, shiftMask, shr_seq, sub_seq, wp_ret_cons,
    Continuation.Return.injEq, List.cons.injEq, and_true, List.append_nil]

@[spec_of "rust-exported" "rust_u64_tests::shr_twice"]
def ShrTwiceSpec : Prop := ∀ (env : HostEnv Unit) (a : UInt64) (n m : UInt32),
  TerminatesWith env «module» 17 «module».initialStore [.i32 m, .i32 n, .i64 a]
    (fun _ rs => 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 env a n m
  apply TerminatesWith.of_wp_entry_for (f := func17Def) rfl
  unfold func17Def func17
  simp only [Function.toLocals, Function.numParams, List.take, List.reverse, List.reverseAux,
    List.map, ValueType.zero, wp_localGet_cons, Locals.get, List.length_cons, List.length_nil,
    List.getElem?_cons_zero, List.getElem?_cons_succ, Nat.reduceAdd, Nat.reduceLT, reduceIte,
    List.drop, shiftAmountFrag, shiftMask, shr_seq, wp_ret_cons, Continuation.Return.injEq,
    List.cons.injEq, and_true, List.append_nil]

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]