Performance considerations for well-typed Wasm programs

[Wolfgang]

Hello,
I'm a masters student at Aarhus university.
We built a verified compiler targeting Wasm (https://popl24.sigplan.org/details/CoqPL-2024-papers/3/CertiCoq-Wasm-Verified-compilation-from-Coq-to-WebAssembly),
which includes a correctness proof that the modules we generate instantiates according to the spec, i.e. they are well-typed.

Given these guarantees, is there an option, that would allow us to omit certain runtime checks to improve performance?

We're evaluating the binaries with Node.js, which doesn't seem to have (publicly documented) flags to disable e.g. type-checking.

I included some numbers below.

Best,
Wolfgang

All times in ms, benchmarks are described in Chapter 8.2 in http://zoep.github.io/thesis_final.pdf

startup: load binary+instantiation
main: main function
pp: pretty printing the resulting S-expression, works by calling an imported function print_char character-wise,
    thus somewhat slow, but not too important for my question here

Node.js: v18.19.1
   demo1-opt_coalesce-locals : startup:    6, main:   0, pp: 28, sum:   34
   demo2-opt_coalesce-locals : startup:    3, main:   0, pp:  8, sum:   11
list_sum-opt_coalesce-locals : startup:    3, main:   0, pp:  2, sum:    5
 vs_easy-opt_coalesce-locals : startup:   10, main:  33, pp:  1, sum:   44
 vs_hard-opt_coalesce-locals : startup:   10, main: 101, pp:  1, sum:  112
   binom-opt_coalesce-locals : startup:   18, main:  10, pp: 24, sum:   52
sha_fast-opt_coalesce-locals : startup:   65, main:  70, pp:  7, sum:  142
   color-opt_coalesce-locals : startup:  132, main:  44, pp:  2, sum:  178

Node.js: v20.11.1
   demo1-opt_coalesce-locals : startup:    1, main:   3, pp: 24, sum:   28
   demo2-opt_coalesce-locals : startup:    2, main:   0, pp: 12, sum:   14
list_sum-opt_coalesce-locals : startup:    2, main:   0, pp:  2, sum:    4
 vs_easy-opt_coalesce-locals : startup:    4, main:  38, pp:  4, sum:   46
 vs_hard-opt_coalesce-locals : startup:    3, main: 110, pp:  3, sum:  116
   binom-opt_coalesce-locals : startup:    3, main:  26, pp: 23, sum:   52
sha_fast-opt_coalesce-locals : startup:    4, main: 228, pp: 10, sum:  242
   color-opt_coalesce-locals : startup:   12, main: 332, pp:  2, sum:  346