udpate hax extraction

cryspen · Dec 3, 2024 · ebd9959 · ebd9959
1 parent d972def
commit ebd9959
Show file tree

Hide file tree

Showing 37 changed files with 1,453 additions and 2,215 deletions.
diff --git a/libcrux-ml-dsa/hax.py b/libcrux-ml-dsa/hax.py
@@ -85,6 +85,7 @@ def __call__(self, parser, args, values, option_string=None) -> None:
             "-libcrux_ml_dsa::hash_functions::simd256::*",
             "-libcrux_ml_dsa::hash_functions::neon::*",
             "+:libcrux_ml_dsa::hash_functions::*::*",
+            "-**::types::non_hax_impls::**",
         ]
         include_str = " ".join(includes)
         interface_include = "+**"

diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Signature.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Signature.fst
@@ -198,13 +198,12 @@ let impl__deserialize
       <:
       Libcrux_ml_dsa.Types.t_VerificationError)
     <:
-    Core.Result.t_Result
-      (Libcrux_ml_dsa.Types.t_Signature v_SIMDUnit v_COMMITMENT_HASH_SIZE v_COLUMNS_IN_A v_ROWS_IN_A
-      ) Libcrux_ml_dsa.Types.t_VerificationError
+    Core.Result.t_Result (t_Signature v_SIMDUnit v_COMMITMENT_HASH_SIZE v_COLUMNS_IN_A v_ROWS_IN_A)
+      Libcrux_ml_dsa.Types.t_VerificationError
   else
     Core.Result.Result_Ok
     ({
-        Libcrux_ml_dsa.Types.f_commitment_hash
+        f_commitment_hash
         =
         Core.Result.impl__unwrap #(t_Array u8 v_COMMITMENT_HASH_SIZE)
           #Core.Array.t_TryFromSliceError
@@ -214,15 +213,14 @@ let impl__deserialize
               commitment_hash
             <:
             Core.Result.t_Result (t_Array u8 v_COMMITMENT_HASH_SIZE) Core.Array.t_TryFromSliceError);
-        Libcrux_ml_dsa.Types.f_signer_response = signer_response;
-        Libcrux_ml_dsa.Types.f_hint = hint
+        f_signer_response = signer_response;
+        f_hint = hint
       }
       <:
-      Libcrux_ml_dsa.Types.t_Signature v_SIMDUnit v_COMMITMENT_HASH_SIZE v_COLUMNS_IN_A v_ROWS_IN_A)
+      t_Signature v_SIMDUnit v_COMMITMENT_HASH_SIZE v_COLUMNS_IN_A v_ROWS_IN_A)
     <:
-    Core.Result.t_Result
-      (Libcrux_ml_dsa.Types.t_Signature v_SIMDUnit v_COMMITMENT_HASH_SIZE v_COLUMNS_IN_A v_ROWS_IN_A
-      ) Libcrux_ml_dsa.Types.t_VerificationError
+    Core.Result.t_Result (t_Signature v_SIMDUnit v_COMMITMENT_HASH_SIZE v_COLUMNS_IN_A v_ROWS_IN_A)
+      Libcrux_ml_dsa.Types.t_VerificationError
 
 let impl__serialize
       (#v_SIMDUnit: Type0)
@@ -231,11 +229,7 @@ let impl__serialize
       (#[FStar.Tactics.Typeclasses.tcresolve ()]
           i1:
           Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit)
-      (self:
-          Libcrux_ml_dsa.Types.t_Signature v_SIMDUnit
-            v_COMMITMENT_HASH_SIZE
-            v_COLUMNS_IN_A
-            v_ROWS_IN_A)
+      (self: t_Signature v_SIMDUnit v_COMMITMENT_HASH_SIZE v_COLUMNS_IN_A v_ROWS_IN_A)
      =
   let signature:t_Array u8 v_SIGNATURE_SIZE = Rust_primitives.Hax.repeat 0uy v_SIGNATURE_SIZE in
   let offset:usize = sz 0 in
@@ -256,7 +250,7 @@ let impl__serialize
               Core.Ops.Range.t_Range usize ]
             <:
             t_Slice u8)
