Merge pull request #151 from cryspen/rejection-sampling-panic

Panic instead of returning an error in rejection sampling if 5 blocks of SHAKE aren't enough
cryspen · Dec 8, 2023 · cb5785e · cb5785e
2 parents 456b566 + a4f63d0
commit cb5785e
Show file tree

Hide file tree

Showing 20 changed files with 152 additions and 304 deletions.
diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Ind_cpa.fst b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Ind_cpa.fst
@@ -358,7 +358,7 @@ let encrypt
       (public_key: t_Slice u8)
       (message: t_Array u8 (sz 32))
       (randomness: t_Slice u8)
-    : (t_Array u8 v_CIPHERTEXT_SIZE & Core.Option.t_Option Libcrux.Kem.Kyber.Types.t_Error) =
+    : t_Array u8 v_CIPHERTEXT_SIZE =
   let tt_as_ntt:t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K =
     deserialize_public_key v_K v_T_AS_NTT_ENCODED_SIZE public_key
   in
@@ -367,9 +367,7 @@ let encrypt
       <:
       Core.Ops.Range.t_RangeFrom usize ]
   in
-  let v_A_transpose, sampling_A_error:(t_Array
-      (t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K) v_K &
-    Core.Option.t_Option Libcrux.Kem.Kyber.Types.t_Error) =
+  let v_A_transpose:t_Array (t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K) v_K =
     Libcrux.Kem.Kyber.Matrix.sample_matrix_A v_K
       (into_padded_array (sz 34) seed <: t_Array u8 (sz 34))
       false
@@ -433,9 +431,7 @@ let encrypt
         <:
         t_Slice u8)
   in
-  ciphertext, sampling_A_error
-  <:
-  (t_Array u8 v_CIPHERTEXT_SIZE & Core.Option.t_Option Libcrux.Kem.Kyber.Types.t_Error)
+  ciphertext
 
 let serialize_secret_key
       (v_K v_OUT_LEN: usize)
@@ -550,15 +546,12 @@ let generate_keypair
       (v_K v_PRIVATE_KEY_SIZE v_PUBLIC_KEY_SIZE v_RANKED_BYTES_PER_RING_ELEMENT v_ETA1 v_ETA1_RANDOMNESS_SIZE:
           usize)
       (key_generation_seed: t_Slice u8)
-    : ((t_Array u8 v_PRIVATE_KEY_SIZE & t_Array u8 v_PUBLIC_KEY_SIZE) &
-      Core.Option.t_Option Libcrux.Kem.Kyber.Types.t_Error) =
+    : (t_Array u8 v_PRIVATE_KEY_SIZE & t_Array u8 v_PUBLIC_KEY_SIZE) =
   let hashed:t_Array u8 (sz 64) = Libcrux.Kem.Kyber.Hash_functions.v_G key_generation_seed in
   let seed_for_A, seed_for_secret_and_error:(t_Slice u8 & t_Slice u8) =
     Core.Slice.impl__split_at (Rust_primitives.unsize hashed <: t_Slice u8) (sz 32)
   in
-  let v_A_transpose, sampling_A_error:(t_Array
-      (t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K) v_K &
-    Core.Option.t_Option Libcrux.Kem.Kyber.Types.t_Error) =
+  let v_A_transpose:t_Array (t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K) v_K =
     Libcrux.Kem.Kyber.Matrix.sample_matrix_A v_K
       (into_padded_array (sz 34) seed_for_A <: t_Array u8 (sz 34))
       true
@@ -583,10 +576,6 @@ let generate_keypair
   let secret_key_serialized:t_Array u8 v_PRIVATE_KEY_SIZE =
     serialize_secret_key v_K v_PRIVATE_KEY_SIZE secret_as_ntt
   in
-  (secret_key_serialized, public_key_serialized
-    <:
-    (t_Array u8 v_PRIVATE_KEY_SIZE & t_Array u8 v_PUBLIC_KEY_SIZE)),
-  sampling_A_error
+  secret_key_serialized, public_key_serialized
   <:
-  ((t_Array u8 v_PRIVATE_KEY_SIZE & t_Array u8 v_PUBLIC_KEY_SIZE) &
-    Core.Option.t_Option Libcrux.Kem.Kyber.Types.t_Error)
+  (t_Array u8 v_PRIVATE_KEY_SIZE & t_Array u8 v_PUBLIC_KEY_SIZE)
diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Kyber1024.fst b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Kyber1024.fst
@@ -81,15 +81,12 @@ let decapsulate_1024_
 let encapsulate_1024_
       (public_key: Libcrux.Kem.Kyber.Types.t_KyberPublicKey (sz 1568))
       (randomness: t_Array u8 (sz 32))
-    : Core.Result.t_Result
-      (Libcrux.Kem.Kyber.Types.t_KyberCiphertext (sz 1568) & t_Array u8 (sz 32))
-      Libcrux.Kem.Kyber.Types.t_Error =
+    : (Libcrux.Kem.Kyber.Types.t_KyberCiphertext (sz 1568) & t_Array u8 (sz 32)) =
   Libcrux.Kem.Kyber.encapsulate (sz 4) (sz 1568) (sz 1568) (sz 1536) (sz 1408) (sz 160) (sz 11)
     (sz 5) (sz 352) (sz 2) (sz 128) (sz 2) (sz 128) public_key randomness
 
 let generate_key_pair_1024_ (randomness: t_Array u8 (sz 64))
-    : Core.Result.t_Result (Libcrux.Kem.Kyber.Types.t_KyberKeyPair (sz 3168) (sz 1568))
-      Libcrux.Kem.Kyber.Types.t_Error =
+    : Libcrux.Kem.Kyber.Types.t_KyberKeyPair (sz 3168) (sz 1568) =
   Libcrux.Kem.Kyber.generate_keypair (sz 4)
     (sz 1536)
     (sz 3168)

diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Kyber512.fst b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Kyber512.fst
@@ -81,14 +81,12 @@ let decapsulate_512_
 let encapsulate_512_
       (public_key: Libcrux.Kem.Kyber.Types.t_KyberPublicKey (sz 800))
       (randomness: t_Array u8 (sz 32))
-    : Core.Result.t_Result (Libcrux.Kem.Kyber.Types.t_KyberCiphertext (sz 768) & t_Array u8 (sz 32))
-      Libcrux.Kem.Kyber.Types.t_Error =
+    : (Libcrux.Kem.Kyber.Types.t_KyberCiphertext (sz 768) & t_Array u8 (sz 32)) =
   Libcrux.Kem.Kyber.encapsulate (sz 2) (sz 768) (sz 800) (sz 768) (sz 640) (sz 128) (sz 10) (sz 4)
     (sz 320) (sz 3) (sz 192) (sz 2) (sz 128) public_key randomness
 
 let generate_key_pair_512_ (randomness: t_Array u8 (sz 64))
-    : Core.Result.t_Result (Libcrux.Kem.Kyber.Types.t_KyberKeyPair (sz 1632) (sz 800))
-      Libcrux.Kem.Kyber.Types.t_Error =
+    : Libcrux.Kem.Kyber.Types.t_KyberKeyPair (sz 1632) (sz 800) =
   Libcrux.Kem.Kyber.generate_keypair (sz 2)
     (sz 768)
     (sz 1632)

diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Kyber768.fst b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Kyber768.fst
@@ -81,15 +81,12 @@ let decapsulate_768_
 let encapsulate_768_
       (public_key: Libcrux.Kem.Kyber.Types.t_KyberPublicKey (sz 1184))
       (randomness: t_Array u8 (sz 32))
-    : Core.Result.t_Result
-      (Libcrux.Kem.Kyber.Types.t_KyberCiphertext (sz 1088) & t_Array u8 (sz 32))
-      Libcrux.Kem.Kyber.Types.t_Error =
+    : (Libcrux.Kem.Kyber.Types.t_KyberCiphertext (sz 1088) & t_Array u8 (sz 32)) =
   Libcrux.Kem.Kyber.encapsulate (sz 3) (sz 1088) (sz 1184) (sz 1152) (sz 960) (sz 128) (sz 10)
     (sz 4) (sz 320) (sz 2) (sz 128) (sz 2) (sz 128) public_key randomness
 
 let generate_key_pair_768_ (randomness: t_Array u8 (sz 64))
-    : Core.Result.t_Result (Libcrux.Kem.Kyber.Types.t_KyberKeyPair (sz 2400) (sz 1184))
-      Libcrux.Kem.Kyber.Types.t_Error =
+    : Libcrux.Kem.Kyber.Types.t_KyberKeyPair (sz 2400) (sz 1184) =
   Libcrux.Kem.Kyber.generate_keypair (sz 3)
     (sz 1152)
     (sz 2400)

diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Matrix.fst b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Matrix.fst
@@ -421,21 +421,15 @@ let compute_vector_u
   result
 
 let sample_matrix_A (v_K: usize) (seed: t_Array u8 (sz 34)) (transpose: bool)
-    : (t_Array (t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K) v_K &
-      Core.Option.t_Option Libcrux.Kem.Kyber.Types.t_Error) =
+    : t_Array (t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K) v_K =
   let v_A_transpose:t_Array (t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K) v_K =
     Rust_primitives.Hax.repeat (Rust_primitives.Hax.repeat Libcrux.Kem.Kyber.Arithmetic.impl__PolynomialRingElement__ZERO
           v_K
         <:
         t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K)
       v_K
   in
-  let sampling_A_error:Core.Option.t_Option Libcrux.Kem.Kyber.Types.t_Error =
-    Core.Option.Option_None <: Core.Option.t_Option Libcrux.Kem.Kyber.Types.t_Error
-  in
-  let v_A_transpose, sampling_A_error:(t_Array
-      (t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K) v_K &
-    Core.Option.t_Option Libcrux.Kem.Kyber.Types.t_Error) =
+  let v_A_transpose:t_Array (t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K) v_K =
     Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
               Core.Ops.Range.f_start = sz 0;
               Core.Ops.Range.f_end = v_K
@@ -444,15 +438,11 @@ let sample_matrix_A (v_K: usize) (seed: t_Array u8 (sz 34)) (transpose: bool)
             Core.Ops.Range.t_Range usize)
         <:
         Core.Ops.Range.t_Range usize)
-      (v_A_transpose, sampling_A_error
-        <:
-        (t_Array (t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K) v_K &
-          Core.Option.t_Option Libcrux.Kem.Kyber.Types.t_Error))
-      (fun temp_0_ i ->
-          let v_A_transpose, sampling_A_error:(t_Array
-              (t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K) v_K &
-            Core.Option.t_Option Libcrux.Kem.Kyber.Types.t_Error) =
-            temp_0_
+      v_A_transpose
+      (fun v_A_transpose i ->
+          let v_A_transpose:t_Array
+            (t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K) v_K =
+            v_A_transpose
           in
           let i:usize = i in
           let seeds:t_Array (t_Array u8 (sz 34)) v_K = Rust_primitives.Hax.repeat seed v_K in
@@ -504,30 +494,17 @@ let sample_matrix_A (v_K: usize) (seed: t_Array u8 (sz 34)) (transpose: bool)
                   Core.Ops.Range.t_Range usize)
               <:
               Core.Ops.Range.t_Range usize)
-            (v_A_transpose, sampling_A_error
-              <:
-              (t_Array (t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K) v_K &
-                Core.Option.t_Option Libcrux.Kem.Kyber.Types.t_Error))
-            (fun temp_0_ j ->
-                let v_A_transpose, sampling_A_error:(t_Array
-                    (t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K) v_K &
-                  Core.Option.t_Option Libcrux.Kem.Kyber.Types.t_Error) =
-                  temp_0_
+            v_A_transpose
+            (fun v_A_transpose j ->
+                let v_A_transpose:t_Array
+                  (t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K) v_K =
+                  v_A_transpose
                 in
                 let j:usize = j in
-                let sampled, error:(Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement &
-                  Core.Option.t_Option Libcrux.Kem.Kyber.Types.t_Error) =
-                  Libcrux.Kem.Kyber.Sampling.sample_from_uniform_distribution (sz 840)
-                    (xof_bytes.[ j ] <: t_Array u8 (sz 840))
-                in
-                let sampling_A_error:Core.Option.t_Option Libcrux.Kem.Kyber.Types.t_Error =
-                  if Core.Option.impl__is_some error
-                  then
-                    let sampling_A_error:Core.Option.t_Option Libcrux.Kem.Kyber.Types.t_Error =
-                      error
-                    in
-                    sampling_A_error
-                  else sampling_A_error
+                let sampled:Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement =
+                  Libcrux.Kem.Kyber.Sampling.sample_from_uniform_distribution (xof_bytes.[ j ]
+                      <:
+                      t_Array u8 (sz 840))
                 in
                 if transpose
                 then
@@ -544,10 +521,7 @@ let sample_matrix_A (v_K: usize) (seed: t_Array u8 (sz 34)) (transpose: bool)
                         <:
                         t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K)
                   in
-                  v_A_transpose, sampling_A_error
-                  <:
-                  (t_Array (t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K) v_K &
-                    Core.Option.t_Option Libcrux.Kem.Kyber.Types.t_Error)
+                  v_A_transpose
                 else
                   let v_A_transpose:t_Array
                     (t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K) v_K =
@@ -562,12 +536,6 @@ let sample_matrix_A (v_K: usize) (seed: t_Array u8 (sz 34)) (transpose: bool)
                         <:
                         t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K)
                   in
-                  v_A_transpose, sampling_A_error
-                  <:
-                  (t_Array (t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K) v_K &
-                    Core.Option.t_Option Libcrux.Kem.Kyber.Types.t_Error)))
+                  v_A_transpose))
   in
-  v_A_transpose, sampling_A_error
-  <:
-  (t_Array (t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K) v_K &
-    Core.Option.t_Option Libcrux.Kem.Kyber.Types.t_Error)
+  v_A_transpose
diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Sampling.fst b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Sampling.fst
@@ -3,6 +3,11 @@ module Libcrux.Kem.Kyber.Sampling
 open Core
 open FStar.Mul
 
+let rejection_sampling_panic_with_diagnostic: Prims.unit =
+  Rust_primitives.Hax.never_to_any (Core.Panicking.panic "explicit panic"
+      <:
+      Rust_primitives.Hax.t_Never)
+
 let sample_from_binomial_distribution_2_ (randomness: t_Slice u8)
     : Prims.Pure Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement
       (requires (Core.Slice.impl__len randomness <: usize) =. (sz 2 *! sz 64 <: usize))
@@ -208,9 +213,8 @@ let sample_from_binomial_distribution (v_ETA: usize) (randomness: t_Slice u8)
         <:
         Rust_primitives.Hax.t_Never)
 
-let sample_from_uniform_distribution (v_SEED_SIZE: usize) (randomness: t_Array u8 v_SEED_SIZE)
-    : (Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement &
-      Core.Option.t_Option Libcrux.Kem.Kyber.Types.t_Error) =
+let sample_from_uniform_distribution (randomness: t_Array u8 (sz 840))
+    : Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement =
   let (sampled_coefficients: usize):usize = sz 0 in
   let (out: Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement):Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement
   =
@@ -313,19 +317,11 @@ let sample_from_uniform_distribution (v_SEED_SIZE: usize) (randomness: t_Array u
             <:
             (bool & Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement & usize))
   in
-  if done
-  then
-    let _:Prims.unit = () <: Prims.unit in
-    out, (Core.Option.Option_None <: Core.Option.t_Option Libcrux.Kem.Kyber.Types.t_Error)
-    <:
-    (Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement &
-      Core.Option.t_Option Libcrux.Kem.Kyber.Types.t_Error)
-  else
-    out,
-    (Core.Option.Option_Some
-      (Libcrux.Kem.Kyber.Types.Error_RejectionSampling <: Libcrux.Kem.Kyber.Types.t_Error)
-      <:
-      Core.Option.t_Option Libcrux.Kem.Kyber.Types.t_Error)
-    <:
-    (Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement &
-      Core.Option.t_Option Libcrux.Kem.Kyber.Types.t_Error)
+  let _:Prims.unit =
+    if ~.done
+    then
+      let _:Prims.unit = rejection_sampling_panic_with_diagnostic in
+      ()
+  in
+  let _:Prims.unit = () <: Prims.unit in
+  out
diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Types.fst b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Types.fst
@@ -3,8 +3,6 @@ module Libcrux.Kem.Kyber.Types
 open Core
 open FStar.Mul
 
-type t_Error = | Error_RejectionSampling : t_Error
-
 type t_KyberCiphertext (v_SIZE: usize) = { f_value:t_Array u8 v_SIZE }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]