gh-130213: update hacl_star_rev to 809c320227eecc61a744953f1ee574b4f24aabe3 #130960

chris-eibl · 2025-03-07T17:42:09Z

Maybe this needs its own issue?

At least the discussion started in #130332 and as an outcome @msprotz implemented hacl-star/hacl-star#1025.

This is a draft PR to integrate hacl-star/hacl-star@809c320 of his PR, since he asked about Python in hacl-star/hacl-star#1025 (comment).

I think it is better to not un-draft before I can sync from hacl-star upstream. But other than that this is ready for review.

Issue: blake2module.c needs to be compiled with libhacl SIMD flags #130213

chris-eibl · 2025-03-07T17:48:46Z

Modules/_hacl/refresh.sh

  include/krml/internal/target.h
+  include/krml/internal/types.h


I now copied types.h and put it into include/krml/internal instead of generating a "simple" one and put it into public include/krml. Also less patching of the headers needed.

@msprotz: is this ok for you?

very happy with that since it's less divergence between upstream and Python

chris-eibl · 2025-03-07T17:53:44Z

Modules/_hacl/refresh.sh

 # Adjust the include path to reflect the local directory structure
-$sed -i 's!#include.*types.h"!#include "krml/types.h"!g' "${all_files[@]}"
-$sed -i 's!#include.*compat.h"!!g' "${all_files[@]}"
+$sed -i 's!#include "fstar_uint128_msvc.h"!#include "krml/fstar_uint128_msvc.h"!g' include/krml/internal/types.h


Given the current directory layout, it seemed best to me to put these two headers from krmllib/dist/minimal into include/krml, like all the other lib_files. But then I need to patch here.

BTW: I am not a sed expert - quite the contrary. For sure this two replacements can/shall be done in one line?

I think we do not need fstar_uint128_msvc.h, see below #130960 (comment)

chris-eibl · 2025-03-07T18:00:04Z

Modules/blake2module.c

