Import Merkle Tree from HACL*

This is based on hacl-star/hacl-star at revision
b78faf7e201303f4bea379d69f3769ae57bbeb48

This establishes Merkle Tree as a standalone project that can be built
atop EverCrypt/HACL in its own repository.

.gitignore

@@ -0,0 +1,4 @@
+obj
+dist
+.depend
+*.exe

Makefile

@@ -0,0 +1,98 @@
+all: test
+
+# Boilerplate
+# -----------
+
+include Makefile.include
+
+FST_FILES=$(wildcard src/*.fst) $(wildcard src/*.fsti)
+
+ifndef NODEPEND
+ifndef MAKE_RESTARTS
+.depend: .FORCE
+	@mkdir -p obj
+	@$(FSTAR) --dep full $(FST_FILES) > $@
+
+.PHONY: .FORCE
+.FORCE:
+endif
+endif
+
+include .depend
+
+.PHONY: clean
+clean:
+	rm -rf obj .depend
+
+# Verification
+# ------------
+
+hints obj:
+	mkdir $@
+
+%.checked: | hints obj
+	$(FSTAR) --hint_file hints/$(notdir $*).hints $(notdir $*) && touch -c $@
+
+%.krml:
+	$(FSTAR) --codegen krml \
+	  --extract_module $(basename $(notdir $(subst .checked,,$<))) \
+	  $(notdir $(subst .checked,,$<))
+
+# Karamel
+# -------
+
+KRML=$(KRML_HOME)/krml
+
+# Making sure that the extern symbols generated in MerkleTree_EverCrypt
+# correspond to the ones found in libevercrypt.so
+VALE_FLAGS= \
+  -library 'Vale.Stdcalls.*' \
+  -no-prefix 'Vale.Stdcalls.*' \
+  -static-header 'Vale.Inline.*' \
+  -library 'Vale.Inline.X64.Fadd_inline' \
+  -library 'Vale.Inline.X64.Fmul_inline' \
+  -library 'Vale.Inline.X64.Fswap_inline' \
+  -library 'Vale.Inline.X64.Fsqr_inline' \
+  -no-prefix 'Vale.Inline.X64.Fadd_inline' \
+  -no-prefix 'Vale.Inline.X64.Fmul_inline' \
+  -no-prefix 'Vale.Inline.X64.Fswap_inline' \
+  -no-prefix 'Vale.Inline.X64.Fsqr_inline' \
+
+
+# The usual bug with prims.krml
+dist/Makefile.basic: $(filter-out %prims.krml,$(ALL_KRML_FILES))
+	$(KRML) $(KOPTS) -library EverCrypt,EverCrypt.* $^ -tmpdir dist -skip-compilation \
+	  -minimal \
+	  -add-include '"krml/internal/target.h"' \
+	  -add-include '"krml/internal/types.h"' \
+	  -add-include '"krml/lowstar_endianness.h"' \
+	  -add-include '<stdint.h>' \
+	  -add-include '<stdbool.h>' \
+	  -add-include '<string.h>' \
+	  -fparentheses \
+	  -o libmerkletree.a \
+	  $(VALE_FLAGS) \
+	  -no-prefix 'MerkleTree' \
+	  -no-prefix 'MerkleTree.EverCrypt' \
+	  -bundle 'MerkleTree+MerkleTree.Init+MerkleTree.EverCrypt+MerkleTree.Low+MerkleTree.Low.Serialization+MerkleTree.Low.Hashfunctions=MerkleTree.*[rename=MerkleTree]' \
+	  -bundle LowStar.* \
+	  -bundle Prims,C.Failure,C,C.String,C.Loops,Spec.Loops,C.Endianness,FStar.*[rename=Merkle_Krmllib] \
+	  -bundle 'Meta.*,Hacl.*,Vale.*,Spec.*,Lib.*,EverCrypt,EverCrypt.*[rename=Merkle_EverCrypt]'
+
+dist/libmerkletree.a: dist/Makefile.basic
+	$(MAKE) -C dist -f Makefile.basic
+
+# Tests
+# -----
+
+.PHONY: test
+test: test.exe
+	./$<
+
+CFLAGS+=-Idist -Itests -I$(KRML_HOME)/include -I$(KRML_HOME)/krmllib/dist/minimal
+
+$(HACL_HOME)/dist/gcc-compatible/libevercrypt.a:
+	$(error Please run make in $(dir $@))
+
+test.exe: tests/merkle_tree_test.c dist/libmerkletree.a $(HACL_HOME)/dist/gcc-compatible/libevercrypt.a
+	$(CC) $(CFLAGS) -Idist -Itests $^ -o $@

Makefile.include

@@ -0,0 +1,33 @@
+MERKLE_HOME ?= $(realpath .)
+
+KRML_HOME ?= $(MERKLE_HOME)/../karamel
+HACL_HOME ?= $(MERKLE_HOME)/../hacl-star
+
+include $(HACL_HOME)/Makefile.include
+
+FSTAR_INCLUDE_PATH= \
+	$(MERKLE_HOME)/src \
+	$(KRML_HOME)/krmllib \
+	$(KRML_HOME)/krmllib/obj \
+	$(ALL_HACL_DIRS)
+
+# In interactive mode, chill out and don't roll over if something isn't cached
+# somewhere.
+FSTAR_CHILL_FLAGS= \
+	$(addprefix --include ,$(FSTAR_INCLUDE_PATH)) \
+	--cache_checked_modules \
+	--cache_dir $(MERKLE_HOME)/obj \
+	--odir $(MERKLE_HOME)/obj \
+	--cmi \
+	--use_hints \
+	--record_hints \
+	$(OTHERFLAGS)
+
+FSTAR_FLAGS=$(FSTAR_CHILL_FLAGS) \
+	--already_cached '*,-MerkleTree,-MerkleTree.*,-Lib.RawBuffer' \
+	--warn_error @241-274 \
+
+FSTAR=$(FSTAR_HOME)/bin/fstar.exe $(FSTAR_FLAGS)
+
+%.fst-in %.fsti-in:
+	@echo $(FSTAR_CHILL_FLAGS)

README.md

@@ -0,0 +1,8 @@
+Merkle Tree
+===========
+
+This repository contains a fully verified Merkle Tree, with a proof by security
+reduction to a collision to the underlying hash function.
+
+We demonstrate how to build a project on top of EverCrypt by only using the
+"public" APIs and a minimal build burden.