aboutsummaryrefslogtreecommitdiff
path: root/README.md
blob: b11cb2d656d5862c4e87cbda3c2a7a2fb01dc2bc (plain)
1
2
3
4
5
6
7
8
9
10
11
Synthesizing Correct-by-Construction Assembly for Cryptographic Primitives
-----

... which would make a good paper title.

To build:

	git clone git@github.mit.edu:plv/bedrock.git
	( cd bedrock && make Bedrock/Word.vo )
	( cd coqprime && make PrimalityTest/Zp.vo PrimalityTest/PocklingtonCertificat.vo )
	make