Quinn (Jan 10 2022 at 15:03): Quinn (Jan 10 2022 at 15:03):has anyone used vst in production? any tips about navigating the compcert licensing in order to do so?
Théo Zimmermann (Jan 10 2022 at 15:12):Not me, but from what I understood, beyond learning, there isn't much that you can do in production without buying a CompCert license.
Alix Trieu (Jan 10 2022 at 15:14):Footnote 2 of this paper says that there seems to be industrial users of VST https://www.cs.princeton.edu/~appel/papers/ecosystem.pdf I don't know anything apart from that.
Karl Palmskog (Jan 10 2022 at 15:14):some caveats here, in particular regarding clightgen: https://github.com/palmskog/coq-program-verification-template#generating-clight-for-coq
Michael Soegtrop (Jan 10 2022 at 16:33):You need to buy a license for Clightgen from AbsInt, but not for CompCert. Clightgen is typically licensed on a per project basis and these project based are not expensive (< 1 engineer man month).
For evaluating purposes - that is for checking if you actually can do what you want - you can use Clightgen based on the evaluation terms. As far as I can tell use for code which is intended for production but not yet used in production is fine, but I would recommend to discuss with AbsInt what they deem to be evaluation.
Karl Palmskog (Jan 10 2022 at 16:39):on the other hand, if you license clightgen and not ccomp, then you will have a "trust gap" between the code you verify and the code you compile
Karl Palmskog (Jan 10 2022 at 16:40):@Michael Soegtrop is there actually any realistic workflow right now where one can compile the code generated by clightgen using CompCert, and not the pre-clightgen code?
Michael Soegtrop (Jan 10 2022 at 16:40):Well yes, but IMHO clightgen + VST is the first step and CompCert the second. I think if you can prove to your management that you can wrangle VST, they will give you the money for CompCert as well.
Karl Palmskog (Jan 10 2022 at 16:43):yeah a clightgen license should allow one to do anything with VST without worry (since VST is not compiling anything)
Michael Soegtrop (Jan 10 2022 at 16:43):@Karl Palmskog : as far as I know not. IMHO it would also make sense to not use extracted OCaml CompCert, but to run it in Coq - it should be fast enough for "final builds".
Karl Palmskog (Jan 10 2022 at 16:45):sure, then you avoid trusting the runtime system and linking and so on, but the CakeML experience shows that ITP-hosted compilation tends to be really slow (CakeML bootstrapping takes a full day!). Maybe if it could be run with native compilation inside Coq
Michael Soegtrop (Jan 10 2022 at 16:45):Well native compilation also uses the OCaml system, doesn't it?
Karl Palmskog (Jan 10 2022 at 16:46):well, at least in a more predictable way than ccomp, right?
Michael Soegtrop (Jan 10 2022 at 16:48):But I would think VM compute might be fast enough - I am usually more impressed by what it can do rather than the other way around. And for final production builds it doesn't matter much if it takes a few hours and ccomp now supports separate compilation.
Michael Soegtrop (Jan 10 2022 at 16:49):It might be faster than checking the VST proofs ...
Karl Palmskog (Jan 10 2022 at 16:49):one might say: we have practically no hope of verifying OCaml and its runtime system anytime soon, but vm_compute and native_compute might become within reach (compare CertiCoq)
Michael Soegtrop (Jan 10 2022 at 16:50):yes, this is true.
Karl Palmskog (Jan 10 2022 at 16:52):but anyway, getting code into VST and specifying it and verifying it is such a large part of obtaining the verified program, that the final compilation is arguably a minor quibble
Karl Palmskog (Jan 10 2022 at 17:01):to verify native_compute, one could probably go for translation validation...
Bas Spitters (Jan 11 2022 at 17:17):There's a nice overview paper on using compcert in a nuclear powerplant. Hopefully shouldn't be too hard to find.
Alexander Gryzlov (Jan 11 2022 at 18:28):I guess this one https://www.absint.com/mtu_fh.htm ?
Last updated: Sep 25 2023 at 12:01 UTC