From 2c7b377febf9f42de6c7313dfe4154efdfb90da1 Mon Sep 17 00:00:00 2001
From: Robert Sloan <varomodt@dhcp-18-189-51-40.dyn.MIT.EDU>
Date: Thu, 10 Sep 2015 18:52:17 -0400
Subject: init our centralized repo

---
 .make/cc.mk             | 20 ++++++++++++++++++++
 .make/coq.mk            | 24 ++++++++++++++++++++++++
 Makefile                | 23 +++++++++++++++++++++++
 README.md               | 13 +++++++++++--
 _CoqProject             |  3 +++
 src/Curves/Curve25519.v | 13 +++++++++++++
 6 files changed, 94 insertions(+), 2 deletions(-)
 create mode 100644 .make/cc.mk
 create mode 100644 .make/coq.mk
 create mode 100644 Makefile
 create mode 100644 _CoqProject
 create mode 100644 src/Curves/Curve25519.v

diff --git a/.make/cc.mk b/.make/cc.mk
new file mode 100644
index 000000000..58724089a
--- /dev/null
+++ b/.make/cc.mk
@@ -0,0 +1,20 @@
+# © 2012–2015 the Massachusetts Institute of Technology
+# @author bbaren
+
+CC = clang
+CXX = clang++
+
+CPPFLAGS = \
+	-Wall \
+	-D_FORTIFY_SOURCE=2
+
+CXXFLAGS = \
+	-std=c++11 \
+	-ftrapv \
+	-fstack-protector-strong --param=ssp-buffer-size=4 \
+	-fPIC \
+	-O2 -g \
+	-ffunction-sections -fdata-sections \
+	-Weverything -Wno-c++98-compat
+
+LDFLAGS = -fPIE -pie
diff --git a/.make/coq.mk b/.make/coq.mk
new file mode 100644
index 000000000..b05c7e59d
--- /dev/null
+++ b/.make/coq.mk
@@ -0,0 +1,24 @@
+# © 2012–2015 the Massachusetts Institute of Technology
+# @author bbaren + rsloan
+
+COQC = coqc
+COQDEP = coqdep
+
+COMPILE.v = $(COQC) -q $(COQLIBS)
+
+.PHONY: check_fiat
+
+check_fiat:
+	@perl -e \
+		'if(! -d "./fiat") { print("you need to link fiat to ./fiat\n"); exit(1) }'
+
+%.vo %.glob: check_fiat %.v
+	$(COMPILE.v) $*
+
+%.v.d: check_fiat %.v
+	@$(COQDEP) -I . $(COQLIBS) "$<" >"$@" \
+	  || (RV=$$?; rm -f "$@"; exit $${RV})
+
+define coq-generated
+$1.vo $1.v.d $1.glob
+endef
diff --git a/Makefile b/Makefile
new file mode 100644
index 000000000..2799187f6
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,23 @@
+# © 2015 the Massachusetts Institute of Technology
+# @author bbaren
+
+SOURCES := $(shell grep -v '^-' _CoqProject | tr '\n' ' ')
+COQLIBS := $(shell grep '^-' _CoqProject | tr '\n' ' ')
+
+include .make/cc.mk
+include .make/coq.mk
+
+FAST_TARGETS += check_fiat clean
+
+.DEFAULT_GOAL = all
+.PHONY: all clean coquille
+
+all: $(SOURCES)
+	@echo "done!"
+
+coquille:
+	vim -c "execute coquille#Launch($(COQLIBS))" -N
+
+clean:
+	$(RM) $(foreach f,$(SOURCES),$(call coq-generated,$(basename $f)))
+
diff --git a/README.md b/README.md
index 77d3aafba..fc87a9f0e 100644
--- a/README.md
+++ b/README.md
@@ -1,2 +1,11 @@
-# fiat-crypto
-Cryptographic Primitive Code Generation in Fiat
+Synthesizing Correct-by-Construction Assembly for Cryptographic Primitives in Fiat
+-----
+
+... which would make a good paper title.
+
+To build:
+
+    ln -s <FIAT_DIR> fiat
+    (cd fiat && make fiat-core)
+    make
+
diff --git a/_CoqProject b/_CoqProject
new file mode 100644
index 000000000..89404292d
--- /dev/null
+++ b/_CoqProject
@@ -0,0 +1,3 @@
+-R src Crypto
+-R fiat/src Fiat
+src/Curves/Curve25519.v
diff --git a/src/Curves/Curve25519.v b/src/Curves/Curve25519.v
new file mode 100644
index 000000000..8bc3d6e20
--- /dev/null
+++ b/src/Curves/Curve25519.v
@@ -0,0 +1,13 @@
+
+Require Import ZModulo.
+(**
+ * The relevant module is ZModulo:
+ *   the constructor you want is of_pos
+ *   the operations you want are in zmod_ops
+ *   the tactics you want are somewhere between Field and CyclicType:
+ *     probs you want to be converting to/from Z pretty frequently
+ *
+ * Coq Reference page:
+ *    https://coq.inria.fr/library/Coq.Numbers.Cyclic.ZModulo.ZModulo.html
+ *)
+
-- 
cgit v1.2.3