qcert
qcert copied to clipboard
querycert
Compilation and Verification of Data-Centric Languages
and we need a new CI... CircleCI doesn't know how to install opam / ocaml / coq anymore _Originally posted by @jeromesimeon in https://github.com/querycert/qcert/issues/162#issuecomment-916438193_ I set up Github Action CI...
The current Wasm backend is implemented in OCaml and translates from Imp to the [AST](https://github.com/WebAssembly/spec/blob/opam-1.0.1/interpreter/syntax/ast.ml) used in the Webassembly reference implementation. Doing `Imp -> Wasm` in OCaml was fine for...
Part of #153. ### Operators - [x] EJsonOpNot - [x] EJsonOpNeg - [x] EJsonOpAnd - [x] EJsonOpOr - [x] EJsonOpLt - [x] EJsonOpLe - [x] EJsonOpGt - [x] EJsonOpGe -...
I'm implementing the last operators for the wasm runtime. I came across the implementation of `EJsonRuntimeCompare` in `qcert-runtime-core.js`. It looks a bit suspicious to me. I cannot judge whether it's...
While working on a different issue, I skimmed the following lines. The use of `LocalGet` / `LocalSet` where we want to handle global variables is almost certainly a bug. https://github.com/querycert/qcert/blob/9969786b1d72672e990a2fe54ef63ad59cec97d5/compiler/wasm/wasm_ir.ml#L261-L265...
The Wasm runtime is implemented in Assemblyscript which is a typescript variant. It might be possible to compile the Assemblyscript runtime to Javascript and reuse it for the JS backend.
When translating Imp to Webassembly, I stumbled upon a small oddity in `EJsonRuntimeOperators.v`. ``` Section Evaluation. ... | EJsonRuntimeCompare => apply_binary (fun d1 d2 => match d1, d2 with |...
JSON is used both at run time (to parse input data and produce outputs), and at compile time (notably generation of Cloudant Map/Reduce views). The JSON support is split in...
The SQLDate foreign type lacks an ocaml implementation, so our evaluators written coq generally choke on anything that contains the type. Ideally, there would be a true implementation in ocaml....
