Stream: general

Topic: interpreters which mirror structure of spec


view this post on Zulip nagisa (Aug 02 2022 at 10:40):

Does anybody know of any interpreters that closely follow the shape and structure of the specification? My goal is to pretty much use it as a reference implementation for some tests after modifying it with changes to the spec that I have in mind. I want to avoid missing implementation-specific details with the modifications, and so for that reason specifically it would be nice if the implementation was mirroring the spec as close to 1:1 as possible, including the instruction reduction mechanism used in the spec. As far as Rust implementations go, wain seems to fit the bill the best so far, but that implementation has chosen to eschew the reduction approach for the more straightforward loop { match { ... } }.

WebAssembly implementation from scratch in Safe Rust with zero dependencies - GitHub - rhysd/wain: WebAssembly implementation from scratch in Safe Rust with zero dependencies

view this post on Zulip Chris Fallin (Aug 02 2022 at 16:20):

@nagisa the spec repository itself has the reference interpreter, which seems to be the best fit I can think of for your request; it's written in a way that basically mirrors the spec's reduction rules into OCaml

view this post on Zulip Chris Fallin (Aug 02 2022 at 16:21):

@Conrad Watt has done work to make it fast with a few tweaks (otherwise it has some unfortunate quadratic behavior) and we use that version as an oracle for fuzzing

view this post on Zulip Conrad Watt (Aug 02 2022 at 17:43):

just to add, you should _definitely_ use the unmodified reference interpreter if you can get away with it, rather than my fork, which contains code generated using a theorem prover and isn't really human-readable

view this post on Zulip nagisa (Aug 02 2022 at 17:49):

Yeah performance is of little concern in my case, integrability into a typical Rust crate’s test suite and ability to modify it is however. I think might be able to live with ocaml as a dep, but I’ll need to see if I can get up to speed with the impl reasonably quickly.

view this post on Zulip Robin Freyler (Aug 08 2022 at 13:49):

It would be pretty useful to have the OCaml based Wasm spec interpreter as a Rust crate on crates.io. I see it fruitful for things like fuzz testing Wasm validation and runtime execution against the Wasm spec interpreter.

view this post on Zulip Andrew Brown (Aug 08 2022 at 15:01):

@Hero Bird, with a little bit of work, the wasm-spec-interpreter crate in Wasmtime (here) could be adapted and published on crates.io. Are you interested in that?

A standalone runtime for WebAssembly. Contribute to bytecodealliance/wasmtime development by creating an account on GitHub.

view this post on Zulip Robin Freyler (Aug 08 2022 at 15:13):

@Andrew Brown If the BytecodeAlliance team appreciates the idea I'd definitely be interested in publishing the wasm-spec-interpreter to crates.io. I could really use this for wasmi. :)

view this post on Zulip Andrew Brown (Aug 08 2022 at 15:17):

Well I think it's a fine idea personally, I think there's a couple of things to figure out:

view this post on Zulip Andrew Brown (Aug 08 2022 at 15:18):

I will bring this up in the Cranelift meeting in a few minutes to see what people think

view this post on Zulip Robin Freyler (Aug 08 2022 at 15:22):

Okay thanks a lot for this information and thanks for bringing up the idea at the next Cranelift meeting! :)
I'd just make the BytecodeAlliance the publisher of the crate as with all other BytecodeAlliance crates. Please keep me updated about this.

view this post on Zulip Robin Freyler (Aug 08 2022 at 15:24):

Maybe having an issue where we can discuss this would be valuable once the decision for this idea has been made.

view this post on Zulip Conrad Watt (Aug 08 2022 at 15:31):

Sorry if I've misunderstood, but will this be discussed at the Wasmtime meeting on the 18th? I can dial in.

EDIT: ah, I guess I missed the relevant call, no worries :)

view this post on Zulip Andrew Brown (Aug 08 2022 at 15:33):

Sure, I can add it as an agenda topic for the Wasmtime meeting as well

view this post on Zulip Conrad Watt (Aug 08 2022 at 15:34):

btw, the version of the interpreter I maintain has a command line switch that lets you use the "original" interpreter definitions

