diff options
| author |  Robert Sloan <varomodt@dhcp-18-189-51-40.dyn.MIT.EDU> | 2015-09-10 18:52:17 -0400 |
|---|---|---|
| committer | Robert Sloan <varomodt@dhcp-18-189-51-40.dyn.MIT.EDU> | 2015-09-10 18:52:17 -0400 |
| commit | 2c7b377febf9f42de6c7313dfe4154efdfb90da1 (patch) | |
| tree | 3cd619d157fd7d228a9f534be23b3d23261bdf33 | |
| parent | f4e1d24da03c54fde2df41aa4a3d8ed17940004e (diff) | |
init our centralized repo
| -rw-r--r-- | .make/cc.mk | 20 | ||||
| -rw-r--r-- | .make/coq.mk | 24 | ||||
| -rw-r--r-- | Makefile | 23 | ||||
| -rw-r--r-- | README.md | 13 | ||||
| -rw-r--r-- | _CoqProject | 3 | ||||
| -rw-r--r-- | src/Curves/Curve25519.v | 13 |
6 files changed, 94 insertions, 2 deletions
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))) + @@ -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 + *) + |