@@ -707,12 +707,12 @@ _blake2_blake2b_copy_impl(Blake2Object *self)
    switch (self->impl) {
 #if HACL_CAN_COMPILE_SIMD256
        case Blake2b_256:
-            cpy->blake2b_256_state = Hacl_Hash_Blake2b_Simd256_copy(self->blake2b_256_state);
+            cpy->blake2b_256_state = Hacl_Hash_Blake2b_Simd256_copy0(self->blake2b_256_state);


This one is interesting. I thought about copying/using dist\portable-gcc-compatible\clients\krmlrenamings.h, but there I'd only get

#define Hacl_Streaming_Blake2b_256_copy Hacl_Hash_Blake2b_Simd256_copy0

which was a too far stretch for me to replace for Hacl_Hash_Blake2b_Simd256_copy, or

#define Hacl_Hash_Blake2b_256_copy Hacl_Hash_Blake2b_Simd256_copy

which does not help, because Hacl_Hash_Blake2b_Simd256_copy does not exist.
Maybe the above line should read

#define Hacl_Hash_Blake2b_256_copy Hacl_Hash_Blake2b_Simd256_copy0

this is a bug in krmlrenamings.h let me look into this

chris-eibl · 2025-03-07T18:03:24Z

Modules/blake2module.c

            break;
 #endif
 #if HACL_CAN_COMPILE_SIMD128
        case Blake2s_128:
-            cpy->blake2s_128_state = Hacl_Hash_Blake2s_Simd128_copy(self->blake2s_128_state);
+            cpy->blake2s_128_state = Hacl_Hash_Blake2s_Simd128_copy0(self->blake2s_128_state);


Same as above.

Additionally, just to reassure I still get an error from clang-cl 18.1.8, I temporarily placed

typedef __m256i bla;

which did result in an error. So I am quite confident, that for (older) clang-cl the visibility of the intrinsincs is no longer an issue!

Thanks a lot @msprotz!

chris-eibl · 2025-03-07T18:15:01Z

Modules/_hacl/include/krml/fstar_uint128_gcc64.h

+
+#include "FStar_UInt128.h"
+#include "FStar_UInt_8_16_32_64.h"
+#include "LowStar_Endianness.h"


Here I only get a warning from clang-cl on Windows:

In file included from e:\cpython_clang\Modules\_hacl\include\krml/internal/types.h:99: e:\cpython_clang\Modules\_hacl\include\krml/fstar_uint128_gcc64.h(28,10): warning : non-portable path to file '"lowstar_endianness.h"'; specified path differs in case from file name on disk [-Wnonportable-include-path] [e:\cpython_clang \PCbuild\pythoncore.vcxproj]

The problem might be, that there are:

hacl-star\dist\karamel\krmllib\dist\minimal\LowStar_Endianness.h

hacl-star\dist\karamel\include\krml\lowstar_endianness.h

Up to now only the latter was copied. Two same names (for Windows, since case insensitive, but clang warns) in different folders. Which one is needed here? If we can change the include to lower case #include "lowstar_endianness.h", then we'd be fine.

If not, where to put the one with capital letters in the current layout and how to patch here?

Obviously, IS_MSVC64 is not defined in case of Windows, since clang-cl reports the warning in fstar_uint128_gcc64.h:

#if !defined(KRML_VERIFIED_UINT128) && defined(IS_MSVC64) #include "krml/fstar_uint128_msvc.h" #elif !defined(KRML_VERIFIED_UINT128) && defined(HAS_INT128) #include "krml/fstar_uint128_gcc64.h"

We anyway only vendored gcc-compatible and not msvc-compatible, so maybe I'll drop fstar_uint128_msvc.h"?

msvc-compatible replaces the usage of VLAs with calls to alloca for the sake of MSVC compatibility -- but for the code that you care about, there should be no such VLAs in the code, so I think we should be ok

uint128 is another, separate problem: the HACL* code assumes the existence of a certain FStar_UInt128_uint128 type, so we need to define it by hand depending on platform and toolchain... there are three options

gcc builtins for 64-bit platforms (fstar_uint128_gcc64.h)

MSVC builtins for 64-bit platforms (fstar_uint128_msvc.h)

portable C implementation, verified (FStar_UInt128_Verified.h)

I think what the previous hand-written types.h did was always pick the portable C implementation on the basis that uint128 was not used in a deep, performance-critical way, and so it was not worth the packaging burden

if you want to retain this behavior but use the same types.h as upstream, you should be able to -DKRML_VERIFIED_UINT128 and then get rid of fstar_uint128_{gcc64,msvc.h} which would simplify the packaging story and would resolve the LowStar_Endianness.h / lowstar_endianness.h issue

regarding the endianness issue, this is an original design mistake: lowercase means hand-written, and uppercase means auto-generated:

LowStar_Endianness.h contains the prototypes expected by the generated code, but no implementation

lowstar_endianness.h contains the hand-written implementation that provides those prototypes

I agree that this is definitely worth fixing, but if we can ditch fstar_uint128_gcc64.h then maybe we can push this to a separate issue

if you want to retain

I am no expert here and fully trust your expertise. Maybe others wanna chime in.
I think this PR is still flying under the radar - I just wanted to see how it goes and whether it helps you getting your PR hacl-star/hacl-star#1025 upstream.

Let me know when you think my PR is ready for others to review or who from Python should be pinged.

This currently fails due to missing make regen-sbom. I'll update and keep this PR draft. Will need another sync anyway when your PR gets upstream.

get rid of fstar_uint128_{gcc64,msvc.h}
Will definitely simplify things.

IIUC, since previously the hand written types.h did

typedef struct FStar_UInt128_uint128_s { uint64_t low; uint64_t high; } FStar_UInt128_uint128, uint128_t;

we won't be any slower and do the same as previously.
But we could be slightly faster with the special implementations.

Maybe keep that for another PR when the renamings are done?

I added commits addressing this.

Maybe keep that for another PR when the renamings are done?

This sounds excellent!

remove fstar_uint128_gcc64.h and fstar_uint128_msvc.h make regen-sbom

#include resolved using non-portable Microsoft search rules

chris-eibl · 2025-03-07T21:12:43Z

PCbuild/pythoncore.vcxproj

@@ -100,7 +100,7 @@
  <ItemDefinitionGroup>
    <ClCompile>
      <AdditionalOptions>/Zm200  %(AdditionalOptions)</AdditionalOptions>
-      <AdditionalIncludeDirectories>$(PySourcePath)Modules\_hacl\include;$(PySourcePath)Modules\_hacl\internal;$(PySourcePath)Python;%(AdditionalIncludeDirectories)</AdditionalIncludeDirectories>
+      <AdditionalIncludeDirectories>$(PySourcePath)Modules\_hacl;$(PySourcePath)Modules\_hacl\include;$(PySourcePath)Python;%(AdditionalIncludeDirectories)</AdditionalIncludeDirectories>


This is now in sync with

LIBHACL_CFLAGS=-I$(srcdir)/Modules/_hacl -I$(srcdir)/Modules/_hacl/include

for the makefile based builds and fixes the warnings

..\Modules\_hacl\internal/Hacl_Hash_Blake2b.h(38,10): warning : #include resolved using non-portable Microsoft search rules as: ..\Modules\_hacl\internal/Hacl_Streaming_Types.h [-Wmicrosoft-include] [e:\cpython_clang\PCbuild\pythoncore. vcxproj] In file included from ..\Modules\_hacl\Hacl_Hash_Blake2s.c:32: ..\Modules\_hacl\internal/Hacl_Hash_Blake2b.h(38,10): warning : #include resolved using non-portable Microsoft search rules as: ..\Modules\_hacl\internal/Hacl_Streaming_Types.h [-Wmicrosoft-include] [e:\cpython_clang\PCbuild\pythoncore. vcxproj] In file included from ..\Modules\_hacl\Hacl_Hash_Blake2b_Simd256.c:26: ..\Modules\_hacl\internal/Hacl_Hash_Blake2b_Simd256.h(39,10): warning : #include resolved using non-portable Microsoft search rules as: ..\Modules\_hacl\libintvector.h [-Wmicrosoft-include] [e:\cpython_clang\PCbuild\pythoncore.vcxproj] In file included from ..\Modules\_hacl\Hacl_Hash_Blake2b_Simd256.c:33: ..\Modules\_hacl\internal/Hacl_Hash_Blake2b.h(38,10): warning : #include resolved using non-portable Microsoft search rules as: ..\Modules\_hacl\internal/Hacl_Streaming_Types.h [-Wmicrosoft-include] [e:\cpython_clang\PCbuild\pythoncore. vcxproj] In file included from ..\Modules\_hacl\Hacl_Hash_Blake2s_Simd128.c:26: ..\Modules\_hacl\internal/Hacl_Hash_Blake2s_Simd128.h(39,10): warning : #include resolved using non-portable Microsoft search rules as: ..\Modules\_hacl\libintvector.h [-Wmicrosoft-include] [e:\cpython_clang\PCbuild\pythoncore.vcxproj] In file included from ..\Modules\_hacl\Hacl_Hash_Blake2s_Simd128.c:32: ..\Modules\_hacl\internal/Hacl_Hash_Blake2b.h(38,10): warning : #include resolved using non-portable Microsoft search rules as: ..\Modules\_hacl\internal/Hacl_Streaming_Types.h [-Wmicrosoft-include] [e:\cpython_clang\PCbuild\pythoncore. vcxproj]

chris-eibl · 2025-03-07T21:15:26Z

Modules/_hacl/refresh.sh

@@ -143,7 +131,7 @@ $sed -i -z 's!\(extern\|typedef\)[^;]*;\n\n!!g' include/krml/FStar_UInt_8_16_32_
 $sed -i 's!#include.*Hacl_Krmllib.h"!!g' "${all_files[@]}"

 # Use globally unique names for the Hacl_ C APIs to avoid linkage conflicts.
-$sed -i -z 's!#include <string.h>\n!#include <string.h>\n#include "python_hacl_namespaces.h"\n!' Hacl_Hash_*.h
+$sed -i -z 's!#include <string.h>!#include <string.h>\n#include "python_hacl_namespaces.h"!' Hacl_Hash_*.h


Without removing the \n, the python_hacl_namespaces.h got nowhere inserted.
No glue why. Maybe because I am running this in WSL?

you might have the evil core.autocrlf setting set to true, in which case git will rewrite the files to have windows-style line endings -- in any case, good to change the sed 👍

Yeah, I thought so, too, but in WSL I have Unix-style endings (there I did run refreh.sh) and on Windows I have Windows-style endings. But that shouldn't be a problem, since I was running refresh.sh on WSL?

So this change is good either way? Great :)

