Update hax extraction

cryspen · Dec 18, 2024 · a9714a4 · a9714a4
1 parent 95c30a2
commit a9714a4
Show file tree

Hide file tree

Showing 38 changed files with 2,063 additions and 1,830 deletions.
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
@@ -14,7 +14,7 @@ let impl__deserialize
       (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)
       (#[FStar.Tactics.Typeclasses.tcresolve ()]
-          i2:
+          i1:
           Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit)
       (serialized: t_Array u8 v_SIGNATURE_SIZE)
      =

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
@@ -25,7 +25,7 @@ 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:
           usize)
-      {| i2: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |}
+      {| i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |}
       (serialized: t_Array u8 v_SIGNATURE_SIZE)
     : Prims.Pure
       (Core.Result.t_Result

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
@@ -3,10 +3,10 @@ module Libcrux_ml_dsa.Hash_functions.Neon
 open Core
 open FStar.Mul
 
-val t_Shake128x4:Type0
+val t_Shake128x4:eqtype
 
 /// Neon SHAKE 256 x4 state
-val t_Shake256x4:Type0
+val t_Shake256x4:eqtype
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 val impl:Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 t_Shake128x4

diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Hash_functions.Portable.fsti b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Hash_functions.Portable.fsti
@@ -4,20 +4,20 @@ open Core
 open FStar.Mul
 
 /// Portable SHAKE 128 state
-val t_Shake128:Type0
+val t_Shake128:eqtype
 
 /// Portable SHAKE 128 x4 state.
 /// We\'re using a portable implementation so this is actually sequential.
-val t_Shake128X4:Type0
+val t_Shake128X4:eqtype
 
 /// Portable SHAKE 256 state
-val t_Shake256:Type0
+val t_Shake256:eqtype
 
 /// Portable SHAKE 256 x4 state.
 /// We\'re using a portable implementation so this is actually sequential.
-val t_Shake256X4:Type0
+val t_Shake256X4:eqtype
 
-val t_Shake256Xof:Type0
+val t_Shake256Xof:eqtype
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 val impl:Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 t_Shake128X4

diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Hash_functions.Simd256.fsti b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Hash_functions.Simd256.fsti
@@ -6,13 +6,13 @@ open FStar.Mul
 /// AVX2 SHAKE 128 state
 /// This only implements the XofX4 API. For the single Xof, the portable
 /// version is used.
-val t_Shake128x4:Type0
-
-/// AVX2 SHAKE 256 x4 state.
-val t_Shake256x4:Type0
+val t_Shake128x4:eqtype
 
 /// AVX2 SHAKE 256 state
-val t_Shake256:Type0
+val t_Shake256:eqtype
+
+/// AVX2 SHAKE 256 x4 state.
+val t_Shake256x4:eqtype
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 val impl:Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 t_Shake128x4

diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_44_.Avx2.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_44_.Avx2.fst
@@ -29,7 +29,7 @@ let sign
      =
   Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.sign (sz 4) (sz 4) (sz 2) (sz 96) (sz 17) 95232l
     (sz 192) (sz 768) (sz 32) (sz 39) (sz 80) (sz 576) (sz 2560) (sz 2420)
-    (Libcrux_ml_dsa.Types.impl__as_raw (sz 2560) signing_key <: t_Array u8 (sz 2560)) message
+    (Libcrux_ml_dsa.Types.impl__as_ref (sz 2560) signing_key <: t_Array u8 (sz 2560)) message
     context randomness
 
 let sign_pre_hashed_shake128
@@ -39,7 +39,7 @@ let sign_pre_hashed_shake128
      =
   Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.sign_pre_hashed_shake128 (sz 4) (sz 4) (sz 2)
     (sz 96) (sz 17) 95232l (sz 192) (sz 768) (sz 32) (sz 39) (sz 80) (sz 576) (sz 2560) (sz 2420)
-    (Libcrux_ml_dsa.Types.impl__as_raw (sz 2560) signing_key <: t_Array u8 (sz 2560)) message
+    (Libcrux_ml_dsa.Types.impl__as_ref (sz 2560) signing_key <: t_Array u8 (sz 2560)) message
     context randomness
 
 let verify
@@ -49,8 +49,8 @@ let verify
      =
   Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.verify (sz 4) (sz 4) (sz 2420) (sz 1312) (sz 17)
     (sz 576) 95232l 78l (sz 192) (sz 768) (sz 32) (sz 39) (sz 80)
-    (Libcrux_ml_dsa.Types.impl_2__as_raw (sz 1312) verification_key <: t_Array u8 (sz 1312)) message
-    context (Libcrux_ml_dsa.Types.impl_4__as_raw (sz 2420) signature <: t_Array u8 (sz 2420))
+    (Libcrux_ml_dsa.Types.impl_2__as_ref (sz 1312) verification_key <: t_Array u8 (sz 1312)) message
+    context (Libcrux_ml_dsa.Types.impl_4__as_ref (sz 2420) signature <: t_Array u8 (sz 2420))
 
 let verify_pre_hashed_shake128
       (verification_key: Libcrux_ml_dsa.Types.t_MLDSAVerificationKey (sz 1312))
@@ -59,5 +59,5 @@ let verify_pre_hashed_shake128
      =
   Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.verify_pre_hashed_shake128 (sz 4) (sz 4)
     (sz 2420) (sz 1312) (sz 17) (sz 576) 95232l 78l (sz 192) (sz 768) (sz 32) (sz 39) (sz 80)
-    (Libcrux_ml_dsa.Types.impl_2__as_raw (sz 1312) verification_key <: t_Array u8 (sz 1312)) message
-    context (Libcrux_ml_dsa.Types.impl_4__as_raw (sz 2420) signature <: t_Array u8 (sz 2420))
+    (Libcrux_ml_dsa.Types.impl_2__as_ref (sz 1312) verification_key <: t_Array u8 (sz 1312)) message
+    context (Libcrux_ml_dsa.Types.impl_4__as_ref (sz 2420) signature <: t_Array u8 (sz 2420))
diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_44_.Neon.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_44_.Neon.fst
@@ -29,7 +29,7 @@ let sign
      =
   Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.sign (sz 4) (sz 4) (sz 2) (sz 96) (sz 17) 95232l
     (sz 192) (sz 768) (sz 32) (sz 39) (sz 80) (sz 576) (sz 2560) (sz 2420)
-    (Libcrux_ml_dsa.Types.impl__as_raw (sz 2560) signing_key <: t_Array u8 (sz 2560)) message
+    (Libcrux_ml_dsa.Types.impl__as_ref (sz 2560) signing_key <: t_Array u8 (sz 2560)) message
     context randomness
 
 let sign_pre_hashed_shake128
@@ -39,7 +39,7 @@ let sign_pre_hashed_shake128
      =
   Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.sign_pre_hashed_shake128 (sz 4) (sz 4) (sz 2)
     (sz 96) (sz 17) 95232l (sz 192) (sz 768) (sz 32) (sz 39) (sz 80) (sz 576) (sz 2560) (sz 2420)
-    (Libcrux_ml_dsa.Types.impl__as_raw (sz 2560) signing_key <: t_Array u8 (sz 2560)) message
+    (Libcrux_ml_dsa.Types.impl__as_ref (sz 2560) signing_key <: t_Array u8 (sz 2560)) message
     context randomness
 
 let verify
@@ -49,8 +49,8 @@ let verify
      =
   Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.verify (sz 4) (sz 4) (sz 2420) (sz 1312) (sz 17)
     (sz 576) 95232l 78l (sz 192) (sz 768) (sz 32) (sz 39) (sz 80)
-    (Libcrux_ml_dsa.Types.impl_2__as_raw (sz 1312) verification_key <: t_Array u8 (sz 1312)) message
-    context (Libcrux_ml_dsa.Types.impl_4__as_raw (sz 2420) signature <: t_Array u8 (sz 2420))
+    (Libcrux_ml_dsa.Types.impl_2__as_ref (sz 1312) verification_key <: t_Array u8 (sz 1312)) message
+    context (Libcrux_ml_dsa.Types.impl_4__as_ref (sz 2420) signature <: t_Array u8 (sz 2420))
 
 let verify_pre_hashed_shake128
       (verification_key: Libcrux_ml_dsa.Types.t_MLDSAVerificationKey (sz 1312))
@@ -59,5 +59,5 @@ let verify_pre_hashed_shake128
      =
   Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.verify_pre_hashed_shake128 (sz 4) (sz 4)
     (sz 2420) (sz 1312) (sz 17) (sz 576) 95232l 78l (sz 192) (sz 768) (sz 32) (sz 39) (sz 80)
-    (Libcrux_ml_dsa.Types.impl_2__as_raw (sz 1312) verification_key <: t_Array u8 (sz 1312)) message
-    context (Libcrux_ml_dsa.Types.impl_4__as_raw (sz 2420) signature <: t_Array u8 (sz 2420))
+    (Libcrux_ml_dsa.Types.impl_2__as_ref (sz 1312) verification_key <: t_Array u8 (sz 1312)) message
+    context (Libcrux_ml_dsa.Types.impl_4__as_ref (sz 2420) signature <: t_Array u8 (sz 2420))
diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_44_.Portable.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_44_.Portable.fst
@@ -29,7 +29,7 @@ let sign
      =
   Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.sign (sz 4) (sz 4) (sz 2) (sz 96) (sz 17)
     95232l (sz 192) (sz 768) (sz 32) (sz 39) (sz 80) (sz 576) (sz 2560) (sz 2420)
-    (Libcrux_ml_dsa.Types.impl__as_raw (sz 2560) signing_key <: t_Array u8 (sz 2560)) message
+    (Libcrux_ml_dsa.Types.impl__as_ref (sz 2560) signing_key <: t_Array u8 (sz 2560)) message
     context randomness
 
 let sign_pre_hashed_shake128
@@ -39,7 +39,7 @@ let sign_pre_hashed_shake128
      =
   Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.sign_pre_hashed_shake128 (sz 4) (sz 4)
     (sz 2) (sz 96) (sz 17) 95232l (sz 192) (sz 768) (sz 32) (sz 39) (sz 80) (sz 576) (sz 2560)
-    (sz 2420) (Libcrux_ml_dsa.Types.impl__as_raw (sz 2560) signing_key <: t_Array u8 (sz 2560))
+    (sz 2420) (Libcrux_ml_dsa.Types.impl__as_ref (sz 2560) signing_key <: t_Array u8 (sz 2560))
     message context randomness
 
 let verify
@@ -49,8 +49,8 @@ let verify
      =
   Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.verify (sz 4) (sz 4) (sz 2420) (sz 1312)
     (sz 17) (sz 576) 95232l 78l (sz 192) (sz 768) (sz 32) (sz 39) (sz 80)
-    (Libcrux_ml_dsa.Types.impl_2__as_raw (sz 1312) verification_key <: t_Array u8 (sz 1312)) message
-    context (Libcrux_ml_dsa.Types.impl_4__as_raw (sz 2420) signature <: t_Array u8 (sz 2420))
+    (Libcrux_ml_dsa.Types.impl_2__as_ref (sz 1312) verification_key <: t_Array u8 (sz 1312)) message
+    context (Libcrux_ml_dsa.Types.impl_4__as_ref (sz 2420) signature <: t_Array u8 (sz 2420))
 
 let verify_pre_hashed_shake128
       (verification_key: Libcrux_ml_dsa.Types.t_MLDSAVerificationKey (sz 1312))
@@ -59,5 +59,5 @@ let verify_pre_hashed_shake128
      =
   Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.verify_pre_hashed_shake128 (sz 4) (sz 4)
     (sz 2420) (sz 1312) (sz 17) (sz 576) 95232l 78l (sz 192) (sz 768) (sz 32) (sz 39) (sz 80)
-    (Libcrux_ml_dsa.Types.impl_2__as_raw (sz 1312) verification_key <: t_Array u8 (sz 1312)) message
-    context (Libcrux_ml_dsa.Types.impl_4__as_raw (sz 2420) signature <: t_Array u8 (sz 2420))
+    (Libcrux_ml_dsa.Types.impl_2__as_ref (sz 1312) verification_key <: t_Array u8 (sz 1312)) message
+    context (Libcrux_ml_dsa.Types.impl_4__as_ref (sz 2420) signature <: t_Array u8 (sz 2420))
diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_44_.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_44_.fst
@@ -29,7 +29,7 @@ let sign
      =
   Libcrux_ml_dsa.Ml_dsa_generic.Multiplexing.sign (sz 4) (sz 4) (sz 2) (sz 96) (sz 17) 95232l
     (sz 192) (sz 768) (sz 32) (sz 39) (sz 80) (sz 576) (sz 2560) (sz 2420)
-    (Libcrux_ml_dsa.Types.impl__as_raw (sz 2560) signing_key <: t_Array u8 (sz 2560)) message
+    (Libcrux_ml_dsa.Types.impl__as_ref (sz 2560) signing_key <: t_Array u8 (sz 2560)) message
     context randomness
 
 let sign_pre_hashed_shake128
@@ -39,7 +39,7 @@ let sign_pre_hashed_shake128
      =
   Libcrux_ml_dsa.Ml_dsa_generic.Multiplexing.sign_pre_hashed_shake128 (sz 4) (sz 4) (sz 2) (sz 96)
     (sz 17) 95232l (sz 192) (sz 768) (sz 32) (sz 39) (sz 80) (sz 576) (sz 2560) (sz 2420)
-    (Libcrux_ml_dsa.Types.impl__as_raw (sz 2560) signing_key <: t_Array u8 (sz 2560)) message
+    (Libcrux_ml_dsa.Types.impl__as_ref (sz 2560) signing_key <: t_Array u8 (sz 2560)) message
     context randomness
 
 let verify
@@ -49,8 +49,8 @@ let verify
      =
   Libcrux_ml_dsa.Ml_dsa_generic.Multiplexing.verify (sz 4) (sz 4) (sz 2420) (sz 1312) (sz 17)
     (sz 576) 95232l 78l (sz 192) (sz 768) (sz 32) (sz 39) (sz 80)
-    (Libcrux_ml_dsa.Types.impl_2__as_raw (sz 1312) verification_key <: t_Array u8 (sz 1312)) message
-    context (Libcrux_ml_dsa.Types.impl_4__as_raw (sz 2420) signature <: t_Array u8 (sz 2420))
+    (Libcrux_ml_dsa.Types.impl_2__as_ref (sz 1312) verification_key <: t_Array u8 (sz 1312)) message
+    context (Libcrux_ml_dsa.Types.impl_4__as_ref (sz 2420) signature <: t_Array u8 (sz 2420))
 
 let verify_pre_hashed_shake128
       (verification_key: Libcrux_ml_dsa.Types.t_MLDSAVerificationKey (sz 1312))
@@ -59,5 +59,5 @@ let verify_pre_hashed_shake128
      =
   Libcrux_ml_dsa.Ml_dsa_generic.Multiplexing.verify_pre_hashed_shake128 (sz 4) (sz 4) (sz 2420)
     (sz 1312) (sz 17) (sz 576) 95232l 78l (sz 192) (sz 768) (sz 32) (sz 39) (sz 80)
-    (Libcrux_ml_dsa.Types.impl_2__as_raw (sz 1312) verification_key <: t_Array u8 (sz 1312)) message
-    context (Libcrux_ml_dsa.Types.impl_4__as_raw (sz 2420) signature <: t_Array u8 (sz 2420))
+    (Libcrux_ml_dsa.Types.impl_2__as_ref (sz 1312) verification_key <: t_Array u8 (sz 1312)) message
+    context (Libcrux_ml_dsa.Types.impl_4__as_ref (sz 2420) signature <: t_Array u8 (sz 2420))
diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_65_.Avx2.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_65_.Avx2.fst
@@ -29,7 +29,7 @@ let sign
      =
   Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.sign (sz 6) (sz 5) (sz 4) (sz 128) (sz 19)
     261888l (sz 128) (sz 768) (sz 48) (sz 49) (sz 55) (sz 640) (sz 4032) (sz 3309)
-    (Libcrux_ml_dsa.Types.impl__as_raw (sz 4032) signing_key <: t_Array u8 (sz 4032)) message
+    (Libcrux_ml_dsa.Types.impl__as_ref (sz 4032) signing_key <: t_Array u8 (sz 4032)) message
     context randomness
 
 let sign_pre_hashed_shake128
@@ -39,7 +39,7 @@ let sign_pre_hashed_shake128
      =
   Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.sign_pre_hashed_shake128 (sz 6) (sz 5) (sz 4)
     (sz 128) (sz 19) 261888l (sz 128) (sz 768) (sz 48) (sz 49) (sz 55) (sz 640) (sz 4032) (sz 3309)
-    (Libcrux_ml_dsa.Types.impl__as_raw (sz 4032) signing_key <: t_Array u8 (sz 4032)) message
+    (Libcrux_ml_dsa.Types.impl__as_ref (sz 4032) signing_key <: t_Array u8 (sz 4032)) message
     context randomness
 
 let verify
@@ -49,8 +49,8 @@ let verify
      =
   Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.verify (sz 6) (sz 5) (sz 3309) (sz 1952) (sz 19)
     (sz 640) 261888l 196l (sz 128) (sz 768) (sz 48) (sz 49) (sz 55)
-    (Libcrux_ml_dsa.Types.impl_2__as_raw (sz 1952) verification_key <: t_Array u8 (sz 1952)) message
-    context (Libcrux_ml_dsa.Types.impl_4__as_raw (sz 3309) signature <: t_Array u8 (sz 3309))
+    (Libcrux_ml_dsa.Types.impl_2__as_ref (sz 1952) verification_key <: t_Array u8 (sz 1952)) message
+    context (Libcrux_ml_dsa.Types.impl_4__as_ref (sz 3309) signature <: t_Array u8 (sz 3309))
 
 let verify_pre_hashed_shake128
       (verification_key: Libcrux_ml_dsa.Types.t_MLDSAVerificationKey (sz 1952))
@@ -59,5 +59,5 @@ let verify_pre_hashed_shake128
      =
   Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.verify_pre_hashed_shake128 (sz 6) (sz 5)
     (sz 3309) (sz 1952) (sz 19) (sz 640) 261888l 196l (sz 128) (sz 768) (sz 48) (sz 49) (sz 55)
-    (Libcrux_ml_dsa.Types.impl_2__as_raw (sz 1952) verification_key <: t_Array u8 (sz 1952)) message
-    context (Libcrux_ml_dsa.Types.impl_4__as_raw (sz 3309) signature <: t_Array u8 (sz 3309))
+    (Libcrux_ml_dsa.Types.impl_2__as_ref (sz 1952) verification_key <: t_Array u8 (sz 1952)) message
+    context (Libcrux_ml_dsa.Types.impl_4__as_ref (sz 3309) signature <: t_Array u8 (sz 3309))
diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_65_.Neon.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_65_.Neon.fst
@@ -29,7 +29,7 @@ let sign
      =
   Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.sign (sz 6) (sz 5) (sz 4) (sz 128) (sz 19)
     261888l (sz 128) (sz 768) (sz 48) (sz 49) (sz 55) (sz 640) (sz 4032) (sz 3309)
-    (Libcrux_ml_dsa.Types.impl__as_raw (sz 4032) signing_key <: t_Array u8 (sz 4032)) message
+    (Libcrux_ml_dsa.Types.impl__as_ref (sz 4032) signing_key <: t_Array u8 (sz 4032)) message
     context randomness
 
 let sign_pre_hashed_shake128
@@ -39,7 +39,7 @@ let sign_pre_hashed_shake128
      =
   Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.sign_pre_hashed_shake128 (sz 6) (sz 5) (sz 4)
     (sz 128) (sz 19) 261888l (sz 128) (sz 768) (sz 48) (sz 49) (sz 55) (sz 640) (sz 4032) (sz 3309)
-    (Libcrux_ml_dsa.Types.impl__as_raw (sz 4032) signing_key <: t_Array u8 (sz 4032)) message
+    (Libcrux_ml_dsa.Types.impl__as_ref (sz 4032) signing_key <: t_Array u8 (sz 4032)) message
     context randomness
 
 let verify
@@ -49,8 +49,8 @@ let verify
      =
   Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.verify (sz 6) (sz 5) (sz 3309) (sz 1952) (sz 19)
     (sz 640) 261888l 196l (sz 128) (sz 768) (sz 48) (sz 49) (sz 55)
-    (Libcrux_ml_dsa.Types.impl_2__as_raw (sz 1952) verification_key <: t_Array u8 (sz 1952)) message
-    context (Libcrux_ml_dsa.Types.impl_4__as_raw (sz 3309) signature <: t_Array u8 (sz 3309))
+    (Libcrux_ml_dsa.Types.impl_2__as_ref (sz 1952) verification_key <: t_Array u8 (sz 1952)) message
+    context (Libcrux_ml_dsa.Types.impl_4__as_ref (sz 3309) signature <: t_Array u8 (sz 3309))
 
 let verify_pre_hashed_shake128
       (verification_key: Libcrux_ml_dsa.Types.t_MLDSAVerificationKey (sz 1952))
@@ -59,5 +59,5 @@ let verify_pre_hashed_shake128
      =
   Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.verify_pre_hashed_shake128 (sz 6) (sz 5)
     (sz 3309) (sz 1952) (sz 19) (sz 640) 261888l 196l (sz 128) (sz 768) (sz 48) (sz 49) (sz 55)
-    (Libcrux_ml_dsa.Types.impl_2__as_raw (sz 1952) verification_key <: t_Array u8 (sz 1952)) message
-    context (Libcrux_ml_dsa.Types.impl_4__as_raw (sz 3309) signature <: t_Array u8 (sz 3309))
+    (Libcrux_ml_dsa.Types.impl_2__as_ref (sz 1952) verification_key <: t_Array u8 (sz 1952)) message
+    context (Libcrux_ml_dsa.Types.impl_4__as_ref (sz 3309) signature <: t_Array u8 (sz 3309))
diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_65_.Portable.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_65_.Portable.fst
@@ -29,7 +29,7 @@ let sign
      =
   Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.sign (sz 6) (sz 5) (sz 4) (sz 128) (sz 19)
     261888l (sz 128) (sz 768) (sz 48) (sz 49) (sz 55) (sz 640) (sz 4032) (sz 3309)
-    (Libcrux_ml_dsa.Types.impl__as_raw (sz 4032) signing_key <: t_Array u8 (sz 4032)) message
+    (Libcrux_ml_dsa.Types.impl__as_ref (sz 4032) signing_key <: t_Array u8 (sz 4032)) message
     context randomness
 
 let sign_pre_hashed_shake128
@@ -39,7 +39,7 @@ let sign_pre_hashed_shake128
      =
   Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.sign_pre_hashed_shake128 (sz 6) (sz 5)
     (sz 4) (sz 128) (sz 19) 261888l (sz 128) (sz 768) (sz 48) (sz 49) (sz 55) (sz 640) (sz 4032)
-    (sz 3309) (Libcrux_ml_dsa.Types.impl__as_raw (sz 4032) signing_key <: t_Array u8 (sz 4032))
+    (sz 3309) (Libcrux_ml_dsa.Types.impl__as_ref (sz 4032) signing_key <: t_Array u8 (sz 4032))
     message context randomness
 
 let verify
@@ -49,8 +49,8 @@ let verify
      =
   Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.verify (sz 6) (sz 5) (sz 3309) (sz 1952)
     (sz 19) (sz 640) 261888l 196l (sz 128) (sz 768) (sz 48) (sz 49) (sz 55)
-    (Libcrux_ml_dsa.Types.impl_2__as_raw (sz 1952) verification_key <: t_Array u8 (sz 1952)) message
-    context (Libcrux_ml_dsa.Types.impl_4__as_raw (sz 3309) signature <: t_Array u8 (sz 3309))
+    (Libcrux_ml_dsa.Types.impl_2__as_ref (sz 1952) verification_key <: t_Array u8 (sz 1952)) message
+    context (Libcrux_ml_dsa.Types.impl_4__as_ref (sz 3309) signature <: t_Array u8 (sz 3309))
 
 let verify_pre_hashed_shake128
       (verification_key: Libcrux_ml_dsa.Types.t_MLDSAVerificationKey (sz 1952))
@@ -59,5 +59,5 @@ let verify_pre_hashed_shake128
      =
   Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.verify_pre_hashed_shake128 (sz 6) (sz 5)
     (sz 3309) (sz 1952) (sz 19) (sz 640) 261888l 196l (sz 128) (sz 768) (sz 48) (sz 49) (sz 55)
-    (Libcrux_ml_dsa.Types.impl_2__as_raw (sz 1952) verification_key <: t_Array u8 (sz 1952)) message
-    context (Libcrux_ml_dsa.Types.impl_4__as_raw (sz 3309) signature <: t_Array u8 (sz 3309))
+    (Libcrux_ml_dsa.Types.impl_2__as_ref (sz 1952) verification_key <: t_Array u8 (sz 1952)) message
+    context (Libcrux_ml_dsa.Types.impl_4__as_ref (sz 3309) signature <: t_Array u8 (sz 3309))