GSoC 2020: Webassembly backend #147

pkel · 2020-08-30T16:41:14Z

I worked on translating Ergo smart contracts to Webassembly (Wasm) as part of Google Summer of Code (GSoC) 2020. You can find an overview of my project in PR #777 on the Ergo repo. TL;DR: Ergo adds a smart contract language frontend to the Q*cert compiler. I extend Q*cert with a proof-of-concept Webassembly backend.

This PR constitutes my GSoC project submission. It's meant to be frozen on the GSoC deadline on 8/31/2020. Future edits should go to Jerome's working PR #142.

In the following, I will try to wrap up some technical aspects of my implementation.

Overview

The Wasm specification contains a reference implementation in OCaml. I implement a translation from Imp(Ejson) to the Wasm reference Ast. We also hook up the reference interpreter as Q*Cert evaluation function for testing. All my code is OCaml and not verified. Jerome did some plumbing on the Coq side.

Preliminaries

We add the opam dependency wasm.1.0.1.
We switch to separate extraction to circumvent cyclic dependencies between Coq and OCaml.

Code generation and evaluation

Code generation and evaluation is implemented in /compiler/wasm/. The main component is the functor in wasm_backend.ml which is instantiated in wasm_ast.ml. The latter provides all functions necessary to extend Q*cert with a new Wasm_ast language target. The functorization is needed since Ergo's extracts its own Imp and OCaml cannot infer their equality.

The translation functions in wasm_backend.ml rely on an incomplete intermediate representation for Wasm (wasm_ir.mli). In Wasm, functions, types, and variables are addressed by their integer index within the module. The IR replaces these integers with OCaml variables for more convenient addressing. It also provides concise constructors for Wasm AST elements.

Another convenience module is wasm_util.ml. It contains a small lookup table implementation based on Hashtable which is used all over the place to get from OCaml values to integer indexes.

In contrast to Imp's block-scoped variables, Wasm has only function-scoped variables. The translation in wasm_backend.ml does not take this into account and relies on unique variable names. We pre-process the Imp using the translation in wasm_imp_scoping.ml in order to resolve this conflict (see #145).

I implement a binary encoding for EJson values in wasm_binary_ejson.ml. This encoding is used for storing constants in the linear memory of the generated Wasm module. It's also used at runtime for communication between the interpreter and the runtime module (see Ergo PR #777). I briefly describe the encoding in the header of source file.

Runtime