view this post on Zulip Conrad Watt (Aug 08 2022 at 15:34):

so there wouldn't be a strict need for any further configuration on that front

view this post on Zulip Conrad Watt (Aug 08 2022 at 15:35):

(although maybe some work is needed in the top-level interpret.ml file of the crate to expose this)

view this post on Zulip Robin Freyler (Aug 08 2022 at 15:54):

Where can I find a link to @Conrad Watt 's interpreter. Is this interpreter also meant to be a spec reference implementation of Wasm?

view this post on Zulip Conrad Watt (Aug 08 2022 at 16:13):

link: https://github.com/conrad-watt/spec/tree/wasmtime_fuzzing/interpreter

its story is a little more complicated - the interpreter is based on a logical model of the spec written in the Isabelle theorem prover - the model is the "reference", and the interpreter isn't meant to be directly readable, but instead trusted because there's a proof that it's correct wrt the model

paper: https://vtss.doc.ic.ac.uk/publications/Watt2021Two.pdf

WebAssembly specification, reference interpreter, and test suite. - spec/interpreter at wasmtime_fuzzing · conrad-watt/spec

view this post on Zulip Conrad Watt (Aug 08 2022 at 16:15):

this approach means I can implement optimisations without breaking the "trust story"

view this post on Zulip Andrew Brown (Aug 08 2022 at 16:17):

Ok, here is the agenda topic for the 18th: https://github.com/bytecodealliance/meetings/pull/12. @Hero Bird, can you make it to that meeting as well?

Contribute to bytecodealliance/meetings development by creating an account on GitHub.

view this post on Zulip Robin Freyler (Aug 08 2022 at 16:57):

@Conrad Watt Thanks for the link and explanations!
@Andrew Brown Never took part in such a meeting but I guess it is about time, right?

view this post on Zulip Conrad Watt (Aug 17 2022 at 20:18):

Unfortunately I've just found out that I'll only be able to join the meeting for the first 30 minutes. I'm very sorry about this, and if it turns out not to be enough time I'm happy to call/message anyone who's interested out-of-band.

view this post on Zulip Robin Freyler (Aug 18 2022 at 07:48):

@Andrew Brown Do I need to contact someone in order to participate in the meeting later or am I already signed up?

view this post on Zulip Andrew Brown (Aug 18 2022 at 13:20):

Not totally sure; perhaps contact @fitzgen (he/him)?

view this post on Zulip Robin Freyler (Aug 18 2022 at 13:23):

okay will do

view this post on Zulip Alex Crichton (Aug 18 2022 at 16:44):

I've created https://github.com/bytecodealliance/wasm-spec-interpreter for a repo here

view this post on Zulip Robin Freyler (Aug 19 2022 at 16:00):

Maybe I am just stupid but GitHub does not allow me to fork the repo or create a bare PR for it because the repo is empty.

view this post on Zulip Andrew Brown (Aug 19 2022 at 16:06):

I'll move the code there in a few minutes so we can get started...

view this post on Zulip Andrew Brown (Aug 19 2022 at 16:16):

@Robin Freyler, what is your GitHub handle?

view this post on Zulip Andrew Brown (Aug 19 2022 at 17:06):

never mind, I think I figured it out

view this post on Zulip Andrew Brown (Aug 19 2022 at 17:09):

@Robin Freyler, @Conrad Watt, @Alex Crichton: I could use some reviews on the setup of that repository, https://github.com/bytecodealliance/wasm-spec-interpreter/pulls. (Not sure what I did wrong in the CI infrastructure one because I thought it would run the CI even in the PR; maybe we need to merge it first to activate GitHub Actions?).

Contribute to bytecodealliance/wasm-spec-interpreter development by creating an account on GitHub.

view this post on Zulip Alex Crichton (Aug 19 2022 at 17:10):

you'll need to merge to main to trigger CI on future PRs

view this post on Zulip Alex Crichton (Aug 19 2022 at 17:10):

CI added just in a PR for the first time doesn't trigger a run automatically


Last updated: Dec 23 2024 at 13:07 UTC