This repository has been archived by the owner on Jun 17, 2024. It is now read-only.
Add support for local verification #239
Open
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…nd safeguards against using the cached results for extraction
msprotz
reviewed
Oct 23, 2019
| @@ -79,7 +79,7 @@ FSTAR_HINTS ?= --use_hints --use_hint_hashes --record_hints | |||
| # verify... see https://github.com/FStarLang/FStar/issues/1652 | |||
| FSTAR_NO_FLAGS = $(FSTAR_HOME)/bin/fstar.exe $(FSTAR_HINTS) \ | |||
| --odir $(OUTPUT_DIR) --cache_checked_modules $(FSTAR_INCLUDES) --cmi \ | |||
| --already_cached 'Prims FStar LowStar C Spec.Loops TestLib WasmSupport Hacl EverCrypt Vale LowParse Lib Spec -FStar.Old.Endianness -FStar.Test -C.Compat' \ | |||
| --already_cached 'Prims FStar LowStar C Spec.Loops TestLib WasmSupport LowParse -FStar.Old.Endianness -FStar.Test -C.Compat' \ | |||
There was a problem hiding this comment.
won't you have "did not expect module XXX to be checked" errors with this?
There was a problem hiding this comment.
They are only warnings e.g. Did not expected EverCrypt.HKDF to be already checked, but found it in an unexpected location ... (sic). I believe it will behave as before except for these warnings.
msprotz
reviewed
Oct 23, 2019
| @@ -16,7 +16,10 @@ INCLUDE_PATHS = \ | |||
| $(QD_HOME)/src/lowparse \ | |||
| $(MITLS_HOME)/src/parsers/generated \ | |||
| $(MITLS_HOME)/src/tls \ | |||
| $(MITLS_HOME)/src/tls/obj | |||
There was a problem hiding this comment.
do you remember or understand why obj needs to be on the include path?
There was a problem hiding this comment.
I think this is only needed to benefit from the cache in interactive mode. I think we can add it only in -in targets, but I'm not absolutely sure.
There was a problem hiding this comment.
We can. I removed it.
…lied by --cache-dir option
Sign up for free
to subscribe to this conversation on GitHub.
Already have an account?
Sign in.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This adds support for verification of modules in
mitls-fstarwithout having to first buildhacl-star.The trick is to verify dependencies in
hacl-star, if needed, withoutproviders/evercrypt/fstin scope. The results are cached locally and used for verification, but can't be used for extraction becausemitls-fstarrelies on--cmito e.g. inlineEverCrypt.StaticConfigandEverCrypt.TargetConfigdefinitions, and for soundness of extraction ofStackInlinefunctions such asEverCrypt.Hash.alloca.This PR will
$(HACL_HOME)/obj/haven't been generated, informing the user to runmake -C $(HACL_HOME) vale-fstfirst.$(HACL_HOME)/obj/EverCrypt.fsti.checkeddoesn't exist, which suggests thathacl-starhasn't been built. The warning tells thathacl-stardependencies will be verified as needed and that cached results can't be used for extraction.hacl-stardependencies, informing the user to delete them and buildhacl-starfirst.Thanks @nik and @msprotz for suggesting this could be useful and discussing solutions.