What's Coq's TCB?
kernel/*.ml ? What's
checker/ is for coqchk
The TCB should also include the dependencies of kernel/ (some stuff in ocaml stdlb, lib/ and clib/)
what is coqchk? can it be used to check generated proofs?
found it https://coq.inria.fr/refman/practical-tools/coq-commands.html?highlight=coqchk#compiled-libraries-checker-coqchk
I guess it would be a bit of a stretch to call coqchk the TCB since one can't tell what it actually checks without knowing how the
.vos got generated, i.e. if the file
foobar.vo contains the proofs corresponding to the theorems stated in
seems like a quite narrow view of TCB to only consider (implementation) code. There are more operational notions of what TCB means here: https://www.ssi.gouv.fr/uploads/2014/11/anssi-requirements-on-the-use-of-coq-in-the-context-of-common-criteria-evaluations-v1.1-en.pdf
quite out of date list of some additional things here: https://github.com/coq/coq/wiki/Presentation#what-do-i-have-to-trust-when-i-see-a-proof-checked-by-coq
Philipp: you can load vo files via Require and inspect their content. Looking at the source isn't necessarily enough, since the statements are the output of elaboration, not just parsing
Would you want to use that to check the 4-color theorem statement is correct?
Even if the alternative means trusting Coq's raw printers, or risking Pollack inconsistency and friends
for a serious audit, I think any tool is on the table, including
Technically you could dump the low-level term representation in votour (we already have debug tools for that) if you really fear Pollack inconsistencies.
True of course. I guess I don't know any reason to use that over Set Printing All, About etc., but I'd change my mind if those pretty printers were more fragile than I think. Maybe we'd want an option to fully qualify all identifiers in output
The pretty-printer is not 100% injective, even with all flags sets. I'd be personally concerned about module shenanigans à la https://github.com/coq/coq/issues/7609.
I'm (personally) not worried about Pollack inconsistencies. I want to trust my own code, or that of someone acting without malicious intent (otherwise there's a quick near infinite regress that includes anecdotes about backdoors planted in C compilers decades ago). For that purpose, it seems indeed that the 3000 lines making up
coqchk serve the purpose pretty well.
note that coqchk depends on part of kernel/
oh, thanks for pointing that out @Gaëtan Gilbert
okay, including the dependencies on kernel/ we're up to a more substantial 18.000 lines for coqchk
are we playing the TCB LOC game? In that case, you can do the Metamath thing and put variable binding outside the checker/core to drop hundreds of LOC, but is that a good idea in general?
Last updated: Oct 04 2023 at 22:01 UTC