# Consequences of technically proving anything in Coq (exploiting a bug)? [closed]

Technically, it is possible to prove anything in Coq proof assistant http ://coq.inria.fr due to a programming feature (or bug). This seems tractable when validating large proofs. Human analysis may catch this.

Question:

What are the consequences of technically proving anything in Coq?

More or less the question had in mind dishonest human provers presenting seemingly valid long computer readable proofs.

Later Coq developers replied little hack'. I saw no official plans or replies of breaking the well formed proof (possibly because of backward compatibility being priority).

The basic technical details are: Hostile ocaml plugins (possibly disguised as proofs in FILE.v) can generate their own .vo proofs (of trivial statements), thus subverting coqchk, and don't giving a chance of "coqc" to even see the "anything proof". The plugin does this with exit(2) after writing .vo. This scenario seems interesting when validating large archives.

Here is a sample session, including links to full source code:

 joro@j:/tmp/test1$tar xvf ../proof.tar fib5.v bLOB joro@j:/tmp/test1$ ls -l
total 16
-rwxr-xr-x 1 joro joro 10301 2011-05-03 12:53 bLOB
-rw-r--r-- 1 joro joro   125 2011-05-03 12:53 fib5.v
joro@j:/tmp/test1$coqc fib5.v Trivially true. coqchk may pass joro@j:/tmp/test1$ ls -l
total 24
-rwxr-xr-x 1 joro joro 10301 2011-05-03 12:53 bLOB
-rw-r--r-- 1 joro joro    51 2011-05-03 12:55 fib5.glob
-rw-r--r-- 1 joro joro   125 2011-05-03 12:53 fib5.v
-rw------- 1 joro joro   812 2011-05-03 12:55 fib5.vo
joro@j:/tmp/test1$coqchk fib5 Welcome to Chicken 8.2pl1 (February 2010) [intern /tmp/test1/fib5.vo ... done] ...snip... Checking library: fib5 *** vo structure validated *** checking cst: <>.fib5.thm1 checking cst: <>.fib5.really Modules were successfully checked joro@j:/tmp/test1$cat fib5.v
Theorem thm1: True.
Proof.
auto.
Qed.
Declare ML Module "bLOB" .
Theorem really: True = False.
Proof.
intuition.
Qed.
#note: there is a zero byte at the end of "bLOB". in addition "bLOB" may be "aux.v"
joro@j:/tmp/test1$coqchk -v The Coq Proof Checker, version 8.2pl1 (February 2010) compiled on Feb 27 2010 16:09:50  to compile the plugin: ocamlopt -o bLOB -shared a.ml the plugin writes valid but unrelated .vo proof and then does exit(2) to prevent coqc from analyzing the "anything proof". a.ml is here tar with the proof is here Possibly the most likely exploit scenario is: Here is a proof of X consisting of about$10^5\$ files. lemma2817.v is the plugin and it doesn't stop the final proof.

Update Possibly a more portable solution (Coq):

Theorem really: True = False.
Proof.
external "/bin/sh" "ESCAPE_SEQ; write_vo_proof; nicely_kill_coq ;" True.
(* this invokes /bin/sh *)
Qed.


tactic external'

-
Dear joro, Is this feature/bug well-known? (Or was it so before now?) Regards, – Matt E May 3 '11 at 14:17
Most likely consequence is that the next version will need some work. – Asaf Karagila May 3 '11 at 14:18
This question amounts to a quite peculiar use of MSE. – Did May 3 '11 at 14:34
I think the response you received on MO makes sense: this isn't really a mathematics question, and you should just report the bug. Closed. – Qiaochu Yuan May 3 '11 at 22:52
the MO thread is at mathoverflow.net/questions/63816 – jorox May 9 '11 at 11:21

## closed as off topic by Asaf Karagila, Did, Qiaochu YuanMay 3 '11 at 22:52

Questions on Mathematics Stack Exchange are expected to relate to math within the scope defined in the FAQ. Consider editing the question or leaving comments for improvement if you believe the question can be reworded to fit within the scope. Read more about closed questions here.