Home page logo
/

fulldisclosure logo Full Disclosure mailing list archives

proving _anything_ in the Coq proof assistant (in addition to code execution). ``coqchk'' passes too
From: Georgi Guninski <guninski () guninski com>
Date: Tue, 3 May 2011 13:34:16 +0300

proving _anything_ in the Coq proof assistant (in addition to code execution). ``coqchk'' passes too

if some poor soul needs help with a coq [1] homework, this may help.

if some poor AV vendor need a proof his solution is bullet proof this may help too...

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$ tail fib5.v
Theorem really: True = False.
Proof.
  intuition.
Qed.


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

a.ml is at: http://j.ludost.net/blog/misc/a.ml
tar with the proof is at: http://j.ludost.net/blog/misc/proof.tar

[1] http://coq.inria.fr/

_______________________________________________
Full-Disclosure - We believe in it.
Charter: http://lists.grok.org.uk/full-disclosure-charter.html
Hosted and sponsored by Secunia - http://secunia.com/


  By Date           By Thread  

Current thread:
[ Nmap | Sec Tools | Mailing Lists | Site News | About/Contact | Advertising | Privacy ]
AlienVault