Merge branch 'master' of https://github.com/mitls/hacl-star

hacl-star · Jul 15, 2017 · 8ca629c · 8ca629c
2 parents 35ae245 + affce42
commit 8ca629c
Show file tree

Hide file tree

Showing 4 changed files with 6 additions and 21 deletions.
diff --git a/secure_api/LowCProvider/Makefile b/secure_api/LowCProvider/Makefile
@@ -6,7 +6,7 @@ CORECRYPTO = $(FSTAR_HOME)/$(CONTRIB)/CoreCrypto/ml
 INCLUDE=-package batteries,zarith -I $(PLATFORM) -I $(CORECRYPTO)
 MARCH?=x86_64
 
-KRML_INCLUDES=$(addprefix -I ,$(KREMLIN_HOME)/kremlib $(KREMLIN_HOME)/test)
+KRML_INCLUDES=$(addprefix -I ,$(KREMLIN_HOME)/kremlib $(KREMLIN_HOME)/test tmp)
 KRML_ARGS=-verbose -ccopt -Wno-error=pointer-sign $(KOPTS)
 KRML=$(KREMLIN_HOME)/krml $(KRML_ARGS) $(KRML_INCLUDES)
 
@@ -15,7 +15,7 @@ OCAMLOPT = ocamlfind opt $(INCLUDE) -g -annot
 OCAMLMKLIB = ocamlfind mklib $(INCLUDE)
 OCAMLDEP = ocamlfind dep
 
-CCOPTS = $(addprefix -ccopt ,-Wall -std=c11 -D__USE_MINGW_ANSI_STDIO)
+CCOPTS = $(addprefix -ccopt ,-Wall -std=c11 -D__USE_MINGW_ANSI_STDIO -DKRML_NOUINT128)
 CCLIBS = $(addprefix -cclib ,-L.)
 
 ifeq ($(OS),Windows_NT)
@@ -43,7 +43,7 @@ else
     endif
 endif
 
-.PHONY: test dep
+.PHONY: test dep tmp
 
 all: tmp LowCProvider.cmxa
 

diff --git a/secure_api/Makefile b/secure_api/Makefile
@@ -19,7 +19,7 @@ else
 endif
 
 KRML_INCLUDES=$(addprefix -I ,aead uf1cma vale vale/asm prf hkdf utils indexing ../code/experimental/aesgcm ../code/bignum ../code/poly1305 ../code/salsa-family ../code/hash ../code/lib/kremlin ../specs $(KREMLIN_HOME)/kremlib $(KREMLIN_HOME)/test)
-KRML_ARGS=$(FPIC) -ccopt -maes \
+KRML_ARGS=$(FPIC) -ccopt -maes -fnouint128 \
   $(KREMLIN_HOME)/test/../kremlib/testlib.c \
   vale/asm/vale.a test/test_hacks.c \
   -drop Hacl.Spe.*,Spec,Hacl.Spec,Spec.*,Hacl.Spec.* \

diff --git a/secure_api/QuicProvider/Makefile b/secure_api/QuicProvider/Makefile
@@ -1,24 +1,9 @@
 FSTAR_HOME ?= ../../../FStar
-CONTRIB=ucontrib
-PLATFORM = $(FSTAR_HOME)/$(CONTRIB)/Platform/ml
-CORECRYPTO = $(FSTAR_HOME)/$(CONTRIB)/CoreCrypto/ml
-INCLUDE=-package batteries,zarith -I $(PLATFORM) -I $(CORECRYPTO)
-MARCH?=x86_64
-
 KREMLIN_HOME ?= ../../../kremlin
-KRML_INCLUDES=$(addprefix -I ,$(KREMLIN_HOME)/kremlib $(KREMLIN_HOME)/test)
-KRML_ARGS=-verbose -ccopt -Wno-error=pointer-sign $(KOPTS)
-KRML=$(KREMLIN_HOME)/krml $(KRML_ARGS) $(KRML_INCLUDES)
-
 MITLS_HOME ?= ../../../mitls-fstar
 
-OCAMLC = ocamlfind c $(INCLUDE) -g -annot
-OCAMLOPT = ocamlfind opt $(INCLUDE) -g -annot
-OCAMLMKLIB = ocamlfind mklib $(INCLUDE)
-OCAMLDEP = ocamlfind dep
+MARCH?=x86_64
 
-CCOPTS = $(addprefix -ccopt ,-Wall -std=c11 -D__USE_MINGW_ANSI_STDIO)
-CCLIBS = $(addprefix -cclib ,-L.)
 COPTS = -fPIC -std=c11 -I tmp -I $(MITLS_HOME)/libs/ffi -I $(KREMLIN_HOME)/kremlib
 
 ifeq ($(OS),Windows_NT)

diff --git a/specs/Spec.SHA2_256.fst b/specs/Spec.SHA2_256.fst
@@ -306,7 +306,7 @@ let lemma_hash_single_prepend_block block msg =
   Seq.lemma_eq_intro (msg_last') (msg_last);
   Seq.lemma_eq_intro (msg_blocks') (block @| msg_blocks)
 
-#set-options "--lax"
+
 
 //
 // Test 1