-          (self.Libcrux_ml_dsa.Types.f_commitment_hash <: t_Slice u8)
+          (self.f_commitment_hash <: t_Slice u8)
         <:
         t_Slice u8)
   in
@@ -292,7 +286,7 @@ let impl__serialize
                   (Libcrux_ml_dsa.Encoding.Gamma1.serialize #v_SIMDUnit
                       v_GAMMA1_EXPONENT
                       v_GAMMA1_RING_ELEMENT_SIZE
-                      (self.Libcrux_ml_dsa.Types.f_signer_response.[ i ]
+                      (self.f_signer_response.[ i ]
                         <:
                         Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)
                     <:
@@ -316,18 +310,17 @@ let impl__serialize
           let signature, true_hints_seen:(t_Array u8 v_SIGNATURE_SIZE & usize) = temp_0_ in
           let i:usize = i in
           let signature, true_hints_seen:(t_Array u8 v_SIGNATURE_SIZE & usize) =
-            Rust_primitives.Hax.Folds.fold_enumerated_slice (self.Libcrux_ml_dsa.Types.f_hint.[ i ]
-                <:
-                t_Array i32 (sz 256))
+            Rust_primitives.Hax.Folds.fold_range (sz 0)
+              (Core.Slice.impl__len #i32 (self.f_hint.[ i ] <: t_Slice i32) <: usize)
               (fun temp_0_ temp_1_ ->
                   let signature, true_hints_seen:(t_Array u8 v_SIGNATURE_SIZE & usize) = temp_0_ in
                   let _:usize = temp_1_ in
                   true)
               (signature, true_hints_seen <: (t_Array u8 v_SIGNATURE_SIZE & usize))
-              (fun temp_0_ temp_1_ ->
+              (fun temp_0_ j ->
                   let signature, true_hints_seen:(t_Array u8 v_SIGNATURE_SIZE & usize) = temp_0_ in
-                  let j, hint:(usize & i32) = temp_1_ in
-                  if hint =. 1l <: bool
+                  let j:usize = j in
+                  if ((self.f_hint.[ i ] <: t_Array i32 (sz 256)).[ j ] <: i32) =. 1l <: bool
                   then
                     let signature:t_Array u8 v_SIGNATURE_SIZE =
                       Rust_primitives.Hax.Monomorphized_update_at.update_at_usize signature

diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Signature.fsti b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Signature.fsti
@@ -9,6 +9,18 @@ let _ =
   let open Libcrux_ml_dsa.Simd.Traits in
   ()
 
+/// A signature
+/// This is only an internal type.
+type t_Signature
+  (v_SIMDUnit: Type0) (v_COMMITMENT_HASH_SIZE: usize) (v_COLUMNS_IN_A: usize) (v_ROWS_IN_A: usize)
+  {| i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |}
+  = {
+  f_commitment_hash:t_Array u8 v_COMMITMENT_HASH_SIZE;
+  f_signer_response:t_Array (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)
+    v_COLUMNS_IN_A;
+  f_hint:t_Array (t_Array i32 (sz 256)) v_ROWS_IN_A
+}
+
 val impl__deserialize
       (#v_SIMDUnit: Type0)
       (v_COMMITMENT_HASH_SIZE v_COLUMNS_IN_A v_ROWS_IN_A v_GAMMA1_EXPONENT v_GAMMA1_RING_ELEMENT_SIZE v_MAX_ONES_IN_HINT v_SIGNATURE_SIZE:
@@ -17,21 +29,13 @@ val impl__deserialize
       (serialized: t_Array u8 v_SIGNATURE_SIZE)
     : Prims.Pure
       (Core.Result.t_Result
-          (Libcrux_ml_dsa.Types.t_Signature v_SIMDUnit
-              v_COMMITMENT_HASH_SIZE
-              v_COLUMNS_IN_A
-              v_ROWS_IN_A) Libcrux_ml_dsa.Types.t_VerificationError)
-      Prims.l_True
-      (fun _ -> Prims.l_True)
+          (t_Signature v_SIMDUnit v_COMMITMENT_HASH_SIZE v_COLUMNS_IN_A v_ROWS_IN_A)
+          Libcrux_ml_dsa.Types.t_VerificationError) Prims.l_True (fun _ -> Prims.l_True)
 
 val impl__serialize
       (#v_SIMDUnit: Type0)
       (v_COMMITMENT_HASH_SIZE v_COLUMNS_IN_A v_ROWS_IN_A v_GAMMA1_EXPONENT v_GAMMA1_RING_ELEMENT_SIZE v_MAX_ONES_IN_HINT v_SIGNATURE_SIZE:
           usize)
       {| i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |}
-      (self:
-          Libcrux_ml_dsa.Types.t_Signature v_SIMDUnit
-            v_COMMITMENT_HASH_SIZE
-            v_COLUMNS_IN_A
-            v_ROWS_IN_A)
+      (self: t_Signature v_SIMDUnit v_COMMITMENT_HASH_SIZE v_COLUMNS_IN_A v_ROWS_IN_A)
     : Prims.Pure (t_Array u8 v_SIGNATURE_SIZE) Prims.l_True (fun _ -> Prims.l_True)
diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Hash_functions.Neon.fsti b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Hash_functions.Neon.fsti
@@ -8,6 +8,12 @@ val t_Shake128x4:Type0
 /// Neon SHAKE 256 x4 state
 val t_Shake256x4:Type0
 
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+val impl:Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 t_Shake128x4
+
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+val impl_1:Libcrux_ml_dsa.Hash_functions.Shake256.t_XofX4 t_Shake256x4
+
 /// Init the state and absorb 4 blocks in parallel.
 val init_absorb (input0 input1 input2 input3: t_Slice u8)
     : Prims.Pure t_Shake128x4 Prims.l_True (fun _ -> Prims.l_True)
@@ -43,239 +49,9 @@ val squeeze_next_block (state: t_Shake128x4)
       Prims.l_True
       (fun _ -> Prims.l_True)
 
-[@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl: Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 t_Shake128x4 =
-  {
-    f_init_absorb_pre
-    =
-    (fun (input0: t_Slice u8) (input1: t_Slice u8) (input2: t_Slice u8) (input3: t_Slice u8) -> true
-    );
-    f_init_absorb_post
-    =
-    (fun
-        (input0: t_Slice u8)
-        (input1: t_Slice u8)
-        (input2: t_Slice u8)
-        (input3: t_Slice u8)
-        (out: t_Shake128x4)
-        ->
-        true);
-    f_init_absorb
-    =
-    (fun (input0: t_Slice u8) (input1: t_Slice u8) (input2: t_Slice u8) (input3: t_Slice u8) ->
-        init_absorb input0 input1 input2 input3);
-    f_squeeze_first_five_blocks_pre
-    =
-    (fun
-        (self: t_Shake128x4)
-        (out0: t_Array u8 (sz 840))
-        (out1: t_Array u8 (sz 840))
-        (out2: t_Array u8 (sz 840))
-        (out3: t_Array u8 (sz 840))
-        ->
-        true);
-    f_squeeze_first_five_blocks_post
-    =
-    (fun
-        (self: t_Shake128x4)
-        (out0: t_Array u8 (sz 840))
-        (out1: t_Array u8 (sz 840))
-        (out2: t_Array u8 (sz 840))
-        (out3: t_Array u8 (sz 840))
-        (out4:
-          (t_Shake128x4 & t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840) &
-            t_Array u8 (sz 840)))
-        ->
-        true);
-    f_squeeze_first_five_blocks
-    =
-    (fun
-        (self: t_Shake128x4)
-        (out0: t_Array u8 (sz 840))
-        (out1: t_Array u8 (sz 840))
-        (out2: t_Array u8 (sz 840))
-        (out3: t_Array u8 (sz 840))
-        ->
-        let tmp0, tmp1, tmp2, tmp3, tmp4:(t_Shake128x4 & t_Array u8 (sz 840) & t_Array u8 (sz 840) &
-          t_Array u8 (sz 840) &
-          t_Array u8 (sz 840)) =
-          squeeze_first_five_blocks self out0 out1 out2 out3
-        in
-        let self:t_Shake128x4 = tmp0 in
-        let out0:t_Array u8 (sz 840) = tmp1 in
-        let out1:t_Array u8 (sz 840) = tmp2 in
-        let out2:t_Array u8 (sz 840) = tmp3 in
-        let out3:t_Array u8 (sz 840) = tmp4 in
-        let _:Prims.unit = () in
-        self, out0, out1, out2, out3
-        <:
-        (t_Shake128x4 & t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840) &
-          t_Array u8 (sz 840)));
-    f_squeeze_next_block_pre = (fun (self: t_Shake128x4) -> true);
-    f_squeeze_next_block_post
-    =
-    (fun
-        (self: t_Shake128x4)
-        (out5:
-          (t_Shake128x4 &
-            (t_Array u8 (sz 168) & t_Array u8 (sz 168) & t_Array u8 (sz 168) & t_Array u8 (sz 168)))
-        )
-        ->
-        true);
-    f_squeeze_next_block
-    =
-    fun (self: t_Shake128x4) ->
-      let tmp0, out4:(t_Shake128x4 &
-        (t_Array u8 (sz 168) & t_Array u8 (sz 168) & t_Array u8 (sz 168) & t_Array u8 (sz 168))) =
-        squeeze_next_block self
-      in
-      let self:t_Shake128x4 = tmp0 in
-      let hax_temp_output:(t_Array u8 (sz 168) & t_Array u8 (sz 168) & t_Array u8 (sz 168) &
-        t_Array u8 (sz 168)) =
-        out4
-      in
-      self, hax_temp_output
-      <:
-      (t_Shake128x4 &
-        (t_Array u8 (sz 168) & t_Array u8 (sz 168) & t_Array u8 (sz 168) & t_Array u8 (sz 168)))
-  }
-
 val squeeze_next_block_x4 (state: t_Shake256x4)
     : Prims.Pure
       (t_Shake256x4 &
         (t_Array u8 (sz 136) & t_Array u8 (sz 136) & t_Array u8 (sz 136) & t_Array u8 (sz 136)))
       Prims.l_True
       (fun _ -> Prims.l_True)
-
-[@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_1: Libcrux_ml_dsa.Hash_functions.Shake256.t_XofX4 t_Shake256x4 =
-  {
-    f_init_absorb_x4_pre
-    =
-    (fun (input0: t_Slice u8) (input1: t_Slice u8) (input2: t_Slice u8) (input3: t_Slice u8) -> true
-    );
-    f_init_absorb_x4_post
-    =
-    (fun
-        (input0: t_Slice u8)
-        (input1: t_Slice u8)
-        (input2: t_Slice u8)
-        (input3: t_Slice u8)
-        (out: t_Shake256x4)
-        ->
-        true);
-    f_init_absorb_x4
-    =
-    (fun (input0: t_Slice u8) (input1: t_Slice u8) (input2: t_Slice u8) (input3: t_Slice u8) ->
-        init_absorb_x4 input0 input1 input2 input3);
-    f_squeeze_first_block_x4_pre = (fun (self: t_Shake256x4) -> true);
-    f_squeeze_first_block_x4_post
-    =
-    (fun
-        (self: t_Shake256x4)
-        (out5:
-          (t_Shake256x4 &
-            (t_Array u8 (sz 136) & t_Array u8 (sz 136) & t_Array u8 (sz 136) & t_Array u8 (sz 136)))
-        )
-        ->
-        true);
-    f_squeeze_first_block_x4
-    =
-    (fun (self: t_Shake256x4) ->
-        let tmp0, out4:(t_Shake256x4 &
-          (t_Array u8 (sz 136) & t_Array u8 (sz 136) & t_Array u8 (sz 136) & t_Array u8 (sz 136))) =
-          squeeze_first_block_x4 self
-        in
-        let self:t_Shake256x4 = tmp0 in
-        let hax_temp_output:(t_Array u8 (sz 136) & t_Array u8 (sz 136) & t_Array u8 (sz 136) &
-          t_Array u8 (sz 136)) =
-          out4
-        in
-        self, hax_temp_output
-        <:
-        (t_Shake256x4 &
-          (t_Array u8 (sz 136) & t_Array u8 (sz 136) & t_Array u8 (sz 136) & t_Array u8 (sz 136))));
-    f_squeeze_next_block_x4_pre = (fun (self: t_Shake256x4) -> true);
-    f_squeeze_next_block_x4_post
-    =
-    (fun
-        (self: t_Shake256x4)
-        (out5:
-          (t_Shake256x4 &
-            (t_Array u8 (sz 136) & t_Array u8 (sz 136) & t_Array u8 (sz 136) & t_Array u8 (sz 136)))
-        )
-        ->
-        true);
-    f_squeeze_next_block_x4
-    =
-    (fun (self: t_Shake256x4) ->
-        let tmp0, out4:(t_Shake256x4 &
-          (t_Array u8 (sz 136) & t_Array u8 (sz 136) & t_Array u8 (sz 136) & t_Array u8 (sz 136))) =
-          squeeze_next_block_x4 self
-        in
-        let self:t_Shake256x4 = tmp0 in
-        let hax_temp_output:(t_Array u8 (sz 136) & t_Array u8 (sz 136) & t_Array u8 (sz 136) &
-          t_Array u8 (sz 136)) =
-          out4
-        in
-        self, hax_temp_output
-        <:
-        (t_Shake256x4 &
-          (t_Array u8 (sz 136) & t_Array u8 (sz 136) & t_Array u8 (sz 136) & t_Array u8 (sz 136))));
-    f_shake256_x4_pre
-    =
-    (fun
-        (v_OUT_LEN: usize)
-        (input0: t_Slice u8)
-        (input1: t_Slice u8)
-        (input2: t_Slice u8)
-        (input3: t_Slice u8)
-        (out0: t_Array u8 v_OUT_LEN)
-        (out1: t_Array u8 v_OUT_LEN)
-        (out2: t_Array u8 v_OUT_LEN)
-        (out3: t_Array u8 v_OUT_LEN)
-        ->
-        true);
-    f_shake256_x4_post
-    =
-    (fun
-        (v_OUT_LEN: usize)
-        (input0: t_Slice u8)
-        (input1: t_Slice u8)
-        (input2: t_Slice u8)
-        (input3: t_Slice u8)
-        (out0: t_Array u8 v_OUT_LEN)
-        (out1: t_Array u8 v_OUT_LEN)
-        (out2: t_Array u8 v_OUT_LEN)
-        (out3: t_Array u8 v_OUT_LEN)
-        (out4:
-          (t_Array u8 v_OUT_LEN & t_Array u8 v_OUT_LEN & t_Array u8 v_OUT_LEN & t_Array u8 v_OUT_LEN
-          ))
-        ->
-        true);
-    f_shake256_x4
-    =
-    fun
-      (v_OUT_LEN: usize)
-      (input0: t_Slice u8)
-      (input1: t_Slice u8)
-      (input2: t_Slice u8)
-      (input3: t_Slice u8)
-      (out0: t_Array u8 v_OUT_LEN)
-      (out1: t_Array u8 v_OUT_LEN)
-      (out2: t_Array u8 v_OUT_LEN)
-      (out3: t_Array u8 v_OUT_LEN)
-      ->
-      let tmp0, tmp1, tmp2, tmp3:(t_Array u8 v_OUT_LEN & t_Array u8 v_OUT_LEN & t_Array u8 v_OUT_LEN &
-        t_Array u8 v_OUT_LEN) =
-        shake256_x4 v_OUT_LEN input0 input1 input2 input3 out0 out1 out2 out3
-      in
-      let out0:t_Array u8 v_OUT_LEN = tmp0 in
-      let out1:t_Array u8 v_OUT_LEN = tmp1 in
-      let out2:t_Array u8 v_OUT_LEN = tmp2 in
-      let out3:t_Array u8 v_OUT_LEN = tmp3 in
-      let _:Prims.unit = () in
-      out0, out1, out2, out3
-      <:
-      (t_Array u8 v_OUT_LEN & t_Array u8 v_OUT_LEN & t_Array u8 v_OUT_LEN & t_Array u8 v_OUT_LEN)
-  }