Philipp G. Haselwarter (Apr 26 2023 at 11:01): Philipp G. Haselwarter (Apr 26 2023 at 11:01):What's Coq's TCB? kernel/*.ml ? What's checker/ ?
Gaëtan Gilbert (Apr 26 2023 at 11:07):checker/ is for coqchk
The TCB should also include the dependencies of kernel/ (some stuff in ocaml stdlb, lib/ and clib/)
Philipp G. Haselwarter (Apr 26 2023 at 11:08):what is coqchk? can it be used to check generated proofs?
Philipp G. Haselwarter (Apr 26 2023 at 11:12):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 foobar.v.
Karl Palmskog (Apr 26 2023 at 12:41):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
Karl Palmskog (Apr 26 2023 at 12:42):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
Paolo Giarrusso (Apr 26 2023 at 17:41):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
Karl Palmskog (Apr 26 2023 at 17:48):votour?
Paolo Giarrusso (Apr 26 2023 at 18:04):Would you want to use that to check the 4-color theorem statement is correct?
Paolo Giarrusso (Apr 26 2023 at 18:05):Even if the alternative means trusting Coq's raw printers, or risking Pollack inconsistency and friends
Karl Palmskog (Apr 26 2023 at 18:47):for a serious audit, I think any tool is on the table, including Require and votour
Pierre-Marie Pédrot (Apr 26 2023 at 18:56):Technically you could dump the low-level term representation in votour (we already have debug tools for that) if you really fear Pollack inconsistencies.
Paolo Giarrusso (Apr 26 2023 at 19:33):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
Pierre-Marie Pédrot (Apr 26 2023 at 20:13):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.
Philipp G. Haselwarter (Apr 26 2023 at 20:26):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.
Gaëtan Gilbert (Apr 26 2023 at 20:27):note that coqchk depends on part of kernel/
Philipp G. Haselwarter (Apr 26 2023 at 20:27):oh, thanks for pointing that out @Gaëtan Gilbert
Philipp G. Haselwarter (Apr 26 2023 at 20:42):okay, including the dependencies on kernel/ we're up to a more substantial 18.000 lines for coqchk
Karl Palmskog (Apr 27 2023 at 07:44):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 13 2024 at 01:02 UTC