From 0a935fefb69b9ed781162b722e56547c2e7643c6 Mon Sep 17 00:00:00 2001 From: karthikbhargavan Date: Sun, 1 Dec 2024 13:06:33 +0000 Subject: [PATCH] fstar --- .../extraction/Libcrux_ml_kem.Ind_cpa.fst | 51 +------------------ .../extraction/Libcrux_ml_kem.Ind_cpa.fsti | 13 ----- .../fstar/extraction/Libcrux_ml_kem.Utils.fst | 47 +++++++++++++++++ .../extraction/Libcrux_ml_kem.Utils.fsti | 13 +++++ 4 files changed, 62 insertions(+), 62 deletions(-) diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fst index 8fb8e250b..073e16e7d 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fst @@ -12,53 +12,6 @@ let _ = let open Libcrux_ml_kem.Vector.Traits in () -#push-options "--z3rlimit 200" - -let prf_input_inc (v_K: usize) (prf_inputs: t_Array (t_Array u8 (sz 33)) v_K) (domain_separator: u8) = - let v__domain_separator_init:u8 = domain_separator in - let v__prf_inputs_init:t_Array (t_Array u8 (sz 33)) v_K = - Core.Clone.f_clone #(t_Array (t_Array u8 (sz 33)) v_K) - #FStar.Tactics.Typeclasses.solve - prf_inputs - in - let domain_separator, prf_inputs:(u8 & t_Array (t_Array u8 (sz 33)) v_K) = - Rust_primitives.Hax.Folds.fold_range (sz 0) - v_K - (fun temp_0_ i -> - let domain_separator, prf_inputs:(u8 & t_Array (t_Array u8 (sz 33)) v_K) = temp_0_ in - let i:usize = i in - v domain_separator == v v__domain_separator_init + v i /\ - (v i < v v_K ==> - (forall (j: nat). - (j >= v i /\ j < v v_K) ==> prf_inputs.[ sz j ] == v__prf_inputs_init.[ sz j ])) /\ - (forall (j: nat). - j < v i ==> - v (Seq.index (Seq.index prf_inputs j) 32) == v v__domain_separator_init + j /\ - Seq.slice (Seq.index prf_inputs j) 0 32 == - Seq.slice (Seq.index v__prf_inputs_init j) 0 32)) - (domain_separator, prf_inputs <: (u8 & t_Array (t_Array u8 (sz 33)) v_K)) - (fun temp_0_ i -> - let domain_separator, prf_inputs:(u8 & t_Array (t_Array u8 (sz 33)) v_K) = temp_0_ in - let i:usize = i in - let prf_inputs:t_Array (t_Array u8 (sz 33)) v_K = - Rust_primitives.Hax.Monomorphized_update_at.update_at_usize prf_inputs - i - (Rust_primitives.Hax.Monomorphized_update_at.update_at_usize (prf_inputs.[ i ] - <: - t_Array u8 (sz 33)) - (sz 32) - domain_separator - <: - t_Array u8 (sz 33)) - in - let domain_separator:u8 = domain_separator +! 1uy in - domain_separator, prf_inputs <: (u8 & t_Array (t_Array u8 (sz 33)) v_K)) - in - let hax_temp_output:u8 = domain_separator in - prf_inputs, hax_temp_output <: (t_Array (t_Array u8 (sz 33)) v_K & u8) - -#pop-options - #push-options "--ext context_pruning" let deserialize_secret_key @@ -236,7 +189,7 @@ let sample_ring_element_cbd let prf_inputs:t_Array (t_Array u8 (sz 33)) v_K = Rust_primitives.Hax.repeat prf_input v_K in let v__domain_separator_init:u8 = domain_separator in let tmp0, out:(t_Array (t_Array u8 (sz 33)) v_K & u8) = - prf_input_inc v_K prf_inputs domain_separator + Libcrux_ml_kem.Utils.prf_input_inc v_K prf_inputs domain_separator in let prf_inputs:t_Array (t_Array u8 (sz 33)) v_K = tmp0 in let domain_separator:u8 = out in @@ -384,7 +337,7 @@ let sample_vector_cbd_then_ntt let prf_inputs:t_Array (t_Array u8 (sz 33)) v_K = Rust_primitives.Hax.repeat prf_input v_K in let v__domain_separator_init:u8 = domain_separator in let tmp0, out:(t_Array (t_Array u8 (sz 33)) v_K & u8) = - prf_input_inc v_K prf_inputs domain_separator + Libcrux_ml_kem.Utils.prf_input_inc v_K prf_inputs domain_separator in let prf_inputs:t_Array (t_Array u8 (sz 33)) v_K = tmp0 in let domain_separator:u8 = out in diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fsti index 8cdc832e0..70c350031 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fsti @@ -12,19 +12,6 @@ let _ = let open Libcrux_ml_kem.Vector.Traits in () -val prf_input_inc (v_K: usize) (prf_inputs: t_Array (t_Array u8 (sz 33)) v_K) (domain_separator: u8) - : Prims.Pure (t_Array (t_Array u8 (sz 33)) v_K & u8) - (requires range (v domain_separator + v v_K) u8_inttype) - (ensures - fun temp_0_ -> - let prf_inputs_future, ds:(t_Array (t_Array u8 (sz 33)) v_K & u8) = temp_0_ in - v ds == v domain_separator + v v_K /\ - (forall (i: nat). - i < v v_K ==> - v (Seq.index (Seq.index prf_inputs_future i) 32) == v domain_separator + i /\ - Seq.slice (Seq.index prf_inputs_future i) 0 32 == - Seq.slice (Seq.index prf_inputs i) 0 32)) - /// Call [`deserialize_to_uncompressed_ring_element`] for each ring element. val deserialize_secret_key (v_K: usize) diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Utils.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Utils.fst index 54769237f..84b152b40 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Utils.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Utils.fst @@ -3,6 +3,53 @@ module Libcrux_ml_kem.Utils open Core open FStar.Mul +#push-options "--z3rlimit 200" + +let prf_input_inc (v_K: usize) (prf_inputs: t_Array (t_Array u8 (sz 33)) v_K) (domain_separator: u8) = + let v__domain_separator_init:u8 = domain_separator in + let v__prf_inputs_init:t_Array (t_Array u8 (sz 33)) v_K = + Core.Clone.f_clone #(t_Array (t_Array u8 (sz 33)) v_K) + #FStar.Tactics.Typeclasses.solve + prf_inputs + in + let domain_separator, prf_inputs:(u8 & t_Array (t_Array u8 (sz 33)) v_K) = + Rust_primitives.Hax.Folds.fold_range (sz 0) + v_K + (fun temp_0_ i -> + let domain_separator, prf_inputs:(u8 & t_Array (t_Array u8 (sz 33)) v_K) = temp_0_ in + let i:usize = i in + v domain_separator == v v__domain_separator_init + v i /\ + (v i < v v_K ==> + (forall (j: nat). + (j >= v i /\ j < v v_K) ==> prf_inputs.[ sz j ] == v__prf_inputs_init.[ sz j ])) /\ + (forall (j: nat). + j < v i ==> + v (Seq.index (Seq.index prf_inputs j) 32) == v v__domain_separator_init + j /\ + Seq.slice (Seq.index prf_inputs j) 0 32 == + Seq.slice (Seq.index v__prf_inputs_init j) 0 32)) + (domain_separator, prf_inputs <: (u8 & t_Array (t_Array u8 (sz 33)) v_K)) + (fun temp_0_ i -> + let domain_separator, prf_inputs:(u8 & t_Array (t_Array u8 (sz 33)) v_K) = temp_0_ in + let i:usize = i in + let prf_inputs:t_Array (t_Array u8 (sz 33)) v_K = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize prf_inputs + i + (Rust_primitives.Hax.Monomorphized_update_at.update_at_usize (prf_inputs.[ i ] + <: + t_Array u8 (sz 33)) + (sz 32) + domain_separator + <: + t_Array u8 (sz 33)) + in + let domain_separator:u8 = domain_separator +! 1uy in + domain_separator, prf_inputs <: (u8 & t_Array (t_Array u8 (sz 33)) v_K)) + in + let hax_temp_output:u8 = domain_separator in + prf_inputs, hax_temp_output <: (t_Array (t_Array u8 (sz 33)) v_K & u8) + +#pop-options + let into_padded_array (v_LEN: usize) (slice: t_Slice u8) = let out:t_Array u8 v_LEN = Rust_primitives.Hax.repeat 0uy v_LEN in let out:t_Array u8 v_LEN = diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Utils.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Utils.fsti index 389070322..033a1e9d3 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Utils.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Utils.fsti @@ -3,6 +3,19 @@ module Libcrux_ml_kem.Utils open Core open FStar.Mul +val prf_input_inc (v_K: usize) (prf_inputs: t_Array (t_Array u8 (sz 33)) v_K) (domain_separator: u8) + : Prims.Pure (t_Array (t_Array u8 (sz 33)) v_K & u8) + (requires range (v domain_separator + v v_K) u8_inttype) + (ensures + fun temp_0_ -> + let prf_inputs_future, ds:(t_Array (t_Array u8 (sz 33)) v_K & u8) = temp_0_ in + v ds == v domain_separator + v v_K /\ + (forall (i: nat). + i < v v_K ==> + v (Seq.index (Seq.index prf_inputs_future i) 32) == v domain_separator + i /\ + Seq.slice (Seq.index prf_inputs_future i) 0 32 == + Seq.slice (Seq.index prf_inputs i) 0 32)) + /// Pad the `slice` with `0`s at the end. val into_padded_array (v_LEN: usize) (slice: t_Slice u8) : Prims.Pure (t_Array u8 v_LEN)