search

WasmCert / WasmCert-Coq

A mechanisation of Wasm in Coq
MIT License
92 stars 11 forks source link

Machine integers #53

Open spitters opened 1 month ago

spitters commented 1 month ago

There may be a possibility to avoid duplication... https://github.com/coq/coq/pull/17043

raoxiaojia commented 2 weeks ago

Thanks for the visibility there -- given that we are basically implementing a wrapper on CompCert numerics, maybe the real question there is whether to merge that as part of the base stdlib of Coq...

andres-erbsen commented 2 days ago

Yes, I am working Zmod (including machine integers) for Coq stdlib. The current status is that the implementation and theory is in good shape, and sufficient for use in several Coq-CI developments, but I have not ported compcert (and it seems like it would not be trivial due to even high-level proofs there unfolding their machine-integer definitions). IMO importing the CompCert implementation to stdlib would be less desirable for projects that do not already depend on it (and I've also been given the sense that bulk imports of old code are less desirable than stdlib-first develpoment in general). I am quite invested in having a Coq-CI-wide Zmod/machineint library and would welcome any collaboration, especially on seeing whether what I have works for your development. Confidence that the current library will work widely is the main thing missing from me submitting it for merge.