The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 08/19/2016 01:40 PM, Robbert Krebbers wrote:
> A way to remedy the issue you describe is to extend coqchk with 
> functionality to print the statement of a lemma and all of the 
> definitions that are used in the statement of that lemma. That way, 
> you can audit that the proof in the .vo file is in fact a proof of the 
> lemma you are interested in.

How complex would this have to be?  And how difficult would it be to do 
the decompilation?  Would you even recognize the decompiled lemma as the 
one you intended, based on all that would need to be omitted (notations, 
implicits, unicode translations, coercions, etc.)?

Also - couldn't you do the following instead: write a test module that 
Requires the target module and checks the types of the lemmas in the 
target module, and make sure that this test module is compiled without 
any plugins.  Perhaps a mode of coqc that refuses to load plugins is all 
that is required...

-- Jonathan

> On 08/19/2016 07:08 PM, Ralf Jung wrote:
> > Hi,
> >
> > [Warning: digression ahead.]
> >
> > On 19.08.2016 18:37, Jonathan Leivent wrote:
> > > For coqchk the issue is that it checks module "inclusion", not actual
> > > definition usage.  Hence it will report that axioms are "present' when
> > > Print Assumptions (even without plugin misbehavior) does not. But, it
> > > doesn't load plugins, hence is safe from "plugin misbehavior".
> >
> > Is this actually true? Sure coqchk does not load plugins, but that still
> > leaves the question open of what coqchk is actually checking. As far as
> > I understand, it checks the .vo files, so if a plugin manages to make
> > "good" .vo files from "bad" .v files, coqchk would not catch that.  For
> > example, the plugin could alter the statement that has been proven such
> > that the .vo file contains a valid proof of *some* statement (but not
> > the one the user wants), and the .v files contains an *invalid* proof
> > (messed with by the plugin) of the statement the user wants.
> >
> > It's not like I have any thoughts on how to remedy this, but I feel like
> > saying "malicious plugins can't harm you if you use coqchk" isn't
> > actually true. Admittedly, it is very unlikely for an accidental bug in
> > a plugin to trigger this.
> >    Or maybe this falls into the same category as "Definition False :=
> > True", though "don't Import/Export any modules / fully qualify
> > everything" doesn't help if the plugin is messing with the parser and
> > pretty-printer.
> >
> > Kind regards,
> > Ralf