chris-eibl · 2025-03-07T21:20:07Z

Modules/_hacl/refresh.sh

+$sed -i 's!#include "fstar_uint128_struct_endianness.h"!#include "krml/fstar_uint128_struct_endianness.h"!g' include/krml/internal/types.h
+
+# use KRML_VERIFIED_UINT128
+$sed -i -z 's!#define KRML_TYPES_H!#define KRML_TYPES_H\n#define KRML_VERIFIED_UINT128!g' include/krml/internal/types.h


As suggested py @msprotz, let's go here with KRML_VERIFIED_UINT128 and do not use fstar_uint128_{gcc64,msvc.h} for now.

from Makefile.pre.in to fix makefile based builds

msprotz · 2025-03-07T21:48:37Z

Ok so I need to debug the krmlrenamings bug and review this PR. I should be able to tackle this early next week. Let me know if this is more pressing and I'll see what I can do. Thanks!

chris-eibl · 2025-03-07T21:53:25Z

Oh for me this is absolutely not pressing.

Have a great weekend!

update to hacl_star_rev=809c320227eecc61a744953f1ee574b4f24aabe3

02f3ebe

bedevere-app bot mentioned this pull request Mar 7, 2025

blake2module.c needs to be compiled with libhacl SIMD flags #130213

Open

