This fuzz target tests the property: any Wasm module that Lucet can
compile should produce an artifact that validates with VeriWasm. We are
looking for both "false positive" bugs in VeriWasm, i.e. compilation
results which are correct but which the validator can't handle, as well
as "true positive" validator errors that result from a genuine Lucet
miscompilation. If we see neither, then we have some more confidence
that both (i) Lucet is less likely to have heap-soundness bugs, and (ii)
VeriWasm is solid enough that one could consider requiring it to pass
before using a module.
This fuzz target tests the property: any Wasm module that Lucet can compile should produce an artifact that validates with VeriWasm. We are looking for both "false positive" bugs in VeriWasm, i.e. compilation results which are correct but which the validator can't handle, as well as "true positive" validator errors that result from a genuine Lucet miscompilation. If we see neither, then we have some more confidence that both (i) Lucet is less likely to have heap-soundness bugs, and (ii) VeriWasm is solid enough that one could consider requiring it to pass before using a module.