The Coq mailing list

[Maxime Dénès <mail AT maximedenes.fr>]

Not much to add to Xavier's answer, except that vm_compute and
native_compute have a special status regarding trust in Coq's
distribution: they are not included in Coq's checker (coqchk).

I guess this was motivated by keeping the core TCB relatively small in
terms of lines of code. However, as pointed out by Xavier, empirical
data seem to indicate that these parts of the kernel are not less
trustworthy than others.

Also, these facilities are meant to be used when the regular interpreter
is not efficient enough. Used this way, they allow users to certify
computations that would otherwise remain unverified, actually increasing
confidence :)

Finally, one can know by inspecting a term if the VM or the native
compiler were used to typecheck it. We may one day provide a
fine-grained command that given a proof would tell the user what TCB
needs to be trusted.

Maxime.

On 10/06/2015 07:09 PM, Xavier Leroy wrote:
> On 30/09/15 17:44, Freek Wiedijk wrote:
>> On the CakeML developers mailing list, there was a mention of:
>> <http://gallium.inria.fr/blog/coq-eval/>
>> Then Magnus wrote; 
>> [...]
>>     I wonder what the trust issues are when computing with the
>>     VM/native mode within Coq. The jumps into and out of the VM/native
>>     mode sound scary regarding the trust story of the prover. Are
>>     these VM/native-mechanisms in fact not trusted and somehow
>>     cleanly separated from the trusted part of Coq's kernel?
> Normally, I'd let the authors of vm_compute and native_compute reply,
> but they are probably busy pumping water off their basements...
> (Big floods near Sophia-Antipolis recently.)
>
> The principles underlying vm_compute (the strong reduction strategy
> and the compilation scheme to VM code) were formalized and verified in
> Coq by Benjamin Grégoire in his PhD thesis.  The actual implementation
> of vm_compute is not formally verified, though, and, yes, it is part
> of the trusted kernel.  Empirically, based on the rate of discovery of
> proofs of False, it looks as reliable as the rest of the Coq
> implementation.
>
> This said, the experiment I mentioned in my blog post (execute
> CompCert within Coq using vm_compute) doesn't aim at 100% formal
> confidence of the CakeML kind.  Instead, it just aims at an alternate
> execution mechanism for CompCert that is independent from Coq's
> extraction and OCaml's compilation of the extracted code.  In the
> context of software certification using a combination of tests and
> formal methods, the existence of two independent implementations that
> produce the same results already has some certification value, not as
> high as a full formal verification, but not negligible either.
> (Motto: "if something is true for two independent reasons, that makes
> it more true!").
>
> Bas Spitters adds:
>
>> There are at least to projects trying to improve the level of trust:
>> http://www.maximedenes.fr/download/coqonut.pdf
>> https://www.cs.princeton.edu/~appel/certicoq/
> The Coqonut project (by Maxime Dénès and I) aims at equipping Coq with
> an evaluation mechanism that is both more efficient and more
> trustworthy than vm_compute and native_compute, via a
> formally-verified JIT compiler from Gallina to x86-64.  The project is
> at an early stage and we're lacking time and manpower to make it
> progress as fast as we'd like, so don't hold your breath.
>
> - Xavier Leroy