Follow-up from "Proto: Use saturated arithmetic to represent gas": Coq-of-ocaml / Property-based testing of `saturation_repr.ml`
The following discussion from !2329 (merged) should be addressed:
-
@clarus1 started a discussion: (+2 comments) Thinking about this MR, this seems to be a good use case to do some verification in Coq, and verify for example that the conversion to saturated arithmetic commutes with all the usual arithmetic operations.
Moreover, more generally, as many properties are expressed in the OCaml code of the tests, we could be able to convert these tests to boolean functions in Coq. Then we could verify them in the general case. That could be a way to increase the quantity of specifications in Coq by importing the ones in the OCaml tests.