-
Notifications
You must be signed in to change notification settings - Fork 9
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
WASM: W-Imp intermediate representation #146
Labels
Comments
Closed
This was referenced Aug 29, 2020
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
The current Wasm backend is implemented in OCaml and translates from Imp to the AST used in the Webassembly reference implementation.
Doing
Imp -> Wasm
in OCaml was fine for quickly providing a seemingly working Webassembly backend. However, the gap between Imp and Wasm is quite big. The former was designed to resemble Javascript, the latter is much more low level. In the long run, it might be worth narrowing this gap by adding a more Wasm-like intermediate representation to Q*Cert.My incomplete wish-list for W-Imp:
listing free variables in blocks would allow to translate Imp blocks to Wasm functionsnot true because Wasm functions can return only one value.EJsonOperator
andEJsonRuntimeOperator
into a singleWasmOperator
. Avoid ADT features,WasmOperator
should be an enumeration.type wasm_model = string ejson
).On a later stage:
WasmOperator
with(namespace, opname) : (string * string)
. We import operators from the runtime anyway and this is all information we need. Most operators will havenamespace = "runtime"
to call into theruntime.wasm
, but certain operators might be provided by the environment (e.g. logging) or separate wasm modules.(string * string) -> WasmOperator
to test functional equivalence of compiled Wasm contracts linked with operators implemented in Coq/OCaml versus operators implemented in the productionruntime.wasm
.The text was updated successfully, but these errors were encountered: