Wolfgang Meier

wat2wasm segfaults on .wat file with many nested if statements

9

Running `wat2wasm` on a rather big file with many nested if-statements segfaults. Version: wabt 1.0.32-1 (debian bookworm) System: Debian (with enough RAM + swap) Steps to reproduce: ``` wasm2wat CertiCoq.Benchmarks.tests.color.wasm...

correctness proof of Codegen doesn't compile

3

The proof of correctness for Codegen doesn't compile with Coq 8.14.1 it is also not included in the CI build (has never been?) for now it would help to know...

Tail call proposal

7

This PR adds support for the tail call proposal: https://webassembly.github.io/tail-call/core/ ### TODO - [x] opsem - [x] types, typechecking, progress, preservation - [x] old interpreter (interpreter_func) - [ ] cleanup:...

### Description The `wasm-bindgen` build command succeeds, but the generated binary crashes with `RuntimeError: memory access out of bounds`. `main.rs` is generated by the https://github.com/AU-COBRA/coq-rust-extraction plugin, it could be a...

Update to MetaCoq 1.3

7

I was looking into extracting the counter module to concordium, using our Wasm [backend](https://github.com/womeier/certicoqwasm) for CertiCoq. CertiCoq is currently on [MetaCoq 1.3](https://github.com/MetaCoq/metacoq/releases/tag/v1.3-8.17), which ConCert doesn't seem to work with. Do...

### Description of the problem The snippet below fails with: ``` : Anomaly "Uncaught exception Not_found." Please report at http://coq.inria.fr/bugs/. : Uncaught exception Type_errors.TypeError(_, _). ``` If line 11 is...