swap_elements_opt3 no specs
0 / 1 exports have a proven spec
Exports
1
Specs
0
Verifications
0
Diagnostics
0
Formal specs
No specs discovered. Mark
defs in Spec.lean with @[spec_of "rust-exported" "swap_elements_opt3::name"].Exported functions
swap_elements rust/swap_elements_opt3/src/exports.rs:1
Wasm-exported entry point for `swap_elements`.
Thin `extern "C"` wrapper around the pure [`crate::swap_elements`]. The
project convention reserves this file for the wasm ABI surface, so the
export table matches exactly what the verifier reasons about.
Receives the array as a `(pointer, length)` pair plus the two indices to
swap. On wasm32 both `usize` and the pointer are 32-bit. The caller must
guarantee `i < data_length` and `j < data_length` and that
`[array_ptr, array_ptr + data_length)` is a valid, aligned `u64` region.
fn swap_elements(array_ptr: *mut u64, data_length: usize, i: usize, j: usize)Program (Lean)
Project.SwapElementsOpt3.module lean/Project/SwapElementsOpt3/Program.lean:6971
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
],
exports := [
{ name := "swap_elements", funcIdx := 0 }
],
memory := some { pagesMin := (17 : UInt32), pagesMax := none, data := [
{ offset := some (1048576 : UInt32), bytes := [(32 : UInt8), (105 : UInt8), (110 : UInt8), (100 : UInt8), (101 : UInt8), (120 : UInt8), (32 : UInt8), (111 : UInt8), (117 : UInt8), (116 : UInt8), (32 : UInt8), (111 : UInt8), (102 : UInt8), (32 : UInt8), (98 : UInt8), (111 : UInt8), (117 : UInt8), (110 : UInt8), (100 : UInt8), (115 : UInt8), (58 : UInt8), (32 : UInt8), (116 : UInt8), (104 : UInt8), (101 : UInt8), (32 : UInt8), (108 : UInt8), (101 : UInt8), (110 : UInt8), (32 : UInt8), (105 : UInt8), (115 : UInt8), (32 : UInt8), (192 : UInt8), (18 : UInt8), (32 : UInt8), (98 : UInt8), (117 : UInt8), (116 : UInt8), (32 : UInt8), (116 : UInt8), (104 : UInt8), (101 : UInt8), (32 : UInt8), (105 : UInt8), (110 : UInt8), (100 : UInt8), (101 : UInt8), (120 : UInt8), (32 : UInt8), (105 : UInt8), (115 : UInt8), (32 : UInt8), (192 : UInt8), (0 : UInt8), (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), (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), (115 : UInt8), (119 : UInt8), (97 : UInt8), (112 : UInt8), (95 : UInt8), (101 : UInt8), (108 : UInt8), (101 : UInt8), (109 : UInt8), (101 : UInt8), (110 : UInt8), (116 : UInt8), (115 : UInt8), (95 : UInt8), (111 : UInt8), (112 : UInt8), (116 : UInt8), (51 : UInt8), (47 : UInt8), (115 : UInt8), (114 : UInt8), (99 : UInt8), (47 : UInt8), (108 : UInt8), (105 : UInt8), (98 : UInt8), (46 : UInt8), (114 : UInt8), (115 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (179 : UInt8), (0 : UInt8), (16 : UInt8), (0 : UInt8), (29 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (9 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (9 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (2 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (12 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (4 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (3 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (4 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (5 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (8 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (4 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (6 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (7 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (8 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (9 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (10 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (16 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (4 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (11 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (12 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (13 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (14 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (109 : UInt8), (93 : UInt8), (203 : UInt8), (214 : UInt8), (44 : UInt8), (80 : UInt8), (235 : UInt8), (99 : UInt8), (120 : UInt8), (65 : UInt8), (166 : UInt8), (87 : UInt8), (113 : UInt8), (27 : UInt8), (139 : UInt8), (185 : UInt8), (21 : UInt8), (162 : UInt8), (92 : UInt8), (85 : UInt8), (52 : UInt8), (85 : UInt8), (7 : UInt8), (212 : UInt8), (83 : UInt8), (120 : UInt8), (173 : UInt8), (129 : UInt8), (81 : UInt8), (240 : UInt8), (163 : UInt8), (247 : UInt8), (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), (136 : 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), (136 : 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), (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), (0 : UInt8), (55 : UInt8), (0 : 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), (48 : UInt8), (48 : UInt8), (48 : UInt8), (49 : UInt8), (48 : UInt8), (50 : UInt8), (48 : UInt8), (51 : UInt8), (48 : UInt8), (52 : UInt8), (48 : UInt8), (53 : UInt8), (48 : UInt8), (54 : UInt8), (48 : UInt8), (55 : UInt8), (48 : UInt8), (56 : UInt8), (48 : UInt8), (57 : UInt8), (49 : UInt8), (48 : UInt8), (49 : UInt8), (49 : UInt8), (49 : UInt8), (50 : UInt8), (49 : UInt8), (51 : UInt8), (49 : UInt8), (52 : UInt8), (49 : UInt8), (53 : UInt8), (49 : UInt8), (54 : UInt8), (49 : UInt8), (55 : UInt8), (49 : UInt8), (56 : UInt8), (49 : UInt8), (57 : UInt8), (50 : UInt8), (48 : UInt8), (50 : UInt8), (49 : UInt8), (50 : UInt8), (50 : UInt8), (50 : UInt8), (51 : UInt8), (50 : UInt8), (52 : UInt8), (50 : UInt8), (53 : UInt8), (50 : UInt8), (54 : UInt8), (50 : UInt8), (55 : UInt8), (50 : UInt8), (56 : UInt8), (50 : UInt8), (57 : UInt8), (51 : UInt8), (48 : UInt8), (51 : UInt8), (49 : UInt8), (51 : UInt8), (50 : UInt8), (51 : UInt8), (51 : UInt8), (51 : UInt8), (52 : UInt8), (51 : UInt8), (53 : UInt8), (51 : UInt8), (54 : UInt8), (51 : UInt8), (55 : UInt8), (51 : UInt8), (56 : UInt8), (51 : UInt8), (57 : UInt8), (52 : UInt8), (48 : UInt8), (52 : UInt8), (49 : UInt8), (52 : UInt8), (50 : UInt8), (52 : UInt8), (51 : UInt8), (52 : UInt8), (52 : UInt8), (52 : UInt8), (53 : UInt8), (52 : UInt8), (54 : UInt8), (52 : UInt8), (55 : UInt8), (52 : UInt8), (56 : UInt8), (52 : UInt8), (57 : UInt8), (53 : UInt8), (48 : UInt8), (53 : UInt8), (49 : UInt8), (53 : UInt8), (50 : UInt8), (53 : UInt8), (51 : UInt8), (53 : UInt8), (52 : UInt8), (53 : UInt8), (53 : UInt8), (53 : UInt8), (54 : UInt8), (53 : UInt8), (55 : UInt8), (53 : UInt8), (56 : UInt8), (53 : UInt8), (57 : UInt8), (54 : UInt8), (48 : UInt8), (54 : UInt8), (49 : UInt8), (54 : UInt8), (50 : UInt8), (54 : UInt8), (51 : UInt8), (54 : UInt8), (52 : UInt8), (54 : UInt8), (53 : UInt8), (54 : UInt8), (54 : UInt8), (54 : UInt8), (55 : UInt8), (54 : UInt8), (56 : UInt8), (54 : UInt8), (57 : UInt8), (55 : UInt8), (48 : UInt8), (55 : UInt8), (49 : UInt8), (55 : UInt8), (50 : UInt8), (55 : UInt8), (51 : UInt8), (55 : UInt8), (52 : UInt8), (55 : UInt8), (53 : UInt8), (55 : UInt8), (54 : UInt8), (55 : UInt8), (55 : UInt8), (55 : UInt8), (56 : UInt8), (55 : UInt8), (57 : UInt8), (56 : UInt8), (48 : UInt8), (56 : UInt8), (49 : UInt8), (56 : UInt8), (50 : UInt8), (56 : UInt8), (51 : UInt8), (56 : UInt8), (52 : UInt8), (56 : UInt8), (53 : UInt8), (56 : UInt8), (54 : UInt8), (56 : UInt8), (55 : UInt8), (56 : UInt8), (56 : UInt8), (56 : UInt8), (57 : UInt8), (57 : UInt8), (48 : UInt8), (57 : UInt8), (49 : UInt8), (57 : UInt8), (50 : UInt8), (57 : UInt8), (51 : UInt8), (57 : UInt8), (52 : UInt8), (57 : UInt8), (53 : UInt8), (57 : UInt8), (54 : UInt8), (57 : UInt8), (55 : UInt8), (57 : UInt8), (56 : UInt8), (57 : UInt8), (57 : UInt8)] }
] },
globals := [
{ init := .i32 (1048576 : UInt32) },
{ init := .i32 (1049793 : UInt32) },
{ init := .i32 (1049808 : UInt32) }
],
types := [
{ params := [.i32, .i32], results := [] },
{ params := [.i32, .i32, .i32], results := [.i32] },
{ params := [.i32, .i32], results := [.i32] },
{ params := [.i32, .i32, .i32, .i32], results := [] },
{ params := [.i32, .i32, .i32], 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] },
{ params := [.i32, .i32, .i32, .i32, .i32, .i32], results := [.i32] },
{ params := [.i32, .i32, .i32, .i32, .i32], results := [.i32] }
],
tables := [
{ min := 18, max := some 18, elemType := .funcref }
],
elements := [
{ tableIdx := some 0, offset := some 1, funcs := [some 16, some 8, some 40, some 39, some 44, some 38, some 37, some 35, some 36, some 9, some 34, some 42, some 41, some 43, some 33, some 32, some 57] }
]
}Diagnostics
No diagnostics.
Source files (appendix)
Lean (4)
lean/Project/SwapElementsOpt3/Equivalence.lean lean · 148 lines
import Project.SwapElements.Spec -- opt-level 0 build + its `swap_elements_correct`
import Project.SwapElementsOpt3.Spec -- opt-level 3 build + its `func0_swap`
/-!
# Equivalence of the two `swap_elements` builds (`opt-level = 0` vs `opt-level = 3`)
`swap_elements` and `swap_elements_opt3` are compiled from **byte-for-byte the
same Rust source** (`arr.swap(i, j)` on a `&mut [u64]`); only the optimisation
level differs.
* `mod0` (`opt-level = 0`) carves a 16-byte shadow-stack frame out of `global 0`,
materialises the slice fat pointer through linear memory, forwards through a
four-deep call chain, and exchanges the two elements via a **scratch slot** at
`1048552`. `swap_elements` is exported at **func 4**.
* `mod3` (`opt-level = 3`) inlines the whole swap path into the exported
function: bounds checks, two `i64.load`s and two `i64.store`s through an
`i64` local. (The module still carries panic/formatting machinery in other
functions, but under the in-bounds preconditions the export never reaches
it.) It touches neither `global 0` nor any scratch memory. `swap_elements`
is exported at **func 0**.
## Why the observation must include memory
`swap_elements` **returns nothing** and communicates only by mutating the
caller's array. Its `Store.host` is `Unit`. So the `Store.host` instance of
observational equivalence — `Wasm.ObservationallyEquiv`, the notion the
`num_integer` `gcd` pair uses — degenerates here to bare *co-termination*: it
says the two builds return `[]` together, and nothing whatsoever about the
array. It is true, and it is nearly vacuous.
The right observation is the one `CodeLib.Equivalence` was generalised for:
`ObservationallyEquivOn` at
fun st => (st.host, st.mem.words64 ptr len.toNat)
— the host state together with **the caller's array, viewed as a `List UInt64`**.
Note this is deliberately weaker than "the final memories are equal", and it has
to be: the two builds' final memories are **not** the same function. `mod0`
additionally writes the exchanged value into the scratch slot at
`[1048552, 1048560)` — a write `mod3` never performs — so the memories agree
only away from that slot. Observing the array *region*, rather than all of
memory, is exactly what separates the caller-visible result from the scratch
traffic. That is the whole point, and it is why `Mem.words64` is the right
vocabulary.
## Preconditions
The two builds do **not** need the same hypotheses: `mod3` needs neither the
shadow-stack pin nor `1048576 ≤ ptr` (it has no scratch frame for the array to
alias). The equivalence is therefore stated under `mod0`'s — the stronger —
preconditions, which are exactly those of the merged `SwapElementsSpec`. On a
store violating them `mod0` can trap where `mod3` still succeeds, so they are
load-bearing, mirroring the `gcd` pair's use of a fixed initial store.
-/
namespace Project.SwapElementsOpt3.Equivalence
open Wasm
-- Both builds' specs share the opt0 `elemAddr` vocabulary, so the two
-- postconditions and the address lemmas below all match syntactically.
open Project.SwapElements.Spec (elemAddr elemAddr_disjoint)
/-- The unoptimised (`opt-level = 0`) build: shadow-stack + scratch-slot version. -/
abbrev mod0 : Wasm.Module := Project.SwapElements.module
/-- The optimised (`opt-level = 3`) build: fully inlined, memory-scratch-free. -/
abbrev mod3 : Wasm.Module := Project.SwapElementsOpt3.module
/-- `swap_elements` is exported at func **4** in the `opt-level = 0` build. -/
abbrev entry0 : Nat := 4
/-- `swap_elements` is exported at func **0** in the `opt-level = 3` build. -/
abbrev entry3 : Nat := 0
/-- **The observation**: what a caller of `swap_elements` can see — the host
state, plus the array `[ptr, ptr + 8*len)` as a list of `u64`s. Scratch traffic
outside the array is deliberately not observed. -/
@[reducible] def arrayObs (ptr len : UInt32) (st : Store Unit) : Unit × List UInt64 :=
(st.host, st.mem.words64 ptr len.toNat)
/-! ## The equivalence
Both builds' specs are stated per element (`read64 (elemAddr ptr k)`);
`Mem.words64_swap'` is the shared bridge to the `Mem.words64` view, so each
side reaches the *same* observation and `of_common_outcome` applies. -/
/-- **Program equivalence of the two `swap_elements` builds.**
For every in-bounds call, the two builds are `Wasm.ObservationallyEquivOn` at
the array observation: they agree on the returned values (`[]`), on the host
state, and on **the caller's array** — while the scratch slot `mod0` dirties,
and which `mod3` never touches, is left unobserved. -/
def SwapOptEquiv : Prop :=
∀ (env : HostEnv Unit) (st : Store Unit) (ptr len i j : UInt32),
i < len → j < len →
ptr.toNat + 8 * len.toNat ≤ st.mem.pages * 65536 →
1048576 ≤ ptr.toNat →
st.mem.pages ≤ 65536 →
st.globals.globals[0]? = some (.i32 1048576) →
ObservationallyEquivOn env mod0 entry0 mod3 entry3 st
[.i32 j, .i32 i, .i32 len, .i32 ptr] (arrayObs ptr len)
/-- The common outcome is the array with `i` and `j` exchanged. The opt0 side
reuses the merged `Project.SwapElements.Spec.swap_elements_correct`; the opt3
side uses `Project.SwapElementsOpt3.Spec.func0_swap`. Both are routed through
`Mem.words64_swap'`, so they land on the *same* observation. -/
theorem swap_opt_equiv : SwapOptEquiv := by
intro env st ptr len i j hi hj hbound hptr hpages hsp
refine ObservationallyEquivOn.of_common_outcome
(r := [])
(o := ((), ((st.mem.words64 ptr len.toNat).set i.toNat
(st.mem.read64 (elemAddr ptr j))).set j.toNat
(st.mem.read64 (elemAddr ptr i)))) ?_ ?_
· -- opt0: the merged total-correctness spec, per element.
refine (Project.SwapElements.Spec.swap_elements_correct
env st ptr len i j hi hj hbound hptr hpages hsp).mono ?_
rintro st' vs ⟨rfl, h_i, h_j, h_k⟩
exact ⟨rfl, Prod.ext rfl (Mem.words64_swap' hi hj h_i h_j h_k)⟩
· -- opt3: the inlined build writes the two elements directly.
refine (Project.SwapElementsOpt3.Spec.func0_swap
env st ptr len i j hi hj hbound hpages).mono ?_
rintro st' vs ⟨rfl, hmem⟩
have hli : i.toNat < len.toNat := hi
have hlj : j.toNat < len.toNat := hj
refine ⟨rfl, Prod.ext rfl (Mem.words64_swap' hi hj ?_ ?_ ?_)⟩
· -- `i = j` is permitted: the two stores then coincide.
show st'.mem.read64 (elemAddr ptr i) = st.mem.read64 (elemAddr ptr j)
by_cases hij : i = j
· subst hij; rw [hmem, Mem.read64_write64_same]
· rw [hmem,
Mem.read64_write64_disjoint _ _ _ _
(elemAddr_disjoint ptr i j (by omega) (by omega) hij),
Mem.read64_write64_same]
· show st'.mem.read64 (elemAddr ptr j) = st.mem.read64 (elemAddr ptr i)
rw [hmem, Mem.read64_write64_same]
· intro k hk hki hkj
show st'.mem.read64 (elemAddr ptr k) = st.mem.read64 (elemAddr ptr k)
have hlk : k.toNat < len.toNat := hk
rw [hmem,
Mem.read64_write64_disjoint _ _ _ _
(elemAddr_disjoint ptr k j (by omega) (by omega) hkj),
Mem.read64_write64_disjoint _ _ _ _
(elemAddr_disjoint ptr k i (by omega) (by omega) hki)]
end Project.SwapElementsOpt3.Equivalence
lean/Project/SwapElementsOpt3/Program.lean lean · 7069 lines
/-
AUTO-GENERATED by `verifier emit`. Do not edit by hand.
-/
import CodeLib
set_option maxRecDepth 1048576
namespace Project.SwapElementsOpt3
open Wasm
/-- export: swap_elements -/
def func0 : Wasm.Program :=
[
.block 0 0 [
.block 0 0 [
.localGet 2,
.localGet 1,
.geU,
.br_if 0,
.localGet 3,
.localGet 1,
.geU,
.br_if 1,
.localGet 0,
.localGet 2,
.const (3 : UInt32),
.shl,
.add,
.localSet 1,
.localGet 1,
.load64 (0 : UInt32),
.localSet 4,
.localGet 1,
.localGet 0,
.localGet 3,
.const (3 : UInt32),
.shl,
.add,
.localSet 2,
.localGet 2,
.load64 (0 : UInt32),
.store64 (0 : UInt32),
.localGet 2,
.localGet 4,
.store64 (0 : UInt32),
.ret
],
.localGet 2,
.localGet 1,
.const (1048788 : UInt32),
.call 52,
.unreachable
],
.localGet 3,
.localGet 1,
.const (1048788 : UInt32),
.call 52,
.unreachable
]
def func0Def : Wasm.Function :=
{ params := [.i32, .i32, .i32, .i32], locals := [.i64], body := func0, results := [] }
def func1 : Wasm.Program :=
[
.localGet 0,
.localGet 1,
.call 18,
.ret
]
def func1Def : Wasm.Function :=
{ params := [.i32, .i32], locals := [], body := func1, results := [.i32] }
def func2 : Wasm.Program :=
[
.localGet 0,
.localGet 1,
.localGet 2,
.call 22,
.ret
]
def func2Def : Wasm.Function :=
{ params := [.i32, .i32, .i32], locals := [], body := func2, results := [] }
def func3 : Wasm.Program :=
[
.localGet 0,
.localGet 1,
.localGet 2,
.localGet 3,
.call 24,
.ret
]
def func3Def : Wasm.Function :=
{ params := [.i32, .i32, .i32, .i32], locals := [], body := func3, results := [.i32] }
def func4 : Wasm.Program :=
[
.ret
]
def func4Def : Wasm.Function :=
{ params := [], locals := [], body := func4, results := [] }
def func5 : Wasm.Program :=
[
.call 21,
.unreachable
]
def func5Def : Wasm.Function :=
{ params := [.i32, .i32], locals := [], body := func5, results := [.i32] }
def func6 : 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 46,
.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 14,
.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 46,
.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 func6Def : Wasm.Function :=
{ params := [.i32, .i32, .i32, .i32, .i32], locals := [.i32], body := func6, results := [] }
def func7 : 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 2
]
]
def func7Def : Wasm.Function :=
{ params := [.i32, .i32], locals := [], body := func7, results := [] }
def func8 : 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 2
]
]
def func8Def : Wasm.Function :=
{ params := [.i32], locals := [.i32], body := func8, results := [] }
def func9 : 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 2
]
]
def func9Def : Wasm.Function :=
{ params := [.i32], locals := [.i32], body := func9, results := [] }
def func10 : Wasm.Program :=
[
.localGet 0,
.call 11,
.unreachable
]
def func10Def : Wasm.Function :=
{ params := [.i32], locals := [], body := func10, results := [] }
def func11 : Wasm.Program :=
[
.localGet 0,
.load32 (0 : UInt32),
.localGet 0,
.load32 (4 : UInt32),
.const (0 : UInt32),
.load32 (1049320 : UInt32),
.localSet 0,
.localGet 0,
.const (1 : UInt32),
.localGet 0,
.select,
.callIndirect 0 0,
.unreachable
]
def func11Def : Wasm.Function :=
{ params := [.i32], locals := [], body := func11, results := [] }
def func12 : Wasm.Program :=
[
.localGet 0,
.call 13,
.unreachable
]
def func12Def : Wasm.Function :=
{ params := [.i32], locals := [], body := func12, results := [] }
def func13 : Wasm.Program :=
[
.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 (1048828 : UInt32),
.localGet 0,
.load32 (4 : UInt32),
.localGet 0,
.load32 (8 : UInt32),
.localSet 0,
.localGet 0,
.load8U (8 : UInt32),
.localGet 0,
.load8U (9 : UInt32),
.call 15,
.unreachable
],
.localGet 1,
.const (2147483648 : UInt32),
.store32 (0 : UInt32),
.localGet 1,
.localGet 0,
.store32 (12 : UInt32),
.localGet 1,
.const (1048856 : UInt32),
.localGet 0,
.load32 (4 : UInt32),
.localGet 0,
.load32 (8 : UInt32),
.localSet 0,
.localGet 0,
.load8U (8 : UInt32),
.localGet 0,
.load8U (9 : UInt32),
.call 15,
.unreachable
]
def func13Def : Wasm.Function :=
{ params := [.i32], locals := [.i32, .i32, .i32], body := func13, results := [] }
def func14 : 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 3,
.localSet 7,
.br 1
],
.block 0 0 [
.localGet 3,
.br_if 0,
.localGet 4,
.localSet 7,
.br 2
],
.call 4,
.localGet 3,
.localGet 4,
.call 1,
.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 func14Def : Wasm.Function :=
{ params := [.i32, .i32, .i32, .i32, .i32, .i32], locals := [.i32, .i32, .i64], body := func14, results := [] }
def func15 : 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 31,
.const (255 : UInt32),
.and,
.brTable [4, 1, 0] 1
],
.const (0 : UInt32),
.load32 (1049324 : UInt32),
.localSet 6,
.localGet 6,
.const (4294967295 : UInt32),
.leS,
.br_if 3,
.const (0 : UInt32),
.localGet 6,
.const (1 : UInt32),
.add,
.store32 (1049324 : UInt32),
.const (0 : UInt32),
.load32 (1049328 : 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 (1049328 : UInt32),
.localGet 5,
.const (16 : UInt32),
.add,
.const (0 : UInt32),
.load32 (1049332 : 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 7
],
.const (0 : UInt32),
.const (0 : UInt32),
.load32 (1049324 : UInt32),
.const (4294967295 : UInt32),
.add,
.store32 (1049324 : UInt32),
.const (0 : UInt32),
.const (0 : UInt32),
.store8 (1049316 : UInt32),
.localGet 3,
.eqz,
.br_if 0,
.localGet 0,
.localGet 1,
.call 17,
.unreachable
],
.unreachable
]
def func15Def : Wasm.Function :=
{ params := [.i32, .i32, .i32, .i32, .i32], locals := [.i32, .i32], body := func15, results := [] }
def func16 : Wasm.Program :=
[
.const (0 : UInt32),
.const (1 : UInt32),
.store8 (1049792 : UInt32)
]
def func16Def : Wasm.Function :=
{ params := [.i32, .i32], locals := [], body := func16, results := [] }
def func17 : Wasm.Program :=
[
.localGet 0,
.localGet 1,
.call 5,
.drop,
.unreachable
]
def func17Def : Wasm.Function :=
{ params := [.i32, .i32], locals := [], body := func17, results := [] }
def func18 : Wasm.Program :=
[
.block 0 0 [
.localGet 1,
.const (9 : UInt32),
.ltU,
.br_if 0,
.localGet 1,
.localGet 0,
.call 19,
.ret
],
.localGet 0,
.call 20
]
def func18Def : Wasm.Function :=
{ params := [.i32, .i32], locals := [], body := func18, results := [.i32] }
def func19 : 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 20,
.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 26,
.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 26
],
.localGet 0,
.const (8 : UInt32),
.add,
.localSet 2
],
.localGet 2
]
def func19Def : Wasm.Function :=
{ params := [.i32, .i32], locals := [.i32, .i32, .i32, .i32, .i32], body := func19, results := [.i32] }
def func20 : 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 (1049752 : 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 (1049748 : 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 (1049484 : UInt32),
.add,
.localSet 0,
.localGet 0,
.localGet 3,
.const (1049492 : 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 (1049756 : UInt32),
.leU,
.br_if 6,
.localGet 0,
.br_if 2,
.const (0 : UInt32),
.load32 (1049752 : UInt32),
.localSet 0,
.localGet 0,
.eqz,
.br_if 6,
.localGet 0,
.ctz,
.const (2 : UInt32),
.shl,
.const (1049340 : 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 (1049340 : 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 (1049748 : 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 (1049484 : UInt32),
.add,
.localSet 8,
.localGet 8,
.localGet 2,
.const (1049492 : 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 (1049748 : 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 (1049756 : UInt32),
.localSet 2,
.localGet 2,
.eqz,
.br_if 0,
.const (0 : UInt32),
.load32 (1049764 : UInt32),
.localSet 3,
.block 0 0 [
.block 0 0 [
.const (0 : UInt32),
.load32 (1049748 : 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 (1049748 : UInt32),
.localGet 2,
.const (4294967288 : UInt32),
.and,
.const (1049484 : UInt32),
.add,
.localSet 2,
.localGet 2,
.localSet 7,
.br 1
],
.localGet 2,
.const (4294967288 : UInt32),
.and,
.localSet 2,
.localGet 2,
.const (1049484 : UInt32),
.add,
.localSet 7,
.localGet 2,
.const (1049492 : 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 (1049764 : UInt32),
.const (0 : UInt32),
.localGet 8,
.store32 (1049756 : UInt32),
.br 4
],
.const (0 : UInt32),
.const (0 : UInt32),
.load32 (1049752 : UInt32),
.const (4294967294 : UInt32),
.localGet 6,
.load32 (28 : UInt32),
.rotl,
.and,
.store32 (1049752 : 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 (1049756 : UInt32),
.localSet 7,
.localGet 7,
.eqz,
.br_if 1,
.const (0 : UInt32),
.load32 (1049764 : UInt32),
.localSet 0,
.block 0 0 [
.block 0 0 [
.const (0 : UInt32),
.load32 (1049748 : 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 (1049748 : UInt32),
.localGet 7,
.const (4294967288 : UInt32),
.and,
.const (1049484 : UInt32),
.add,
.localSet 7,
.localGet 7,
.localSet 9,
.br 1
],
.localGet 7,
.const (4294967288 : UInt32),
.and,
.localSet 7,
.localGet 7,
.const (1049484 : UInt32),
.add,
.localSet 9,
.localGet 7,
.const (1049492 : 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 (1049764 : UInt32),
.const (0 : UInt32),
.localGet 2,
.store32 (1049756 : 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 (1049340 : 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 (1049340 : 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 (1049756 : 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 (1049340 : 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 (1049752 : UInt32),
.const (4294967294 : UInt32),
.localGet 8,
.load32 (28 : UInt32),
.rotl,
.and,
.store32 (1049752 : 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 30,
.br 2
],
.block 0 0 [
.block 0 0 [
.const (0 : UInt32),
.load32 (1049748 : 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 (1049748 : UInt32),
.localGet 2,
.const (248 : UInt32),
.and,
.const (1049484 : UInt32),
.add,
.localSet 2,
.localGet 2,
.localSet 6,
.br 1
],
.localGet 2,
.const (248 : UInt32),
.and,
.localSet 2,
.localGet 2,
.const (1049484 : UInt32),
.add,
.localSet 6,
.localGet 2,
.const (1049492 : 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 (1049756 : UInt32),
.localSet 0,
.localGet 0,
.localGet 3,
.geU,
.br_if 0,
.block 0 0 [
.const (0 : UInt32),
.load32 (1049760 : UInt32),
.localSet 0,
.localGet 0,
.localGet 3,
.gtU,
.br_if 0,
.localGet 1,
.const (4 : UInt32),
.add,
.const (1049792 : UInt32),
.localGet 3,
.const (65583 : UInt32),
.add,
.const (4294901760 : UInt32),
.and,
.call 45,
.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 (1049772 : UInt32),
.localGet 1,
.load32 (8 : UInt32),
.localSet 9,
.localGet 9,
.add,
.localSet 0,
.localGet 0,
.store32 (1049772 : UInt32),
.const (0 : UInt32),
.localGet 0,
.const (0 : UInt32),
.load32 (1049776 : UInt32),
.localSet 2,
.localGet 2,
.localGet 0,
.localGet 2,
.gtU,
.select,
.store32 (1049776 : UInt32),
.block 0 0 [
.block 0 0 [
.block 0 0 [
.const (0 : UInt32),
.load32 (1049768 : UInt32),
.localSet 2,
.localGet 2,
.eqz,
.br_if 0,
.const (1049468 : 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 (1049784 : UInt32),
.localSet 0,
.localGet 0,
.eqz,
.br_if 0,
.localGet 6,
.localGet 0,
.geU,
.br_if 1
],
.const (0 : UInt32),
.localGet 6,
.store32 (1049784 : UInt32)
],
.const (0 : UInt32),
.const (4095 : UInt32),
.store32 (1049788 : UInt32),
.const (0 : UInt32),
.localGet 5,
.store32 (1049480 : UInt32),
.const (0 : UInt32),
.localGet 9,
.store32 (1049472 : UInt32),
.const (0 : UInt32),
.localGet 6,
.store32 (1049468 : UInt32),
.const (0 : UInt32),
.const (1049484 : UInt32),
.store32 (1049496 : UInt32),
.const (0 : UInt32),
.const (1049492 : UInt32),
.store32 (1049504 : UInt32),
.const (0 : UInt32),
.const (1049484 : UInt32),
.store32 (1049492 : UInt32),
.const (0 : UInt32),
.const (1049500 : UInt32),
.store32 (1049512 : UInt32),
.const (0 : UInt32),
.const (1049492 : UInt32),
.store32 (1049500 : UInt32),
.const (0 : UInt32),
.const (1049508 : UInt32),
.store32 (1049520 : UInt32),
.const (0 : UInt32),
.const (1049500 : UInt32),
.store32 (1049508 : UInt32),
.const (0 : UInt32),
.const (1049516 : UInt32),
.store32 (1049528 : UInt32),
.const (0 : UInt32),
.const (1049508 : UInt32),
.store32 (1049516 : UInt32),
.const (0 : UInt32),
.const (1049524 : UInt32),
.store32 (1049536 : UInt32),
.const (0 : UInt32),
.const (1049516 : UInt32),
.store32 (1049524 : UInt32),
.const (0 : UInt32),
.const (1049532 : UInt32),
.store32 (1049544 : UInt32),
.const (0 : UInt32),
.const (1049524 : UInt32),
.store32 (1049532 : UInt32),
.const (0 : UInt32),
.const (1049540 : UInt32),
.store32 (1049552 : UInt32),
.const (0 : UInt32),
.const (1049532 : UInt32),
.store32 (1049540 : UInt32),
.const (0 : UInt32),
.const (1049548 : UInt32),
.store32 (1049560 : UInt32),
.const (0 : UInt32),
.const (1049540 : UInt32),
.store32 (1049548 : UInt32),
.const (0 : UInt32),
.const (1049548 : UInt32),
.store32 (1049556 : UInt32),
.const (0 : UInt32),
.const (1049556 : UInt32),
.store32 (1049568 : UInt32),
.const (0 : UInt32),
.const (1049556 : UInt32),
.store32 (1049564 : UInt32),
.const (0 : UInt32),
.const (1049564 : UInt32),
.store32 (1049576 : UInt32),
.const (0 : UInt32),
.const (1049564 : UInt32),
.store32 (1049572 : UInt32),
.const (0 : UInt32),
.const (1049572 : UInt32),
.store32 (1049584 : UInt32),
.const (0 : UInt32),
.const (1049572 : UInt32),
.store32 (1049580 : UInt32),
.const (0 : UInt32),
.const (1049580 : UInt32),
.store32 (1049592 : UInt32),
.const (0 : UInt32),
.const (1049580 : UInt32),
.store32 (1049588 : UInt32),
.const (0 : UInt32),
.const (1049588 : UInt32),
.store32 (1049600 : UInt32),
.const (0 : UInt32),
.const (1049588 : UInt32),
.store32 (1049596 : UInt32),
.const (0 : UInt32),
.const (1049596 : UInt32),
.store32 (1049608 : UInt32),
.const (0 : UInt32),
.const (1049596 : UInt32),
.store32 (1049604 : UInt32),
.const (0 : UInt32),
.const (1049604 : UInt32),
.store32 (1049616 : UInt32),
.const (0 : UInt32),
.const (1049604 : UInt32),
.store32 (1049612 : UInt32),
.const (0 : UInt32),
.const (1049612 : UInt32),
.store32 (1049624 : UInt32),
.const (0 : UInt32),
.const (1049620 : UInt32),
.store32 (1049632 : UInt32),
.const (0 : UInt32),
.const (1049612 : UInt32),
.store32 (1049620 : UInt32),
.const (0 : UInt32),
.const (1049628 : UInt32),
.store32 (1049640 : UInt32),
.const (0 : UInt32),
.const (1049620 : UInt32),
.store32 (1049628 : UInt32),
.const (0 : UInt32),
.const (1049636 : UInt32),
.store32 (1049648 : UInt32),
.const (0 : UInt32),
.const (1049628 : UInt32),
.store32 (1049636 : UInt32),
.const (0 : UInt32),
.const (1049644 : UInt32),
.store32 (1049656 : UInt32),
.const (0 : UInt32),
.const (1049636 : UInt32),
.store32 (1049644 : UInt32),
.const (0 : UInt32),
.const (1049652 : UInt32),
.store32 (1049664 : UInt32),
.const (0 : UInt32),
.const (1049644 : UInt32),
.store32 (1049652 : UInt32),
.const (0 : UInt32),
.const (1049660 : UInt32),
.store32 (1049672 : UInt32),
.const (0 : UInt32),
.const (1049652 : UInt32),
.store32 (1049660 : UInt32),
.const (0 : UInt32),
.const (1049668 : UInt32),
.store32 (1049680 : UInt32),
.const (0 : UInt32),
.const (1049660 : UInt32),
.store32 (1049668 : UInt32),
.const (0 : UInt32),
.const (1049676 : UInt32),
.store32 (1049688 : UInt32),
.const (0 : UInt32),
.const (1049668 : UInt32),
.store32 (1049676 : UInt32),
.const (0 : UInt32),
.const (1049684 : UInt32),
.store32 (1049696 : UInt32),
.const (0 : UInt32),
.const (1049676 : UInt32),
.store32 (1049684 : UInt32),
.const (0 : UInt32),
.const (1049692 : UInt32),
.store32 (1049704 : UInt32),
.const (0 : UInt32),
.const (1049684 : UInt32),
.store32 (1049692 : UInt32),
.const (0 : UInt32),
.const (1049700 : UInt32),
.store32 (1049712 : UInt32),
.const (0 : UInt32),
.const (1049692 : UInt32),
.store32 (1049700 : UInt32),
.const (0 : UInt32),
.const (1049708 : UInt32),
.store32 (1049720 : UInt32),
.const (0 : UInt32),
.const (1049700 : UInt32),
.store32 (1049708 : UInt32),
.const (0 : UInt32),
.const (1049716 : UInt32),
.store32 (1049728 : UInt32),
.const (0 : UInt32),
.const (1049708 : UInt32),
.store32 (1049716 : UInt32),
.const (0 : UInt32),
.const (1049724 : UInt32),
.store32 (1049736 : UInt32),
.const (0 : UInt32),
.const (1049716 : UInt32),
.store32 (1049724 : UInt32),
.const (0 : UInt32),
.const (1049732 : UInt32),
.store32 (1049744 : UInt32),
.const (0 : UInt32),
.const (1049724 : UInt32),
.store32 (1049732 : 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 (1049768 : UInt32),
.const (0 : UInt32),
.const (1049732 : UInt32),
.store32 (1049740 : 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 (1049760 : 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 (1049780 : 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 (1049784 : UInt32),
.localSet 0,
.localGet 0,
.localGet 6,
.localGet 0,
.localGet 6,
.ltU,
.select,
.store32 (1049784 : UInt32),
.localGet 6,
.localGet 9,
.add,
.localSet 8,
.const (1049468 : 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 (1049468 : 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 (1049768 : 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 (1049760 : 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 (1049780 : 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 (1049468 : UInt32),
.localSet 10,
.localGet 7,
.const (16 : UInt32),
.add,
.const (0 : UInt32),
.load64 (1049476 : 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 (1049480 : UInt32),
.const (0 : UInt32),
.localGet 9,
.store32 (1049472 : UInt32),
.const (0 : UInt32),
.localGet 6,
.store32 (1049468 : UInt32),
.const (0 : UInt32),
.localGet 0,
.store32 (1049476 : 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 30,
.br 8
],
.block 0 0 [
.block 0 0 [
.const (0 : UInt32),
.load32 (1049748 : 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 (1049748 : UInt32),
.localGet 0,
.const (248 : UInt32),
.and,
.const (1049484 : UInt32),
.add,
.localSet 0,
.localGet 0,
.localSet 8,
.br 1
],
.localGet 0,
.const (248 : UInt32),
.and,
.localSet 0,
.localGet 0,
.const (1049484 : UInt32),
.add,
.localSet 8,
.localGet 0,
.const (1049492 : 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 (1049768 : UInt32),
.eq,
.br_if 3,
.localGet 2,
.const (0 : UInt32),
.load32 (1049764 : 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 25,
.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 30,
.br 6
],
.block 0 0 [
.block 0 0 [
.const (0 : UInt32),
.load32 (1049748 : 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 (1049748 : UInt32),
.localGet 3,
.const (248 : UInt32),
.and,
.const (1049484 : UInt32),
.add,
.localSet 3,
.localGet 3,
.localSet 2,
.br 1
],
.localGet 3,
.const (248 : UInt32),
.and,
.localSet 3,
.localGet 3,
.const (1049484 : UInt32),
.add,
.localSet 2,
.localGet 3,
.const (1049492 : 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 (1049760 : UInt32),
.const (0 : UInt32),
.const (0 : UInt32),
.load32 (1049768 : UInt32),
.localSet 0,
.localGet 0,
.localGet 3,
.add,
.localSet 8,
.localGet 8,
.store32 (1049768 : 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 (1049764 : 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 (1049764 : UInt32),
.const (0 : UInt32),
.const (0 : UInt32),
.store32 (1049756 : 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 (1049756 : UInt32),
.const (0 : UInt32),
.localGet 2,
.localGet 3,
.add,
.localSet 6,
.localGet 6,
.store32 (1049764 : 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 (1049768 : 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 (1049768 : UInt32),
.const (0 : UInt32),
.localGet 0,
.localGet 2,
.sub,
.const (0 : UInt32),
.load32 (1049760 : UInt32),
.localGet 9,
.add,
.localSet 2,
.localGet 2,
.add,
.const (8 : UInt32),
.add,
.localSet 6,
.localGet 6,
.store32 (1049760 : 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 (1049780 : UInt32),
.br 3
],
.const (0 : UInt32),
.localGet 0,
.store32 (1049768 : UInt32),
.const (0 : UInt32),
.const (0 : UInt32),
.load32 (1049760 : UInt32),
.localGet 3,
.add,
.localSet 3,
.localGet 3,
.store32 (1049760 : UInt32),
.localGet 0,
.localGet 3,
.const (1 : UInt32),
.or,
.store32 (4 : UInt32),
.br 1
],
.const (0 : UInt32),
.localGet 0,
.store32 (1049764 : UInt32),
.const (0 : UInt32),
.const (0 : UInt32),
.load32 (1049756 : UInt32),
.localGet 3,
.add,
.localSet 3,
.localGet 3,
.store32 (1049756 : 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 (1049760 : UInt32),
.localSet 2,
.localGet 2,
.localGet 3,
.leU,
.br_if 0,
.const (0 : UInt32),
.localGet 2,
.localGet 3,
.sub,
.localSet 2,
.localGet 2,
.store32 (1049760 : UInt32),
.const (0 : UInt32),
.const (0 : UInt32),
.load32 (1049768 : UInt32),
.localSet 0,
.localGet 0,
.localGet 3,
.add,
.localSet 8,
.localGet 8,
.store32 (1049768 : 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 func20Def : Wasm.Function :=
{ params := [.i32], locals := [.i32, .i32, .i32, .i32, .i32, .i32, .i32, .i32, .i32, .i64], body := func20, results := [.i32] }
def func21 : Wasm.Program :=
[
.unreachable
]
def func21Def : Wasm.Function :=
{ params := [], locals := [], body := func21, results := [] }
def func22 : 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 23,
.ret
],
.const (1048916 : UInt32),
.const (46 : UInt32),
.const (1048964 : UInt32),
.call 49,
.unreachable
],
.const (1048980 : UInt32),
.const (46 : UInt32),
.const (1049028 : UInt32),
.call 49,
.unreachable
]
def func22Def : Wasm.Function :=
{ params := [.i32, .i32, .i32], locals := [.i32, .i32], body := func22, results := [] }
def func23 : 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 (1049764 : 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 (1049756 : 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 25
],
.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 (1049768 : UInt32),
.eq,
.br_if 2,
.localGet 3,
.const (0 : UInt32),
.load32 (1049764 : UInt32),
.eq,
.br_if 3,
.localGet 3,
.localGet 2,
.const (4294967288 : UInt32),
.and,
.localSet 2,
.localGet 2,
.call 25,
.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 (1049764 : UInt32),
.ne,
.br_if 1,
.const (0 : UInt32),
.localGet 0,
.store32 (1049756 : 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 30,
.const (0 : UInt32),
.const (0 : UInt32),
.load32 (1049788 : UInt32),
.const (4294967295 : UInt32),
.add,
.localSet 1,
.localGet 1,
.store32 (1049788 : UInt32),
.localGet 1,
.br_if 6,
.const (0 : UInt32),
.load32 (1049476 : UInt32),
.localSet 0,
.localGet 0,
.br_if 2,
.const (4095 : UInt32),
.localSet 1,
.br 3
],
.const (0 : UInt32),
.localGet 1,
.store32 (1049768 : UInt32),
.const (0 : UInt32),
.const (0 : UInt32),
.load32 (1049760 : UInt32),
.localGet 0,
.add,
.localSet 0,
.localGet 0,
.store32 (1049760 : UInt32),
.localGet 1,
.localGet 0,
.const (1 : UInt32),
.or,
.store32 (4 : UInt32),
.block 0 0 [
.localGet 1,
.const (0 : UInt32),
.load32 (1049764 : UInt32),
.ne,
.br_if 0,
.const (0 : UInt32),
.const (0 : UInt32),
.store32 (1049756 : UInt32),
.const (0 : UInt32),
.const (0 : UInt32),
.store32 (1049764 : UInt32)
],
.localGet 0,
.const (0 : UInt32),
.load32 (1049780 : UInt32),
.localSet 2,
.localGet 2,
.leU,
.br_if 5,
.const (0 : UInt32),
.load32 (1049768 : UInt32),
.localSet 0,
.localGet 0,
.eqz,
.br_if 5,
.const (0 : UInt32),
.load32 (1049760 : UInt32),
.localSet 4,
.localGet 4,
.const (41 : UInt32),
.ltU,
.br_if 4,
.const (1049468 : 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 (1049764 : UInt32),
.const (0 : UInt32),
.const (0 : UInt32),
.load32 (1049756 : UInt32),
.localGet 0,
.add,
.localSet 0,
.localGet 0,
.store32 (1049756 : 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 (1049788 : UInt32),
.ret
],
.block 0 0 [
.block 0 0 [
.const (0 : UInt32),
.load32 (1049748 : 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 (1049748 : UInt32),
.localGet 0,
.const (248 : UInt32),
.and,
.const (1049484 : UInt32),
.add,
.localSet 0,
.localGet 0,
.localSet 3,
.br 1
],
.localGet 0,
.const (248 : UInt32),
.and,
.localSet 0,
.localGet 0,
.const (1049484 : UInt32),
.add,
.localSet 3,
.localGet 0,
.const (1049492 : 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 (1049476 : 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 (1049788 : UInt32),
.localGet 4,
.localGet 2,
.leU,
.br_if 0,
.const (0 : UInt32),
.const (4294967295 : UInt32),
.store32 (1049780 : UInt32)
]
]
def func23Def : Wasm.Function :=
{ params := [.i32], locals := [.i32, .i32, .i32, .i32], body := func23, results := [] }
def func24 : 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 19,
.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 (1049768 : UInt32),
.eq,
.br_if 1,
.block 0 0 [
.localGet 7,
.const (0 : UInt32),
.load32 (1049764 : 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 25,
.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 26,
.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 (1049756 : 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 (1049764 : UInt32),
.const (0 : UInt32),
.localGet 6,
.store32 (1049756 : 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 26,
.br 6
],
.const (0 : UInt32),
.load32 (1049760 : 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 (1048980 : UInt32),
.const (46 : UInt32),
.const (1049028 : UInt32),
.call 49,
.unreachable
],
.const (1048916 : UInt32),
.const (46 : UInt32),
.const (1048964 : UInt32),
.call 49,
.unreachable
],
.const (1048980 : UInt32),
.const (46 : UInt32),
.const (1049028 : UInt32),
.call 49,
.unreachable
],
.const (1048916 : UInt32),
.const (46 : UInt32),
.const (1048964 : UInt32),
.call 49,
.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 (1049760 : UInt32),
.const (0 : UInt32),
.localGet 5,
.store32 (1049768 : UInt32)
],
.localGet 8,
.eqz,
.br_if 0,
.localGet 0,
.ret
],
.localGet 3,
.call 20,
.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 23
],
.localGet 2
]
def func24Def : Wasm.Function :=
{ params := [.i32, .i32, .i32, .i32], locals := [.i32, .i32, .i32, .i32, .i32, .i32], body := func24, results := [.i32] }
def func25 : 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 (1049340 : 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 (1049748 : UInt32),
.const (4294967294 : UInt32),
.localGet 1,
.const (3 : UInt32),
.shrU,
.rotl,
.and,
.store32 (1049748 : 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 (1049752 : UInt32),
.const (4294967294 : UInt32),
.localGet 0,
.load32 (28 : UInt32),
.rotl,
.and,
.store32 (1049752 : UInt32)
]
def func25Def : Wasm.Function :=
{ params := [.i32, .i32], locals := [.i32, .i32, .i32, .i32], body := func25, results := [] }
def func26 : 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 (1049764 : 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 (1049756 : 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 25
],
.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 (1049768 : UInt32),
.eq,
.br_if 2,
.localGet 2,
.const (0 : UInt32),
.load32 (1049764 : UInt32),
.eq,
.br_if 3,
.localGet 2,
.localGet 3,
.const (4294967288 : UInt32),
.and,
.localSet 3,
.localGet 3,
.call 25,
.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 (1049764 : UInt32),
.ne,
.br_if 1,
.const (0 : UInt32),
.localGet 1,
.store32 (1049756 : 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 30,
.ret
],
.block 0 0 [
.block 0 0 [
.const (0 : UInt32),
.load32 (1049748 : 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 (1049748 : UInt32),
.localGet 1,
.const (248 : UInt32),
.and,
.const (1049484 : UInt32),
.add,
.localSet 1,
.localGet 1,
.localSet 2,
.br 1
],
.localGet 1,
.const (248 : UInt32),
.and,
.localSet 1,
.localGet 1,
.const (1049484 : UInt32),
.add,
.localSet 2,
.localGet 1,
.const (1049492 : 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 (1049768 : UInt32),
.const (0 : UInt32),
.const (0 : UInt32),
.load32 (1049760 : UInt32),
.localGet 1,
.add,
.localSet 1,
.localGet 1,
.store32 (1049760 : UInt32),
.localGet 0,
.localGet 1,
.const (1 : UInt32),
.or,
.store32 (4 : UInt32),
.localGet 0,
.const (0 : UInt32),
.load32 (1049764 : UInt32),
.ne,
.br_if 1,
.const (0 : UInt32),
.const (0 : UInt32),
.store32 (1049756 : UInt32),
.const (0 : UInt32),
.const (0 : UInt32),
.store32 (1049764 : UInt32),
.ret
],
.const (0 : UInt32),
.localGet 0,
.store32 (1049764 : UInt32),
.const (0 : UInt32),
.const (0 : UInt32),
.load32 (1049756 : UInt32),
.localGet 1,
.add,
.localSet 1,
.localGet 1,
.store32 (1049756 : UInt32),
.localGet 0,
.localGet 1,
.const (1 : UInt32),
.or,
.store32 (4 : UInt32),
.localGet 0,
.localGet 1,
.add,
.localGet 1,
.store32 (0 : UInt32),
.ret
]
]
def func26Def : Wasm.Function :=
{ params := [.i32, .i32], locals := [.i32, .i32], body := func26, results := [] }
def func27 : 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 12,
.unreachable
]
def func27Def : Wasm.Function :=
{ params := [.i32], locals := [.i32, .i64], body := func27, results := [] }
def func28 : Wasm.Program :=
[
.localGet 1,
.localGet 0,
.call 29,
.unreachable
]
def func28Def : Wasm.Function :=
{ params := [.i32, .i32], locals := [], body := func28, results := [] }
def func29 : 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 10,
.unreachable
]
def func29Def : Wasm.Function :=
{ params := [.i32, .i32], locals := [.i32], body := func29, results := [] }
def func30 : 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 (1049340 : UInt32),
.add,
.localSet 3,
.block 0 0 [
.const (0 : UInt32),
.load32 (1049752 : 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 (1049752 : UInt32),
.localGet 4,
.or,
.store32 (1049752 : 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 func30Def : Wasm.Function :=
{ params := [.i32, .i32], locals := [.i32, .i32, .i32, .i32], body := func30, results := [] }
def func31 : Wasm.Program :=
[
.const (0 : UInt32),
.localSet 1,
.const (0 : UInt32),
.const (0 : UInt32),
.load32 (1049336 : UInt32),
.localSet 2,
.localGet 2,
.const (1 : UInt32),
.add,
.store32 (1049336 : UInt32),
.block 0 0 [
.localGet 2,
.const (0 : UInt32),
.ltS,
.br_if 0,
.const (1 : UInt32),
.localSet 1,
.const (0 : UInt32),
.load8U (1049316 : UInt32),
.br_if 0,
.const (0 : UInt32),
.localGet 0,
.store8 (1049316 : UInt32),
.const (0 : UInt32),
.const (0 : UInt32),
.load32 (1049312 : UInt32),
.const (1 : UInt32),
.add,
.store32 (1049312 : UInt32),
.const (2 : UInt32),
.localSet 1
],
.localGet 1
]
def func31Def : Wasm.Function :=
{ params := [.i32], locals := [.i32, .i32], body := func31, results := [.i32] }
def func32 : Wasm.Program :=
[
.localGet 0,
.const (0 : UInt32),
.load64 (1048908 : UInt32),
.store64 (8 : UInt32),
.localGet 0,
.const (0 : UInt32),
.load64 (1048900 : UInt32),
.store64 (0 : UInt32)
]
def func32Def : Wasm.Function :=
{ params := [.i32, .i32], locals := [], body := func32, results := [] }
def func33 : Wasm.Program :=
[
.localGet 0,
.const (0 : UInt32),
.load64 (1048892 : UInt32),
.store64 (8 : UInt32),
.localGet 0,
.const (0 : UInt32),
.load64 (1048884 : UInt32),
.store64 (0 : UInt32)
]
def func33Def : Wasm.Function :=
{ params := [.i32, .i32], locals := [], body := func33, results := [] }
def func34 : 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 56,
.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 51
]
def func34Def : Wasm.Function :=
{ params := [.i32, .i32], locals := [], body := func34, results := [.i32] }
def func35 : Wasm.Program :=
[
.localGet 0,
.const (1049044 : UInt32),
.store32 (4 : UInt32),
.localGet 0,
.localGet 1,
.store32 (0 : UInt32)
]
def func35Def : Wasm.Function :=
{ params := [.i32, .i32], locals := [], body := func35, results := [] }
def func36 : Wasm.Program :=
[
.localGet 0,
.localGet 1,
.load64 (0 : UInt32),
.store64 (0 : UInt32)
]
def func36Def : Wasm.Function :=
{ params := [.i32, .i32], locals := [], body := func36, results := [] }
def func37 : Wasm.Program :=
[
.localGet 1,
.load32 (4 : UInt32),
.localSet 2,
.localGet 1,
.load32 (0 : UInt32),
.localSet 3,
.call 4,
.block 0 0 [
.const (8 : UInt32),
.const (4 : UInt32),
.call 1,
.localSet 1,
.localGet 1,
.br_if 0,
.const (4 : UInt32),
.const (8 : UInt32),
.call 47,
.unreachable
],
.localGet 1,
.localGet 2,
.store32 (4 : UInt32),
.localGet 1,
.localGet 3,
.store32 (0 : UInt32),
.localGet 0,
.const (1049044 : UInt32),
.store32 (4 : UInt32),
.localGet 0,
.localGet 1,
.store32 (0 : UInt32)
]
def func37Def : Wasm.Function :=
{ params := [.i32, .i32], locals := [.i32, .i32], body := func37, results := [] }
def func38 : Wasm.Program :=
[
.localGet 1,
.localGet 0,
.load32 (0 : UInt32),
.localGet 0,
.load32 (4 : UInt32),
.call 56
]
def func38Def : Wasm.Function :=
{ params := [.i32, .i32], locals := [], body := func38, results := [.i32] }
def func39 : 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 6,
.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 func39Def : Wasm.Function :=
{ params := [.i32, .i32], locals := [.i32, .i32, .i32, .i32, .i32, .i32], body := func39, results := [.i32] }
def func40 : 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 6,
.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 func40Def : Wasm.Function :=
{ params := [.i32, .i32, .i32], locals := [.i32], body := func40, results := [.i32] }
def func41 : 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 (1048804 : UInt32),
.localGet 3,
.load32 (0 : UInt32),
.localSet 3,
.localGet 3,
.load32 (0 : UInt32),
.localGet 3,
.load32 (4 : UInt32),
.call 51,
.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 (1049060 : UInt32),
.store32 (4 : UInt32),
.localGet 0,
.localGet 1,
.store32 (0 : UInt32),
.localGet 2,
.const (32 : UInt32),
.add,
.globalSet 0
]
def func41Def : Wasm.Function :=
{ params := [.i32, .i32], locals := [.i32, .i32, .i64], body := func41, results := [] }
def func42 : 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 (1048804 : UInt32),
.localGet 3,
.load32 (0 : UInt32),
.localSet 3,
.localGet 3,
.load32 (0 : UInt32),
.localGet 3,
.load32 (4 : UInt32),
.call 51,
.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 4,
.block 0 0 [
.const (12 : UInt32),
.const (4 : UInt32),
.call 1,
.localSet 1,
.localGet 1,
.br_if 0,
.const (4 : UInt32),
.const (12 : UInt32),
.call 47,
.unreachable
],
.localGet 1,
.localGet 2,
.load32 (16 : UInt32),
.store32 (8 : UInt32),
.localGet 1,
.localGet 2,
.load64 (8 : UInt32),
.store64 (0 : UInt32),
.localGet 0,
.const (1049060 : UInt32),
.store32 (4 : UInt32),
.localGet 0,
.localGet 1,
.store32 (0 : UInt32),
.localGet 2,
.const (48 : UInt32),
.add,
.globalSet 0
]
def func42Def : Wasm.Function :=
{ params := [.i32, .i32], locals := [.i32, .i32, .i64], body := func42, results := [] }
def func43 : Wasm.Program :=
[
.localGet 0,
.const (0 : UInt32),
.store32 (0 : UInt32)
]
def func43Def : Wasm.Function :=
{ params := [.i32, .i32], locals := [], body := func43, results := [] }
def func44 : Wasm.Program :=
[
.localGet 0,
.const (1048804 : UInt32),
.localGet 1,
.localGet 2,
.call 51
]
def func44Def : Wasm.Function :=
{ params := [.i32, .i32, .i32], locals := [], body := func44, results := [.i32] }
def func45 : 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 func45Def : Wasm.Function :=
{ params := [.i32, .i32, .i32], locals := [.i32, .i32], body := func45, results := [] }
def func46 : Wasm.Program :=
[
.block 0 0 [
.localGet 0,
.eqz,
.br_if 0,
.localGet 0,
.localGet 1,
.call 47,
.unreachable
],
.call 48,
.unreachable
]
def func46Def : Wasm.Function :=
{ params := [.i32, .i32], locals := [], body := func46, results := [] }
def func47 : Wasm.Program :=
[
.localGet 1,
.localGet 0,
.call 28,
.unreachable
]
def func47Def : Wasm.Function :=
{ params := [.i32, .i32], locals := [], body := func47, results := [] }
def func48 : Wasm.Program :=
[
.const (1049076 : UInt32),
.const (35 : UInt32),
.const (1049096 : UInt32),
.call 50,
.unreachable
]
def func48Def : Wasm.Function :=
{ params := [], locals := [], body := func48, results := [] }
def func49 : Wasm.Program :=
[
.localGet 0,
.localGet 1,
.const (1 : UInt32),
.shl,
.const (1 : UInt32),
.or,
.localGet 2,
.call 50,
.unreachable
]
def func49Def : Wasm.Function :=
{ params := [.i32, .i32, .i32], locals := [], body := func49, results := [] }
def func50 : 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 27,
.unreachable
]
def func50Def : Wasm.Function :=
{ params := [.i32, .i32, .i32], locals := [.i32], body := func50, results := [] }
def func51 : 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 func51Def : Wasm.Function :=
{ params := [.i32, .i32, .i32, .i32], locals := [.i32, .i32, .i32, .i32, .i32, .i32, .i32, .i32], body := func51, results := [.i32] }
def func52 : Wasm.Program :=
[
.globalGet 0,
.const (32 : UInt32),
.sub,
.localSet 3,
.localGet 3,
.globalSet 0,
.localGet 3,
.localGet 1,
.store32 (12 : UInt32),
.localGet 3,
.localGet 0,
.store32 (8 : UInt32),
.localGet 3,
.const (17 : UInt32),
.extendUI32,
.constI64 (32 : UInt64),
.shlI64,
.localSet 4,
.localGet 4,
.localGet 3,
.const (8 : UInt32),
.add,
.extendUI32,
.orI64,
.store64 (24 : UInt32),
.localGet 3,
.localGet 4,
.localGet 3,
.const (12 : UInt32),
.add,
.extendUI32,
.orI64,
.store64 (16 : UInt32),
.const (1048576 : UInt32),
.localGet 3,
.const (16 : UInt32),
.add,
.localGet 2,
.call 50,
.unreachable
]
def func52Def : Wasm.Function :=
{ params := [.i32, .i32, .i32], locals := [.i32, .i64], body := func52, results := [] }
def func53 : Wasm.Program :=
[
.const (43 : UInt32),
.const (1114112 : UInt32),
.localGet 0,
.load32 (8 : UInt32),
.localSet 6,
.localGet 6,
.const (2097152 : UInt32),
.and,
.localSet 7,
.localGet 7,
.select,
.localSet 8,
.localGet 7,
.const (21 : UInt32),
.shrU,
.const (1 : UInt32),
.localGet 1,
.select,
.localGet 5,
.add,
.localSet 9,
.block 0 0 [
.block 0 0 [
.localGet 6,
.const (8388608 : UInt32),
.and,
.br_if 0,
.const (0 : UInt32),
.localSet 2,
.br 1
],
.block 0 0 [
.block 0 0 [
.localGet 3,
.const (16 : UInt32),
.ltU,
.br_if 0,
.localGet 2,
.localGet 3,
.call 54,
.localSet 7,
.br 1
],
.block 0 0 [
.localGet 3,
.br_if 0,
.const (0 : UInt32),
.localSet 7,
.br 1
],
.localGet 3,
.const (3 : UInt32),
.and,
.localSet 10,
.const (0 : UInt32),
.localSet 11,
.const (0 : UInt32),
.localSet 7,
.block 0 0 [
.localGet 3,
.const (4 : UInt32),
.ltU,
.br_if 0,
.localGet 3,
.const (12 : UInt32),
.and,
.localSet 12,
.const (0 : UInt32),
.localSet 11,
.const (0 : UInt32),
.localSet 7,
.loop 0 0 [
.localGet 7,
.localGet 2,
.localGet 11,
.add,
.localSet 13,
.localGet 13,
.load8S (0 : UInt32),
.const (4294967231 : UInt32),
.gtS,
.add,
.localGet 13,
.const (1 : UInt32),
.add,
.load8S (0 : UInt32),
.const (4294967231 : UInt32),
.gtS,
.add,
.localGet 13,
.const (2 : UInt32),
.add,
.load8S (0 : UInt32),
.const (4294967231 : UInt32),
.gtS,
.add,
.localGet 13,
.const (3 : UInt32),
.add,
.load8S (0 : UInt32),
.const (4294967231 : UInt32),
.gtS,
.add,
.localSet 7,
.localGet 12,
.localGet 11,
.const (4 : UInt32),
.add,
.localSet 11,
.localGet 11,
.ne,
.br_if 0
],
.localGet 10,
.eqz,
.br_if 1
],
.localGet 2,
.localGet 11,
.add,
.localSet 13,
.loop 0 0 [
.localGet 7,
.localGet 13,
.load8S (0 : UInt32),
.const (4294967231 : UInt32),
.gtS,
.add,
.localSet 7,
.localGet 13,
.const (1 : UInt32),
.add,
.localSet 13,
.localGet 10,
.const (4294967295 : UInt32),
.add,
.localSet 10,
.localGet 10,
.br_if 0
]
],
.localGet 7,
.localGet 9,
.add,
.localSet 9
],
.localGet 8,
.const (45 : UInt32),
.localGet 1,
.select,
.localSet 12,
.block 0 0 [
.block 0 0 [
.localGet 9,
.localGet 0,
.load16U (12 : UInt32),
.localSet 1,
.localGet 1,
.geU,
.br_if 0,
.block 0 0 [
.block 0 0 [
.block 0 0 [
.localGet 6,
.const (16777216 : UInt32),
.and,
.br_if 0,
.localGet 1,
.localGet 9,
.sub,
.localSet 8,
.const (0 : UInt32),
.localSet 7,
.const (0 : UInt32),
.localSet 1,
.block 0 0 [
.block 0 0 [
.block 0 0 [
.localGet 6,
.const (29 : UInt32),
.shrU,
.const (3 : UInt32),
.and,
.brTable [2, 0, 1, 0] 2
],
.localGet 8,
.localSet 1,
.br 1
],
.localGet 8,
.const (65534 : UInt32),
.and,
.const (1 : UInt32),
.shrU,
.localSet 1
],
.localGet 6,
.const (2097151 : UInt32),
.and,
.localSet 9,
.localGet 0,
.load32 (4 : UInt32),
.localSet 11,
.localGet 0,
.load32 (0 : UInt32),
.localSet 10,
.loop 0 0 [
.localGet 7,
.const (65535 : UInt32),
.and,
.localGet 1,
.const (65535 : UInt32),
.and,
.geU,
.br_if 2,
.const (1 : UInt32),
.localSet 13,
.localGet 7,
.const (1 : UInt32),
.add,
.localSet 7,
.localGet 10,
.localGet 9,
.localGet 11,
.load32 (16 : UInt32),
.callIndirect 2 0,
.eqz,
.br_if 0,
.br 5
]
],
.localGet 0,
.localGet 0,
.load64 (8 : UInt32),
.localSet 14,
.localGet 14,
.wrapI64,
.const (2682257408 : UInt32),
.and,
.const (536870960 : UInt32),
.or,
.store32 (8 : UInt32),
.const (1 : UInt32),
.localSet 13,
.localGet 0,
.load32 (0 : UInt32),
.localSet 10,
.localGet 10,
.localGet 0,
.load32 (4 : UInt32),
.localSet 11,
.localGet 11,
.localGet 12,
.localGet 2,
.localGet 3,
.call 55,
.br_if 3,
.const (0 : UInt32),
.localSet 7,
.localGet 1,
.localGet 9,
.sub,
.const (65535 : UInt32),
.and,
.localSet 2,
.loop 0 0 [
.localGet 7,
.const (65535 : UInt32),
.and,
.localGet 2,
.geU,
.br_if 2,
.const (1 : UInt32),
.localSet 13,
.localGet 7,
.const (1 : UInt32),
.add,
.localSet 7,
.localGet 10,
.const (48 : UInt32),
.localGet 11,
.load32 (16 : UInt32),
.callIndirect 2 0,
.eqz,
.br_if 0,
.br 4
]
],
.const (1 : UInt32),
.localSet 13,
.localGet 10,
.localGet 11,
.localGet 12,
.localGet 2,
.localGet 3,
.call 55,
.br_if 2,
.localGet 10,
.localGet 4,
.localGet 5,
.localGet 11,
.load32 (12 : UInt32),
.callIndirect 1 0,
.br_if 2,
.const (0 : UInt32),
.localSet 7,
.localGet 8,
.localGet 1,
.sub,
.const (65535 : UInt32),
.and,
.localSet 0,
.loop 0 0 [
.localGet 7,
.const (65535 : UInt32),
.and,
.localSet 2,
.localGet 2,
.localGet 0,
.ltU,
.localSet 13,
.localGet 2,
.localGet 0,
.geU,
.br_if 3,
.localGet 7,
.const (1 : UInt32),
.add,
.localSet 7,
.localGet 10,
.localGet 9,
.localGet 11,
.load32 (16 : UInt32),
.callIndirect 2 0,
.eqz,
.br_if 0,
.br 3
]
],
.const (1 : UInt32),
.localSet 13,
.localGet 10,
.localGet 4,
.localGet 5,
.localGet 11,
.load32 (12 : UInt32),
.callIndirect 1 0,
.br_if 1,
.localGet 0,
.localGet 14,
.store64 (8 : UInt32),
.const (0 : UInt32),
.ret
],
.const (1 : UInt32),
.localSet 13,
.localGet 0,
.load32 (0 : UInt32),
.localSet 7,
.localGet 7,
.localGet 0,
.load32 (4 : UInt32),
.localSet 10,
.localGet 10,
.localGet 12,
.localGet 2,
.localGet 3,
.call 55,
.br_if 0,
.localGet 7,
.localGet 4,
.localGet 5,
.localGet 10,
.load32 (12 : UInt32),
.callIndirect 1 0,
.localSet 13
],
.localGet 13
]
def func53Def : Wasm.Function :=
{ params := [.i32, .i32, .i32, .i32, .i32, .i32], locals := [.i32, .i32, .i32, .i32, .i32, .i32, .i32, .i32, .i64], body := func53, results := [.i32] }
def func54 : Wasm.Program :=
[
.block 0 0 [
.block 0 0 [
.localGet 1,
.localGet 0,
.const (3 : UInt32),
.add,
.const (4294967292 : UInt32),
.and,
.localSet 2,
.localGet 2,
.localGet 0,
.sub,
.localSet 3,
.localGet 3,
.ltU,
.br_if 0,
.localGet 1,
.localGet 3,
.sub,
.localSet 4,
.localGet 4,
.const (2 : UInt32),
.shrU,
.localSet 5,
.localGet 5,
.eqz,
.br_if 0,
.localGet 4,
.const (3 : UInt32),
.and,
.localSet 6,
.const (0 : UInt32),
.localSet 7,
.const (0 : UInt32),
.localSet 1,
.block 0 0 [
.localGet 2,
.localGet 0,
.eq,
.br_if 0,
.const (0 : UInt32),
.localSet 8,
.const (0 : UInt32),
.localSet 1,
.block 0 0 [
.localGet 0,
.localGet 2,
.sub,
.localSet 9,
.localGet 9,
.const (4294967292 : UInt32),
.gtU,
.br_if 0,
.const (0 : UInt32),
.localSet 8,
.const (0 : UInt32),
.localSet 1,
.loop 0 0 [
.localGet 1,
.localGet 0,
.localGet 8,
.add,
.localSet 2,
.localGet 2,
.load8S (0 : UInt32),
.const (4294967231 : UInt32),
.gtS,
.add,
.localGet 2,
.const (1 : UInt32),
.add,
.load8S (0 : UInt32),
.const (4294967231 : UInt32),
.gtS,
.add,
.localGet 2,
.const (2 : UInt32),
.add,
.load8S (0 : UInt32),
.const (4294967231 : UInt32),
.gtS,
.add,
.localGet 2,
.const (3 : UInt32),
.add,
.load8S (0 : UInt32),
.const (4294967231 : UInt32),
.gtS,
.add,
.localSet 1,
.localGet 8,
.const (4 : UInt32),
.add,
.localSet 8,
.localGet 8,
.br_if 0
]
],
.localGet 0,
.localGet 8,
.add,
.localSet 2,
.loop 0 0 [
.localGet 1,
.localGet 2,
.load8S (0 : UInt32),
.const (4294967231 : UInt32),
.gtS,
.add,
.localSet 1,
.localGet 2,
.const (1 : UInt32),
.add,
.localSet 2,
.localGet 9,
.const (1 : UInt32),
.add,
.localSet 9,
.localGet 9,
.br_if 0
]
],
.localGet 0,
.localGet 3,
.add,
.localSet 9,
.block 0 0 [
.localGet 6,
.eqz,
.br_if 0,
.localGet 9,
.localGet 4,
.const (2147483644 : UInt32),
.and,
.add,
.localSet 2,
.localGet 2,
.load8S (0 : UInt32),
.const (4294967231 : UInt32),
.gtS,
.localSet 7,
.localGet 6,
.const (1 : UInt32),
.eq,
.br_if 0,
.localGet 7,
.localGet 2,
.load8S (1 : UInt32),
.const (4294967231 : UInt32),
.gtS,
.add,
.localSet 7,
.localGet 6,
.const (2 : UInt32),
.eq,
.br_if 0,
.localGet 7,
.localGet 2,
.load8S (2 : UInt32),
.const (4294967231 : UInt32),
.gtS,
.add,
.localSet 7
],
.localGet 7,
.localGet 1,
.add,
.localSet 8,
.loop 0 0 [
.localGet 9,
.localSet 3,
.localGet 5,
.eqz,
.br_if 2,
.localGet 5,
.const (192 : UInt32),
.localGet 5,
.const (192 : UInt32),
.ltU,
.select,
.localSet 7,
.localGet 7,
.const (3 : UInt32),
.and,
.localSet 6,
.block 0 0 [
.block 0 0 [
.localGet 7,
.const (2 : UInt32),
.shl,
.localSet 4,
.localGet 4,
.const (1008 : UInt32),
.and,
.localSet 1,
.localGet 1,
.br_if 0,
.const (0 : UInt32),
.localSet 2,
.br 1
],
.localGet 3,
.localGet 1,
.add,
.localSet 0,
.const (0 : UInt32),
.localSet 2,
.localGet 3,
.localSet 1,
.loop 0 0 [
.localGet 1,
.const (12 : UInt32),
.add,
.load32 (0 : UInt32),
.localSet 9,
.localGet 9,
.const (4294967295 : UInt32),
.xor,
.const (7 : UInt32),
.shrU,
.localGet 9,
.const (6 : UInt32),
.shrU,
.or,
.const (16843009 : UInt32),
.and,
.localGet 1,
.const (8 : UInt32),
.add,
.load32 (0 : UInt32),
.localSet 9,
.localGet 9,
.const (4294967295 : UInt32),
.xor,
.const (7 : UInt32),
.shrU,
.localGet 9,
.const (6 : UInt32),
.shrU,
.or,
.const (16843009 : UInt32),
.and,
.localGet 1,
.const (4 : UInt32),
.add,
.load32 (0 : UInt32),
.localSet 9,
.localGet 9,
.const (4294967295 : UInt32),
.xor,
.const (7 : UInt32),
.shrU,
.localGet 9,
.const (6 : UInt32),
.shrU,
.or,
.const (16843009 : UInt32),
.and,
.localGet 1,
.load32 (0 : UInt32),
.localSet 9,
.localGet 9,
.const (4294967295 : UInt32),
.xor,
.const (7 : UInt32),
.shrU,
.localGet 9,
.const (6 : UInt32),
.shrU,
.or,
.const (16843009 : UInt32),
.and,
.localGet 2,
.add,
.add,
.add,
.add,
.localSet 2,
.localGet 1,
.const (16 : UInt32),
.add,
.localSet 1,
.localGet 1,
.localGet 0,
.ne,
.br_if 0
]
],
.localGet 5,
.localGet 7,
.sub,
.localSet 5,
.localGet 3,
.localGet 4,
.add,
.localSet 9,
.localGet 2,
.const (8 : UInt32),
.shrU,
.const (16711935 : UInt32),
.and,
.localGet 2,
.const (16711935 : UInt32),
.and,
.add,
.const (65537 : UInt32),
.mul,
.const (16 : UInt32),
.shrU,
.localGet 8,
.add,
.localSet 8,
.localGet 6,
.eqz,
.br_if 0
],
.localGet 3,
.localGet 7,
.const (252 : UInt32),
.and,
.const (2 : UInt32),
.shl,
.add,
.localSet 2,
.localGet 2,
.load32 (0 : UInt32),
.localSet 1,
.localGet 1,
.const (4294967295 : UInt32),
.xor,
.const (7 : UInt32),
.shrU,
.localGet 1,
.const (6 : UInt32),
.shrU,
.or,
.const (16843009 : UInt32),
.and,
.localSet 1,
.block 0 0 [
.localGet 6,
.const (1 : UInt32),
.eq,
.br_if 0,
.localGet 2,
.load32 (4 : UInt32),
.localSet 9,
.localGet 9,
.const (4294967295 : UInt32),
.xor,
.const (7 : UInt32),
.shrU,
.localGet 9,
.const (6 : UInt32),
.shrU,
.or,
.const (16843009 : UInt32),
.and,
.localGet 1,
.add,
.localSet 1,
.localGet 6,
.const (2 : UInt32),
.eq,
.br_if 0,
.localGet 2,
.load32 (8 : UInt32),
.localSet 2,
.localGet 2,
.const (4294967295 : UInt32),
.xor,
.const (7 : UInt32),
.shrU,
.localGet 2,
.const (6 : UInt32),
.shrU,
.or,
.const (16843009 : UInt32),
.and,
.localGet 1,
.add,
.localSet 1
],
.localGet 1,
.const (8 : UInt32),
.shrU,
.const (459007 : UInt32),
.and,
.localGet 1,
.const (16711935 : UInt32),
.and,
.add,
.const (65537 : UInt32),
.mul,
.const (16 : UInt32),
.shrU,
.localGet 8,
.add,
.localSet 8,
.br 1
],
.block 0 0 [
.localGet 1,
.br_if 0,
.const (0 : UInt32),
.ret
],
.localGet 1,
.const (3 : UInt32),
.and,
.localSet 2,
.const (0 : UInt32),
.localSet 9,
.const (0 : UInt32),
.localSet 8,
.block 0 0 [
.localGet 1,
.const (4 : UInt32),
.ltU,
.br_if 0,
.localGet 1,
.const (4294967292 : UInt32),
.and,
.localSet 5,
.const (0 : UInt32),
.localSet 8,
.const (0 : UInt32),
.localSet 9,
.loop 0 0 [
.localGet 8,
.localGet 0,
.localGet 9,
.add,
.localSet 1,
.localGet 1,
.load8S (0 : UInt32),
.const (4294967231 : UInt32),
.gtS,
.add,
.localGet 1,
.const (1 : UInt32),
.add,
.load8S (0 : UInt32),
.const (4294967231 : UInt32),
.gtS,
.add,
.localGet 1,
.const (2 : UInt32),
.add,
.load8S (0 : UInt32),
.const (4294967231 : UInt32),
.gtS,
.add,
.localGet 1,
.const (3 : UInt32),
.add,
.load8S (0 : UInt32),
.const (4294967231 : UInt32),
.gtS,
.add,
.localSet 8,
.localGet 5,
.localGet 9,
.const (4 : UInt32),
.add,
.localSet 9,
.localGet 9,
.ne,
.br_if 0
],
.localGet 2,
.eqz,
.br_if 1
],
.localGet 0,
.localGet 9,
.add,
.localSet 1,
.loop 0 0 [
.localGet 8,
.localGet 1,
.load8S (0 : UInt32),
.const (4294967231 : UInt32),
.gtS,
.add,
.localSet 8,
.localGet 1,
.const (1 : UInt32),
.add,
.localSet 1,
.localGet 2,
.const (4294967295 : UInt32),
.add,
.localSet 2,
.localGet 2,
.br_if 0
]
],
.localGet 8
]
def func54Def : Wasm.Function :=
{ params := [.i32, .i32], locals := [.i32, .i32, .i32, .i32, .i32, .i32, .i32, .i32], body := func54, results := [.i32] }
def func55 : Wasm.Program :=
[
.block 0 0 [
.localGet 2,
.const (1114112 : UInt32),
.eq,
.br_if 0,
.localGet 0,
.localGet 2,
.localGet 1,
.load32 (16 : UInt32),
.callIndirect 2 0,
.eqz,
.br_if 0,
.const (1 : UInt32),
.ret
],
.block 0 0 [
.localGet 3,
.br_if 0,
.const (0 : UInt32),
.ret
],
.localGet 0,
.localGet 3,
.localGet 4,
.localGet 1,
.load32 (12 : UInt32),
.callIndirect 1 0
]
def func55Def : Wasm.Function :=
{ params := [.i32, .i32, .i32, .i32, .i32], locals := [], body := func55, results := [.i32] }
def func56 : Wasm.Program :=
[
.localGet 0,
.load32 (0 : UInt32),
.localGet 1,
.localGet 2,
.localGet 0,
.load32 (4 : UInt32),
.load32 (12 : UInt32),
.callIndirect 1 0
]
def func56Def : Wasm.Function :=
{ params := [.i32, .i32, .i32], locals := [], body := func56, results := [.i32] }
def func57 : Wasm.Program :=
[
.globalGet 0,
.const (16 : UInt32),
.sub,
.localSet 2,
.localGet 2,
.globalSet 0,
.const (10 : UInt32),
.localSet 3,
.localGet 0,
.load32 (0 : UInt32),
.localSet 4,
.localGet 4,
.localSet 5,
.block 0 0 [
.localGet 4,
.const (1000 : UInt32),
.ltU,
.br_if 0,
.const (10 : UInt32),
.localSet 3,
.localGet 4,
.localSet 5,
.loop 0 0 [
.localGet 2,
.const (6 : UInt32),
.add,
.localGet 3,
.add,
.localSet 6,
.localGet 6,
.const (4294967292 : UInt32),
.add,
.localGet 5,
.localSet 0,
.localGet 0,
.localGet 0,
.const (10000 : UInt32),
.divU,
.localSet 5,
.localGet 5,
.const (10000 : UInt32),
.mul,
.sub,
.localSet 7,
.localGet 7,
.const (65535 : UInt32),
.and,
.const (100 : UInt32),
.divU,
.localSet 8,
.localGet 8,
.const (1 : UInt32),
.shl,
.load16U (1049112 : UInt32),
.store16 (0 : UInt32),
.localGet 6,
.const (4294967294 : UInt32),
.add,
.localGet 7,
.localGet 8,
.const (100 : UInt32),
.mul,
.sub,
.const (65535 : UInt32),
.and,
.const (1 : UInt32),
.shl,
.load16U (1049112 : UInt32),
.store16 (0 : UInt32),
.localGet 3,
.const (4294967292 : UInt32),
.add,
.localSet 3,
.localGet 0,
.const (9999999 : UInt32),
.gtU,
.br_if 0
]
],
.block 0 0 [
.block 0 0 [
.localGet 5,
.const (9 : UInt32),
.gtU,
.br_if 0,
.localGet 5,
.localSet 0,
.br 1
],
.localGet 2,
.const (6 : UInt32),
.add,
.localGet 3,
.const (4294967294 : UInt32),
.add,
.localSet 3,
.localGet 3,
.add,
.localGet 5,
.localGet 5,
.const (65535 : UInt32),
.and,
.const (100 : UInt32),
.divU,
.localSet 0,
.localGet 0,
.const (100 : UInt32),
.mul,
.sub,
.const (65535 : UInt32),
.and,
.const (1 : UInt32),
.shl,
.load16U (1049112 : UInt32),
.store16 (0 : UInt32)
],
.block 0 0 [
.block 0 0 [
.localGet 4,
.eqz,
.br_if 0,
.localGet 0,
.eqz,
.br_if 1
],
.localGet 2,
.const (6 : UInt32),
.add,
.localGet 3,
.const (4294967295 : UInt32),
.add,
.localSet 3,
.localGet 3,
.add,
.localGet 0,
.const (1 : UInt32),
.shl,
.load8U (1049113 : UInt32),
.store8 (0 : UInt32)
],
.localGet 1,
.const (1 : UInt32),
.const (1 : UInt32),
.const (0 : UInt32),
.localGet 2,
.const (6 : UInt32),
.add,
.localGet 3,
.add,
.const (10 : UInt32),
.localGet 3,
.sub,
.call 53,
.localSet 3,
.localGet 2,
.const (16 : UInt32),
.add,
.globalSet 0,
.localGet 3
]
def func57Def : Wasm.Function :=
{ params := [.i32, .i32], locals := [.i32, .i32, .i32, .i32, .i32, .i32, .i32], body := func57, results := [.i32] }
def «module» : Wasm.Module :=
{
imports := [],
funcs := [
func0Def,
func1Def,
func2Def,
func3Def,
func4Def,
func5Def,
func6Def,
func7Def,
func8Def,
func9Def,
func10Def,
func11Def,
func12Def,
func13Def,
func14Def,
func15Def,
func16Def,
func17Def,
func18Def,
func19Def,
func20Def,
func21Def,
func22Def,
func23Def,
func24Def,
func25Def,
func26Def,
func27Def,
func28Def,
func29Def,
func30Def,
func31Def,
func32Def,
func33Def,
func34Def,
func35Def,
func36Def,
func37Def,
func38Def,
func39Def,
func40Def,
func41Def,
func42Def,
func43Def,
func44Def,
func45Def,
func46Def,
func47Def,
func48Def,
func49Def,
func50Def,
func51Def,
func52Def,
func53Def,
func54Def,
func55Def,
func56Def,
func57Def
],
exports := [
{ name := "swap_elements", funcIdx := 0 }
],
memory := some { pagesMin := (17 : UInt32), pagesMax := none, data := [
{ offset := some (1048576 : UInt32), bytes := [(32 : UInt8), (105 : UInt8), (110 : UInt8), (100 : UInt8), (101 : UInt8), (120 : UInt8), (32 : UInt8), (111 : UInt8), (117 : UInt8), (116 : UInt8), (32 : UInt8), (111 : UInt8), (102 : UInt8), (32 : UInt8), (98 : UInt8), (111 : UInt8), (117 : UInt8), (110 : UInt8), (100 : UInt8), (115 : UInt8), (58 : UInt8), (32 : UInt8), (116 : UInt8), (104 : UInt8), (101 : UInt8), (32 : UInt8), (108 : UInt8), (101 : UInt8), (110 : UInt8), (32 : UInt8), (105 : UInt8), (115 : UInt8), (32 : UInt8), (192 : UInt8), (18 : UInt8), (32 : UInt8), (98 : UInt8), (117 : UInt8), (116 : UInt8), (32 : UInt8), (116 : UInt8), (104 : UInt8), (101 : UInt8), (32 : UInt8), (105 : UInt8), (110 : UInt8), (100 : UInt8), (101 : UInt8), (120 : UInt8), (32 : UInt8), (105 : UInt8), (115 : UInt8), (32 : UInt8), (192 : UInt8), (0 : UInt8), (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), (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), (115 : UInt8), (119 : UInt8), (97 : UInt8), (112 : UInt8), (95 : UInt8), (101 : UInt8), (108 : UInt8), (101 : UInt8), (109 : UInt8), (101 : UInt8), (110 : UInt8), (116 : UInt8), (115 : UInt8), (95 : UInt8), (111 : UInt8), (112 : UInt8), (116 : UInt8), (51 : UInt8), (47 : UInt8), (115 : UInt8), (114 : UInt8), (99 : UInt8), (47 : UInt8), (108 : UInt8), (105 : UInt8), (98 : UInt8), (46 : UInt8), (114 : UInt8), (115 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (179 : UInt8), (0 : UInt8), (16 : UInt8), (0 : UInt8), (29 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (9 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (9 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (2 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (12 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (4 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (3 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (4 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (5 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (8 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (4 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (6 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (7 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (8 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (9 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (10 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (16 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (4 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (11 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (12 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (13 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (14 : UInt8), (0 : UInt8), (0 : UInt8), (0 : UInt8), (109 : UInt8), (93 : UInt8), (203 : UInt8), (214 : UInt8), (44 : UInt8), (80 : UInt8), (235 : UInt8), (99 : UInt8), (120 : UInt8), (65 : UInt8), (166 : UInt8), (87 : UInt8), (113 : UInt8), (27 : UInt8), (139 : UInt8), (185 : UInt8), (21 : UInt8), (162 : UInt8), (92 : UInt8), (85 : UInt8), (52 : UInt8), (85 : UInt8), (7 : UInt8), (212 : UInt8), (83 : UInt8), (120 : UInt8), (173 : UInt8), (129 : UInt8), (81 : UInt8), (240 : UInt8), (163 : UInt8), (247 : UInt8), (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), (136 : 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), (136 : 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), (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), (0 : UInt8), (55 : UInt8), (0 : 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), (48 : UInt8), (48 : UInt8), (48 : UInt8), (49 : UInt8), (48 : UInt8), (50 : UInt8), (48 : UInt8), (51 : UInt8), (48 : UInt8), (52 : UInt8), (48 : UInt8), (53 : UInt8), (48 : UInt8), (54 : UInt8), (48 : UInt8), (55 : UInt8), (48 : UInt8), (56 : UInt8), (48 : UInt8), (57 : UInt8), (49 : UInt8), (48 : UInt8), (49 : UInt8), (49 : UInt8), (49 : UInt8), (50 : UInt8), (49 : UInt8), (51 : UInt8), (49 : UInt8), (52 : UInt8), (49 : UInt8), (53 : UInt8), (49 : UInt8), (54 : UInt8), (49 : UInt8), (55 : UInt8), (49 : UInt8), (56 : UInt8), (49 : UInt8), (57 : UInt8), (50 : UInt8), (48 : UInt8), (50 : UInt8), (49 : UInt8), (50 : UInt8), (50 : UInt8), (50 : UInt8), (51 : UInt8), (50 : UInt8), (52 : UInt8), (50 : UInt8), (53 : UInt8), (50 : UInt8), (54 : UInt8), (50 : UInt8), (55 : UInt8), (50 : UInt8), (56 : UInt8), (50 : UInt8), (57 : UInt8), (51 : UInt8), (48 : UInt8), (51 : UInt8), (49 : UInt8), (51 : UInt8), (50 : UInt8), (51 : UInt8), (51 : UInt8), (51 : UInt8), (52 : UInt8), (51 : UInt8), (53 : UInt8), (51 : UInt8), (54 : UInt8), (51 : UInt8), (55 : UInt8), (51 : UInt8), (56 : UInt8), (51 : UInt8), (57 : UInt8), (52 : UInt8), (48 : UInt8), (52 : UInt8), (49 : UInt8), (52 : UInt8), (50 : UInt8), (52 : UInt8), (51 : UInt8), (52 : UInt8), (52 : UInt8), (52 : UInt8), (53 : UInt8), (52 : UInt8), (54 : UInt8), (52 : UInt8), (55 : UInt8), (52 : UInt8), (56 : UInt8), (52 : UInt8), (57 : UInt8), (53 : UInt8), (48 : UInt8), (53 : UInt8), (49 : UInt8), (53 : UInt8), (50 : UInt8), (53 : UInt8), (51 : UInt8), (53 : UInt8), (52 : UInt8), (53 : UInt8), (53 : UInt8), (53 : UInt8), (54 : UInt8), (53 : UInt8), (55 : UInt8), (53 : UInt8), (56 : UInt8), (53 : UInt8), (57 : UInt8), (54 : UInt8), (48 : UInt8), (54 : UInt8), (49 : UInt8), (54 : UInt8), (50 : UInt8), (54 : UInt8), (51 : UInt8), (54 : UInt8), (52 : UInt8), (54 : UInt8), (53 : UInt8), (54 : UInt8), (54 : UInt8), (54 : UInt8), (55 : UInt8), (54 : UInt8), (56 : UInt8), (54 : UInt8), (57 : UInt8), (55 : UInt8), (48 : UInt8), (55 : UInt8), (49 : UInt8), (55 : UInt8), (50 : UInt8), (55 : UInt8), (51 : UInt8), (55 : UInt8), (52 : UInt8), (55 : UInt8), (53 : UInt8), (55 : UInt8), (54 : UInt8), (55 : UInt8), (55 : UInt8), (55 : UInt8), (56 : UInt8), (55 : UInt8), (57 : UInt8), (56 : UInt8), (48 : UInt8), (56 : UInt8), (49 : UInt8), (56 : UInt8), (50 : UInt8), (56 : UInt8), (51 : UInt8), (56 : UInt8), (52 : UInt8), (56 : UInt8), (53 : UInt8), (56 : UInt8), (54 : UInt8), (56 : UInt8), (55 : UInt8), (56 : UInt8), (56 : UInt8), (56 : UInt8), (57 : UInt8), (57 : UInt8), (48 : UInt8), (57 : UInt8), (49 : UInt8), (57 : UInt8), (50 : UInt8), (57 : UInt8), (51 : UInt8), (57 : UInt8), (52 : UInt8), (57 : UInt8), (53 : UInt8), (57 : UInt8), (54 : UInt8), (57 : UInt8), (55 : UInt8), (57 : UInt8), (56 : UInt8), (57 : UInt8), (57 : UInt8)] }
] },
globals := [
{ init := .i32 (1048576 : UInt32) },
{ init := .i32 (1049793 : UInt32) },
{ init := .i32 (1049808 : UInt32) }
],
types := [
{ params := [.i32, .i32], results := [] },
{ params := [.i32, .i32, .i32], results := [.i32] },
{ params := [.i32, .i32], results := [.i32] },
{ params := [.i32, .i32, .i32, .i32], results := [] },
{ params := [.i32, .i32, .i32], 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] },
{ params := [.i32, .i32, .i32, .i32, .i32, .i32], results := [.i32] },
{ params := [.i32, .i32, .i32, .i32, .i32], results := [.i32] }
],
tables := [
{ min := 18, max := some 18, elemType := .funcref }
],
elements := [
{ tableIdx := some 0, offset := some 1, funcs := [some 16, some 8, some 40, some 39, some 44, some 38, some 37, some 35, some 36, some 9, some 34, some 42, some 41, some 43, some 33, some 32, some 57] }
]
}
end Project.SwapElementsOpt3
lean/Project/SwapElementsOpt3/SmallStepEquivalence.lean lean · 466 lines
import CodeLib.Equivalence
import Project.SwapElements.Address
import Project.SwapElements.SwapSepLogic
import Project.SwapElementsOpt3.Program
/-!
# Authoritative small-step equivalence smoke test
This compares the real unoptimized exported call chain with the optimized
inlined export. The observation deliberately contains the caller-visible
two-word array and excludes the unoptimized implementation's private scratch
traffic.
-/
namespace Project.SwapElementsOpt3.SmallStepEquivalence
open Iris Iris.ProgramLogic Language.Notation Std
open Wasm
open Wasm.SepLogic
set_option maxHeartbeats 4000000 in
/-- Universal Iris rule for the optimized inlined export on distinct element
addresses. Both bounds checks, both address calculations, and both physical
loads/stores execute through the authoritative small-step semantics. -/
theorem opt3_func0_distinct_smallStep_wp
[Wasm.SmallStep.WasmSmallStepGS hlc]
{s : Stuckness} {E : CoPset}
(ptr len i j : UInt32) (oldA oldB : UInt64)
(hi : i < len) (hj : j < len)
(hroomI : ((i <<< (3 % 32)) + ptr).toNat + 8 ≤ 4294967296)
(hroomJ : ((j <<< (3 % 32)) + ptr).toNat + 8 ≤ 4294967296) :
let addressI := (i <<< (3 % 32)) + ptr
let addressJ := (j <<< (3 % 32)) + ptr
pointsTo_u64 addressI oldA ∗ pointsTo_u64 addressJ oldB ⊢
WP (Wasm.SmallStep.Expr.running
⟨⟨[.i32 ptr, .i32 len, .i32 i, .i32 j], [.i64 0], []⟩,
Project.SwapElementsOpt3.func0, 0, [], [], []⟩ :
Wasm.SmallStep.Expr Unit) @ s; E
{{ values, ⌜values = []⌝ ∗
pointsTo_u64 addressI oldB ∗ pointsTo_u64 addressJ oldA }} := by
dsimp only
let addressI := (i <<< (3 % 32)) + ptr
let addressJ := (j <<< (3 % 32)) + ptr
have hroomI' : addressI.toNat + 8 ≤ 4294967296 := by
simpa [addressI] using hroomI
have hroomJ' : addressJ.toNat + 8 ≤ 4294967296 := by
simpa [addressJ] using hroomJ
have hi1 : (addressI + 1).toNat = addressI.toNat + 1 := by
simpa using UInt32.add_ofNat_toNat_noWrap addressI 1 (by omega) (by omega)
have hi2 : (addressI + 2).toNat = addressI.toNat + 2 := by
simpa using UInt32.add_ofNat_toNat_noWrap addressI 2 (by omega) (by omega)
have hi3 : (addressI + 3).toNat = addressI.toNat + 3 := by
simpa using UInt32.add_ofNat_toNat_noWrap addressI 3 (by omega) (by omega)
have hi4 : (addressI + 4).toNat = addressI.toNat + 4 := by
simpa using UInt32.add_ofNat_toNat_noWrap addressI 4 (by omega) (by omega)
have hi5 : (addressI + 5).toNat = addressI.toNat + 5 := by
simpa using UInt32.add_ofNat_toNat_noWrap addressI 5 (by omega) (by omega)
have hi6 : (addressI + 6).toNat = addressI.toNat + 6 := by
simpa using UInt32.add_ofNat_toNat_noWrap addressI 6 (by omega) (by omega)
have hi7 : (addressI + 7).toNat = addressI.toNat + 7 := by
simpa using UInt32.add_ofNat_toNat_noWrap addressI 7 (by omega) (by omega)
have hj1 : (addressJ + 1).toNat = addressJ.toNat + 1 := by
simpa using UInt32.add_ofNat_toNat_noWrap addressJ 1 (by omega) (by omega)
have hj2 : (addressJ + 2).toNat = addressJ.toNat + 2 := by
simpa using UInt32.add_ofNat_toNat_noWrap addressJ 2 (by omega) (by omega)
have hj3 : (addressJ + 3).toNat = addressJ.toNat + 3 := by
simpa using UInt32.add_ofNat_toNat_noWrap addressJ 3 (by omega) (by omega)
have hj4 : (addressJ + 4).toNat = addressJ.toNat + 4 := by
simpa using UInt32.add_ofNat_toNat_noWrap addressJ 4 (by omega) (by omega)
have hj5 : (addressJ + 5).toNat = addressJ.toNat + 5 := by
simpa using UInt32.add_ofNat_toNat_noWrap addressJ 5 (by omega) (by omega)
have hj6 : (addressJ + 6).toNat = addressJ.toNat + 6 := by
simpa using UInt32.add_ofNat_toNat_noWrap addressJ 6 (by omega) (by omega)
have hj7 : (addressJ + 7).toNat = addressJ.toNat + 7 := by
simpa using UInt32.add_ofNat_toNat_noWrap addressJ 7 (by omega) (by omega)
iintro ⟨HA, HB⟩
simp only [Project.SwapElementsOpt3.func0]
iapply Wasm.SmallStep.wp_block
inext
iapply Wasm.SmallStep.wp_block
inext
iapply Wasm.SmallStep.wp_localGet rfl
inext
iapply Wasm.SmallStep.wp_localGet rfl
inext
iapply Wasm.SmallStep.wp_geU (result := 0)
(by simp [show ¬i ≥ len from not_le_of_gt hi])
inext
iapply Wasm.SmallStep.wp_brIfZero
inext
iapply Wasm.SmallStep.wp_localGet rfl
inext
iapply Wasm.SmallStep.wp_localGet rfl
inext
iapply Wasm.SmallStep.wp_geU (result := 0)
(by simp [show ¬j ≥ len from not_le_of_gt hj])
inext
iapply Wasm.SmallStep.wp_brIfZero
inext
iapply Wasm.SmallStep.wp_localGet rfl
inext
iapply Wasm.SmallStep.wp_localGet rfl
inext
iapply Wasm.SmallStep.wp_const
inext
iapply Wasm.SmallStep.wp_shl
inext
iapply Wasm.SmallStep.wp_add
inext
iapply Wasm.SmallStep.wp_localSet rfl
inext
simp only [List.set]
iapply Wasm.SmallStep.wp_localGet rfl
inext
ihave HALater : ▷ pointsTo_u64 (addressI + 0) oldA $$ [HA]
· inext
rw [UInt32.add_zero]
iexact HA
iapply Wasm.SmallStep.wp_load64 oldA (by simp)
(by simpa using hi1) (by simpa using hi2) (by simpa using hi3)
(by simpa using hi4) (by simpa using hi5) (by simpa using hi6)
(by simpa using hi7) $$ HALater
inext
iintro HA
iapply Wasm.SmallStep.wp_localSet rfl
inext
simp only [List.length_cons, List.length_nil, Nat.reduceAdd, Nat.reduceSub,
List.set]
iapply Wasm.SmallStep.wp_localGet rfl
inext
iapply Wasm.SmallStep.wp_localGet rfl
inext
iapply Wasm.SmallStep.wp_localGet rfl
inext
iapply Wasm.SmallStep.wp_const
inext
iapply Wasm.SmallStep.wp_shl
inext
iapply Wasm.SmallStep.wp_add
inext
iapply Wasm.SmallStep.wp_localSet rfl
inext
simp only [List.set]
iapply Wasm.SmallStep.wp_localGet rfl
inext
ihave HBLater : ▷ pointsTo_u64 (addressJ + 0) oldB $$ [HB]
· inext
rw [UInt32.add_zero]
iexact HB
iapply Wasm.SmallStep.wp_load64 oldB (by simp)
(by simpa using hj1) (by simpa using hj2) (by simpa using hj3)
(by simpa using hj4) (by simpa using hj5) (by simpa using hj6)
(by simpa using hj7) $$ HBLater
inext
iintro HB
ihave HALater : ▷ pointsTo_u64 (addressI + 0) oldA $$ [HA]
· inext
rw [UInt32.add_zero]
iexact HA
iapply Wasm.SmallStep.wp_store64 oldA (by simp)
(by simpa using hi1) (by simpa using hi2) (by simpa using hi3)
(by simpa using hi4) (by simpa using hi5) (by simpa using hi6)
(by simpa using hi7) $$ HALater
inext
iintro HA
iapply Wasm.SmallStep.wp_localGet rfl
inext
iapply Wasm.SmallStep.wp_localGet rfl
inext
ihave HBLater : ▷ pointsTo_u64 (addressJ + 0) oldB $$ [HB]
· inext
rw [UInt32.add_zero]
iexact HB
iapply Wasm.SmallStep.wp_store64 oldB (by simp)
(by simpa using hj1) (by simpa using hj2) (by simpa using hj3)
(by simpa using hj4) (by simpa using hj5) (by simpa using hj6)
(by simpa using hj7) $$ HBLater
inext
iintro HB
iapply Wasm.SmallStep.wp_returnFromFunction
inext
iapply wp_value'
isplitr
· ipureintro
rfl
· rw [show (i <<< (3 % 32)) + ptr = addressI by rfl,
show (j <<< (3 % 32)) + ptr = addressJ by rfl]
simp only [UInt32.add_zero]
iframe
/-- Authoritative entry configuration for the optimized export. -/
def opt3ConfigFromStore (wasm : Store Unit)
(ptr len i j : UInt32) : Wasm.SmallStep.Config Unit :=
{ expr := .running
⟨⟨[.i32 ptr, .i32 len, .i32 i, .i32 j], [.i64 0], []⟩,
Project.SwapElementsOpt3.func0, 0, [], [], []⟩
store :=
{ runtime := { module := Project.SwapElementsOpt3.module, host := {} }
wasm := wasm } }
/-- Universal physical-store partial correctness for the optimized export.
The heap footprint owns exactly the two distinct array elements; globals and
all unrelated memory remain framed. -/
theorem opt3_func0_distinct_store_partiallyMeets
(wasm : Store Unit) (ptr len i j : UInt32)
(oldA oldB : UInt64)
(σ : WasmHeapMap (Option UInt8))
(globalσ : WasmGlobalMap Value)
(hi : i < len) (hj : j < len)
(hroomI : ((i <<< (3 % 32)) + ptr).toNat + 8 ≤ 4294967296)
(hroomJ : ((j <<< (3 % 32)) + ptr).toNat + 8 ≤ 4294967296)
(hagree : heapAgreesWithMem σ wasm.mem)
(hinBounds : heapAddressesInBounds σ wasm.mem)
(hglobals : globalHeapAgrees globalσ wasm.globals)
(hresources : ∀ [WasmHeapGS],
([∗map] address ↦ value ∈ σ,
pointsTo (GF := WasmHeapGF) (H := WasmHeapMap)
address (DFrac.own 1) value) ⊢
pointsTo_u64 ((i <<< (3 % 32)) + ptr) oldA ∗
pointsTo_u64 ((j <<< (3 % 32)) + ptr) oldB) :
Wasm.SmallStep.PartiallyMeets
(opt3ConfigFromStore wasm ptr len i j)
(fun values store =>
values = [] ∧
store.wasm.mem.read64 ((i <<< (3 % 32)) + ptr) = oldB ∧
store.wasm.mem.read64 ((j <<< (3 % 32)) + ptr) = oldA) := by
let addressI := (i <<< (3 % 32)) + ptr
let addressJ := (j <<< (3 % 32)) + ptr
have hroomI' : addressI.toNat + 8 ≤ 4294967296 := by
simpa [addressI] using hroomI
have hroomJ' : addressJ.toNat + 8 ≤ 4294967296 := by
simpa [addressJ] using hroomJ
have hi1 : (addressI + 1).toNat = addressI.toNat + 1 := by
simpa using UInt32.add_ofNat_toNat_noWrap addressI 1 (by omega) (by omega)
have hi2 : (addressI + 2).toNat = addressI.toNat + 2 := by
simpa using UInt32.add_ofNat_toNat_noWrap addressI 2 (by omega) (by omega)
have hi3 : (addressI + 3).toNat = addressI.toNat + 3 := by
simpa using UInt32.add_ofNat_toNat_noWrap addressI 3 (by omega) (by omega)
have hi4 : (addressI + 4).toNat = addressI.toNat + 4 := by
simpa using UInt32.add_ofNat_toNat_noWrap addressI 4 (by omega) (by omega)
have hi5 : (addressI + 5).toNat = addressI.toNat + 5 := by
simpa using UInt32.add_ofNat_toNat_noWrap addressI 5 (by omega) (by omega)
have hi6 : (addressI + 6).toNat = addressI.toNat + 6 := by
simpa using UInt32.add_ofNat_toNat_noWrap addressI 6 (by omega) (by omega)
have hi7 : (addressI + 7).toNat = addressI.toNat + 7 := by
simpa using UInt32.add_ofNat_toNat_noWrap addressI 7 (by omega) (by omega)
have hj1 : (addressJ + 1).toNat = addressJ.toNat + 1 := by
simpa using UInt32.add_ofNat_toNat_noWrap addressJ 1 (by omega) (by omega)
have hj2 : (addressJ + 2).toNat = addressJ.toNat + 2 := by
simpa using UInt32.add_ofNat_toNat_noWrap addressJ 2 (by omega) (by omega)
have hj3 : (addressJ + 3).toNat = addressJ.toNat + 3 := by
simpa using UInt32.add_ofNat_toNat_noWrap addressJ 3 (by omega) (by omega)
have hj4 : (addressJ + 4).toNat = addressJ.toNat + 4 := by
simpa using UInt32.add_ofNat_toNat_noWrap addressJ 4 (by omega) (by omega)
have hj5 : (addressJ + 5).toNat = addressJ.toNat + 5 := by
simpa using UInt32.add_ofNat_toNat_noWrap addressJ 5 (by omega) (by omega)
have hj6 : (addressJ + 6).toNat = addressJ.toNat + 6 := by
simpa using UInt32.add_ofNat_toNat_noWrap addressJ 6 (by omega) (by omega)
have hj7 : (addressJ + 7).toNat = addressJ.toNat + 7 := by
simpa using UInt32.add_ofNat_toNat_noWrap addressJ 7 (by omega) (by omega)
apply
Wasm.SmallStep.wasm_smallStep_heap_globals_runtime_store_partiallyMeets.{0}
(α := Unit) (σ := σ) (globalσ := globalσ)
· exact hagree
· exact hinBounds
· exact hglobals
· intro gs
iintro ⟨Hheap, Hglobals, Hruntime⟩
ihave Hwords := hresources $$ Hheap
icases Hwords with ⟨HA, HB⟩
have hpost : ∀ values : List Value,
(iprop% ⌜values = []⌝ ∗
pointsTo_u64 addressI oldB ∗ pointsTo_u64 addressJ oldA) ⊢
(iprop% ∀ (store : Wasm.SmallStep.MachineStore Unit)
(_observations : List Wasm.SmallStep.StepKind),
stateInterp (GF := WasmHeapGF) store 0 [] 0 -∗
⌜values = [] ∧ store.wasm.mem.read64 addressI = oldB ∧
store.wasm.mem.read64 addressJ = oldA⌝) := by
intro values
iintro ⟨%hvalues, HA, HB⟩ %store %_observations Hstate
imod Wasm.SmallStep.stateInterp_pointsTo_u64_facts_frame
store 0 [] 0 addressI oldB hi1 hi2 hi3 hi4 hi5 hi6 hi7 $$
[$Hstate $HA] with ⟨Hstate, _HA, %HfactsI⟩
imod Wasm.SmallStep.stateInterp_pointsTo_u64_facts
store 0 [] 0 addressJ oldA hj1 hj2 hj3 hj4 hj5 hj6 hj7 $$
[$Hstate $HB] with %HfactsJ
ipureintro
exact ⟨hvalues, HfactsI.1, HfactsJ.1⟩
iclear Hglobals Hruntime
iapply wp_mono hpost
simp only [opt3ConfigFromStore]
iapply opt3_func0_distinct_smallStep_wp
ptr len i j oldA oldB hi hj hroomI hroomJ
iframe
/-- Symbolic finite termination of the optimized straight-line happy path.
This is deliberately separate from the Iris rule: it supplies totality while
the Iris proof supplies the physical-memory postcondition. -/
theorem opt3_func0_terminates
(wasm : Store Unit) (ptr len i j : UInt32)
(hi : i < len) (hj : j < len)
(hboundI :
((i <<< (3 % 32)) + ptr).toNat + 8 ≤ wasm.mem.pages * 65536)
(hboundJ :
((j <<< (3 % 32)) + ptr).toNat + 8 ≤ wasm.mem.pages * 65536) :
Wasm.SmallStep.TerminatesWith
(opt3ConfigFromStore wasm ptr len i j)
(fun values _store => values = []) := by
simp only [opt3ConfigFromStore, Project.SwapElementsOpt3.func0]
apply Wasm.SmallStep.TerminatesWith.prepend Wasm.SmallStep.Step.block
apply Wasm.SmallStep.TerminatesWith.prepend Wasm.SmallStep.Step.block
apply Wasm.SmallStep.TerminatesWith.prepend
(Wasm.SmallStep.Step.localGet rfl)
apply Wasm.SmallStep.TerminatesWith.prepend
(Wasm.SmallStep.Step.localGet rfl)
apply Wasm.SmallStep.TerminatesWith.prepend
(Wasm.SmallStep.Step.geU (result := 0) (by simp [not_le_of_gt hi]))
apply Wasm.SmallStep.TerminatesWith.prepend Wasm.SmallStep.Step.brIfZero
apply Wasm.SmallStep.TerminatesWith.prepend
(Wasm.SmallStep.Step.localGet rfl)
apply Wasm.SmallStep.TerminatesWith.prepend
(Wasm.SmallStep.Step.localGet rfl)
apply Wasm.SmallStep.TerminatesWith.prepend
(Wasm.SmallStep.Step.geU (result := 0) (by simp [not_le_of_gt hj]))
apply Wasm.SmallStep.TerminatesWith.prepend Wasm.SmallStep.Step.brIfZero
apply Wasm.SmallStep.TerminatesWith.prepend
(Wasm.SmallStep.Step.localGet rfl)
apply Wasm.SmallStep.TerminatesWith.prepend
(Wasm.SmallStep.Step.localGet rfl)
apply Wasm.SmallStep.TerminatesWith.prepend Wasm.SmallStep.Step.const
apply Wasm.SmallStep.TerminatesWith.prepend Wasm.SmallStep.Step.shl
apply Wasm.SmallStep.TerminatesWith.prepend Wasm.SmallStep.Step.add
apply Wasm.SmallStep.TerminatesWith.prepend
(Wasm.SmallStep.Step.localSet rfl)
simp only [List.set]
apply Wasm.SmallStep.TerminatesWith.prepend
(Wasm.SmallStep.Step.localGet rfl)
apply Wasm.SmallStep.TerminatesWith.prepend
(Wasm.SmallStep.Step.load64 rfl (by simpa using hboundI))
apply Wasm.SmallStep.TerminatesWith.prepend
(Wasm.SmallStep.Step.localSet rfl)
simp only [List.length_cons, List.length_nil, Nat.reduceAdd, Nat.reduceSub,
List.set]
apply Wasm.SmallStep.TerminatesWith.prepend
(Wasm.SmallStep.Step.localGet rfl)
apply Wasm.SmallStep.TerminatesWith.prepend
(Wasm.SmallStep.Step.localGet rfl)
apply Wasm.SmallStep.TerminatesWith.prepend
(Wasm.SmallStep.Step.localGet rfl)
apply Wasm.SmallStep.TerminatesWith.prepend Wasm.SmallStep.Step.const
apply Wasm.SmallStep.TerminatesWith.prepend Wasm.SmallStep.Step.shl
apply Wasm.SmallStep.TerminatesWith.prepend Wasm.SmallStep.Step.add
apply Wasm.SmallStep.TerminatesWith.prepend
(Wasm.SmallStep.Step.localSet rfl)
simp only [List.set]
apply Wasm.SmallStep.TerminatesWith.prepend
(Wasm.SmallStep.Step.localGet rfl)
apply Wasm.SmallStep.TerminatesWith.prepend
(Wasm.SmallStep.Step.load64 rfl (by simpa using hboundJ))
apply Wasm.SmallStep.TerminatesWith.prepend
(Wasm.SmallStep.Step.store64 rfl (by simpa using hboundI))
apply Wasm.SmallStep.TerminatesWith.prepend
(Wasm.SmallStep.Step.localGet rfl)
apply Wasm.SmallStep.TerminatesWith.prepend
(Wasm.SmallStep.Step.localGet rfl)
apply Wasm.SmallStep.TerminatesWith.prepend
(Wasm.SmallStep.Step.store64 rfl (by
simpa [Wasm.SmallStep.setMemory_eq] using hboundJ))
apply Wasm.SmallStep.TerminatesWith.prepend
Wasm.SmallStep.Step.returnFromFunction
simp only [List.take_zero, List.nil_append]
exact ⟨[], [], _, .refl _, rfl⟩
/-- Universal total correctness for the optimized distinct-index export,
obtained by combining its explicit finite trace with its Iris physical-store
partial correctness theorem. -/
theorem opt3_func0_distinct_store_terminatesWith
(wasm : Store Unit) (ptr len i j : UInt32)
(oldA oldB : UInt64)
(σ : WasmHeapMap (Option UInt8))
(globalσ : WasmGlobalMap Value)
(hi : i < len) (hj : j < len)
(hboundI :
((i <<< (3 % 32)) + ptr).toNat + 8 ≤ wasm.mem.pages * 65536)
(hboundJ :
((j <<< (3 % 32)) + ptr).toNat + 8 ≤ wasm.mem.pages * 65536)
(hroomI : ((i <<< (3 % 32)) + ptr).toNat + 8 ≤ 4294967296)
(hroomJ : ((j <<< (3 % 32)) + ptr).toNat + 8 ≤ 4294967296)
(hagree : heapAgreesWithMem σ wasm.mem)
(hinBounds : heapAddressesInBounds σ wasm.mem)
(hglobals : globalHeapAgrees globalσ wasm.globals)
(hresources : ∀ [WasmHeapGS],
([∗map] address ↦ value ∈ σ,
pointsTo (GF := WasmHeapGF) (H := WasmHeapMap)
address (DFrac.own 1) value) ⊢
pointsTo_u64 ((i <<< (3 % 32)) + ptr) oldA ∗
pointsTo_u64 ((j <<< (3 % 32)) + ptr) oldB) :
Wasm.SmallStep.TerminatesWith
(opt3ConfigFromStore wasm ptr len i j)
(fun values store =>
values = [] ∧
store.wasm.mem.read64 ((i <<< (3 % 32)) + ptr) = oldB ∧
store.wasm.mem.read64 ((j <<< (3 % 32)) + ptr) = oldA) := by
apply Wasm.SmallStep.TerminatesWith.of_termination_and_partial
((opt3_func0_terminates wasm ptr len i j hi hj hboundI hboundJ).mono
(fun _ _ _ => trivial))
exact opt3_func0_distinct_store_partiallyMeets
wasm ptr len i j oldA oldB σ globalσ hi hj hroomI hroomJ
hagree hinBounds hglobals hresources
abbrev opt0ExampleConfig : Wasm.SmallStep.Config Unit :=
Project.SwapElements.SwapSepLogic.func4ExampleConfig
/-- The optimized export on the same physical Wasm store and arguments as the
unoptimized two-element example. -/
def opt3ExampleConfig : Wasm.SmallStep.Config Unit :=
{ expr := .running
⟨⟨[.i32 0, .i32 2, .i32 0, .i32 1], [.i64 0], []⟩,
Project.SwapElementsOpt3.func0, 0, [], [], []⟩
store :=
{ runtime :=
{ module := Project.SwapElementsOpt3.module
host := {} }
wasm := opt0ExampleConfig.store.wasm } }
/-- Caller-visible array observation. Private scratch and spill locations are
intentionally absent. -/
def arrayObservation (store : Wasm.SmallStep.MachineStore Unit) :
UInt64 × UInt64 :=
(store.wasm.mem.read64 0, store.wasm.mem.read64 8)
theorem opt0Example_terminates_with_observation :
Wasm.SmallStep.TerminatesWith opt0ExampleConfig
(fun values store =>
values = [] ∧ arrayObservation store = (22, 11)) := by
apply Wasm.SmallStep.TerminatesWith.of_termination_and_partial
(Project.SwapElements.SwapSepLogic.func4Example_terminates.mono
(fun _ _ _ => trivial))
intro trace values store execution
have h :=
Project.SwapElements.SwapSepLogic.func4Example_store_smallStep
trace values store execution
exact ⟨h.1, Prod.ext h.2.1 h.2.2⟩
theorem opt3Example_terminates_with_observation :
Wasm.SmallStep.TerminatesWith opt3ExampleConfig
(fun values store =>
values = [] ∧ arrayObservation store = (22, 11)) := by
apply Wasm.SmallStep.runSteps_checked_terminates (fuel := 100)
(fun values store =>
(values == []) && (arrayObservation store == (22, 11)))
· native_decide
· intro values store h
simpa [Bool.and_eq_true] using h
/-- The two actual generated exports have exactly the same terminal outcomes
under the caller-visible array observation for the concrete regression. -/
theorem example_observationally_equivalent :
Wasm.SmallStep.ObservationallyEquivOn
opt0ExampleConfig opt3ExampleConfig arrayObservation :=
Wasm.SmallStep.ObservationallyEquivOn.of_common_outcome
opt0Example_terminates_with_observation
opt3Example_terminates_with_observation
end Project.SwapElementsOpt3.SmallStepEquivalence
lean/Project/SwapElementsOpt3/Spec.lean lean · 88 lines
import Project.SwapElementsOpt3.Program
import Project.SwapElements.Address
/-!
# Specification and proof for `swap_elements_opt3`
The `opt-level = 3` build of byte-for-byte the same Rust source as
`swap_elements`:
```rust
pub fn swap_elements(arr: &mut [u64], i: usize, j: usize) {
arr.swap(i, j);
}
```
## What the optimiser did
At `opt-level = 0` the export (`func4`) carves a 16-byte shadow-stack frame,
materialises the slice fat pointer through memory, and forwards through a
four-deep call chain (`func3`/`func0`/`func1`/`func2`), exchanging the two
elements via a **scratch slot** at `1048552`.
At `opt-level = 3` the whole thing collapses into the exported `func0`: it
bounds-checks `i, j < len` (both `panic` branches are unreachable under the
preconditions), computes the two element addresses, and performs the exchange
with two `i64.load`s and two `i64.store`s through an `i64` local. It never
reads or writes `global 0`, and it never touches the scratch slot.
Consequently this build needs *strictly fewer* preconditions than the opt0 one:
no shadow-stack pin on `global 0`, and no `1048576 ≤ ptr` (there is no scratch
frame for the array to alias). The two builds' final memories therefore are not
the same function — opt0 additionally writes the scratch slot at
`[1048552, 1048560)`, which this build never touches — while agreeing on the
array itself. Relating them is the subject of
`Project.SwapElementsOpt3.Equivalence`.
-/
namespace Project.SwapElementsOpt3.Spec
open Wasm
-- The element-address vocabulary (`elemAddr` and its arithmetic lemmas) is
-- shared with the opt0 build's spec, so the two postconditions match
-- syntactically and the equivalence proof needs no normalisation step.
open Project.SwapElements.Spec (elemAddr elemAddr_of_shl elemAddr_toNat)
set_option maxRecDepth 1048576
/-- `func0` (index 0, the export): bounds checks fused with the exchange. -/
theorem func0_swap (env : HostEnv Unit) (st : Store Unit) (ptr len i j : UInt32)
(hi : i < len) (hj : j < len)
(hbound : ptr.toNat + 8 * len.toNat ≤ st.mem.pages * 65536)
(hpages : st.mem.pages ≤ 65536) :
TerminatesWith env «module» 0 st [.i32 j, .i32 i, .i32 len, .i32 ptr]
(fun st' vs => vs = []
∧ st'.mem =
(st.mem.write64 (elemAddr ptr i) (st.mem.read64 (elemAddr ptr j))).write64
(elemAddr ptr j) (st.mem.read64 (elemAddr ptr i))) := by
have hbnd : st.mem.pages * 65536 ≤ 4294967296 := by
have := Nat.mul_le_mul_right 65536 hpages; omega
have hli : i.toNat < len.toNat := hi
have hlj : j.toNat < len.toNat := hj
have hwi : ptr.toNat + 8 * i.toNat < 4294967296 := by omega
have hwj : ptr.toNat + 8 * j.toNat < 4294967296 := by omega
have gpi : ¬ (st.mem.pages * 65536 < (elemAddr ptr i).toNat + 8) := by
rw [elemAddr_toNat ptr i hwi]; omega
have gpj : ¬ (st.mem.pages * 65536 < (elemAddr ptr j).toNat + 8) := by
rw [elemAddr_toNat ptr j hwj]; omega
-- the two `panic` branches: `i, j < len` refutes each `geU` test
have hgi : ¬ (i ≥ len) := by intro h; have : len.toNat ≤ i.toNat := h; omega
have hgj : ¬ (j ≥ len) := by intro h; have : len.toNat ≤ j.toNat := h; omega
apply TerminatesWith.of_wp_entry_for (f := func0Def) rfl
unfold func0Def func0
apply wp_block_cons
apply wp_block_cons
simp only [wp_simp, Locals.get, Locals.set?, Function.toLocals,
Function.numParams, List.take, List.drop,
List.length, List.map, ValueType.zero,
List.reverse_cons, List.reverse_nil, List.cons_append, List.nil_append, List.append_nil,
List.getElem?_cons_zero, List.getElem?_cons_succ,
List.set_cons_zero, List.set_cons_succ,
Nat.reduceLT, Nat.reduceAdd, Nat.reduceSub, reduceIte,
UInt32.reduceToNat, UInt32.add_zero, Mem.write64_pages,
hgi, hgj, elemAddr_of_shl, gpi, gpj]
exact ⟨trivial, trivial⟩
end Project.SwapElementsOpt3.Spec
Rust (2)
rust/swap_elements_opt3/src/exports.rs rust · 16 lines
/// Wasm-exported entry point for `swap_elements`.
///
/// Thin `extern "C"` wrapper around the pure [`crate::swap_elements`]. The
/// project convention reserves this file for the wasm ABI surface, so the
/// export table matches exactly what the verifier reasons about.
///
/// Receives the array as a `(pointer, length)` pair plus the two indices to
/// swap. On wasm32 both `usize` and the pointer are 32-bit. The caller must
/// guarantee `i < data_length` and `j < data_length` and that
/// `[array_ptr, array_ptr + data_length)` is a valid, aligned `u64` region.
#[unsafe(no_mangle)]
pub extern "C" fn swap_elements(array_ptr: *mut u64, data_length: usize, i: usize, j: usize) {
let arr = unsafe { core::slice::from_raw_parts_mut(array_ptr, data_length) };
crate::swap_elements(arr, i, j);
}
rust/swap_elements_opt3/src/lib.rs rust · 11 lines
mod exports;
/// Swap the elements at indices `i` and `j` of a mutable slice.
///
/// Pure logic kept here; the wasm ABI surface (raw pointer + length) lives in
/// `exports.rs`. Both `i` and `j` are assumed to be in bounds (`< arr.len()`),
/// matching the contract documented on the export.
pub fn swap_elements(arr: &mut [u64], i: usize, j: usize) {
arr.swap(i, j);
}
Other (1)
rust/swap_elements_opt3/Cargo.toml toml · 10 lines
[package]
name = "swap_elements_opt3"
version = "0.1.0"
edition = "2024"
[lib]
crate-type = ["cdylib", "rlib"]
[dependencies]