The generated wasm module relies on a Wasm runtime for execution (see Ergo PR #777). This runtime is implemented in Assemblyscript (NPM ecosystem) and lives in /runtimes/assemblyscript/. We build the runtime with npm run asbuild:untouched and run some tests with npm test. The Assemblyscript source resides in assembly/index.ts, the compiled Wasm in build/untouched.wasm.

We add a dune rule that encodes the binary runtime build/untouched.wasm into an wasm_runtime.ml file and bundles it into wasm_backend.ml.

Tests

We provide some rudimentary tests under /tests/imp_ejson/ which can be run all at once using the command make -C tests wasm-imp-spec. The tests evaluate pieces of Imp(Ejson) on a given input in order to produce the expected output. Then the Imp code gets translated to Wasm and executed with the same input on the Wasm reference interpreter. The resulting output is compared with the expected output (should be equal).

Issues

We do not support all Imp operators (WASM: Priority list of runtime & operators #133).
It might be useful to verify some aspects of the new backend (WASM: W-Imp intermediate representation #146).
We should better integrate the new tests with the existing tests.
After supporting all operators, we should run all existing tests on the Wasm backend.
We have to double check that the operators are implemented in a functional way (no mutation) (WASM: Functional Operators #148).

Signed-off-by: Jerome Simeon <[email protected]>

Signed-off-by: Patrik Keller <[email protected]>

I'm struggling with RuntimeOpRecDot. make -C tests wasm I need debugger access to the generated wasm and provided ejson argument.

This PoC demonstrates how Assemblyscript could be used to implement a runtime for imp_ejson. The next step on this road would be to implement a pair functions that read/write JS Ejson from/to Assemblyscript's managed memory.

This commit adds a pair of functions that read/write JS Ejson from/to Assemblyscript's managed memory. Executing a imp function compiled to wasm is now easy. Next steps: - Test the set op implemented operators. - Hook the new runtime into the compiler pipeline.

The runtime allows to run qcert queries compiled to wasm modules in chrome. DevTools enable stepwise debugging. This predates the recent effort to implement the IMP operators in Assemblyscript.

This commit removes the Imp(Wasm) runtime operators that have been implemented before. Instead we call imported functions. These functions are defined in an Assemblyscript module. As a side effect, we lost support for constants and EjsonRuntimeOperator(s). Next steps: - Unit test the set op implemented operators. - Provide engine that links the compiled module with the runtime. - Compile constants - Support EjsonRuntimeOperator(s).

This commit add a PoC engine that executes a compiled to wasm qcert query on NodeJS. It dynamically links the IMP runtime that we implement in AssemblyScript and compile to a separate wasm module.

We can compile the following OQL queries: 3.14 not (true or false) 3.14 <. 4.5 pi pi <. e greet And execute them on input: { "pi" : 3.14, "e" : 2.72, "greet" : "Hello World!" }

Before, each use of an IMP constant lead to a fresh allocation in the AssemblyScript runtime. Additionally, strings were entirely encoded in the AST (as function that allocate and inititalize the corresponding string in the runtime). Now, constants are serialized into the linear memory of the compiled module. On first use, a corresponding value is allocated in the memory of the AssemblyScript runtime. Repeated use of a constant uses the same value on the runtime side.

We now use the AssemblyScript runtime. The old runtime is not needed anymore.

- Make explicit, that be transfer bytes of an UTF8 string. - Allocate a single, correctly sized buffer on the runtime side.

Avoids headache on Javascript/Wasm interface.

Signed-off-by: Jerome Simeon <[email protected]>

- fixes incompatibility with node ("invalid block type error" when loading compiled wasm module) - removes dependencies to wat2wasm/wasm2wat

Before, if-then-else became if-then-then Signed-off-by: Patrik Keller <[email protected]>

Q*cert's `EJsonRuntimeCompare a b` returns sign(b - a). Before this fix the Wasm implementation of this operator returned sign(a - b). Signed-off-by: Patrik Keller <[email protected]>

Signed-off-by: Jerome Simeon <[email protected]>

Signed-off-by: Patrik Keller <[email protected]>

Signed-off-by: Jerome Simeon <[email protected]>

- derive the expected output from Imp eval. - avoid bash for loop for iteration

Signed-off-by: Jerome Simeon <[email protected]>

- add a small binary (tools/binary_to_string.(ml|exe) that escapes a binary string to a valid OCaml string using hex codes. - add a dune rule that reads binary runtime.wasm into a generated ml file. - use the resulting OCaml value in for the wasm spec eval.

Signed-off-by: Jerome Simeon <[email protected]>

pkel · 2021-02-18T16:48:22Z

Some other pages link to this PR as my GSoC project report. Let's keep it as is. We can track progress in #153.

jeromesimeon and others added 30 commits August 13, 2020 15:00

feature(wasm) per-module extraction and add wasm_ast to compiler

7576568

Signed-off-by: Jerome Simeon <[email protected]>

feature(wasm) Add preliminary wasm backend

f122f29

Signed-off-by: Patrik Keller <[email protected]>

Compile a few more operators and add testing

6b36856

I'm struggling with RuntimeOpRecDot. make -C tests wasm I need debugger access to the generated wasm and provided ejson argument.

Fix ejson object & array allocation.

8fb58c5

Implement Ejson operators in AssemblyScript.

53f5d55

This PoC demonstrates how Assemblyscript could be used to implement a runtime for imp_ejson. The next step on this road would be to implement a pair functions that read/write JS Ejson from/to Assemblyscript's managed memory.

Add debugging runtime for pre Assemblyscript modules.

7076c71

The runtime allows to run qcert queries compiled to wasm modules in chrome. DevTools enable stepwise debugging. This predates the recent effort to implement the IMP operators in Assemblyscript.

Compile constants (not strings and foreign)

a70299d

Link runtime with compiled module and execute.

1379e77

This commit add a PoC engine that executes a compiled to wasm qcert query on NodeJS. It dynamically links the IMP runtime that we implement in AssemblyScript and compile to a separate wasm module.

Compile string constants and parts of EJsonRuntimeOperator.

7ad82db

We can compile the following OQL queries: 3.14 not (true or false) 3.14 <. 4.5 pi pi <. e greet And execute them on input: { "pi" : 3.14, "e" : 2.72, "greet" : "Hello World!" }

CircleCI update OCaml and add wasm dependency

c68d7a2

Delete redundant OCaml modules.

9aa0400

We now use the AssemblyScript runtime. The old runtime is not needed anymore.

Improve String constant allocation.

f1eb4a1

- Make explicit, that be transfer bytes of an UTF8 string. - Allocate a single, correctly sized buffer on the runtime side.

High priority runtime operators (#133).

3174793

Add some unit tests for a subset of operators

ccc9389

Compile BigInt's as f64.

df300cd

Avoids headache on Javascript/Wasm interface.

Test runtimeCompare operator on BigInt. Fix BigInt write.

2b3c277

Test runtimeRecConcat and runtimeRecDot.

c4161fe

Test runtime operators Either / ToLeft / ToRight.

90c0816

WIP(Imp) An ImpEJson parser proof of concept

017592a

Signed-off-by: Jerome Simeon <[email protected]>

WIP(imp) Generalizes runtime calls in imp parser

0e6853b

Signed-off-by: Jerome Simeon <[email protected]>

WIP(imp) functions always contain a block, more tests

9cb1fb0

Signed-off-by: Jerome Simeon <[email protected]>

WIP(Imp) Add objects / array constructors to parser + more tests

f3e166c

Signed-off-by: Jerome Simeon <[email protected]>

fix(test) Remove generated files from tests

1ea8403

Signed-off-by: Jerome Simeon <[email protected]>

Compile if statements

3c319db

Compile for loop (range style)

a335198

Compile for loops (for each style)

991d4dc

Fix type of opMathTrunc

47b4bb7

pkel and others added 22 commits August 18, 2020 11:29

Downgrade to wasm.1.0.*

a3fb170

- fixes incompatibility with node ("invalid block type error" when loading compiled wasm module) - removes dependencies to wat2wasm/wasm2wat

Fix wasm version in CircleCI config

54ac529

fix(WASM) compilation of if-then-else

10959a8

Before, if-then-else became if-then-then Signed-off-by: Patrik Keller <[email protected]>

fix(WASM) flip sign of EJsonRuntimeCompare

9949570

Q*cert's `EJsonRuntimeCompare a b` returns sign(b - a). Before this fix the Wasm implementation of this operator returned sign(a - b). Signed-off-by: Patrik Keller <[email protected]>

fix(wasm) Add float to nat conversion to runtime

fa77ae6

Signed-off-by: Jerome Simeon <[email protected]>

fix(wasm) Uses <i64> casting syntax for integer coercion in runtime

6094f56

Signed-off-by: Jerome Simeon <[email protected]>

Rename Imp variables for wasm function scoping (OCaml)

8766b38

Signed-off-by: Patrik Keller <[email protected]>

fix(wasm) Fixes some tests

d1b56dd

Signed-off-by: Jerome Simeon <[email protected]>

test(wasm) One more block scoping test for wasm

49dd640

Signed-off-by: Jerome Simeon <[email protected]>

fix(test) comments

83f555c

Signed-off-by: Jerome Simeon <[email protected]>

chore(wasm) clean-up imp_ejson tests

2dfff08

- derive the expected output from Imp eval. - avoid bash for loop for iteration

fix(wasm) return None on failed eval

4739dd6

fix(wasm) cast operator does not change the object

eb30829

chore(wasm) remove unmaintained OQL->wasm tests

06a5a9b

feature(wasm) Add union and distinct to runtime

0a8f2ae

Signed-off-by: Jerome Simeon <[email protected]>

fix(wasm) Catches errors in cli-runner invoke

68f55b6

Signed-off-by: Jerome Simeon <[email protected]>

fix(wasm) Slightly more consistent error

ed33829

Signed-off-by: Jerome Simeon <[email protected]>

fix(wasm) more on cli-runner error

8f674ad

Signed-off-by: Jerome Simeon <[email protected]>

fix(wasm) Another fix to error in cli-runner.js

507a7f7

Signed-off-by: Jerome Simeon <[email protected]>

feature(wasm) Add array flatten to runtime

aec1b75

Signed-off-by: Jerome Simeon <[email protected]>

fix(build) build runtimes before compiler

26dd1ef

Signed-off-by: Jerome Simeon <[email protected]>

pkel mentioned this pull request Aug 30, 2020

GSoC 2020: Webassembly backend for the Ergo compiler accordproject/ergo#777

Closed

fix(wasm) promote generated wasm_runtime.ml to source dir

8381ed4

pkel marked this pull request as ready for review August 31, 2020 16:33

jeromesimeon mentioned this pull request Sep 1, 2020

WebAssembly Backend #142

Closed

pkel mentioned this pull request Feb 18, 2021

Webassembly backend #153

Merged

pkel closed this Feb 18, 2021

jeromesimeon deleted the gsoc2020-wasm branch May 19, 2022 21:16

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

GSoC 2020: Webassembly backend #147

GSoC 2020: Webassembly backend #147

pkel commented Aug 30, 2020 •

edited

Loading

pkel commented Feb 18, 2021

GSoC 2020: Webassembly backend #147

GSoC 2020: Webassembly backend #147

Conversation

pkel commented Aug 30, 2020 • edited Loading

Overview

Preliminaries

Code generation and evaluation

Runtime

Tests

Issues

pkel commented Feb 18, 2021

pkel commented Aug 30, 2020 •

edited

Loading