chris-eibl commented Mar 7, 2025

View reviewed changes

chris-eibl added 2 commits March 7, 2025 21:42

fix #include "python_hacl_namespaces.h"

94bcca9

remove fstar_uint128_gcc64.h and fstar_uint128_msvc.h make regen-sbom

fix clang-cl warnings

5db43ba

#include resolved using non-portable Microsoft search rules

chris-eibl commented Mar 7, 2025

View reviewed changes

chris-eibl added 2 commits March 7, 2025 22:23

remove Modules/_hacl/include/krml/fstar_uint128_gcc64.h

75edcdd

from Makefile.pre.in to fix makefile based builds

make regen-sbom

35052e8

chris-eibl mentioned this pull request Mar 9, 2025

use -flto=thin for clang-cl on Windows #131005

Draft

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

gh-130213: update hacl_star_rev to 809c320227eecc61a744953f1ee574b4f24aabe3 #130960

gh-130213: update hacl_star_rev to 809c320227eecc61a744953f1ee574b4f24aabe3 #130960

chris-eibl commented Mar 7, 2025 •

edited

Loading

chris-eibl Mar 7, 2025 •

edited

Loading

msprotz Mar 7, 2025

chris-eibl Mar 7, 2025

chris-eibl Mar 7, 2025

chris-eibl Mar 7, 2025

msprotz Mar 7, 2025

chris-eibl Mar 7, 2025

chris-eibl Mar 7, 2025 •

edited

Loading

chris-eibl Mar 7, 2025

msprotz Mar 7, 2025

msprotz Mar 7, 2025

chris-eibl Mar 7, 2025

msprotz Mar 7, 2025

chris-eibl Mar 7, 2025

chris-eibl Mar 7, 2025

msprotz Mar 7, 2025

chris-eibl Mar 7, 2025

chris-eibl Mar 7, 2025

msprotz commented Mar 7, 2025

chris-eibl commented Mar 7, 2025

gh-130213: update hacl_star_rev to 809c320227eecc61a744953f1ee574b4f24aabe3 #130960

Are you sure you want to change the base?

gh-130213: update hacl_star_rev to 809c320227eecc61a744953f1ee574b4f24aabe3 #130960

Conversation

chris-eibl commented Mar 7, 2025 • edited Loading

chris-eibl Mar 7, 2025 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

chris-eibl Mar 7, 2025 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

msprotz commented Mar 7, 2025

chris-eibl commented Mar 7, 2025

chris-eibl commented Mar 7, 2025 •

edited

Loading

chris-eibl Mar 7, 2025 •

edited

Loading

chris-eibl Mar 7, 2025 •

edited

Loading