Merge pull request #195 from cryspen/lucas/fix-kyber-extraction

Kyber: hax: fix extraction
cryspen · Jan 31, 2024 · 9794fff · 9794fff
2 parents 4f8e208 + 170777e
commit 9794fff
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 7 deletions.
diff --git 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::**",

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;