From fcd795e6d33fb44130a9db4c989202bce5d00122 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 1 Feb 2024 11:03:43 +0100 Subject: [PATCH] patches --- proofs/fstar/extraction-edited.patch | 299 ++++++++---------- .../fstar/extraction-secret-independent.patch | 285 ++++++++--------- 2 files changed, 269 insertions(+), 315 deletions(-) diff --git a/proofs/fstar/extraction-edited.patch b/proofs/fstar/extraction-edited.patch index 62d11c66f..d47933a9c 100644 --- a/proofs/fstar/extraction-edited.patch +++ b/proofs/fstar/extraction-edited.patch @@ -1,5 +1,5 @@ diff -ruN extraction/Libcrux.Digest.fst extraction-edited/Libcrux.Digest.fst ---- extraction/Libcrux.Digest.fst 2024-01-31 17:22:55.439848529 +0100 +--- extraction/Libcrux.Digest.fst 2024-02-01 11:03:26.797761034 +0100 +++ extraction-edited/Libcrux.Digest.fst 1970-01-01 01:00:00.000000000 +0100 @@ -1,48 +0,0 @@ -module Libcrux.Digest @@ -51,8 +51,8 @@ diff -ruN extraction/Libcrux.Digest.fst extraction-edited/Libcrux.Digest.fst - then shake128x4_256_ v_LEN data0 data1 data2 data3 - else shake128x4_portable v_LEN data0 data1 data2 data3 diff -ruN extraction/Libcrux.Digest.fsti extraction-edited/Libcrux.Digest.fsti ---- extraction/Libcrux.Digest.fsti 2024-01-31 17:22:55.427848779 +0100 -+++ extraction-edited/Libcrux.Digest.fsti 2024-01-31 17:22:55.502847217 +0100 +--- extraction/Libcrux.Digest.fsti 2024-02-01 11:03:26.785761386 +0100 ++++ extraction-edited/Libcrux.Digest.fsti 2024-02-01 11:03:26.852759421 +0100 @@ -1,31 +1,41 @@ module Libcrux.Digest #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" @@ -124,7 +124,7 @@ diff -ruN extraction/Libcrux.Digest.fsti extraction-edited/Libcrux.Digest.fsti +val shake256 (v_LEN: usize) (data: t_Slice u8) : t_Array u8 v_LEN diff -ruN extraction/Libcrux.Kem.fst extraction-edited/Libcrux.Kem.fst --- extraction/Libcrux.Kem.fst 1970-01-01 01:00:00.000000000 +0100 -+++ extraction-edited/Libcrux.Kem.fst 2024-01-31 17:22:55.489847488 +0100 ++++ extraction-edited/Libcrux.Kem.fst 2024-02-01 11:03:26.840759773 +0100 @@ -0,0 +1,6 @@ +module Libcrux.Kem +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" @@ -133,8 +133,8 @@ diff -ruN extraction/Libcrux.Kem.fst extraction-edited/Libcrux.Kem.fst + + diff -ruN extraction/Libcrux.Kem.Kyber.Arithmetic.fst extraction-edited/Libcrux.Kem.Kyber.Arithmetic.fst ---- extraction/Libcrux.Kem.Kyber.Arithmetic.fst 2024-01-31 17:22:55.443848446 +0100 -+++ extraction-edited/Libcrux.Kem.Kyber.Arithmetic.fst 2024-01-31 17:22:55.483847613 +0100 +--- extraction/Libcrux.Kem.Kyber.Arithmetic.fst 2024-02-01 11:03:26.800760946 +0100 ++++ extraction-edited/Libcrux.Kem.Kyber.Arithmetic.fst 2024-02-01 11:03:26.836759890 +0100 @@ -1,81 +1,356 @@ module Libcrux.Kem.Kyber.Arithmetic -#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" @@ -532,8 +532,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Arithmetic.fst extraction-edited/Libcrux. + + diff -ruN extraction/Libcrux.Kem.Kyber.Arithmetic.fsti extraction-edited/Libcrux.Kem.Kyber.Arithmetic.fsti ---- extraction/Libcrux.Kem.Kyber.Arithmetic.fsti 2024-01-31 17:22:55.417848987 +0100 -+++ extraction-edited/Libcrux.Kem.Kyber.Arithmetic.fsti 2024-01-31 17:22:55.475847780 +0100 +--- extraction/Libcrux.Kem.Kyber.Arithmetic.fsti 2024-02-01 11:03:26.775761679 +0100 ++++ extraction-edited/Libcrux.Kem.Kyber.Arithmetic.fsti 2024-02-01 11:03:26.829760095 +0100 @@ -3,10 +3,32 @@ open Core open FStar.Mul @@ -567,7 +567,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Arithmetic.fsti extraction-edited/Libcrux let t_FieldElementTimesMontgomeryR = i32 unfold -@@ -16,119 +38,222 @@ +@@ -16,119 +38,211 @@ let v_BARRETT_SHIFT: i64 = 26L @@ -596,11 +596,6 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Arithmetic.fsti extraction-edited/Libcrux -val get_n_least_significant_bits (n: u8) (value: u32) - : Prims.Pure u32 - (requires n =. 4uy || n =. 5uy || n =. 10uy || n =. 11uy || n =. v_MONTGOMERY_SHIFT) -+let wf_fe_to_spec_fe (m: wfFieldElement): Spec.Kyber.field_element = -+ if v m < 0 -+ then v m + v Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS -+ else v m -+ +let to_spec_fe (m:i32) : Spec.Kyber.field_element = + int_to_spec_fe (v m) + @@ -771,12 +766,6 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Arithmetic.fsti extraction-edited/Libcrux + assert (forall i. Seq.index p i < v Spec.Kyber.v_FIELD_MODULUS); + p + -+let wf_poly_to_spec_poly (re: wfPolynomialRingElement): Spec.Kyber.polynomial -+ = let p = Spec.Kyber.map' (fun x -> wf_fe_to_spec_fe x <: nat) re.f_coefficients in -+ introduce forall i. Seq.index p i < v Spec.Kyber.v_FIELD_MODULUS -+ with assert (Seq.index p i == Seq.index p (v (sz i))); -+ p -+ +let to_spec_poly_b #b (m:t_PolynomialRingElement_b b) : (Spec.Kyber.polynomial) = + to_spec_poly (derefine_poly_b m) + @@ -884,8 +873,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Arithmetic.fsti extraction-edited/Libcrux - <: - bool)) diff -ruN extraction/Libcrux.Kem.Kyber.Compress.fst extraction-edited/Libcrux.Kem.Kyber.Compress.fst ---- extraction/Libcrux.Kem.Kyber.Compress.fst 2024-01-31 17:22:55.422848883 +0100 -+++ extraction-edited/Libcrux.Kem.Kyber.Compress.fst 2024-01-31 17:22:55.465847988 +0100 +--- extraction/Libcrux.Kem.Kyber.Compress.fst 2024-02-01 11:03:26.780761533 +0100 ++++ extraction-edited/Libcrux.Kem.Kyber.Compress.fst 2024-02-01 11:03:26.819760389 +0100 @@ -1,39 +1,79 @@ module Libcrux.Kem.Kyber.Compress -#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" @@ -989,8 +978,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Compress.fst extraction-edited/Libcrux.Ke + res <: Libcrux.Kem.Kyber.Arithmetic.i32_b 3328 +#pop-options diff -ruN extraction/Libcrux.Kem.Kyber.Compress.fsti extraction-edited/Libcrux.Kem.Kyber.Compress.fsti ---- extraction/Libcrux.Kem.Kyber.Compress.fsti 2024-01-31 17:22:55.404849258 +0100 -+++ extraction-edited/Libcrux.Kem.Kyber.Compress.fsti 2024-01-31 17:22:55.497847322 +0100 +--- extraction/Libcrux.Kem.Kyber.Compress.fsti 2024-02-01 11:03:26.762762061 +0100 ++++ extraction-edited/Libcrux.Kem.Kyber.Compress.fsti 2024-02-01 11:03:26.847759568 +0100 @@ -3,8 +3,19 @@ open Core open FStar.Mul @@ -1056,8 +1045,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Compress.fsti extraction-edited/Libcrux.K + (requires fe =. 0l || fe =. 1l) + (fun result -> v result >= 0 /\ v result < 3329) diff -ruN extraction/Libcrux.Kem.Kyber.Constants.fsti extraction-edited/Libcrux.Kem.Kyber.Constants.fsti ---- extraction/Libcrux.Kem.Kyber.Constants.fsti 2024-01-31 17:22:55.437848571 +0100 -+++ extraction-edited/Libcrux.Kem.Kyber.Constants.fsti 2024-01-31 17:22:55.467847946 +0100 +--- extraction/Libcrux.Kem.Kyber.Constants.fsti 2024-02-01 11:03:26.795761093 +0100 ++++ extraction-edited/Libcrux.Kem.Kyber.Constants.fsti 2024-02-01 11:03:26.821760330 +0100 @@ -15,7 +15,8 @@ let v_FIELD_MODULUS: i32 = 3329l @@ -1069,8 +1058,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Constants.fsti extraction-edited/Libcrux. let v_REJECTION_SAMPLING_SEED_SIZE: usize = sz 168 *! sz 5 diff -ruN extraction/Libcrux.Kem.Kyber.Constant_time_ops.fst extraction-edited/Libcrux.Kem.Kyber.Constant_time_ops.fst ---- extraction/Libcrux.Kem.Kyber.Constant_time_ops.fst 2024-01-31 17:22:55.445848404 +0100 -+++ extraction-edited/Libcrux.Kem.Kyber.Constant_time_ops.fst 2024-01-31 17:22:55.478847717 +0100 +--- extraction/Libcrux.Kem.Kyber.Constant_time_ops.fst 2024-02-01 11:03:26.802760887 +0100 ++++ extraction-edited/Libcrux.Kem.Kyber.Constant_time_ops.fst 2024-02-01 11:03:26.832760008 +0100 @@ -4,56 +4,163 @@ open FStar.Mul @@ -1256,8 +1245,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Constant_time_ops.fst extraction-edited/L + ) +#pop-options diff -ruN extraction/Libcrux.Kem.Kyber.Constant_time_ops.fsti extraction-edited/Libcrux.Kem.Kyber.Constant_time_ops.fsti ---- extraction/Libcrux.Kem.Kyber.Constant_time_ops.fsti 2024-01-31 17:22:55.441848488 +0100 -+++ extraction-edited/Libcrux.Kem.Kyber.Constant_time_ops.fsti 2024-01-31 17:22:55.485847571 +0100 +--- extraction/Libcrux.Kem.Kyber.Constant_time_ops.fsti 2024-02-01 11:03:26.798761005 +0100 ++++ extraction-edited/Libcrux.Kem.Kyber.Constant_time_ops.fsti 2024-02-01 11:03:26.837759861 +0100 @@ -20,7 +20,8 @@ val compare_ciphertexts_in_constant_time (v_CIPHERTEXT_SIZE: usize) (lhs rhs: t_Slice u8) @@ -1289,8 +1278,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Constant_time_ops.fsti extraction-edited/ + Hax_lib.implies (selector =. 0uy <: bool) (fun _ -> result =. lhs <: bool) && + Hax_lib.implies (selector <>. 0uy <: bool) (fun _ -> result =. rhs <: bool)) diff -ruN extraction/Libcrux.Kem.Kyber.fst extraction-edited/Libcrux.Kem.Kyber.fst ---- extraction/Libcrux.Kem.Kyber.fst 2024-01-31 17:22:55.405849237 +0100 -+++ extraction-edited/Libcrux.Kem.Kyber.fst 2024-01-31 17:22:55.470847884 +0100 +--- extraction/Libcrux.Kem.Kyber.fst 2024-02-01 11:03:26.764762002 +0100 ++++ extraction-edited/Libcrux.Kem.Kyber.fst 2024-02-01 11:03:26.824760242 +0100 @@ -1,12 +1,29 @@ module Libcrux.Kem.Kyber -#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" @@ -1565,8 +1554,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.fst extraction-edited/Libcrux.Kem.Kyber.f + (Core.Convert.f_into public_key <: Libcrux.Kem.Kyber.Types.t_KyberPublicKey v_PUBLIC_KEY_SIZE) + diff -ruN extraction/Libcrux.Kem.Kyber.fsti extraction-edited/Libcrux.Kem.Kyber.fsti ---- extraction/Libcrux.Kem.Kyber.fsti 2024-01-31 17:22:55.432848675 +0100 -+++ extraction-edited/Libcrux.Kem.Kyber.fsti 2024-01-31 17:22:55.500847259 +0100 +--- extraction/Libcrux.Kem.Kyber.fsti 2024-02-01 11:03:26.791761210 +0100 ++++ extraction-edited/Libcrux.Kem.Kyber.fsti 2024-02-01 11:03:26.850759480 +0100 @@ -4,42 +4,81 @@ open FStar.Mul @@ -1671,8 +1660,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.fsti extraction-edited/Libcrux.Kem.Kyber. + (ensures (fun kp -> + (kp.f_sk.f_value,kp.f_pk.f_value) == Spec.Kyber.ind_cca_generate_keypair p randomness)) diff -ruN extraction/Libcrux.Kem.Kyber.Hash_functions.fst extraction-edited/Libcrux.Kem.Kyber.Hash_functions.fst ---- extraction/Libcrux.Kem.Kyber.Hash_functions.fst 2024-01-31 17:22:55.446848384 +0100 -+++ extraction-edited/Libcrux.Kem.Kyber.Hash_functions.fst 2024-01-31 17:22:55.476847759 +0100 +--- extraction/Libcrux.Kem.Kyber.Hash_functions.fst 2024-02-01 11:03:26.803760858 +0100 ++++ extraction-edited/Libcrux.Kem.Kyber.Hash_functions.fst 2024-02-01 11:03:26.830760066 +0100 @@ -3,18 +3,27 @@ open Core open FStar.Mul @@ -1712,8 +1701,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Hash_functions.fst extraction-edited/Libc + admit(); //P-F out diff -ruN extraction/Libcrux.Kem.Kyber.Hash_functions.fsti extraction-edited/Libcrux.Kem.Kyber.Hash_functions.fsti ---- extraction/Libcrux.Kem.Kyber.Hash_functions.fsti 2024-01-31 17:22:55.400849341 +0100 -+++ extraction-edited/Libcrux.Kem.Kyber.Hash_functions.fsti 2024-01-31 17:22:55.505847155 +0100 +--- extraction/Libcrux.Kem.Kyber.Hash_functions.fsti 2024-02-01 11:03:26.758762178 +0100 ++++ extraction-edited/Libcrux.Kem.Kyber.Hash_functions.fsti 2024-02-01 11:03:26.855759333 +0100 @@ -3,12 +3,24 @@ open Core open FStar.Mul @@ -1744,8 +1733,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Hash_functions.fsti extraction-edited/Lib + (forall i. i < v v_K ==> Seq.index res i == Spec.Kyber.v_XOF (sz 840) (Seq.index input i)))) + diff -ruN extraction/Libcrux.Kem.Kyber.Ind_cpa.fst extraction-edited/Libcrux.Kem.Kyber.Ind_cpa.fst ---- extraction/Libcrux.Kem.Kyber.Ind_cpa.fst 2024-01-31 17:22:55.407849196 +0100 -+++ extraction-edited/Libcrux.Kem.Kyber.Ind_cpa.fst 2024-01-31 17:22:55.504847176 +0100 +--- extraction/Libcrux.Kem.Kyber.Ind_cpa.fst 2024-02-01 11:03:26.765761973 +0100 ++++ extraction-edited/Libcrux.Kem.Kyber.Ind_cpa.fst 2024-02-01 11:03:26.853759392 +0100 @@ -1,5 +1,5 @@ module Libcrux.Kem.Kyber.Ind_cpa -#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" @@ -2456,8 +2445,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Ind_cpa.fst extraction-edited/Libcrux.Kem + res + diff -ruN extraction/Libcrux.Kem.Kyber.Ind_cpa.fsti extraction-edited/Libcrux.Kem.Kyber.Ind_cpa.fsti ---- extraction/Libcrux.Kem.Kyber.Ind_cpa.fsti 2024-01-31 17:22:55.450848300 +0100 -+++ extraction-edited/Libcrux.Kem.Kyber.Ind_cpa.fsti 2024-01-31 17:22:55.492847426 +0100 +--- extraction/Libcrux.Kem.Kyber.Ind_cpa.fsti 2024-02-01 11:03:26.806760770 +0100 ++++ extraction-edited/Libcrux.Kem.Kyber.Ind_cpa.fsti 2024-02-01 11:03:26.843759685 +0100 @@ -1,80 +1,152 @@ module Libcrux.Kem.Kyber.Ind_cpa -#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" @@ -2660,8 +2649,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Ind_cpa.fsti extraction-edited/Libcrux.Ke + + diff -ruN extraction/Libcrux.Kem.Kyber.Kyber1024.fst extraction-edited/Libcrux.Kem.Kyber.Kyber1024.fst ---- extraction/Libcrux.Kem.Kyber.Kyber1024.fst 2024-01-31 17:22:55.434848633 +0100 -+++ extraction-edited/Libcrux.Kem.Kyber.Kyber1024.fst 2024-01-31 17:22:55.460848092 +0100 +--- extraction/Libcrux.Kem.Kyber.Kyber1024.fst 2024-02-01 11:03:26.792761181 +0100 ++++ extraction-edited/Libcrux.Kem.Kyber.Kyber1024.fst 2024-02-01 11:03:26.815760506 +0100 @@ -3,37 +3,23 @@ open Core open FStar.Mul @@ -2714,8 +2703,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Kyber1024.fst extraction-edited/Libcrux.K (sz 3168) (sz 1568) diff -ruN extraction/Libcrux.Kem.Kyber.Kyber1024.fsti extraction-edited/Libcrux.Kem.Kyber.Kyber1024.fsti ---- extraction/Libcrux.Kem.Kyber.Kyber1024.fsti 2024-01-31 17:22:55.429848737 +0100 -+++ extraction-edited/Libcrux.Kem.Kyber.Kyber1024.fsti 2024-01-31 17:22:55.462848050 +0100 +--- extraction/Libcrux.Kem.Kyber.Kyber1024.fsti 2024-02-01 11:03:26.787761327 +0100 ++++ extraction-edited/Libcrux.Kem.Kyber.Kyber1024.fsti 2024-02-01 11:03:26.816760477 +0100 @@ -63,32 +63,27 @@ Libcrux.Kem.Kyber.Constants.v_SHARED_SECRET_SIZE +! v_CPA_PKE_CIPHERTEXT_SIZE_1024_ @@ -2761,8 +2750,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Kyber1024.fsti extraction-edited/Libcrux. Prims.l_True (fun _ -> Prims.l_True) diff -ruN extraction/Libcrux.Kem.Kyber.Kyber512.fst extraction-edited/Libcrux.Kem.Kyber.Kyber512.fst ---- extraction/Libcrux.Kem.Kyber.Kyber512.fst 2024-01-31 17:22:55.398849383 +0100 -+++ extraction-edited/Libcrux.Kem.Kyber.Kyber512.fst 2024-01-31 17:22:55.482847634 +0100 +--- extraction/Libcrux.Kem.Kyber.Kyber512.fst 2024-02-01 11:03:26.756762236 +0100 ++++ extraction-edited/Libcrux.Kem.Kyber.Kyber512.fst 2024-02-01 11:03:26.835759920 +0100 @@ -3,37 +3,23 @@ open Core open FStar.Mul @@ -2815,8 +2804,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Kyber512.fst extraction-edited/Libcrux.Ke (sz 1632) (sz 800) diff -ruN extraction/Libcrux.Kem.Kyber.Kyber512.fsti extraction-edited/Libcrux.Kem.Kyber.Kyber512.fsti ---- extraction/Libcrux.Kem.Kyber.Kyber512.fsti 2024-01-31 17:22:55.435848613 +0100 -+++ extraction-edited/Libcrux.Kem.Kyber.Kyber512.fsti 2024-01-31 17:22:55.457848154 +0100 +--- extraction/Libcrux.Kem.Kyber.Kyber512.fsti 2024-02-01 11:03:26.794761122 +0100 ++++ extraction-edited/Libcrux.Kem.Kyber.Kyber512.fsti 2024-02-01 11:03:26.812760594 +0100 @@ -63,32 +63,27 @@ Libcrux.Kem.Kyber.Constants.v_SHARED_SECRET_SIZE +! v_CPA_PKE_CIPHERTEXT_SIZE_512_ @@ -2862,8 +2851,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Kyber512.fsti extraction-edited/Libcrux.K Prims.l_True (fun _ -> Prims.l_True) diff -ruN extraction/Libcrux.Kem.Kyber.Kyber768.fst extraction-edited/Libcrux.Kem.Kyber.Kyber768.fst ---- extraction/Libcrux.Kem.Kyber.Kyber768.fst 2024-01-31 17:22:55.402849300 +0100 -+++ extraction-edited/Libcrux.Kem.Kyber.Kyber768.fst 2024-01-31 17:22:55.480847675 +0100 +--- extraction/Libcrux.Kem.Kyber.Kyber768.fst 2024-02-01 11:03:26.760762119 +0100 ++++ extraction-edited/Libcrux.Kem.Kyber.Kyber768.fst 2024-02-01 11:03:26.833759978 +0100 @@ -3,37 +3,24 @@ open Core open FStar.Mul @@ -2917,8 +2906,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Kyber768.fst extraction-edited/Libcrux.Ke (sz 2400) (sz 1184) diff -ruN extraction/Libcrux.Kem.Kyber.Kyber768.fsti extraction-edited/Libcrux.Kem.Kyber.Kyber768.fsti ---- extraction/Libcrux.Kem.Kyber.Kyber768.fsti 2024-01-31 17:22:55.425848821 +0100 -+++ extraction-edited/Libcrux.Kem.Kyber.Kyber768.fsti 2024-01-31 17:22:55.468847925 +0100 +--- extraction/Libcrux.Kem.Kyber.Kyber768.fsti 2024-02-01 11:03:26.784761415 +0100 ++++ extraction-edited/Libcrux.Kem.Kyber.Kyber768.fsti 2024-02-01 11:03:26.822760301 +0100 @@ -63,32 +63,30 @@ Libcrux.Kem.Kyber.Constants.v_SHARED_SECRET_SIZE +! v_CPA_PKE_CIPHERTEXT_SIZE_768_ @@ -2973,8 +2962,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Kyber768.fsti extraction-edited/Libcrux.K + (ensures (fun kp -> (kp.f_sk.f_value,kp.f_pk.f_value) == Spec.Kyber.kyber768_generate_keypair randomness)) + diff -ruN extraction/Libcrux.Kem.Kyber.Matrix.fst extraction-edited/Libcrux.Kem.Kyber.Matrix.fst ---- extraction/Libcrux.Kem.Kyber.Matrix.fst 2024-01-31 17:22:55.412849091 +0100 -+++ extraction-edited/Libcrux.Kem.Kyber.Matrix.fst 2024-01-31 17:22:55.509847072 +0100 +--- extraction/Libcrux.Kem.Kyber.Matrix.fst 2024-02-01 11:03:26.770761826 +0100 ++++ extraction-edited/Libcrux.Kem.Kyber.Matrix.fst 2024-02-01 11:03:26.858759245 +0100 @@ -3,192 +3,188 @@ open Core open FStar.Mul @@ -3765,8 +3754,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Matrix.fst extraction-edited/Libcrux.Kem. + admit(); //P-F v_A_transpose diff -ruN extraction/Libcrux.Kem.Kyber.Matrix.fsti extraction-edited/Libcrux.Kem.Kyber.Matrix.fsti ---- extraction/Libcrux.Kem.Kyber.Matrix.fsti 2024-01-31 17:22:55.418848967 +0100 -+++ extraction-edited/Libcrux.Kem.Kyber.Matrix.fsti 2024-01-31 17:22:55.491847446 +0100 +--- extraction/Libcrux.Kem.Kyber.Matrix.fsti 2024-02-01 11:03:26.777761621 +0100 ++++ extraction-edited/Libcrux.Kem.Kyber.Matrix.fsti 2024-02-01 11:03:26.842759714 +0100 @@ -3,39 +3,71 @@ open Core open FStar.Mul @@ -3869,8 +3858,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Matrix.fsti extraction-edited/Libcrux.Kem + if transpose then Libcrux.Kem.Kyber.Arithmetic.to_spec_matrix_b #p res == matrix_A + else Libcrux.Kem.Kyber.Arithmetic.to_spec_matrix_b #p res == Spec.Kyber.matrix_transpose matrix_A) diff -ruN extraction/Libcrux.Kem.Kyber.Ntt.fst extraction-edited/Libcrux.Kem.Kyber.Ntt.fst ---- extraction/Libcrux.Kem.Kyber.Ntt.fst 2024-01-31 17:22:55.420848925 +0100 -+++ extraction-edited/Libcrux.Kem.Kyber.Ntt.fst 2024-01-31 17:22:55.473847821 +0100 +--- extraction/Libcrux.Kem.Kyber.Ntt.fst 2024-02-01 11:03:26.779761562 +0100 ++++ extraction-edited/Libcrux.Kem.Kyber.Ntt.fst 2024-02-01 11:03:26.827760154 +0100 @@ -1,56 +1,130 @@ module Libcrux.Kem.Kyber.Ntt -#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" @@ -4801,8 +4790,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Ntt.fst extraction-edited/Libcrux.Kem.Kyb + down_cast_poly_b #(8*3328) #3328 re +#pop-options diff -ruN extraction/Libcrux.Kem.Kyber.Ntt.fsti extraction-edited/Libcrux.Kem.Kyber.Ntt.fsti ---- extraction/Libcrux.Kem.Kyber.Ntt.fsti 2024-01-31 17:22:55.424848842 +0100 -+++ extraction-edited/Libcrux.Kem.Kyber.Ntt.fsti 2024-01-31 17:22:55.455848196 +0100 +--- extraction/Libcrux.Kem.Kyber.Ntt.fsti 2024-02-01 11:03:26.782761474 +0100 ++++ extraction-edited/Libcrux.Kem.Kyber.Ntt.fsti 2024-02-01 11:03:26.811760624 +0100 @@ -2,223 +2,80 @@ #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core @@ -5095,8 +5084,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Ntt.fsti extraction-edited/Libcrux.Kem.Ky + (ensures fun _ -> True) + diff -ruN extraction/Libcrux.Kem.Kyber.Sampling.fst extraction-edited/Libcrux.Kem.Kyber.Sampling.fst ---- extraction/Libcrux.Kem.Kyber.Sampling.fst 2024-01-31 17:22:55.448848342 +0100 -+++ extraction-edited/Libcrux.Kem.Kyber.Sampling.fst 2024-01-31 17:22:55.498847301 +0100 +--- extraction/Libcrux.Kem.Kyber.Sampling.fst 2024-02-01 11:03:26.805760800 +0100 ++++ extraction-edited/Libcrux.Kem.Kyber.Sampling.fst 2024-02-01 11:03:26.849759509 +0100 @@ -3,27 +3,34 @@ open Core open FStar.Mul @@ -5509,8 +5498,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Sampling.fst extraction-edited/Libcrux.Ke + out +#pop-options diff -ruN extraction/Libcrux.Kem.Kyber.Sampling.fsti extraction-edited/Libcrux.Kem.Kyber.Sampling.fsti ---- extraction/Libcrux.Kem.Kyber.Sampling.fsti 2024-01-31 17:22:55.415849029 +0100 -+++ extraction-edited/Libcrux.Kem.Kyber.Sampling.fsti 2024-01-31 17:22:55.507847113 +0100 +--- extraction/Libcrux.Kem.Kyber.Sampling.fsti 2024-02-01 11:03:26.774761709 +0100 ++++ extraction-edited/Libcrux.Kem.Kyber.Sampling.fsti 2024-02-01 11:03:26.856759304 +0100 @@ -3,77 +3,37 @@ open Core open FStar.Mul @@ -5611,9 +5600,9 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Sampling.fsti extraction-edited/Libcrux.K +// (ensures fun result -> (forall i. v (result.f_coefficients.[i]) >= 0)) + diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.Kem.Kyber.Serialize.fst ---- extraction/Libcrux.Kem.Kyber.Serialize.fst 2024-01-31 17:22:55.430848717 +0100 -+++ extraction-edited/Libcrux.Kem.Kyber.Serialize.fst 2024-01-31 17:22:55.463848030 +0100 -@@ -1,8 +1,13 @@ +--- extraction/Libcrux.Kem.Kyber.Serialize.fst 2024-02-01 11:03:26.789761269 +0100 ++++ extraction-edited/Libcrux.Kem.Kyber.Serialize.fst 2024-02-01 11:03:26.818760418 +0100 +@@ -1,8 +1,14 @@ module Libcrux.Kem.Kyber.Serialize -#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +#set-options "--fuel 0 --ifuel 0 --z3rlimit 50 --retry 3" @@ -5624,17 +5613,19 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K + +open MkSeq + -+#push-options "--z3rlimit 50" ++#push-options "--z3rlimit 80" ++[@@"opaque_to_smt"] let compress_coefficients_10_ (coefficient1 coefficient2 coefficient3 coefficient4: i32) = let coef1:u8 = cast (coefficient1 &. 255l <: i32) <: u8 in let coef2:u8 = -@@ -19,11 +24,11 @@ +@@ -19,11 +25,12 @@ in let coef5:u8 = cast ((coefficient4 >>! 2l <: i32) &. 255l <: i32) <: u8 in coef1, coef2, coef3, coef4, coef5 <: (u8 & u8 & u8 & u8 & u8) +#pop-options +#push-options "--ifuel 1 --z3rlimit 600 --split_queries always" ++[@@"opaque_to_smt"] let compress_coefficients_11_ - (coefficient1 coefficient2 coefficient3 coefficient4 coefficient5 coefficient6 coefficient7 coefficient8: - i32) @@ -5643,7 +5634,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K let coef1:u8 = cast (coefficient1 <: i32) <: u8 in let coef2:u8 = ((cast (coefficient2 &. 31l <: i32) <: u8) <>! 2l <: u8) in coef1, coef2, coef3, coef4, coef5 <: (u8 & u8 & u8 & u8 & u8) @@ -5682,6 +5675,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K -let decompress_coefficients_10_ (byte2 byte1 byte3 byte4 byte5: i32) = +#push-options "--z3rlimit 500" ++[@@"opaque_to_smt"] +let decompress_coefficients_10_ byte2 byte1 byte3 byte4 byte5 = let coefficient1:i32 = ((byte2 &. 3l <: i32) <>! 2l <: i32) in @@ -5696,6 +5690,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K +#pop-options +#push-options "--z3rlimit 300" ++[@@"opaque_to_smt"] let decompress_coefficients_11_ - (byte2 byte1 byte3 byte5 byte4 byte6 byte7 byte9 byte8 byte10 byte11: i32) - = @@ -5703,7 +5698,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K let coefficient1:i32 = ((byte2 &. 7l <: i32) <>! 3l <: i32) in let coefficient3:i32 = -@@ -109,6 +125,14 @@ +@@ -109,6 +131,14 @@ in let coefficient7:i32 = ((byte10 &. 31l <: i32) <>! 2l <: i32) in let coefficient8:i32 = (byte11 <>! 5l <: i32) in @@ -5718,7 +5713,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K coefficient1, coefficient2, coefficient3, -@@ -117,15 +141,19 @@ +@@ -117,15 +147,21 @@ coefficient6, coefficient7, coefficient8 @@ -5728,22 +5723,25 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K -let decompress_coefficients_4_ (byte: u8) = +#push-options "--z3rlimit 50" ++[@@"opaque_to_smt"] +let decompress_coefficients_4_ byte = let coefficient1:i32 = cast (byte &. 15uy <: u8) <: i32 in let coefficient2:i32 = cast ((byte >>! 4l <: u8) &. 15uy <: u8) <: i32 in - coefficient1, coefficient2 <: (i32 & i32) +- +-let decompress_coefficients_5_ (byte1 byte2 byte3 byte4 byte5: i32) = + lemma_get_bit_bounded' coefficient1 4; + lemma_get_bit_bounded' coefficient2 4; + coefficient1, coefficient2 +#pop-options - --let decompress_coefficients_5_ (byte1 byte2 byte3 byte4 byte5: i32) = ++ +#push-options "--z3rlimit 400" ++[@@"opaque_to_smt"] +let decompress_coefficients_5_ byte1 byte2 byte3 byte4 byte5 = let coefficient1:i32 = byte1 &. 31l in let coefficient2:i32 = ((byte2 &. 3l <: i32) <>! 5l <: i32) in let coefficient3:i32 = (byte2 >>! 2l <: i32) &. 31l in -@@ -134,6 +162,14 @@ +@@ -134,6 +170,14 @@ let coefficient6:i32 = (byte4 >>! 1l <: i32) &. 31l in let coefficient7:i32 = ((byte5 &. 7l <: i32) <>! 6l <: i32) in let coefficient8:i32 = byte5 >>! 3l in @@ -5758,14 +5756,14 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K coefficient1, coefficient2, coefficient3, -@@ -142,31 +178,50 @@ +@@ -142,31 +186,54 @@ coefficient6, coefficient7, coefficient8 - <: - (i32 & i32 & i32 & i32 & i32 & i32 & i32 & i32) +#pop-options - ++ +let cast_bound_lemma + #t #u + (n: int_t t) @@ -5775,7 +5773,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K + [SMTPat (bounded n d); SMTPat (cast #(int_t t) #(int_t u) n)] + = () + -+#push-options "--z3rlimit 60" ++#push-options "--z3rlimit 90" ++[@@"opaque_to_smt"] +let int_t_d_cast_lemma #t #u d (n: int_t_d t d) + : Lemma (requires bits t < bits u /\ v n >= 0) + (ensures bounded (cast #(int_t t) #(int_t u) n) d) @@ -5789,8 +5788,11 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K + = Math.Lemmas.pow2_plus 8 8; + Math.Lemmas.pow2_le_compat 32 16 +#pop-options + ++#restart-solver + +#push-options "--fuel 0 --ifuel 1 --query_stats --z3rlimit 100" ++[@@"opaque_to_smt"] let compress_then_serialize_10_ - (v_OUT_LEN: usize) - (re: Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement) @@ -5828,13 +5830,14 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K let coefficient1:i32 = Libcrux.Kem.Kyber.Compress.compress_ciphertext_coefficient 10uy (Libcrux.Kem.Kyber.Arithmetic.to_unsigned_representative (coefficients.[ sz 0 ] <: i32 -@@ -226,79 +281,95 @@ +@@ -226,79 +293,96 @@ serialized) in serialized +#pop-options -+ + +#push-options "--fuel 0 --ifuel 0 --z3rlimit 30" ++[@@"opaque_to_smt"] +let update5 + #n + (s: t_Array 't n) @@ -5856,7 +5859,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K + let s = update_at_usize s (offset +! sz 4) i4 in + s +#pop-options - ++ +#push-options "--fuel 0 --ifuel 1 --z3rlimit 100 --query_stats --split_queries no" let compress_then_serialize_11_ - (v_OUT_LEN: usize) @@ -5948,7 +5951,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K Libcrux.Kem.Kyber.Compress.compress_ciphertext_coefficient 11uy (Libcrux.Kem.Kyber.Arithmetic.to_unsigned_representative (coefficients.[ sz 7 ] <: i32 ) -@@ -324,6 +395,8 @@ +@@ -324,6 +408,8 @@ coefficient7 coefficient8 in @@ -5957,7 +5960,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K let serialized:t_Array u8 v_OUT_LEN = Rust_primitives.Hax.Monomorphized_update_at.update_at_usize serialized (sz 11 *! i <: usize) -@@ -382,29 +455,20 @@ +@@ -382,29 +468,20 @@ serialized) in serialized @@ -5995,7 +5998,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K let coefficient1:u8 = cast (Libcrux.Kem.Kyber.Compress.compress_ciphertext_coefficient 4uy (Libcrux.Kem.Kyber.Arithmetic.to_unsigned_representative (coefficients.[ sz 0 ] -@@ -439,27 +503,20 @@ +@@ -439,27 +516,20 @@ serialized let compress_then_serialize_5_ @@ -6032,7 +6035,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K let coefficient1:u8 = cast (Libcrux.Kem.Kyber.Compress.compress_ciphertext_coefficient 5uy (Libcrux.Kem.Kyber.Arithmetic.to_unsigned_representative (coefficients.[ sz 0 ] -@@ -544,6 +601,14 @@ +@@ -544,6 +614,14 @@ <: u8 in @@ -6047,7 +6050,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K let coefficient8:u8 = cast (Libcrux.Kem.Kyber.Compress.compress_ciphertext_coefficient 5uy (Libcrux.Kem.Kyber.Arithmetic.to_unsigned_representative (coefficients.[ sz 7 ] -@@ -566,6 +631,8 @@ +@@ -566,6 +644,8 @@ coefficient6 coefficient8 in @@ -6056,7 +6059,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K let serialized:t_Array u8 v_OUT_LEN = Rust_primitives.Hax.Monomorphized_update_at.update_at_usize serialized (sz 5 *! i <: usize) -@@ -595,35 +662,24 @@ +@@ -595,35 +675,24 @@ in serialized @@ -6102,7 +6105,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K let coefficient:u16 = Libcrux.Kem.Kyber.Arithmetic.to_unsigned_representative coefficient in -@@ -636,27 +692,35 @@ +@@ -636,27 +705,35 @@ <: t_Array u8 (sz 32)) in @@ -6147,7 +6150,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K match cast (v_COMPRESSION_FACTOR <: usize) <: u32 with | 4ul -> compress_then_serialize_4_ v_OUT_LEN re | 5ul -> compress_then_serialize_5_ v_OUT_LEN re -@@ -665,32 +729,49 @@ +@@ -665,32 +742,49 @@ <: Rust_primitives.Hax.t_Never) @@ -6216,7 +6219,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -698,14 +779,12 @@ +@@ -698,14 +792,12 @@ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re .Libcrux.Kem.Kyber.Arithmetic.f_coefficients (sz 4 *! i <: usize) @@ -6234,7 +6237,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -713,14 +792,12 @@ +@@ -713,14 +805,12 @@ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re .Libcrux.Kem.Kyber.Arithmetic.f_coefficients ((sz 4 *! i <: usize) +! sz 1 <: usize) @@ -6252,7 +6255,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -728,14 +805,12 @@ +@@ -728,14 +818,12 @@ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re .Libcrux.Kem.Kyber.Arithmetic.f_coefficients ((sz 4 *! i <: usize) +! sz 2 <: usize) @@ -6270,7 +6273,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -743,44 +818,43 @@ +@@ -743,44 +831,43 @@ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re .Libcrux.Kem.Kyber.Arithmetic.f_coefficients ((sz 4 *! i <: usize) +! sz 3 <: usize) @@ -6341,7 +6344,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K let coefficient1, coefficient2, -@@ -789,11 +863,21 @@ +@@ -789,11 +876,21 @@ coefficient5, coefficient6, coefficient7, @@ -6365,7 +6368,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -801,14 +885,12 @@ +@@ -801,14 +898,12 @@ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re .Libcrux.Kem.Kyber.Arithmetic.f_coefficients (sz 8 *! i <: usize) @@ -6383,7 +6386,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -816,14 +898,12 @@ +@@ -816,14 +911,12 @@ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re .Libcrux.Kem.Kyber.Arithmetic.f_coefficients ((sz 8 *! i <: usize) +! sz 1 <: usize) @@ -6401,7 +6404,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -831,14 +911,12 @@ +@@ -831,14 +924,12 @@ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re .Libcrux.Kem.Kyber.Arithmetic.f_coefficients ((sz 8 *! i <: usize) +! sz 2 <: usize) @@ -6419,7 +6422,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -846,14 +924,12 @@ +@@ -846,14 +937,12 @@ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re .Libcrux.Kem.Kyber.Arithmetic.f_coefficients ((sz 8 *! i <: usize) +! sz 3 <: usize) @@ -6437,7 +6440,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -861,14 +937,12 @@ +@@ -861,14 +950,12 @@ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re .Libcrux.Kem.Kyber.Arithmetic.f_coefficients ((sz 8 *! i <: usize) +! sz 4 <: usize) @@ -6455,7 +6458,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -876,14 +950,12 @@ +@@ -876,14 +963,12 @@ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re .Libcrux.Kem.Kyber.Arithmetic.f_coefficients ((sz 8 *! i <: usize) +! sz 5 <: usize) @@ -6473,7 +6476,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -891,14 +963,12 @@ +@@ -891,14 +976,12 @@ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re .Libcrux.Kem.Kyber.Arithmetic.f_coefficients ((sz 8 *! i <: usize) +! sz 6 <: usize) @@ -6491,7 +6494,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -906,35 +976,33 @@ +@@ -906,35 +989,33 @@ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re .Libcrux.Kem.Kyber.Arithmetic.f_coefficients ((sz 8 *! i <: usize) +! sz 7 <: usize) @@ -6542,7 +6545,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -947,9 +1015,9 @@ +@@ -947,9 +1028,9 @@ i32) } <: @@ -6554,7 +6557,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -962,33 +1030,32 @@ +@@ -962,33 +1043,32 @@ i32) } <: @@ -6605,7 +6608,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K let coefficient1, coefficient2, -@@ -997,10 +1064,25 @@ +@@ -997,10 +1077,25 @@ coefficient5, coefficient6, coefficient7, @@ -6633,7 +6636,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -1008,14 +1090,12 @@ +@@ -1008,14 +1103,12 @@ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re .Libcrux.Kem.Kyber.Arithmetic.f_coefficients (sz 8 *! i <: usize) @@ -6651,7 +6654,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -1023,14 +1103,12 @@ +@@ -1023,14 +1116,12 @@ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re .Libcrux.Kem.Kyber.Arithmetic.f_coefficients ((sz 8 *! i <: usize) +! sz 1 <: usize) @@ -6669,7 +6672,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -1038,14 +1116,12 @@ +@@ -1038,14 +1129,12 @@ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re .Libcrux.Kem.Kyber.Arithmetic.f_coefficients ((sz 8 *! i <: usize) +! sz 2 <: usize) @@ -6687,7 +6690,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -1053,14 +1129,12 @@ +@@ -1053,14 +1142,12 @@ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re .Libcrux.Kem.Kyber.Arithmetic.f_coefficients ((sz 8 *! i <: usize) +! sz 3 <: usize) @@ -6705,7 +6708,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -1068,14 +1142,12 @@ +@@ -1068,14 +1155,12 @@ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re .Libcrux.Kem.Kyber.Arithmetic.f_coefficients ((sz 8 *! i <: usize) +! sz 4 <: usize) @@ -6723,7 +6726,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -1083,14 +1155,12 @@ +@@ -1083,14 +1168,12 @@ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re .Libcrux.Kem.Kyber.Arithmetic.f_coefficients ((sz 8 *! i <: usize) +! sz 5 <: usize) @@ -6741,7 +6744,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -1098,14 +1168,12 @@ +@@ -1098,14 +1181,12 @@ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re .Libcrux.Kem.Kyber.Arithmetic.f_coefficients ((sz 8 *! i <: usize) +! sz 6 <: usize) @@ -6759,7 +6762,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -1113,33 +1181,27 @@ +@@ -1113,33 +1194,27 @@ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re .Libcrux.Kem.Kyber.Arithmetic.f_coefficients ((sz 8 *! i <: usize) +! sz 7 <: usize) @@ -6803,7 +6806,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K let i, byte:(usize & u8) = temp_1_ in Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({ Core.Ops.Range.f_start = sz 0; -@@ -1151,10 +1213,11 @@ +@@ -1151,10 +1226,11 @@ Core.Ops.Range.t_Range usize) re (fun re j -> @@ -6817,7 +6820,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -1168,19 +1231,20 @@ +@@ -1168,19 +1244,20 @@ i32) } <: @@ -6844,7 +6847,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K match cast (v_COMPRESSION_FACTOR <: usize) <: u32 with | 10ul -> deserialize_then_decompress_10_ serialized | 11ul -> deserialize_then_decompress_11_ serialized -@@ -1190,11 +1254,11 @@ +@@ -1190,11 +1267,11 @@ <: Rust_primitives.Hax.t_Never) @@ -6860,7 +6863,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K match cast (v_COMPRESSION_FACTOR <: usize) <: u32 with | 4ul -> deserialize_then_decompress_4_ serialized | 5ul -> deserialize_then_decompress_5_ serialized -@@ -1203,27 +1267,32 @@ +@@ -1203,27 +1280,32 @@ <: Rust_primitives.Hax.t_Never) @@ -6869,7 +6872,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K + res -let deserialize_to_uncompressed_ring_element (serialized: t_Slice u8) = -+#push-options "--z3rlimit 100" ++#push-options "--z3rlimit 220" +let deserialize_to_uncompressed_ring_element (serialized: t_Slice u8) = let _:Prims.unit = () <: Prims.unit in - let re:Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement = @@ -6909,7 +6912,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -1231,12 +1300,12 @@ +@@ -1231,12 +1313,12 @@ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re .Libcrux.Kem.Kyber.Arithmetic.f_coefficients (sz 2 *! i <: usize) @@ -6925,7 +6928,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -1244,34 +1313,43 @@ +@@ -1244,34 +1326,28 @@ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re .Libcrux.Kem.Kyber.Arithmetic.f_coefficients ((sz 2 *! i <: usize) +! sz 1 <: usize) @@ -6940,23 +6943,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K in re +#pop-options -+ -+module A = Libcrux.Kem.Kyber.Arithmetic -let serialize_uncompressed_ring_element (re: Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement) = -+let bitwise_equality #len #d (p1 p2: (p: t_Array nat len {forall i. Seq.index p i < pow2 d})) -+ : Lemma -+ (requires forall i. bit_vec_of_nat_array p1 d i == bit_vec_of_nat_array p2 d i) -+ (ensures p1 == p2) -+ = admit () -+ -+let eq_rw #len (re_poly: t_Array nat len) -+ : Lemma ( -+ -+ bit_vec_to_int_t_array 8 (bit_vec_of_nat_array re_poly 12) -+ ) -+ = admit () -+ +#push-options "--z3rlimit 100" +let serialize_uncompressed_ring_element (re: Libcrux.Kem.Kyber.Arithmetic.wfPolynomialRingElement) = let serialized:t_Array u8 (sz 384) = Rust_primitives.Hax.repeat 0uy (sz 384) in @@ -6985,7 +6973,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K let coefficient1:u16 = Libcrux.Kem.Kyber.Arithmetic.to_unsigned_representative (coefficients.[ sz 0 ] <: i32) in -@@ -1281,6 +1359,8 @@ +@@ -1281,6 +1357,8 @@ let coef1, coef2, coef3:(u8 & u8 & u8) = compress_coefficients_3_ coefficient1 coefficient2 in @@ -6994,24 +6982,15 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K let serialized:t_Array u8 (sz 384) = Rust_primitives.Hax.Monomorphized_update_at.update_at_usize serialized (sz 3 *! i <: usize) -@@ -1298,4 +1378,13 @@ - in +@@ -1299,3 +1377,4 @@ serialized) in -+ // admitP (bitwise_equality serialized (Spec.Kyber.byte_encode 12 (A.wf_poly_to_spec_poly re))); -+ // admitP (serialized == Spec.Kyber.byte_encode 12 (A.wf_poly_to_spec_poly re)); -+ let re_poly = A.wf_poly_to_spec_poly re in -+ assert ( -+ bit_vec_to_int_t_array 8 (bit_vec_of_nat_array re_poly 12) -+ == Spec.Kyber.byte_encode 12 re_poly -+ ); -+ admit (); serialized +#pop-options diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fsti extraction-edited/Libcrux.Kem.Kyber.Serialize.fsti ---- extraction/Libcrux.Kem.Kyber.Serialize.fsti 2024-01-31 17:22:55.410849133 +0100 -+++ extraction-edited/Libcrux.Kem.Kyber.Serialize.fsti 2024-01-31 17:22:55.494847384 +0100 -@@ -2,118 +2,195 @@ +--- extraction/Libcrux.Kem.Kyber.Serialize.fsti 2024-02-01 11:03:26.769761855 +0100 ++++ extraction-edited/Libcrux.Kem.Kyber.Serialize.fsti 2024-02-01 11:03:26.845759626 +0100 +@@ -2,118 +2,193 @@ #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core open FStar.Mul @@ -7268,15 +7247,13 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fsti extraction-edited/Libcrux. + (requires (length serialized == Spec.Kyber.v_BYTES_PER_RING_ELEMENT)) + (ensures fun _ -> True) + -+module A = Libcrux.Kem.Kyber.Arithmetic -+ +val serialize_uncompressed_ring_element (re: Libcrux.Kem.Kyber.Arithmetic.wfPolynomialRingElement) + : Pure (t_Array u8 (sz 384)) + (requires True) -+ (ensures (fun res -> res == Spec.Kyber.byte_encode 12 (A.wf_poly_to_spec_poly re))) ++ (ensures (fun res -> True)) diff -ruN extraction/Libcrux.Kem.Kyber.Types.fst extraction-edited/Libcrux.Kem.Kyber.Types.fst ---- extraction/Libcrux.Kem.Kyber.Types.fst 2024-01-31 17:22:55.414849050 +0100 -+++ extraction-edited/Libcrux.Kem.Kyber.Types.fst 2024-01-31 17:22:55.487847530 +0100 +--- extraction/Libcrux.Kem.Kyber.Types.fst 2024-02-01 11:03:26.772761767 +0100 ++++ extraction-edited/Libcrux.Kem.Kyber.Types.fst 2024-02-01 11:03:26.839759802 +0100 @@ -3,31 +3,33 @@ open Core open FStar.Mul @@ -7547,8 +7524,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Types.fst extraction-edited/Libcrux.Kem.K + (self: t_KyberKeyPair v_PRIVATE_KEY_SIZE v_PUBLIC_KEY_SIZE) : t_Array u8 v_PRIVATE_KEY_SIZE = impl_12__as_slice v_PRIVATE_KEY_SIZE self.f_sk diff -ruN extraction/Libcrux_platform.fsti extraction-edited/Libcrux_platform.fsti ---- extraction/Libcrux_platform.fsti 2024-01-31 17:22:55.409849154 +0100 -+++ extraction-edited/Libcrux_platform.fsti 2024-01-31 17:22:55.472847842 +0100 +--- extraction/Libcrux_platform.fsti 2024-02-01 11:03:26.767761914 +0100 ++++ extraction-edited/Libcrux_platform.fsti 2024-02-01 11:03:26.826760184 +0100 @@ -1,20 +1,4 @@ module Libcrux_platform #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" @@ -7573,7 +7550,7 @@ diff -ruN extraction/Libcrux_platform.fsti extraction-edited/Libcrux_platform.fs +val simd256_support: bool diff -ruN extraction/MkSeq.fst extraction-edited/MkSeq.fst --- extraction/MkSeq.fst 1970-01-01 01:00:00.000000000 +0100 -+++ extraction-edited/MkSeq.fst 2024-01-31 17:22:55.459848113 +0100 ++++ extraction-edited/MkSeq.fst 2024-02-01 11:03:26.814760535 +0100 @@ -0,0 +1,91 @@ +module MkSeq +open Core @@ -7668,7 +7645,7 @@ diff -ruN extraction/MkSeq.fst extraction-edited/MkSeq.fst +%splice[] (init 13 (fun i -> create_gen_tac (i + 1))) diff -ruN extraction/Spec.Kyber.fst extraction-edited/Spec.Kyber.fst --- extraction/Spec.Kyber.fst 1970-01-01 01:00:00.000000000 +0100 -+++ extraction-edited/Spec.Kyber.fst 2024-01-31 17:22:55.495847363 +0100 ++++ extraction-edited/Spec.Kyber.fst 2024-02-01 11:03:26.846759597 +0100 @@ -0,0 +1,433 @@ +module Spec.Kyber +#set-options "--fuel 0 --ifuel 1 --z3rlimit 100" diff --git a/proofs/fstar/extraction-secret-independent.patch b/proofs/fstar/extraction-secret-independent.patch index cf6406004..2bade06c4 100644 --- a/proofs/fstar/extraction-secret-independent.patch +++ b/proofs/fstar/extraction-secret-independent.patch @@ -1,6 +1,6 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Arithmetic.fst extraction-secret-independent/Libcrux.Kem.Kyber.Arithmetic.fst ---- extraction-edited/Libcrux.Kem.Kyber.Arithmetic.fst 2024-01-31 17:22:55.483847613 +0100 -+++ extraction-secret-independent/Libcrux.Kem.Kyber.Arithmetic.fst 2024-01-31 17:22:55.560846010 +0100 +--- extraction-edited/Libcrux.Kem.Kyber.Arithmetic.fst 2024-02-01 11:03:26.836759890 +0100 ++++ extraction-secret-independent/Libcrux.Kem.Kyber.Arithmetic.fst 2024-02-01 11:03:26.911757691 +0100 @@ -1,356 +1,81 @@ module Libcrux.Kem.Kyber.Arithmetic -#set-options "--fuel 0 --ifuel 1 --z3rlimit 100" @@ -397,8 +397,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Arithmetic.fst extraction-secret-i - - diff -ruN extraction-edited/Libcrux.Kem.Kyber.Arithmetic.fsti extraction-secret-independent/Libcrux.Kem.Kyber.Arithmetic.fsti ---- extraction-edited/Libcrux.Kem.Kyber.Arithmetic.fsti 2024-01-31 17:22:55.475847780 +0100 -+++ extraction-secret-independent/Libcrux.Kem.Kyber.Arithmetic.fsti 2024-01-31 17:22:55.551846197 +0100 +--- extraction-edited/Libcrux.Kem.Kyber.Arithmetic.fsti 2024-02-01 11:03:26.829760095 +0100 ++++ extraction-secret-independent/Libcrux.Kem.Kyber.Arithmetic.fsti 2024-02-01 11:03:26.901757984 +0100 @@ -3,32 +3,10 @@ open Core open FStar.Mul @@ -432,7 +432,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Arithmetic.fsti extraction-secret- let t_FieldElementTimesMontgomeryR = i32 unfold -@@ -36,224 +14,122 @@ +@@ -36,213 +14,122 @@ let v_BARRETT_MULTIPLIER: i64 = 20159L @@ -461,11 +461,6 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Arithmetic.fsti extraction-secret- - m_v + v Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS - else m_v - --let wf_fe_to_spec_fe (m: wfFieldElement): Spec.Kyber.field_element = -- if v m < 0 -- then v m + v Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS -- else v m -- -let to_spec_fe (m:i32) : Spec.Kyber.field_element = - int_to_spec_fe (v m) - @@ -638,12 +633,6 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Arithmetic.fsti extraction-secret- - assert (forall i. Seq.index p i < v Spec.Kyber.v_FIELD_MODULUS); - p - --let wf_poly_to_spec_poly (re: wfPolynomialRingElement): Spec.Kyber.polynomial -- = let p = Spec.Kyber.map' (fun x -> wf_fe_to_spec_fe x <: nat) re.f_coefficients in -- introduce forall i. Seq.index p i < v Spec.Kyber.v_FIELD_MODULUS -- with assert (Seq.index p i == Seq.index p (v (sz i))); -- p -- -let to_spec_poly_b #b (m:t_PolynomialRingElement_b b) : (Spec.Kyber.polynomial) = - to_spec_poly (derefine_poly_b m) - @@ -755,8 +744,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Arithmetic.fsti extraction-secret- + <: + bool)) diff -ruN extraction-edited/Libcrux.Kem.Kyber.Compress.fst extraction-secret-independent/Libcrux.Kem.Kyber.Compress.fst ---- extraction-edited/Libcrux.Kem.Kyber.Compress.fst 2024-01-31 17:22:55.465847988 +0100 -+++ extraction-secret-independent/Libcrux.Kem.Kyber.Compress.fst 2024-01-31 17:22:55.538846468 +0100 +--- extraction-edited/Libcrux.Kem.Kyber.Compress.fst 2024-02-01 11:03:26.819760389 +0100 ++++ extraction-secret-independent/Libcrux.Kem.Kyber.Compress.fst 2024-02-01 11:03:26.888758365 +0100 @@ -1,79 +1,39 @@ module Libcrux.Kem.Kyber.Compress -#set-options "--fuel 0 --ifuel 0 --z3rlimit 200" @@ -861,8 +850,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Compress.fst extraction-secret-ind + (Core.Ops.Arith.Neg.neg fe <: i32) &. + ((Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS +! 1l <: i32) /! 2l <: i32) diff -ruN extraction-edited/Libcrux.Kem.Kyber.Compress.fsti extraction-secret-independent/Libcrux.Kem.Kyber.Compress.fsti ---- extraction-edited/Libcrux.Kem.Kyber.Compress.fsti 2024-01-31 17:22:55.497847322 +0100 -+++ extraction-secret-independent/Libcrux.Kem.Kyber.Compress.fsti 2024-01-31 17:22:55.561845989 +0100 +--- extraction-edited/Libcrux.Kem.Kyber.Compress.fsti 2024-02-01 11:03:26.847759568 +0100 ++++ extraction-secret-independent/Libcrux.Kem.Kyber.Compress.fsti 2024-02-01 11:03:26.913757632 +0100 @@ -3,42 +3,44 @@ open Core open FStar.Mul @@ -934,8 +923,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Compress.fsti extraction-secret-in - (fun result -> v result >= 0 /\ v result < 3329) + : Prims.Pure i32 (requires fe =. 0l || fe =. 1l) (fun _ -> Prims.l_True) diff -ruN extraction-edited/Libcrux.Kem.Kyber.Constants.fsti extraction-secret-independent/Libcrux.Kem.Kyber.Constants.fsti ---- extraction-edited/Libcrux.Kem.Kyber.Constants.fsti 2024-01-31 17:22:55.467847946 +0100 -+++ extraction-secret-independent/Libcrux.Kem.Kyber.Constants.fsti 2024-01-31 17:22:55.546846301 +0100 +--- extraction-edited/Libcrux.Kem.Kyber.Constants.fsti 2024-02-01 11:03:26.821760330 +0100 ++++ extraction-secret-independent/Libcrux.Kem.Kyber.Constants.fsti 2024-02-01 11:03:26.896758131 +0100 @@ -15,8 +15,7 @@ let v_FIELD_MODULUS: i32 = 3329l @@ -947,8 +936,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Constants.fsti extraction-secret-i let v_REJECTION_SAMPLING_SEED_SIZE: usize = sz 168 *! sz 5 diff -ruN extraction-edited/Libcrux.Kem.Kyber.Constant_time_ops.fst extraction-secret-independent/Libcrux.Kem.Kyber.Constant_time_ops.fst ---- extraction-edited/Libcrux.Kem.Kyber.Constant_time_ops.fst 2024-01-31 17:22:55.478847717 +0100 -+++ extraction-secret-independent/Libcrux.Kem.Kyber.Constant_time_ops.fst 2024-01-31 17:22:55.520846843 +0100 +--- extraction-edited/Libcrux.Kem.Kyber.Constant_time_ops.fst 2024-02-01 11:03:26.832760008 +0100 ++++ extraction-secret-independent/Libcrux.Kem.Kyber.Constant_time_ops.fst 2024-02-01 11:03:26.869758923 +0100 @@ -4,163 +4,61 @@ open FStar.Mul @@ -1137,8 +1126,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Constant_time_ops.fst extraction-s -#pop-options + out diff -ruN extraction-edited/Libcrux.Kem.Kyber.Constant_time_ops.fsti extraction-secret-independent/Libcrux.Kem.Kyber.Constant_time_ops.fsti ---- extraction-edited/Libcrux.Kem.Kyber.Constant_time_ops.fsti 2024-01-31 17:22:55.485847571 +0100 -+++ extraction-secret-independent/Libcrux.Kem.Kyber.Constant_time_ops.fsti 2024-01-31 17:22:55.554846135 +0100 +--- extraction-edited/Libcrux.Kem.Kyber.Constant_time_ops.fsti 2024-02-01 11:03:26.837759861 +0100 ++++ extraction-secret-independent/Libcrux.Kem.Kyber.Constant_time_ops.fsti 2024-02-01 11:03:26.905757867 +0100 @@ -20,26 +20,30 @@ val compare_ciphertexts_in_constant_time (v_CIPHERTEXT_SIZE: usize) (lhs rhs: t_Slice u8) @@ -1182,7 +1171,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Constant_time_ops.fsti extraction- + result = rhs <: bool)) diff -ruN extraction-edited/Libcrux.Kem.Kyber.Conversions.fst extraction-secret-independent/Libcrux.Kem.Kyber.Conversions.fst --- extraction-edited/Libcrux.Kem.Kyber.Conversions.fst 1970-01-01 01:00:00.000000000 +0100 -+++ extraction-secret-independent/Libcrux.Kem.Kyber.Conversions.fst 2024-01-31 17:22:55.517846905 +0100 ++++ extraction-secret-independent/Libcrux.Kem.Kyber.Conversions.fst 2024-02-01 11:03:26.865759040 +0100 @@ -0,0 +1,87 @@ +module Libcrux.Kem.Kyber.Conversions +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" @@ -1273,8 +1262,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Conversions.fst extraction-secret- + cast (fe +! ((fe >>! 15l <: i32) &. Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS <: i32)) <: u16 \ Pas de fin de ligne à la fin du fichier diff -ruN extraction-edited/Libcrux.Kem.Kyber.fst extraction-secret-independent/Libcrux.Kem.Kyber.fst ---- extraction-edited/Libcrux.Kem.Kyber.fst 2024-01-31 17:22:55.470847884 +0100 -+++ extraction-secret-independent/Libcrux.Kem.Kyber.fst 2024-01-31 17:22:55.535846530 +0100 +--- extraction-edited/Libcrux.Kem.Kyber.fst 2024-02-01 11:03:26.824760242 +0100 ++++ extraction-secret-independent/Libcrux.Kem.Kyber.fst 2024-02-01 11:03:26.885758453 +0100 @@ -1,29 +1,12 @@ module Libcrux.Kem.Kyber -#set-options "--fuel 0 --ifuel 1 --z3rlimit 100" @@ -1518,8 +1507,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.fst extraction-secret-independent/ (Core.Convert.f_into public_key <: Libcrux.Kem.Kyber.Types.t_KyberPublicKey v_PUBLIC_KEY_SIZE) - diff -ruN extraction-edited/Libcrux.Kem.Kyber.fsti extraction-secret-independent/Libcrux.Kem.Kyber.fsti ---- extraction-edited/Libcrux.Kem.Kyber.fsti 2024-01-31 17:22:55.500847259 +0100 -+++ extraction-secret-independent/Libcrux.Kem.Kyber.fsti 2024-01-31 17:22:55.544846343 +0100 +--- extraction-edited/Libcrux.Kem.Kyber.fsti 2024-02-01 11:03:26.850759480 +0100 ++++ extraction-secret-independent/Libcrux.Kem.Kyber.fsti 2024-02-01 11:03:26.895758160 +0100 @@ -10,75 +10,31 @@ Libcrux.Kem.Kyber.Constants.v_CPA_PKE_KEY_GENERATION_SEED_SIZE +! Libcrux.Kem.Kyber.Constants.v_SHARED_SECRET_SIZE @@ -1609,8 +1598,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.fsti extraction-secret-independent + Prims.l_True + (fun _ -> Prims.l_True) diff -ruN extraction-edited/Libcrux.Kem.Kyber.Hash_functions.fst extraction-secret-independent/Libcrux.Kem.Kyber.Hash_functions.fst ---- extraction-edited/Libcrux.Kem.Kyber.Hash_functions.fst 2024-01-31 17:22:55.476847759 +0100 -+++ extraction-secret-independent/Libcrux.Kem.Kyber.Hash_functions.fst 2024-01-31 17:22:55.543846364 +0100 +--- extraction-edited/Libcrux.Kem.Kyber.Hash_functions.fst 2024-02-01 11:03:26.830760066 +0100 ++++ extraction-secret-independent/Libcrux.Kem.Kyber.Hash_functions.fst 2024-02-01 11:03:26.893758219 +0100 @@ -3,27 +3,18 @@ open Core open FStar.Mul @@ -1659,8 +1648,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Hash_functions.fst extraction-secr - admit(); //P-F out diff -ruN extraction-edited/Libcrux.Kem.Kyber.Hash_functions.fsti extraction-secret-independent/Libcrux.Kem.Kyber.Hash_functions.fsti ---- extraction-edited/Libcrux.Kem.Kyber.Hash_functions.fsti 2024-01-31 17:22:55.505847155 +0100 -+++ extraction-secret-independent/Libcrux.Kem.Kyber.Hash_functions.fsti 2024-01-31 17:22:55.519846863 +0100 +--- extraction-edited/Libcrux.Kem.Kyber.Hash_functions.fsti 2024-02-01 11:03:26.855759333 +0100 ++++ extraction-secret-independent/Libcrux.Kem.Kyber.Hash_functions.fsti 2024-02-01 11:03:26.867758981 +0100 @@ -3,24 +3,12 @@ open Core open FStar.Mul @@ -1692,7 +1681,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Hash_functions.fsti extraction-sec + : Prims.Pure (t_Array (t_Array u8 (sz 840)) v_K) Prims.l_True (fun _ -> Prims.l_True) diff -ruN extraction-edited/Libcrux.Kem.Kyber.Helper.fst extraction-secret-independent/Libcrux.Kem.Kyber.Helper.fst --- extraction-edited/Libcrux.Kem.Kyber.Helper.fst 1970-01-01 01:00:00.000000000 +0100 -+++ extraction-secret-independent/Libcrux.Kem.Kyber.Helper.fst 2024-01-31 17:22:55.552846176 +0100 ++++ extraction-secret-independent/Libcrux.Kem.Kyber.Helper.fst 2024-02-01 11:03:26.903757925 +0100 @@ -0,0 +1,6 @@ +module Libcrux.Kem.Kyber.Helper +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" @@ -1701,8 +1690,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Helper.fst extraction-secret-indep + + diff -ruN extraction-edited/Libcrux.Kem.Kyber.Ind_cpa.fst extraction-secret-independent/Libcrux.Kem.Kyber.Ind_cpa.fst ---- extraction-edited/Libcrux.Kem.Kyber.Ind_cpa.fst 2024-01-31 17:22:55.504847176 +0100 -+++ extraction-secret-independent/Libcrux.Kem.Kyber.Ind_cpa.fst 2024-01-31 17:22:55.548846259 +0100 +--- extraction-edited/Libcrux.Kem.Kyber.Ind_cpa.fst 2024-02-01 11:03:26.853759392 +0100 ++++ extraction-secret-independent/Libcrux.Kem.Kyber.Ind_cpa.fst 2024-02-01 11:03:26.898758072 +0100 @@ -1,5 +1,5 @@ module Libcrux.Kem.Kyber.Ind_cpa -#set-options "--fuel 0 --ifuel 1 --z3rlimit 100" @@ -2413,8 +2402,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Ind_cpa.fst extraction-secret-inde - res - diff -ruN extraction-edited/Libcrux.Kem.Kyber.Ind_cpa.fsti extraction-secret-independent/Libcrux.Kem.Kyber.Ind_cpa.fsti ---- extraction-edited/Libcrux.Kem.Kyber.Ind_cpa.fsti 2024-01-31 17:22:55.492847426 +0100 -+++ extraction-secret-independent/Libcrux.Kem.Kyber.Ind_cpa.fsti 2024-01-31 17:22:55.515846947 +0100 +--- extraction-edited/Libcrux.Kem.Kyber.Ind_cpa.fsti 2024-02-01 11:03:26.843759685 +0100 ++++ extraction-secret-independent/Libcrux.Kem.Kyber.Ind_cpa.fsti 2024-02-01 11:03:26.864759069 +0100 @@ -1,152 +1,80 @@ module Libcrux.Kem.Kyber.Ind_cpa -#set-options "--fuel 0 --ifuel 1 --z3rlimit 100" @@ -2617,8 +2606,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Ind_cpa.fsti extraction-secret-ind + Prims.l_True + (fun _ -> Prims.l_True) diff -ruN extraction-edited/Libcrux.Kem.Kyber.Kyber1024.fst extraction-secret-independent/Libcrux.Kem.Kyber.Kyber1024.fst ---- extraction-edited/Libcrux.Kem.Kyber.Kyber1024.fst 2024-01-31 17:22:55.460848092 +0100 -+++ extraction-secret-independent/Libcrux.Kem.Kyber.Kyber1024.fst 2024-01-31 17:22:55.525846739 +0100 +--- extraction-edited/Libcrux.Kem.Kyber.Kyber1024.fst 2024-02-01 11:03:26.815760506 +0100 ++++ extraction-secret-independent/Libcrux.Kem.Kyber.Kyber1024.fst 2024-02-01 11:03:26.874758776 +0100 @@ -3,23 +3,22 @@ open Core open FStar.Mul @@ -2652,8 +2641,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Kyber1024.fst extraction-secret-in (sz 3168) (sz 1568) diff -ruN extraction-edited/Libcrux.Kem.Kyber.Kyber512.fst extraction-secret-independent/Libcrux.Kem.Kyber.Kyber512.fst ---- extraction-edited/Libcrux.Kem.Kyber.Kyber512.fst 2024-01-31 17:22:55.482847634 +0100 -+++ extraction-secret-independent/Libcrux.Kem.Kyber.Kyber512.fst 2024-01-31 17:22:55.564845926 +0100 +--- extraction-edited/Libcrux.Kem.Kyber.Kyber512.fst 2024-02-01 11:03:26.835759920 +0100 ++++ extraction-secret-independent/Libcrux.Kem.Kyber.Kyber512.fst 2024-02-01 11:03:26.917757515 +0100 @@ -5,21 +5,20 @@ let decapsulate_512_ @@ -2684,8 +2673,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Kyber512.fst extraction-secret-ind (sz 1632) (sz 800) diff -ruN extraction-edited/Libcrux.Kem.Kyber.Kyber768.fst extraction-secret-independent/Libcrux.Kem.Kyber.Kyber768.fst ---- extraction-edited/Libcrux.Kem.Kyber.Kyber768.fst 2024-01-31 17:22:55.480847675 +0100 -+++ extraction-secret-independent/Libcrux.Kem.Kyber.Kyber768.fst 2024-01-31 17:22:55.558846051 +0100 +--- extraction-edited/Libcrux.Kem.Kyber.Kyber768.fst 2024-02-01 11:03:26.833759978 +0100 ++++ extraction-secret-independent/Libcrux.Kem.Kyber.Kyber768.fst 2024-02-01 11:03:26.910757720 +0100 @@ -3,24 +3,22 @@ open Core open FStar.Mul @@ -2719,8 +2708,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Kyber768.fst extraction-secret-ind (sz 2400) (sz 1184) diff -ruN extraction-edited/Libcrux.Kem.Kyber.Kyber768.fsti extraction-secret-independent/Libcrux.Kem.Kyber.Kyber768.fsti ---- extraction-edited/Libcrux.Kem.Kyber.Kyber768.fsti 2024-01-31 17:22:55.468847925 +0100 -+++ extraction-secret-independent/Libcrux.Kem.Kyber.Kyber768.fsti 2024-01-31 17:22:55.530846634 +0100 +--- extraction-edited/Libcrux.Kem.Kyber.Kyber768.fsti 2024-02-01 11:03:26.822760301 +0100 ++++ extraction-secret-independent/Libcrux.Kem.Kyber.Kyber768.fsti 2024-02-01 11:03:26.879758629 +0100 @@ -74,19 +74,16 @@ val decapsulate_768_ (secret_key: Libcrux.Kem.Kyber.Types.t_KyberPrivateKey (sz 2400)) @@ -2749,8 +2738,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Kyber768.fsti extraction-secret-in + Prims.l_True + (fun _ -> Prims.l_True) diff -ruN extraction-edited/Libcrux.Kem.Kyber.Matrix.fst extraction-secret-independent/Libcrux.Kem.Kyber.Matrix.fst ---- extraction-edited/Libcrux.Kem.Kyber.Matrix.fst 2024-01-31 17:22:55.509847072 +0100 -+++ extraction-secret-independent/Libcrux.Kem.Kyber.Matrix.fst 2024-01-31 17:22:55.533846572 +0100 +--- extraction-edited/Libcrux.Kem.Kyber.Matrix.fst 2024-02-01 11:03:26.858759245 +0100 ++++ extraction-secret-independent/Libcrux.Kem.Kyber.Matrix.fst 2024-02-01 11:03:26.883758512 +0100 @@ -3,418 +3,432 @@ open Core open FStar.Mul @@ -3559,8 +3548,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Matrix.fst extraction-secret-indep - admit(); //P-F v_A_transpose diff -ruN extraction-edited/Libcrux.Kem.Kyber.Matrix.fsti extraction-secret-independent/Libcrux.Kem.Kyber.Matrix.fsti ---- extraction-edited/Libcrux.Kem.Kyber.Matrix.fsti 2024-01-31 17:22:55.491847446 +0100 -+++ extraction-secret-independent/Libcrux.Kem.Kyber.Matrix.fsti 2024-01-31 17:22:55.555846114 +0100 +--- extraction-edited/Libcrux.Kem.Kyber.Matrix.fsti 2024-02-01 11:03:26.842759714 +0100 ++++ extraction-secret-independent/Libcrux.Kem.Kyber.Matrix.fsti 2024-02-01 11:03:26.906757837 +0100 @@ -3,71 +3,39 @@ open Core open FStar.Mul @@ -3663,8 +3652,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Matrix.fsti extraction-secret-inde + Prims.l_True + (fun _ -> Prims.l_True) diff -ruN extraction-edited/Libcrux.Kem.Kyber.Ntt.fst extraction-secret-independent/Libcrux.Kem.Kyber.Ntt.fst ---- extraction-edited/Libcrux.Kem.Kyber.Ntt.fst 2024-01-31 17:22:55.473847821 +0100 -+++ extraction-secret-independent/Libcrux.Kem.Kyber.Ntt.fst 2024-01-31 17:22:55.541846405 +0100 +--- extraction-edited/Libcrux.Kem.Kyber.Ntt.fst 2024-02-01 11:03:26.827760154 +0100 ++++ extraction-secret-independent/Libcrux.Kem.Kyber.Ntt.fst 2024-02-01 11:03:26.892758248 +0100 @@ -1,130 +1,56 @@ module Libcrux.Kem.Kyber.Ntt -#set-options "--fuel 0 --ifuel 1 --z3rlimit 100" @@ -4595,8 +4584,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Ntt.fst extraction-secret-independ -#pop-options + re diff -ruN extraction-edited/Libcrux.Kem.Kyber.Ntt.fsti extraction-secret-independent/Libcrux.Kem.Kyber.Ntt.fsti ---- extraction-edited/Libcrux.Kem.Kyber.Ntt.fsti 2024-01-31 17:22:55.455848196 +0100 -+++ extraction-secret-independent/Libcrux.Kem.Kyber.Ntt.fsti 2024-01-31 17:22:55.563845947 +0100 +--- extraction-edited/Libcrux.Kem.Kyber.Ntt.fsti 2024-02-01 11:03:26.811760624 +0100 ++++ extraction-secret-independent/Libcrux.Kem.Kyber.Ntt.fsti 2024-02-01 11:03:26.915757574 +0100 @@ -2,80 +2,224 @@ #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core @@ -4890,8 +4879,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Ntt.fsti extraction-secret-indepen + <: + bool)) diff -ruN extraction-edited/Libcrux.Kem.Kyber.Sampling.fst extraction-secret-independent/Libcrux.Kem.Kyber.Sampling.fst ---- extraction-edited/Libcrux.Kem.Kyber.Sampling.fst 2024-01-31 17:22:55.498847301 +0100 -+++ extraction-secret-independent/Libcrux.Kem.Kyber.Sampling.fst 2024-01-31 17:22:55.514846968 +0100 +--- extraction-edited/Libcrux.Kem.Kyber.Sampling.fst 2024-02-01 11:03:26.849759509 +0100 ++++ extraction-secret-independent/Libcrux.Kem.Kyber.Sampling.fst 2024-02-01 11:03:26.862759128 +0100 @@ -3,34 +3,27 @@ open Core open FStar.Mul @@ -5328,8 +5317,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Sampling.fst extraction-secret-ind -#pop-options + out diff -ruN extraction-edited/Libcrux.Kem.Kyber.Sampling.fsti extraction-secret-independent/Libcrux.Kem.Kyber.Sampling.fsti ---- extraction-edited/Libcrux.Kem.Kyber.Sampling.fsti 2024-01-31 17:22:55.507847113 +0100 -+++ extraction-secret-independent/Libcrux.Kem.Kyber.Sampling.fsti 2024-01-31 17:22:55.549846239 +0100 +--- extraction-edited/Libcrux.Kem.Kyber.Sampling.fsti 2024-02-01 11:03:26.856759304 +0100 ++++ extraction-secret-independent/Libcrux.Kem.Kyber.Sampling.fsti 2024-02-01 11:03:26.899758043 +0100 @@ -3,37 +3,77 @@ open Core open FStar.Mul @@ -5430,9 +5419,9 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Sampling.fsti extraction-secret-in + Prims.l_True + (fun _ -> Prims.l_True) diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-independent/Libcrux.Kem.Kyber.Serialize.fst ---- extraction-edited/Libcrux.Kem.Kyber.Serialize.fst 2024-01-31 17:22:55.463848030 +0100 -+++ extraction-secret-independent/Libcrux.Kem.Kyber.Serialize.fst 2024-01-31 17:22:55.532846593 +0100 -@@ -1,13 +1,8 @@ +--- extraction-edited/Libcrux.Kem.Kyber.Serialize.fst 2024-02-01 11:03:26.818760418 +0100 ++++ extraction-secret-independent/Libcrux.Kem.Kyber.Serialize.fst 2024-02-01 11:03:26.881758571 +0100 +@@ -1,14 +1,8 @@ module Libcrux.Kem.Kyber.Serialize -#set-options "--fuel 0 --ifuel 0 --z3rlimit 50 --retry 3" +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" @@ -5443,17 +5432,19 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in - -open MkSeq - --#push-options "--z3rlimit 50" +-#push-options "--z3rlimit 80" +-[@@"opaque_to_smt"] let compress_coefficients_10_ (coefficient1 coefficient2 coefficient3 coefficient4: i32) = let coef1:u8 = cast (coefficient1 &. 255l <: i32) <: u8 in let coef2:u8 = -@@ -24,11 +19,11 @@ +@@ -25,12 +19,11 @@ in let coef5:u8 = cast ((coefficient4 >>! 2l <: i32) &. 255l <: i32) <: u8 in coef1, coef2, coef3, coef4, coef5 <: (u8 & u8 & u8 & u8 & u8) -#pop-options -#push-options "--ifuel 1 --z3rlimit 600 --split_queries always" +-[@@"opaque_to_smt"] let compress_coefficients_11_ - coefficient1 coefficient2 coefficient3 coefficient4 coefficient5 coefficient6 coefficient7 coefficient8 = + (coefficient1 coefficient2 coefficient3 coefficient4 coefficient5 coefficient6 coefficient7 coefficient8: @@ -5462,13 +5453,14 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in let coef1:u8 = cast (coefficient1 <: i32) <: u8 in let coef2:u8 = ((cast (coefficient2 &. 31l <: i32) <: u8) <>! 2l <: u8) in coef1, coef2, coef3, coef4, coef5 <: (u8 & u8 & u8 & u8 & u8) -#pop-options -#push-options "--z3rlimit 500" +-[@@"opaque_to_smt"] -let decompress_coefficients_10_ byte2 byte1 byte3 byte4 byte5 = +let decompress_coefficients_10_ (byte2 byte1 byte3 byte4 byte5: i32) = let coefficient1:i32 = ((byte2 &. 3l <: i32) <>! 3l <: i32) in let coefficient3:i32 = -@@ -125,14 +109,6 @@ +@@ -131,14 +109,6 @@ in let coefficient7:i32 = ((byte10 &. 31l <: i32) <>! 2l <: i32) in let coefficient8:i32 = (byte11 <>! 5l <: i32) in @@ -5537,7 +5532,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in coefficient1, coefficient2, coefficient3, -@@ -141,19 +117,15 @@ +@@ -147,21 +117,15 @@ coefficient6, coefficient7, coefficient8 @@ -5546,6 +5541,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in + (i32 & i32 & i32 & i32 & i32 & i32 & i32 & i32) -#push-options "--z3rlimit 50" +-[@@"opaque_to_smt"] -let decompress_coefficients_4_ byte = +let decompress_coefficients_4_ (byte: u8) = let coefficient1:i32 = cast (byte &. 15uy <: u8) <: i32 in @@ -5554,15 +5550,17 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in - lemma_get_bit_bounded' coefficient2 4; - coefficient1, coefficient2 -#pop-options -+ coefficient1, coefficient2 <: (i32 & i32) - +- -#push-options "--z3rlimit 400" +-[@@"opaque_to_smt"] -let decompress_coefficients_5_ byte1 byte2 byte3 byte4 byte5 = ++ coefficient1, coefficient2 <: (i32 & i32) ++ +let decompress_coefficients_5_ (byte1 byte2 byte3 byte4 byte5: i32) = let coefficient1:i32 = byte1 &. 31l in let coefficient2:i32 = ((byte2 &. 3l <: i32) <>! 5l <: i32) in let coefficient3:i32 = (byte2 >>! 2l <: i32) &. 31l in -@@ -162,14 +134,6 @@ +@@ -170,14 +134,6 @@ let coefficient6:i32 = (byte4 >>! 1l <: i32) &. 31l in let coefficient7:i32 = ((byte5 &. 7l <: i32) <>! 6l <: i32) in let coefficient8:i32 = byte5 >>! 3l in @@ -5577,7 +5575,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in coefficient1, coefficient2, coefficient3, -@@ -178,50 +142,31 @@ +@@ -186,54 +142,31 @@ coefficient6, coefficient7, coefficient8 @@ -5592,7 +5590,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in - [SMTPat (bounded n d); SMTPat (cast #(int_t t) #(int_t u) n)] - = () - --#push-options "--z3rlimit 60" +-#push-options "--z3rlimit 90" +-[@@"opaque_to_smt"] -let int_t_d_cast_lemma #t #u d (n: int_t_d t d) - : Lemma (requires bits t < bits u /\ v n >= 0) - (ensures bounded (cast #(int_t t) #(int_t u) n) d) @@ -5606,10 +5605,13 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in - = Math.Lemmas.pow2_plus 8 8; - Math.Lemmas.pow2_le_compat 32 16 -#pop-options +- +-#restart-solver + <: + (i32 & i32 & i32 & i32 & i32 & i32 & i32 & i32) -#push-options "--fuel 0 --ifuel 1 --query_stats --z3rlimit 100" +-[@@"opaque_to_smt"] let compress_then_serialize_10_ - v_OUT_LEN - re @@ -5647,13 +5649,14 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in let coefficient1:i32 = Libcrux.Kem.Kyber.Compress.compress_ciphertext_coefficient 10uy (Libcrux.Kem.Kyber.Arithmetic.to_unsigned_representative (coefficients.[ sz 0 ] <: i32 -@@ -281,95 +226,79 @@ +@@ -293,96 +226,79 @@ serialized) in serialized -#pop-options -- + -#push-options "--fuel 0 --ifuel 0 --z3rlimit 30" +-[@@"opaque_to_smt"] -let update5 - #n - (s: t_Array 't n) @@ -5675,7 +5678,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in - let s = update_at_usize s (offset +! sz 4) i4 in - s -#pop-options - +- -#push-options "--fuel 0 --ifuel 1 --z3rlimit 100 --query_stats --split_queries no" let compress_then_serialize_11_ - v_OUT_LEN re @@ -5767,7 +5770,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in Libcrux.Kem.Kyber.Compress.compress_ciphertext_coefficient 11uy (Libcrux.Kem.Kyber.Arithmetic.to_unsigned_representative (coefficients.[ sz 7 ] <: i32 ) -@@ -395,8 +324,6 @@ +@@ -408,8 +324,6 @@ coefficient7 coefficient8 in @@ -5776,7 +5779,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in let serialized:t_Array u8 v_OUT_LEN = Rust_primitives.Hax.Monomorphized_update_at.update_at_usize serialized (sz 11 *! i <: usize) -@@ -455,20 +382,29 @@ +@@ -468,20 +382,29 @@ serialized) in serialized @@ -5814,7 +5817,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in let coefficient1:u8 = cast (Libcrux.Kem.Kyber.Compress.compress_ciphertext_coefficient 4uy (Libcrux.Kem.Kyber.Arithmetic.to_unsigned_representative (coefficients.[ sz 0 ] -@@ -503,20 +439,27 @@ +@@ -516,20 +439,27 @@ serialized let compress_then_serialize_5_ @@ -5851,7 +5854,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in let coefficient1:u8 = cast (Libcrux.Kem.Kyber.Compress.compress_ciphertext_coefficient 5uy (Libcrux.Kem.Kyber.Arithmetic.to_unsigned_representative (coefficients.[ sz 0 ] -@@ -601,14 +544,6 @@ +@@ -614,14 +544,6 @@ <: u8 in @@ -5866,7 +5869,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in let coefficient8:u8 = cast (Libcrux.Kem.Kyber.Compress.compress_ciphertext_coefficient 5uy (Libcrux.Kem.Kyber.Arithmetic.to_unsigned_representative (coefficients.[ sz 7 ] -@@ -631,8 +566,6 @@ +@@ -644,8 +566,6 @@ coefficient6 coefficient8 in @@ -5875,7 +5878,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in let serialized:t_Array u8 v_OUT_LEN = Rust_primitives.Hax.Monomorphized_update_at.update_at_usize serialized (sz 5 *! i <: usize) -@@ -662,24 +595,35 @@ +@@ -675,24 +595,35 @@ in serialized @@ -5921,7 +5924,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in let coefficient:u16 = Libcrux.Kem.Kyber.Arithmetic.to_unsigned_representative coefficient in -@@ -692,36 +636,28 @@ +@@ -705,36 +636,28 @@ <: t_Array u8 (sz 32)) in @@ -5969,7 +5972,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in | 4ul -> compress_then_serialize_4_ v_OUT_LEN re | 5ul -> compress_then_serialize_5_ v_OUT_LEN re | _ -> -@@ -729,49 +665,32 @@ +@@ -742,49 +665,32 @@ <: Rust_primitives.Hax.t_Never) @@ -6038,7 +6041,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -779,12 +698,14 @@ +@@ -792,12 +698,14 @@ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re .Libcrux.Kem.Kyber.Arithmetic.f_coefficients (sz 4 *! i <: usize) @@ -6056,7 +6059,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -792,12 +713,14 @@ +@@ -805,12 +713,14 @@ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re .Libcrux.Kem.Kyber.Arithmetic.f_coefficients ((sz 4 *! i <: usize) +! sz 1 <: usize) @@ -6074,7 +6077,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -805,12 +728,14 @@ +@@ -818,12 +728,14 @@ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re .Libcrux.Kem.Kyber.Arithmetic.f_coefficients ((sz 4 *! i <: usize) +! sz 2 <: usize) @@ -6092,7 +6095,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -818,43 +743,44 @@ +@@ -831,43 +743,44 @@ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re .Libcrux.Kem.Kyber.Arithmetic.f_coefficients ((sz 4 *! i <: usize) +! sz 3 <: usize) @@ -6163,7 +6166,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in let coefficient1, coefficient2, -@@ -863,21 +789,11 @@ +@@ -876,21 +789,11 @@ coefficient5, coefficient6, coefficient7, @@ -6187,7 +6190,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -885,12 +801,14 @@ +@@ -898,12 +801,14 @@ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re .Libcrux.Kem.Kyber.Arithmetic.f_coefficients (sz 8 *! i <: usize) @@ -6205,7 +6208,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -898,12 +816,14 @@ +@@ -911,12 +816,14 @@ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re .Libcrux.Kem.Kyber.Arithmetic.f_coefficients ((sz 8 *! i <: usize) +! sz 1 <: usize) @@ -6223,7 +6226,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -911,12 +831,14 @@ +@@ -924,12 +831,14 @@ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re .Libcrux.Kem.Kyber.Arithmetic.f_coefficients ((sz 8 *! i <: usize) +! sz 2 <: usize) @@ -6241,7 +6244,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -924,12 +846,14 @@ +@@ -937,12 +846,14 @@ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re .Libcrux.Kem.Kyber.Arithmetic.f_coefficients ((sz 8 *! i <: usize) +! sz 3 <: usize) @@ -6259,7 +6262,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -937,12 +861,14 @@ +@@ -950,12 +861,14 @@ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re .Libcrux.Kem.Kyber.Arithmetic.f_coefficients ((sz 8 *! i <: usize) +! sz 4 <: usize) @@ -6277,7 +6280,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -950,12 +876,14 @@ +@@ -963,12 +876,14 @@ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re .Libcrux.Kem.Kyber.Arithmetic.f_coefficients ((sz 8 *! i <: usize) +! sz 5 <: usize) @@ -6295,7 +6298,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -963,12 +891,14 @@ +@@ -976,12 +891,14 @@ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re .Libcrux.Kem.Kyber.Arithmetic.f_coefficients ((sz 8 *! i <: usize) +! sz 6 <: usize) @@ -6313,7 +6316,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -976,33 +906,35 @@ +@@ -989,33 +906,35 @@ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re .Libcrux.Kem.Kyber.Arithmetic.f_coefficients ((sz 8 *! i <: usize) +! sz 7 <: usize) @@ -6364,7 +6367,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -1015,9 +947,9 @@ +@@ -1028,9 +947,9 @@ i32) } <: @@ -6376,7 +6379,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -1030,32 +962,33 @@ +@@ -1043,32 +962,33 @@ i32) } <: @@ -6427,7 +6430,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in let coefficient1, coefficient2, -@@ -1064,25 +997,10 @@ +@@ -1077,25 +997,10 @@ coefficient5, coefficient6, coefficient7, @@ -6455,7 +6458,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -1090,12 +1008,14 @@ +@@ -1103,12 +1008,14 @@ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re .Libcrux.Kem.Kyber.Arithmetic.f_coefficients (sz 8 *! i <: usize) @@ -6473,7 +6476,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -1103,12 +1023,14 @@ +@@ -1116,12 +1023,14 @@ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re .Libcrux.Kem.Kyber.Arithmetic.f_coefficients ((sz 8 *! i <: usize) +! sz 1 <: usize) @@ -6491,7 +6494,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -1116,12 +1038,14 @@ +@@ -1129,12 +1038,14 @@ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re .Libcrux.Kem.Kyber.Arithmetic.f_coefficients ((sz 8 *! i <: usize) +! sz 2 <: usize) @@ -6509,7 +6512,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -1129,12 +1053,14 @@ +@@ -1142,12 +1053,14 @@ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re .Libcrux.Kem.Kyber.Arithmetic.f_coefficients ((sz 8 *! i <: usize) +! sz 3 <: usize) @@ -6527,7 +6530,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -1142,12 +1068,14 @@ +@@ -1155,12 +1068,14 @@ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re .Libcrux.Kem.Kyber.Arithmetic.f_coefficients ((sz 8 *! i <: usize) +! sz 4 <: usize) @@ -6545,7 +6548,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -1155,12 +1083,14 @@ +@@ -1168,12 +1083,14 @@ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re .Libcrux.Kem.Kyber.Arithmetic.f_coefficients ((sz 8 *! i <: usize) +! sz 5 <: usize) @@ -6563,7 +6566,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -1168,12 +1098,14 @@ +@@ -1181,12 +1098,14 @@ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re .Libcrux.Kem.Kyber.Arithmetic.f_coefficients ((sz 8 *! i <: usize) +! sz 6 <: usize) @@ -6581,7 +6584,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -1181,27 +1113,33 @@ +@@ -1194,27 +1113,33 @@ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re .Libcrux.Kem.Kyber.Arithmetic.f_coefficients ((sz 8 *! i <: usize) +! sz 7 <: usize) @@ -6625,7 +6628,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in let i, byte:(usize & u8) = temp_1_ in Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({ Core.Ops.Range.f_start = sz 0; -@@ -1213,11 +1151,10 @@ +@@ -1226,11 +1151,10 @@ Core.Ops.Range.t_Range usize) re (fun re j -> @@ -6639,7 +6642,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -1231,21 +1168,20 @@ +@@ -1244,21 +1168,20 @@ i32) } <: @@ -6668,7 +6671,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in | 10ul -> deserialize_then_decompress_10_ serialized | 11ul -> deserialize_then_decompress_11_ serialized | _ -> -@@ -1254,12 +1190,12 @@ +@@ -1267,12 +1190,12 @@ <: Rust_primitives.Hax.t_Never) @@ -6686,7 +6689,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in | 4ul -> deserialize_then_decompress_4_ serialized | 5ul -> deserialize_then_decompress_5_ serialized | _ -> -@@ -1267,32 +1203,27 @@ +@@ -1280,32 +1203,27 @@ <: Rust_primitives.Hax.t_Never) @@ -6694,7 +6697,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in - admit(); //P-F - res --#push-options "--z3rlimit 100" +-#push-options "--z3rlimit 220" -let deserialize_to_uncompressed_ring_element (serialized: t_Slice u8) = +let deserialize_to_uncompressed_ring_element (serialized: t_Slice u8) = let _:Prims.unit = () <: Prims.unit in @@ -6735,7 +6738,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -1300,12 +1231,12 @@ +@@ -1313,12 +1231,12 @@ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re .Libcrux.Kem.Kyber.Arithmetic.f_coefficients (sz 2 *! i <: usize) @@ -6751,7 +6754,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in { re with Libcrux.Kem.Kyber.Arithmetic.f_coefficients -@@ -1313,43 +1244,34 @@ +@@ -1326,28 +1244,34 @@ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re .Libcrux.Kem.Kyber.Arithmetic.f_coefficients ((sz 2 *! i <: usize) +! sz 1 <: usize) @@ -6766,22 +6769,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in in re -#pop-options -- --module A = Libcrux.Kem.Kyber.Arithmetic --let bitwise_equality #len #d (p1 p2: (p: t_Array nat len {forall i. Seq.index p i < pow2 d})) -- : Lemma -- (requires forall i. bit_vec_of_nat_array p1 d i == bit_vec_of_nat_array p2 d i) -- (ensures p1 == p2) -- = admit () -- --let eq_rw #len (re_poly: t_Array nat len) -- : Lemma ( -- -- bit_vec_to_int_t_array 8 (bit_vec_of_nat_array re_poly 12) -- ) -- = admit () -- -#push-options "--z3rlimit 100" -let serialize_uncompressed_ring_element (re: Libcrux.Kem.Kyber.Arithmetic.wfPolynomialRingElement) = +let serialize_uncompressed_ring_element (re: Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement) = @@ -6811,7 +6799,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in let coefficient1:u16 = Libcrux.Kem.Kyber.Arithmetic.to_unsigned_representative (coefficients.[ sz 0 ] <: i32) in -@@ -1359,8 +1281,6 @@ +@@ -1357,8 +1281,6 @@ let coef1, coef2, coef3:(u8 & u8 & u8) = compress_coefficients_3_ coefficient1 coefficient2 in @@ -6820,24 +6808,15 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in let serialized:t_Array u8 (sz 384) = Rust_primitives.Hax.Monomorphized_update_at.update_at_usize serialized (sz 3 *! i <: usize) -@@ -1378,13 +1298,4 @@ - in +@@ -1377,4 +1299,3 @@ serialized) in -- // admitP (bitwise_equality serialized (Spec.Kyber.byte_encode 12 (A.wf_poly_to_spec_poly re))); -- // admitP (serialized == Spec.Kyber.byte_encode 12 (A.wf_poly_to_spec_poly re)); -- let re_poly = A.wf_poly_to_spec_poly re in -- assert ( -- bit_vec_to_int_t_array 8 (bit_vec_of_nat_array re_poly 12) -- == Spec.Kyber.byte_encode 12 re_poly -- ); -- admit (); serialized -#pop-options diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fsti extraction-secret-independent/Libcrux.Kem.Kyber.Serialize.fsti ---- extraction-edited/Libcrux.Kem.Kyber.Serialize.fsti 2024-01-31 17:22:55.494847384 +0100 -+++ extraction-secret-independent/Libcrux.Kem.Kyber.Serialize.fsti 2024-01-31 17:22:55.522846801 +0100 -@@ -2,195 +2,118 @@ +--- extraction-edited/Libcrux.Kem.Kyber.Serialize.fsti 2024-02-01 11:03:26.845759626 +0100 ++++ extraction-secret-independent/Libcrux.Kem.Kyber.Serialize.fsti 2024-02-01 11:03:26.870758893 +0100 +@@ -2,193 +2,118 @@ #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core open FStar.Mul @@ -7088,12 +7067,10 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fsti extraction-secret-i - (requires (length serialized == Spec.Kyber.v_BYTES_PER_RING_ELEMENT)) - (ensures fun _ -> True) - --module A = Libcrux.Kem.Kyber.Arithmetic -- -val serialize_uncompressed_ring_element (re: Libcrux.Kem.Kyber.Arithmetic.wfPolynomialRingElement) - : Pure (t_Array u8 (sz 384)) - (requires True) -- (ensures (fun res -> res == Spec.Kyber.byte_encode 12 (A.wf_poly_to_spec_poly re))) +- (ensures (fun res -> True)) + : Prims.Pure Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement + Prims.l_True + (fun _ -> Prims.l_True) @@ -7101,8 +7078,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fsti extraction-secret-i +val serialize_uncompressed_ring_element (re: Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement) + : Prims.Pure (t_Array u8 (sz 384)) Prims.l_True (fun _ -> Prims.l_True) diff -ruN extraction-edited/Libcrux.Kem.Kyber.Types.fst extraction-secret-independent/Libcrux.Kem.Kyber.Types.fst ---- extraction-edited/Libcrux.Kem.Kyber.Types.fst 2024-01-31 17:22:55.487847530 +0100 -+++ extraction-secret-independent/Libcrux.Kem.Kyber.Types.fst 2024-01-31 17:22:55.527846697 +0100 +--- extraction-edited/Libcrux.Kem.Kyber.Types.fst 2024-02-01 11:03:26.839759802 +0100 ++++ extraction-secret-independent/Libcrux.Kem.Kyber.Types.fst 2024-02-01 11:03:26.875758746 +0100 @@ -3,8 +3,6 @@ open Core open FStar.Mul @@ -7149,8 +7126,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Types.fst extraction-secret-indepe type t_KyberKeyPair (v_PRIVATE_KEY_SIZE: usize) (v_PUBLIC_KEY_SIZE: usize) = { diff -ruN extraction-edited/Libcrux_platform.fsti extraction-secret-independent/Libcrux_platform.fsti ---- extraction-edited/Libcrux_platform.fsti 2024-01-31 17:22:55.472847842 +0100 -+++ extraction-secret-independent/Libcrux_platform.fsti 2024-01-31 17:22:55.536846509 +0100 +--- extraction-edited/Libcrux_platform.fsti 2024-02-01 11:03:26.826760184 +0100 ++++ extraction-secret-independent/Libcrux_platform.fsti 2024-02-01 11:03:26.887758395 +0100 @@ -1,4 +1,4 @@ module Libcrux_platform #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" @@ -7158,7 +7135,7 @@ diff -ruN extraction-edited/Libcrux_platform.fsti extraction-secret-independent/ -val simd256_support: bool +val simd256_support : unit -> bool diff -ruN extraction-edited/MkSeq.fst extraction-secret-independent/MkSeq.fst ---- extraction-edited/MkSeq.fst 2024-01-31 17:22:55.459848113 +0100 +--- extraction-edited/MkSeq.fst 2024-02-01 11:03:26.814760535 +0100 +++ extraction-secret-independent/MkSeq.fst 1970-01-01 01:00:00.000000000 +0100 @@ -1,91 +0,0 @@ -module MkSeq @@ -7253,7 +7230,7 @@ diff -ruN extraction-edited/MkSeq.fst extraction-secret-independent/MkSeq.fst - -%splice[] (init 13 (fun i -> create_gen_tac (i + 1))) diff -ruN extraction-edited/Spec.Kyber.fst extraction-secret-independent/Spec.Kyber.fst ---- extraction-edited/Spec.Kyber.fst 2024-01-31 17:22:55.495847363 +0100 +--- extraction-edited/Spec.Kyber.fst 2024-02-01 11:03:26.846759597 +0100 +++ extraction-secret-independent/Spec.Kyber.fst 1970-01-01 01:00:00.000000000 +0100 @@ -1,433 +0,0 @@ -module Spec.Kyber