This adds support for verification of modules in mitls-fstar without having to first build hacl-star.
The trick is to verify dependencies in hacl-star, if needed, without providers/evercrypt/fst in scope. The results are cached locally and used for verification, but can't be used for extraction because mitls-fstar relies on --cmi to e.g. inline EverCrypt.StaticConfig and EverCrypt.TargetConfig definitions, and for soundness of extraction of StackInline functions such as EverCrypt.Hash.alloca.
This PR will
error out before verification if the required Vale dependencies in $(HACL_HOME)/obj/ haven't been generated, informing the user to run make -C $(HACL_HOME) vale-fst first.
warn before verification if $(HACL_HOME)/obj/EverCrypt.fsti.checked doesn't exist, which suggests that hacl-star hasn't been built. The warning tells that hacl-star dependencies will be verified as needed and that cached results can't be used for extraction.
error out before extraction if there are locally cached hacl-star dependencies, informing the user to delete them and build hacl-star first.
Thanks @nik and @msprotz for suggesting this could be useful and discussing solutions.
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.