From 6243218c840e82c8bc8860a271e407c053ca9a83 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 30 Jan 2025 13:29:54 +0100 Subject: [PATCH] proofs(mldsa): use newer z3 & context pruning by default --- .../Libcrux_ml_dsa.Simd.Portable.Encoding.Commitment.fst | 2 +- libcrux-ml-dsa/proofs/fstar/extraction/Makefile | 2 ++ libcrux-ml-dsa/src/simd/portable/encoding/commitment.rs | 2 +- 3 files changed, 4 insertions(+), 2 deletions(-) diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Encoding.Commitment.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Encoding.Commitment.fst index 5f32ec627..5517e87bb 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Encoding.Commitment.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Encoding.Commitment.fst @@ -3,7 +3,7 @@ module Libcrux_ml_dsa.Simd.Portable.Encoding.Commitment open Core open FStar.Mul -#set-options "--fuel 0 --ifuel 1 --z3rlimit 300 --z3version 4.13.3 --ext context_pruning" +#set-options "--fuel 0 --ifuel 1 --z3rlimit 300 --ext context_pruning" let encode_4_ (coefficients: t_Slice i32) = let coefficient0:u8 = cast (coefficients.[ mk_usize 0 ] <: i32) <: u8 in diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Makefile b/libcrux-ml-dsa/proofs/fstar/extraction/Makefile index f88297130..9c387eb5d 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Makefile +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Makefile @@ -3,5 +3,7 @@ ADMIT_MODULES = FSTAR_INCLUDE_DIRS_EXTRA += $(shell git rev-parse --show-toplevel)/fstar-helpers/fstar-bitvec \ $(shell git rev-parse --show-toplevel)/libcrux-ml-kem/proofs/fstar/spec \ $(shell git rev-parse --show-toplevel)/libcrux-intrinsics/proofs/fstar/extraction +OTHERFLAGS += --z3version 4.13.3 +OTHERFLAGS += --ext context_pruning include $(shell git rev-parse --show-toplevel)/fstar-helpers/Makefile.base diff --git a/libcrux-ml-dsa/src/simd/portable/encoding/commitment.rs b/libcrux-ml-dsa/src/simd/portable/encoding/commitment.rs index 9f0c73b72..229d60ad0 100644 --- a/libcrux-ml-dsa/src/simd/portable/encoding/commitment.rs +++ b/libcrux-ml-dsa/src/simd/portable/encoding/commitment.rs @@ -3,7 +3,7 @@ use crate::{helper::cloop, simd::portable::vector_type::Coefficients}; #[inline(always)] #[hax_lib::fstar::before( r#" -#set-options "--fuel 0 --ifuel 1 --z3rlimit 300 --z3version 4.13.3 --ext context_pruning" +#set-options "--fuel 0 --ifuel 1 --z3rlimit 300" "# )] #[hax_lib::requires(fstar!(r"Seq.length ${coefficients} == 2 /\ (forall i. bounded (Seq.index ${coefficients} i) 4)"))]