chore(kyber/fstar): refresh snapshot

cryspen · Jan 31, 2024 · 170777e · 170777e
1 parent a398406
commit 170777e
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 6 deletions.
diff --git a/proofs/fstar/extraction/Libcrux.Digest.fsti b/proofs/fstar/extraction/Libcrux.Digest.fsti
@@ -3,6 +3,11 @@ module Libcrux.Digest
 open Core
 open FStar.Mul
 
+val shake128x4_256_ (v_LEN: usize) (data0 data1 data2 data3: t_Slice u8)
+    : Prims.Pure (t_Array u8 v_LEN & t_Array u8 v_LEN & t_Array u8 v_LEN & t_Array u8 v_LEN)
+      Prims.l_True
+      (fun _ -> Prims.l_True)
+
 val sha3_256_ (payload: t_Slice u8)
     : Prims.Pure (t_Array u8 (sz 32)) Prims.l_True (fun _ -> Prims.l_True)
 
@@ -20,11 +25,6 @@ val shake128x4_portable (v_LEN: usize) (data0 data1 data2 data3: t_Slice u8)
       Prims.l_True
       (fun _ -> Prims.l_True)
 
-val shake128x4_256_ (v_LEN: usize) (data0 data1 data2 data3: t_Slice u8)
-    : Prims.Pure (t_Array u8 v_LEN & t_Array u8 v_LEN & t_Array u8 v_LEN & t_Array u8 v_LEN)
-      Prims.l_True
-      (fun _ -> Prims.l_True)
-
 val shake128x4 (v_LEN: usize) (data0 data1 data2 data3: t_Slice u8)
     : Prims.Pure (t_Array u8 v_LEN & t_Array u8 v_LEN & t_Array u8 v_LEN & t_Array u8 v_LEN)
       Prims.l_True

diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Hash_functions.fst b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Hash_functions.fst
@@ -14,7 +14,7 @@ let v_XOFx4 (v_K: usize) (input: t_Array (t_Array u8 (sz 34)) v_K) =
     Rust_primitives.Hax.repeat (Rust_primitives.Hax.repeat 0uy (sz 840) <: t_Array u8 (sz 840)) v_K
   in
   let out:t_Array (t_Array u8 (sz 840)) v_K =
-    if ~.(Libcrux_platform.simd256_support () <: bool) || ~.false
+    if ~.(Libcrux_platform.simd256_support () <: bool) || ~.true
     then
       Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
                 Core.Ops.Range.f_start = sz 0;