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...

[Feature request] get passwords/TOTP via system tray menu

1

I was happy with the old app for >5 years, never had serious issues. With the new app and NK3, it seems one can't (yet) run the app in the...

When adding new passwords, the old app has a button to generate random passwords. I'm missing this in the new app. thanks!