diff --git a/Makefile b/Makefile
index fdbd4c7..27b41fb 100644
--- a/Makefile
+++ b/Makefile
@@ -31,7 +31,7 @@ hints obj:
 	mkdir $@
 
 %.checked: | hints obj
-	$(FSTAR) --hint_file hints/$(notdir $*).hints $(notdir $*) && touch -c $@
+	$(FSTAR) --hint_dir hints $(notdir $*) && touch -c $@
 
 %.krml:
 	$(FSTAR) --codegen krml \
diff --git a/MerkleTree.fst.config.json b/MerkleTree.fst.config.json
new file mode 100644
index 0000000..25ea1ab
--- /dev/null
+++ b/MerkleTree.fst.config.json
@@ -0,0 +1,86 @@
+{
+  "fstar_exe": "fstar.exe",
+  "options": [
+    "--cache_dir", "obj",
+    "--odir", "obj",
+    "--cmi",
+    "--use_hints",
+    "--record_hints",
+    "--already_cached", "*,-MerkleTree,-MerkleTree.*,-Lib.RawBuffer",
+    "--warn_error", "@241-274",
+    "--hint_dir", "hints"
+  ],
+  "include_dirs": [
+    "src",
+    "${KRML_HOME}/krmllib",
+    "${KRML_HOME}/krmllib/obj",
+    "${KRML_HOME}/runtime",
+    "${HACL_HOME}/lib",
+    "${HACL_HOME}/specs",
+    "${HACL_HOME}/specs/lemmas",
+    "${HACL_HOME}/specs/tests",
+    "${HACL_HOME}/specs/drbg",
+    "${HACL_HOME}/specs/frodo",
+    "${HACL_HOME}/specs/tests/p256",
+    "${HACL_HOME}/code/hash",
+    "${HACL_HOME}/code/hmac",
+    "${HACL_HOME}/code/hkdf",
+    "${HACL_HOME}/code/drbg",
+    "${HACL_HOME}/code/hpke",
+    "${HACL_HOME}/code/sha3",
+    "${HACL_HOME}/code/sha2-mb",
+    "${HACL_HOME}/code/ecdsap256",
+    "${HACL_HOME}/code/poly1305",
+    "${HACL_HOME}/code/streaming",
+    "${HACL_HOME}/code/blake2",
+    "${HACL_HOME}/code/chacha20",
+    "${HACL_HOME}/code/chacha20poly1305",
+    "${HACL_HOME}/code/curve25519",
+    "${HACL_HOME}/code/tests",
+    "${HACL_HOME}/code/ed25519",
+    "${HACL_HOME}/code/salsa20",
+    "${HACL_HOME}/code/nacl-box",
+    "${HACL_HOME}/code/meta",
+    "${HACL_HOME}/code/frodo",
+    "${HACL_HOME}/code/fallback",
+    "${HACL_HOME}/code/bignum",
+    "${HACL_HOME}/code/rsapss",
+    "${HACL_HOME}/code/ffdhe",
+    "${HACL_HOME}/code/k256",
+    "${HACL_HOME}/vale/code/arch",
+    "${HACL_HOME}/vale/code/arch/x64",
+    "${HACL_HOME}/vale/code/arch/x64/interop",
+    "${HACL_HOME}/vale/code/arch/ppc64le",
+    "${HACL_HOME}/vale/code/crypto/aes",
+    "${HACL_HOME}/vale/code/crypto/aes/x64",
+    "${HACL_HOME}/vale/code/crypto/aes/ppc64le",
+    "${HACL_HOME}/vale/code/crypto/bignum",
+    "${HACL_HOME}/vale/code/crypto/ecc/curve25519",
+    "${HACL_HOME}/vale/code/crypto/poly1305",
+    "${HACL_HOME}/vale/code/crypto/poly1305/x64",
+    "${HACL_HOME}/vale/code/crypto/sha",
+    "${HACL_HOME}/vale/code/lib/collections",
+    "${HACL_HOME}/vale/code/lib/math",
+    "${HACL_HOME}/vale/code/lib/util",
+    "${HACL_HOME}/vale/code/lib/util/x64",
+    "${HACL_HOME}/vale/code/lib/util/x64/stdcalls",
+    "${HACL_HOME}/vale/code/lib/transformers",
+    "${HACL_HOME}/vale/code/test",
+    "${HACL_HOME}/vale/code/thirdPartyPorts/Intel/aes/x64",
+    "${HACL_HOME}/vale/code/thirdPartyPorts/OpenSSL/aes",
+    "${HACL_HOME}/vale/code/thirdPartyPorts/OpenSSL/poly1305/x64",
+    "${HACL_HOME}/vale/code/thirdPartyPorts/OpenSSL/sha",
+    "${HACL_HOME}/vale/code/thirdPartyPorts/rfc7748/curve25519/x64",
+    "${HACL_HOME}/vale/code/thirdPartyPorts/SymCrypt/bignum",
+    "${HACL_HOME}/vale/specs/crypto",
+    "${HACL_HOME}/vale/specs/defs",
+    "${HACL_HOME}/vale/specs/hardware",
+    "${HACL_HOME}/vale/specs/interop",
+    "${HACL_HOME}/vale/specs/math",
+    "${HACL_HOME}/providers/evercrypt",
+    "${HACL_HOME}/providers/evercrypt/fst",
+    "${HACL_HOME}/providers/test",
+    "${HACL_HOME}/providers/test/vectors",
+    "${HACL_HOME}/obj"
+  ]
+}