From 170777ed6ef37621ab271a35874e9a9d2190e274 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Wed, 31 Jan 2024 07:54:08 +0100 Subject: [PATCH] chore(kyber/fstar): refresh snapshot --- proofs/fstar/extraction/Libcrux.Digest.fsti | 10 +++++----- .../extraction/Libcrux.Kem.Kyber.Hash_functions.fst | 2 +- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/proofs/fstar/extraction/Libcrux.Digest.fsti b/proofs/fstar/extraction/Libcrux.Digest.fsti index 59887e419..337c30672 100644 --- 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 index 7eab70b00..019708119 100644 --- 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;