From c967919cafbb9ece765388a677691a405f2f2185 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Thu, 14 Nov 2024 15:53:01 +0100 Subject: [PATCH] Remove obsolete .fst --- .../fstar/extraction/Libcrux_ml_dsa.Simd.Traits.fst | 11 ----------- 1 file changed, 11 deletions(-) delete mode 100644 libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Traits.fst diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Traits.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Traits.fst deleted file mode 100644 index 5bf547714..000000000 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Traits.fst +++ /dev/null @@ -1,11 +0,0 @@ -module Libcrux_ml_dsa.Simd.Traits -#set-options "--fuel 0 --ifuel 1 --z3rlimit 100" -open Core -open FStar.Mul - -let montgomery_multiply_by_fer - (#v_S: Type0) - (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Operations v_S) - (simd_unit: v_S) - (fer: i32) - = f_montgomery_multiply_by_constant #v_S #FStar.Tactics.Typeclasses.solve simd_unit fer