filipeom

> What do you think about doing something like test-comp ? I.e. having the all Wasm code in a git submodule and just keep the OCaml code needed to run...

There's also the Gillian Debugger. It uses the DAP protocol https://vtss.doc.ic.ac.uk/publications/KarmiosAyoun2023SymbolicDebugging.pdf

I can look into it to see if I can share any insights ☺️

> I think it's definitely worth exploring, bench-marking is the best-way to know because it probably also depends on the tests you have and the kinds of operations they use....

> In particular, reaching Unsat is possible if someones does owi_assume(false) and then calls owi_assert(false). We should try to display something better. I don't understand this, if I do `owi_assume(false)`...

> Yes, I wrote owi_assume(false) to simplify. But here the idea was that @S41d was doing some solver-aided programming and added something that was actually unsat. I maybe was not...

Thanks! Very interesting. We tried doing something similar following https://dl.acm.org/doi/10.1145/2393596.2393665. But it was never merged https://github.com/formalsec/smtml/tree/caching, experimental results weren't great. It would be interesting to have a proper go at...

> mark our `getopt` as weak (as I believe we've already been doing for other functions) Maybe we should mark every symbol in our standard library as weak? It would...

Frederico was working on something similar: https://github.com/frediramos/LibcSummaries I don't know the current state of the project. But, our libc was a very early version of his work which I extended...

For `popcnt` I can add some dumb function to calculate it now. For `memory.blit` and `memory.fill` these should work well with the new memory model :smile: