Remove kyber cycles

hax-driver.py

@@ -6,7 +6,7 @@
 import sys
 
 
-def shell(command, expect=0, cwd=None):
+def shell(command, expect=0, cwd=None, env={}):
     subprocess_stdout = subprocess.DEVNULL
 
     print("Command: ", end="")
@@ -18,7 +18,10 @@ def shell(command, expect=0, cwd=None):
 
     print("\nDirectory: {}".format(cwd))
 
-    ret = subprocess.run(command, cwd=cwd)
+    os_env = os.environ
+    os_env.update(env)
+
+    ret = subprocess.run(command, cwd=cwd, env=os_env)
     if ret.returncode != expect:
         raise Exception("Error {}. Expected {}.".format(ret, expect))
 
@@ -71,6 +74,18 @@ def shell(command, expect=0, cwd=None):
     default="",
     help="Space-separated list of modules to exclude from extraction. The module names must be fully qualified.",
 )
+typecheck_parser = parser.add_subparsers(
+    description="Typecheck libcrux",
+    dest="typecheck",
+    help="Run F* etc. to typecheck the extracted libcrux code.",
+)
+typecheck_parser = typecheck_parser.add_parser("typecheck")
+typecheck_parser.add_argument(
+    "--lax",
+    action="store_true",
+    dest="lax",
+    help="Lax typecheck the code only",
+)
 
 options = parser.parse_args()
 
@@ -96,6 +111,13 @@ def shell(command, expect=0, cwd=None):
     else:
         filter_string += " {}".format(options.exclude_modules)
 
+if options.typecheck:
+    custom_env = {}
+    if options.lax:
+        custom_env.update({"OTHERFLAGS": "--lax"})
+    shell(["make", "-C", "proofs/fstar/extraction/"], custom_env)
+    exit(0)
+
 if options.kyber_reference:
     shell(
         [

libcrux.fst.config.json

@@ -0,0 +1,19 @@
+{
+    "fstar_exe": "fstar.exe",
+    "options": [
+        "--cmi",
+        "--warn_error",
+        "-331",
+        "--cache_checked_modules",
+        "--cache_dir",
+        "${HAX_HOME}/proof-libs/fstar/.cache",
+        "--already_cached",
+        "+Prims+FStar+LowStar+C+Spec.Loops+TestLib"
+    ],
+    "include_dirs": [
+        "${HACL_HOME}/lib",
+        "${HAX_HOME}/proof-libs/fstar/rust_primitives",
+        "${HAX_HOME}/proof-libs/fstar/core",
+        "${HAX_HOME}/proof-libs/fstar/hax_lib"
+    ]
+}

proofs/fstar/extraction/Libcrux.Digest.fst → proofs/fstar/extraction/Libcrux.Digest.fsti

@@ -1,5 +1,6 @@
 module Libcrux.Digest
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Rust_primitives
 open Core
 
 type t_Algorithm =
@@ -29,10 +30,10 @@ let digest_size (mode: t_Algorithm) : usize =
   | Algorithm_Sha3_384_  -> sz 48
   | Algorithm_Sha3_512_  -> sz 64
 
-let sha3_256_ (payload: slice u8) : array u8 (sz 32) = Libcrux.Hacl.Sha3.sha256 payload
+val sha3_256_ (payload: t_Slice u8) : t_Array u8 (sz 32)
 
-let sha3_512_ (payload: slice u8) : array u8 (sz 64) = Libcrux.Hacl.Sha3.sha512 payload
+val sha3_512_ (payload: t_Slice u8) : t_Array u8 (sz 64)
 
-let shake128 (#v_LEN: usize) (data: slice u8) : array u8 v_LEN = Libcrux.Hacl.Sha3.shake128 data
+val shake128 (#v_LEN: usize) (data: t_Slice u8) : t_Array u8 v_LEN
 
-let shake256 (#v_LEN: usize) (data: slice u8) : array u8 v_LEN = Libcrux.Hacl.Sha3.shake256 data
+val shake256 (#v_LEN: usize) (data: t_Slice u8) : t_Array u8 v_LEN

proofs/fstar/extraction/Libcrux.Kem.Kyber.Ind_cpa.fst

@@ -2,102 +2,6 @@ module Libcrux.Kem.Kyber.Ind_cpa
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
 open Core
 
-type t_PrivateKey (#v_SIZE: usize) = { f_value:t_Array u8 v_SIZE }
-
-let impl (#v_SIZE: usize) : Core.Convert.t_AsRef (t_PrivateKey v_SIZE) (t_Slice u8) =
-  {
-    f_as_ref
-    =
-    fun (#v_SIZE: usize) (self: t_PrivateKey v_SIZE) -> Rust_primitives.unsize self.f_value
-  }
-
-let impl_1 (#v_SIZE: usize) : Core.Convert.t_From (t_PrivateKey v_SIZE) (t_Array u8 v_SIZE) =
-  { f_from = fun (#v_SIZE: usize) (value: t_Array u8 v_SIZE) -> { f_value = value } }
-
-let impl_2 (#v_SIZE: usize) : Core.Convert.t_From (t_PrivateKey v_SIZE) (t_Array u8 v_SIZE) =
-  {
-    f_from
-    =
-    fun (#v_SIZE: usize) (value: t_Array u8 v_SIZE) -> { f_value = Core.Clone.f_clone value }
-  }
-
-let impl_3 (#v_SIZE: usize) : Core.Convert.t_From (t_Array u8 v_SIZE) (t_PrivateKey v_SIZE) =
-  { f_from = fun (#v_SIZE: usize) (value: t_PrivateKey v_SIZE) -> value.f_value }
-
-let impl_4 (#v_SIZE: usize) : Core.Convert.t_TryFrom (t_PrivateKey v_SIZE) (t_Slice u8) =
-  {
-    f_Error = Core.Array.t_TryFromSliceError;
-    f_try_from
-    =
-    fun (#v_SIZE: usize) (value: t_Slice u8) ->
-      Rust_primitives.Hax.Control_flow_monad.Mexception.run (let* hoist2:t_Array u8 v_SIZE =
-            match
-              Core.Ops.Try_trait.f_branch (Core.Convert.f_try_into value
-                  <:
-                  Core.Result.t_Result (t_Array u8 v_SIZE) Core.Array.t_TryFromSliceError)
-            with
-            | Core.Ops.Control_flow.ControlFlow_Break residual ->
-              let* hoist1:Rust_primitives.Hax.t_Never =
-                Core.Ops.Control_flow.ControlFlow.v_Break (Core.Ops.Try_trait.f_from_residual residual
-
-                    <:
-                    Core.Result.t_Result (t_PrivateKey v_SIZE) Core.Array.t_TryFromSliceError)
-              in
-              Core.Ops.Control_flow.ControlFlow_Continue (Rust_primitives.Hax.never_to_any hoist1)
-            | Core.Ops.Control_flow.ControlFlow_Continue v_val ->
-              Core.Ops.Control_flow.ControlFlow_Continue v_val
-          in
-          Core.Ops.Control_flow.ControlFlow_Continue
-          (let hoist3:t_PrivateKey v_SIZE = { f_value = hoist2 } in
-            Core.Result.Result_Ok hoist3))
-  }
-
-let impl_5 (#v_SIZE: usize) : Core.Ops.Index.t_Index (t_PrivateKey v_SIZE) usize =
-  {
-    f_Output = u8;
-    f_index
-    =
-    fun (#v_SIZE: usize) (self: t_PrivateKey v_SIZE) (index: usize) -> self.f_value.[ index ]
-  }
-
-let impl_6 (#v_SIZE: usize)
-    : Core.Ops.Index.t_Index (t_PrivateKey v_SIZE) (Core.Ops.Range.t_Range usize) =
-  {
-    f_Output = t_Slice u8;
-    f_index
-    =
-    fun (#v_SIZE: usize) (self: t_PrivateKey v_SIZE) (range: Core.Ops.Range.t_Range usize) ->
-      self.f_value.[ range ]
-  }
-
-let impl_7 (#v_SIZE: usize)
-    : Core.Ops.Index.t_Index (t_PrivateKey v_SIZE) (Core.Ops.Range.t_RangeTo usize) =
-  {
-    f_Output = t_Slice u8;
-    f_index
-    =
-    fun (#v_SIZE: usize) (self: t_PrivateKey v_SIZE) (range: Core.Ops.Range.t_RangeTo usize) ->
-      self.f_value.[ range ]
-  }
-
-let impl_8 (#v_SIZE: usize)
-    : Core.Ops.Index.t_Index (t_PrivateKey v_SIZE) (Core.Ops.Range.t_RangeFrom usize) =
-  {
-    f_Output = t_Slice u8;
-    f_index
-    =
-    fun (#v_SIZE: usize) (self: t_PrivateKey v_SIZE) (range: Core.Ops.Range.t_RangeFrom usize) ->
-      self.f_value.[ range ]
-  }
-
-let impl_9__as_slice (#v_SIZE: usize) (self: t_PrivateKey v_SIZE) : t_Array u8 v_SIZE = self.f_value
-
-let impl_9__split_at (#v_SIZE: usize) (self: t_PrivateKey v_SIZE) (mid: usize)
-    : (t_Slice u8 & t_Slice u8) =
-  Core.Slice.impl__split_at (Rust_primitives.unsize self.f_value <: t_Slice u8) mid
-
-let impl_9__len (#v_SIZE: usize) (self: t_PrivateKey v_SIZE) : usize = v_SIZE
-
 let serialize_secret_key
       (#v_SERIALIZED_KEY_LEN: usize)
       (private_key public_key implicit_rejection_value: t_Slice u8)
@@ -128,7 +32,7 @@ let serialize_secret_key
 
 let sample_matrix_A (#v_K: usize) (seed: t_Array u8 (sz 34)) (transpose: bool)
     : (t_Array (t_Array Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement v_K) v_K &
-      Core.Option.t_Option Libcrux.Kem.Kyber.t_BadRejectionSamplingRandomnessError) =
+      Core.Option.t_Option Libcrux.Kem.Kyber.Types.t_Error) =
   let v_A_transpose:t_Array (t_Array Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement v_K)
     v_K =
     Rust_primitives.Hax.repeat (Rust_primitives.Hax.repeat Libcrux.Kem.Kyber.Arithmetic.impl__KyberPolynomialRingElement__ZERO
@@ -137,13 +41,12 @@ let sample_matrix_A (#v_K: usize) (seed: t_Array u8 (sz 34)) (transpose: bool)
         t_Array Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement v_K)
       v_K
   in
-  let sampling_A_error:Core.Option.t_Option Libcrux.Kem.Kyber.t_BadRejectionSamplingRandomnessError
-  =
+  let sampling_A_error:Core.Option.t_Option Libcrux.Kem.Kyber.Types.t_Error =
     Core.Option.Option_None
   in
   let v_A_transpose, sampling_A_error:(t_Array
       (t_Array Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement v_K) v_K &
-    Core.Option.t_Option Libcrux.Kem.Kyber.t_BadRejectionSamplingRandomnessError) =
+    Core.Option.t_Option Libcrux.Kem.Kyber.Types.t_Error) =
     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
@@ -194,17 +97,15 @@ let sample_matrix_A (#v_K: usize) (seed: t_Array u8 (sz 34)) (transpose: bool)
             (v_A_transpose, sampling_A_error)
             (fun (v_A_transpose, sampling_A_error) j ->
                 let sampled, error:(Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement &
-                  Core.Option.t_Option Libcrux.Kem.Kyber.t_BadRejectionSamplingRandomnessError) =
+                  Core.Option.t_Option Libcrux.Kem.Kyber.Types.t_Error) =
                   Libcrux.Kem.Kyber.Sampling.sample_from_uniform_distribution (xof_bytes.[ j ]
                       <:
                       t_Array u8 (sz 840))
                 in
-                let sampling_A_error:Core.Option.t_Option
-                Libcrux.Kem.Kyber.t_BadRejectionSamplingRandomnessError =
+                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.t_BadRejectionSamplingRandomnessError =
+                    let sampling_A_error:Core.Option.t_Option Libcrux.Kem.Kyber.Types.t_Error =
                       error
                     in
                     sampling_A_error
@@ -344,8 +245,9 @@ 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_PrivateKey v_PRIVATE_KEY_SIZE & Libcrux.Kem.Kyber.t_KyberPublicKey v_PUBLIC_KEY_SIZE) &
-      Core.Option.t_Option Libcrux.Kem.Kyber.t_BadRejectionSamplingRandomnessError) =
+    : ((Libcrux.Kem.Kyber.Types.t_PrivateKey v_PRIVATE_KEY_SIZE &
+        Libcrux.Kem.Kyber.Types.t_KyberPublicKey v_PUBLIC_KEY_SIZE) &
+      Core.Option.t_Option Libcrux.Kem.Kyber.Types.t_Error) =
   let (prf_input: t_Array u8 (sz 33)):t_Array u8 (sz 33) = Rust_primitives.Hax.repeat 0uy (sz 33) in
   let secret_as_ntt:t_Array Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement v_K =
     Rust_primitives.Hax.repeat Libcrux.Kem.Kyber.Arithmetic.impl__KyberPolynomialRingElement__ZERO
@@ -362,7 +264,7 @@ let generate_keypair
   in
   let v_A_transpose, sampling_A_error:(t_Array
       (t_Array Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement v_K) v_K &
-    Core.Option.t_Option Libcrux.Kem.Kyber.t_BadRejectionSamplingRandomnessError) =
+    Core.Option.t_Option Libcrux.Kem.Kyber.Types.t_Error) =
     sample_matrix_A (Libcrux.Kem.Kyber.Conversions.into_padded_array seed_for_A
         <:
         t_Array u8 (sz 34))
@@ -531,8 +433,8 @@ let encrypt
       (public_key: t_Slice u8)
       (message: t_Array u8 (sz 32))
       (randomness: t_Slice u8)
-    : (Libcrux.Kem.Kyber.t_KyberCiphertext v_CIPHERTEXT_SIZE &
-      Core.Option.t_Option Libcrux.Kem.Kyber.t_BadRejectionSamplingRandomnessError) =
+    : (Libcrux.Kem.Kyber.Types.t_KyberCiphertext v_CIPHERTEXT_SIZE &
+      Core.Option.t_Option Libcrux.Kem.Kyber.Types.t_Error) =
   let tt_as_ntt:t_Array Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement v_K =
     Rust_primitives.Hax.repeat Libcrux.Kem.Kyber.Arithmetic.impl__KyberPolynomialRingElement__ZERO
       v_K
@@ -564,7 +466,7 @@ let encrypt
   let seed:t_Slice u8 = public_key.[ { Core.Ops.Range.f_start = v_T_AS_NTT_ENCODED_SIZE } ] in
   let v_A_transpose, sampling_A_error:(t_Array
       (t_Array Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement v_K) v_K &
-    Core.Option.t_Option Libcrux.Kem.Kyber.t_BadRejectionSamplingRandomnessError) =
+    Core.Option.t_Option Libcrux.Kem.Kyber.Types.t_Error) =
     sample_matrix_A (Libcrux.Kem.Kyber.Conversions.into_padded_array seed <: t_Array u8 (sz 34))
       false
   in
@@ -656,7 +558,7 @@ let decrypt
       (#v_K #v_CIPHERTEXT_SIZE #v_VECTOR_U_ENCODED_SIZE #v_VECTOR_U_COMPRESSION_FACTOR #v_VECTOR_V_COMPRESSION_FACTOR:
           usize)
       (secret_key: t_Slice u8)
-      (ciphertext: Libcrux.Kem.Kyber.t_KyberCiphertext v_CIPHERTEXT_SIZE)
+      (ciphertext: Libcrux.Kem.Kyber.Types.t_KyberCiphertext v_CIPHERTEXT_SIZE)
     : t_Array u8 (sz 32) =
   let u_as_ntt:t_Array Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement v_K =
     Rust_primitives.Hax.repeat Libcrux.Kem.Kyber.Arithmetic.impl__KyberPolynomialRingElement__ZERO

proofs/fstar/extraction/Libcrux.Kem.Kyber.Kyber1024.fst

@@ -61,25 +61,24 @@ let v_ETA2_RANDOMNESS_SIZE: usize = v_ETA2 *! sz 64
 let v_IMPLICIT_REJECTION_HASH_INPUT_SIZE: usize =
   Libcrux.Kem.Kyber.Constants.v_SHARED_SECRET_SIZE +! v_CPA_PKE_CIPHERTEXT_SIZE_1024_
 
-let t_Kyber1024Ciphertext = Libcrux.Kem.Kyber.t_KyberCiphertext (sz 1568)
+let t_Kyber1024Ciphertext = Libcrux.Kem.Kyber.Types.t_KyberCiphertext (sz 1568)
 
-let t_Kyber1024PrivateKey = Libcrux.Kem.Kyber.t_KyberPrivateKey (sz 3168)
+let t_Kyber1024PrivateKey = Libcrux.Kem.Kyber.Types.t_KyberPrivateKey (sz 3168)
 
-let t_Kyber1024PublicKey = Libcrux.Kem.Kyber.t_KyberPublicKey (sz 1568)
+let t_Kyber1024PublicKey = Libcrux.Kem.Kyber.Types.t_KyberPublicKey (sz 1568)
 
 let generate_key_pair_1024_ (randomness: t_Array u8 (sz 64))
-    : Core.Result.t_Result (Libcrux.Kem.Kyber.t_KyberKeyPair (sz 3168) (sz 1568))
-      Libcrux.Kem.Kyber.t_BadRejectionSamplingRandomnessError =
-  Libcrux.Kem.Kyber.generate_keypair randomness
+    : Core.Result.t_Result (Libcrux.Kem.Kyber.Types.t_KyberKeyPair (sz 3168) (sz 1568))
+      Libcrux.Kem.Kyber.Types.t_Error = Libcrux.Kem.Kyber.generate_keypair randomness
 
 let encapsulate_1024_
-      (public_key: Libcrux.Kem.Kyber.t_KyberPublicKey (sz 1568))
+      (public_key: Libcrux.Kem.Kyber.Types.t_KyberPublicKey (sz 1568))
       (randomness: t_Array u8 (sz 32))
-    : Core.Result.t_Result (Libcrux.Kem.Kyber.t_KyberCiphertext (sz 1568) & t_Array u8 (sz 32))
-      Libcrux.Kem.Kyber.t_BadRejectionSamplingRandomnessError =
-  Libcrux.Kem.Kyber.encapsulate public_key randomness
+    : 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.encapsulate public_key randomness
 
 let decapsulate_1024_
-      (secret_key: Libcrux.Kem.Kyber.t_KyberPrivateKey (sz 3168))
-      (ciphertext: Libcrux.Kem.Kyber.t_KyberCiphertext (sz 1568))
+      (secret_key: Libcrux.Kem.Kyber.Types.t_KyberPrivateKey (sz 3168))
+      (ciphertext: Libcrux.Kem.Kyber.Types.t_KyberCiphertext (sz 1568))
     : t_Array u8 (sz 32) = Libcrux.Kem.Kyber.decapsulate secret_key ciphertext

proofs/fstar/extraction/Libcrux.Kem.Kyber.Kyber512.fst

@@ -61,25 +61,23 @@ let v_ETA2_RANDOMNESS_SIZE: usize = v_ETA2 *! sz 64
 let v_IMPLICIT_REJECTION_HASH_INPUT_SIZE: usize =
   Libcrux.Kem.Kyber.Constants.v_SHARED_SECRET_SIZE +! v_CPA_PKE_CIPHERTEXT_SIZE_512_
 
-let t_Kyber512Ciphertext = Libcrux.Kem.Kyber.t_KyberCiphertext (sz 768)
+let t_Kyber512Ciphertext = Libcrux.Kem.Kyber.Types.t_KyberCiphertext (sz 768)
 
-let t_Kyber512PrivateKey = Libcrux.Kem.Kyber.t_KyberPrivateKey (sz 1632)
+let t_Kyber512PrivateKey = Libcrux.Kem.Kyber.Types.t_KyberPrivateKey (sz 1632)
 
-let t_Kyber512PublicKey = Libcrux.Kem.Kyber.t_KyberPublicKey (sz 800)
+let t_Kyber512PublicKey = Libcrux.Kem.Kyber.Types.t_KyberPublicKey (sz 800)
 
 let generate_key_pair_512_ (randomness: t_Array u8 (sz 64))
-    : Core.Result.t_Result (Libcrux.Kem.Kyber.t_KyberKeyPair (sz 1632) (sz 800))
-      Libcrux.Kem.Kyber.t_BadRejectionSamplingRandomnessError =
-  Libcrux.Kem.Kyber.generate_keypair randomness
+    : Core.Result.t_Result (Libcrux.Kem.Kyber.Types.t_KyberKeyPair (sz 1632) (sz 800))
+      Libcrux.Kem.Kyber.Types.t_Error = Libcrux.Kem.Kyber.generate_keypair randomness
 
 let encapsulate_512_
-      (public_key: Libcrux.Kem.Kyber.t_KyberPublicKey (sz 800))
+      (public_key: Libcrux.Kem.Kyber.Types.t_KyberPublicKey (sz 800))
       (randomness: t_Array u8 (sz 32))
-    : Core.Result.t_Result (Libcrux.Kem.Kyber.t_KyberCiphertext (sz 768) & t_Array u8 (sz 32))
-      Libcrux.Kem.Kyber.t_BadRejectionSamplingRandomnessError =
-  Libcrux.Kem.Kyber.encapsulate public_key randomness
+    : 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.encapsulate public_key randomness
 
 let decapsulate_512_
-      (secret_key: Libcrux.Kem.Kyber.t_KyberPrivateKey (sz 1632))
-      (ciphertext: Libcrux.Kem.Kyber.t_KyberCiphertext (sz 768))
+      (secret_key: Libcrux.Kem.Kyber.Types.t_KyberPrivateKey (sz 1632))
+      (ciphertext: Libcrux.Kem.Kyber.Types.t_KyberCiphertext (sz 768))
     : t_Array u8 (sz 32) = Libcrux.Kem.Kyber.decapsulate secret_key ciphertext