From 72f04723d1b41b9722c0b547b96f8098b5f431f6 Mon Sep 17 00:00:00 2001 From: Karthikeyan Bhargavan Date: Wed, 30 Oct 2024 08:44:43 +0100 Subject: [PATCH] removed fstar libs needed for ml-kem from this PR --- fstar-helpers/Makefile.base | 2 +- .../proofs/fstar/extraction/Libcrux_platform.Platform.fsti | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/fstar-helpers/Makefile.base b/fstar-helpers/Makefile.base index 6eb4fc9cc..54c2552b1 100644 --- a/fstar-helpers/Makefile.base +++ b/fstar-helpers/Makefile.base @@ -10,5 +10,5 @@ EXTRA_HELPMESSAGE += printf "Libcrux specifics:\n"; EXTRA_HELPMESSAGE += target SLOW_MODULES 'a list of modules to verify fully only when `VERIFY_SLOW_MODULES` is set to `yes`. When `VERIFY_SLOW_MODULES`, those modules are admitted.'; EXTRA_HELPMESSAGE += target VERIFY_SLOW_MODULES '`yes` or `no`, defaults to `no`'; -FSTAR_INCLUDE_DIRS_EXTRA += $(HACL_HOME)/specs $(shell git rev-parse --show-toplevel)/fstar-helpers/fstar-bitvec +FSTAR_INCLUDE_DIRS_EXTRA += $(HACL_HOME)/specs include $(shell git rev-parse --show-toplevel)/fstar-helpers/Makefile.generic diff --git a/sys/platform/proofs/fstar/extraction/Libcrux_platform.Platform.fsti b/sys/platform/proofs/fstar/extraction/Libcrux_platform.Platform.fsti index e8713dad5..95dad6932 100644 --- a/sys/platform/proofs/fstar/extraction/Libcrux_platform.Platform.fsti +++ b/sys/platform/proofs/fstar/extraction/Libcrux_platform.Platform.fsti @@ -1,5 +1,5 @@ module Libcrux_platform.Platform -#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +#set-options "--fuel 0 --ifuel 1 --z3rlimit 80" open Core open FStar.Mul