From a398406be1c35f6a66a215ae68234932aa8faf1c Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Wed, 31 Jan 2024 07:53:54 +0100 Subject: [PATCH 1/2] fix(kyber/hax): exclude `libcrux_platform` submodules --- hax-driver.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/hax-driver.py b/hax-driver.py index 7ea434ed0..a9a5a8d3d 100755 --- a/hax-driver.py +++ b/hax-driver.py @@ -124,7 +124,7 @@ def shell(command, expect=0, cwd=None, env={}): "-C", "-p", "libcrux", "-p", "libcrux-platform", ";", "into", "-i", - f"-** +libcrux::kem::kyber::** +libcrux_platform::** {exclude_sha3_implementations} -libcrux::**::types::index_impls::**", + f"-** +libcrux::kem::kyber::** +!libcrux_platform::* {exclude_sha3_implementations} -libcrux::**::types::index_impls::**", "fstar", "--interfaces", "+* -libcrux::kem::kyber::types +!libcrux_platform::**", From 170777ed6ef37621ab271a35874e9a9d2190e274 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Wed, 31 Jan 2024 07:54:08 +0100 Subject: [PATCH 2/2] 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;