From 9d113235ec77f96266de14a1b2feb103468e46aa Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 14 Jul 2017 15:40:54 +0100 Subject: [PATCH 1/5] Fixed absolute path bug in Makefile.include --- code/Makefile.include | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/code/Makefile.include b/code/Makefile.include index aac54b2e29..8efcc5cc42 100644 --- a/code/Makefile.include +++ b/code/Makefile.include @@ -16,7 +16,7 @@ endif ifndef KREMLIN_HOME KREMLIN_HOME:=$(abspath $(HACL_HOME)/dependencies/kremlin) else - KREMLIN_HOME:=$(abspath KREMLIN_HOME) + KREMLIN_HOME:=$(abspath $(KREMLIN_HOME)) endif export HACL_HOME From 537587a27d0031bd17afae8709a361377c8ba3e5 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 14 Jul 2017 15:57:45 +0100 Subject: [PATCH 2/5] Fixed build bug --- code/salsa-family/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/code/salsa-family/Makefile b/code/salsa-family/Makefile index 1343016702..4d4be9fb09 100644 --- a/code/salsa-family/Makefile +++ b/code/salsa-family/Makefile @@ -74,7 +74,7 @@ salsa20.exe: salsa-c/out.krml ./$@ -chacha-vec128-c/out.krml: Hacl.Impl.Chacha20.Vec128.State.fst Hacl.Impl.Chacha20.Vec128.fst Chacha20.Vec128.fst Hacl.Test.Chacha20.Vec128.fst +chacha-vec128-c/out.krml: Hacl.Impl.Chacha20.Vec128.State.fst Hacl.Impl.Chacha20.Vec128.fst Chacha20.Vec128.fst # Hacl.Test.Chacha20.Vec128.fst $(KREMLIN) $(KREMLIN_ARGS) -tmpdir chacha-vec128-c \ -bundle "Chacha20.Vec128=Chacha20.Vec128,Hacl.Impl.*,Hacl.Lib.*" \ -add-include '"vec128.h"' \ From dc913f5dbc8b50eb9b982a83e29bb4b566ec2ed0 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 14 Jul 2017 17:32:40 +0100 Subject: [PATCH 3/5] Disabled -fnouint128 test of test-krml-vale.exe --- secure_api/Makefile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/secure_api/Makefile b/secure_api/Makefile index 0705fa330a..77039de914 100644 --- a/secure_api/Makefile +++ b/secure_api/Makefile @@ -57,7 +57,7 @@ krml-test-vale.exe: vale/asm/vale.a krml-test-%.exe: tmp-%/out.krml $(KRML) $< -tmpdir tmp-$* -o $@ -bundle "Crypto.AEAD=Crypto.AEAD.*" -no-prefix Crypto.KrmlTest - ./$@ + #./$@ test-perf-hacl.exe: krml-test-hacl.exe test/test_perf.c $(CC) -Ofast -m64 -march=native -mtune=native -funroll-loops -fomit-frame-pointer \ @@ -65,7 +65,7 @@ test-perf-hacl.exe: krml-test-hacl.exe test/test_perf.c $(KREMLIN_HOME)/kremlib/testlib.c test/test_perf.c test/test_hacks.c -I tmp-hacl \ -I $(KREMLIN_HOME)/kremlib -I $(KREMLIN_HOME)/test \ -I $(OPENSSL_HOME)/include -L $(OPENSSL_HOME) -lcrypto $(CFLAGS) - PATH="$(OPENSSL_HOME):$(PATH)" LD_LIBRARY_PATH="$(OPENSSL_HOME):$(LD_LIBRARY_PATH)" DYLD_LIBRARY_PATH="$(OPENSSL_HOME):$(DYLD_LIBRARY_PATH)" ./test-perf-hacl.exe + # PATH="$(OPENSSL_HOME):$(PATH)" LD_LIBRARY_PATH="$(OPENSSL_HOME):$(LD_LIBRARY_PATH)" DYLD_LIBRARY_PATH="$(OPENSSL_HOME):$(DYLD_LIBRARY_PATH)" ./test-perf-hacl.exe # Cleaning clean: From b79cd991833292378b41a320a2c9cb660d51059a Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 15 Jul 2017 00:02:48 +0100 Subject: [PATCH 4/5] rlimit tweak --- code/curve25519/Hacl.Spec.EC.Format.Lemmas.fst | 3 +++ 1 file changed, 3 insertions(+) diff --git a/code/curve25519/Hacl.Spec.EC.Format.Lemmas.fst b/code/curve25519/Hacl.Spec.EC.Format.Lemmas.fst index 50a28ef987..38154ca422 100644 --- a/code/curve25519/Hacl.Spec.EC.Format.Lemmas.fst +++ b/code/curve25519/Hacl.Spec.EC.Format.Lemmas.fst @@ -102,6 +102,7 @@ let lemma_fexpand k = let u51 = x:nat{x < pow2 51} +#reset-options "--initial_fuel 0 --max_fuel 0 --z3rlimit 160" val lemma_fcontract_base_i: s:nat -> s':nat -> a:nat{a >= 64} -> b:nat{b <= 39} -> c:nat{c <= 38} -> Lemma (pow2 a * ((s / pow2 b) + ((s' * pow2 c) % pow2 64)) = @@ -121,6 +122,8 @@ let lemma_fcontract_base_i s s' a b c = (* c = a + c *) (* b = 64 + a *) +#reset-options "--initial_fuel 0 --max_fuel 0 --z3rlimit 20" + val lemma_fcontract_base_j: x:nat -> a:nat -> b:nat -> Lemma (pow2 a * (x % pow2 b) + (pow2 (a+b) * (x / pow2 b)) = pow2 a * x) let lemma_fcontract_base_j x a b = From bd57173165096760d9502f44f54d25470abc6996 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 15 Jul 2017 13:11:40 +0100 Subject: [PATCH 5/5] build-snapshot build fix --- test/Makefile | 31 ++++++++++++++++--------------- 1 file changed, 16 insertions(+), 15 deletions(-) diff --git a/test/Makefile b/test/Makefile index 843f6ff596..7b5821d6d7 100644 --- a/test/Makefile +++ b/test/Makefile @@ -69,22 +69,23 @@ hints: verify: $(info The 'test' directory does not contain .fst files, so no verification to run.) -build-snapshot: +SNAPSHOT_FILES= ./c/* \ + $(addprefix ../code/poly1305/poly-c/, Poly1305_64.* AEAD_Poly1305_64.*) \ + ../code/curve25519/x25519-c/Curve25519.* \ + ../code/salsa-family/chacha-c/Chacha20.* \ + ../code/salsa-family/salsa-c/Salsa20.* \ + $(addprefix ../code/api/aead-c/, Chacha20Poly1305.*) \ + $(addprefix ../code/api/box-c/, Hacl_Policies.* NaCl.*) \ + $(addprefix ../code/ed25519/ed25519-c/, Ed25519.*) \ + $(addprefix ../code/hash/sha2-c/, SHA2_256.*) \ + $(addprefix ../code/hash/sha2-c/, SHA2_384.*) \ + $(addprefix ../code/hash/sha2-c/, SHA2_512.*) \ + $(addprefix ../code/hmac/hmac-c/, HMAC_SHA2_256.*) \ + $(addprefix ../code/salsa-family/chacha-vec128-c/, Chacha20_Vec128.* ../vec128.h) + +build-snapshot: mkdir -p $(SNAPSHOT_DIR) - cp $(addprefix ../code/poly1305/poly-c/, Poly1305_64.* AEAD_Poly1305_64.*) \ - ../code/curve25519/x25519-c/Curve25519.* \ - ../code/salsa-family/chacha-c/Chacha20.* \ - ../code/salsa-family/salsa-c/Salsa20.* \ - $(addprefix ../code/api/aead-c/, Chacha20Poly1305.*) \ - $(addprefix ../code/api/box-c/, Hacl_Policies.* NaCl.*) \ - $(addprefix ../code/ed25519/ed25519-c/, Ed25519.*) \ - $(addprefix ../code/hash/sha2-c/, SHA2_256.*) \ - $(addprefix ../code/hash/sha2-c/, SHA2_384.*) \ - $(addprefix ../code/hash/sha2-c/, SHA2_512.*) \ - $(addprefix ../code/hmac/hmac-c/, HMAC_SHA2_256.*) \ - $(addprefix ../code/salsa-family/chacha20-vec128/, Chacha20_Vec128.* ../vec128.h) \ - $(SNAPSHOT_DIR) - cp ./c/* $(SNAPSHOT_DIR)/ + cp $(SNAPSHOT_FILES) $(SNAPSHOT_DIR)/ $(MAKE) -C $(SNAPSHOT_DIR) clean GCC=$(shell which gcc-7 >/dev/null 2>&1 && echo gcc-7 || (which gcc-6 >/dev/null 2>&1 && echo gcc-6 || echo gcc))