Skip to content

Commit

Permalink
MerkleTree.fst.config.json: add config for VS Code extension
Browse files Browse the repository at this point in the history
Also change Makefile to use --hint_dir instead of --hint_file.
  • Loading branch information
mtzguido committed Feb 4, 2024
1 parent bd89df8 commit cc76685
Show file tree
Hide file tree
Showing 2 changed files with 87 additions and 1 deletion.
2 changes: 1 addition & 1 deletion Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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 \
Expand Down
86 changes: 86 additions & 0 deletions MerkleTree.fst.config.json
Original file line number Diff line number Diff line change
@@ -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"
]
}

0 comments on commit cc76685

Please sign in to comment.