proofs(mldsa): use newer z3 & context pruning by default

cryspen · Jan 30, 2025 · 6243218 · 6243218
1 parent b4495e7
commit 6243218
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 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
@@ -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
@@ -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
@@ -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)"))]