Enable more instances of the C Abstract Struct pattern by msprotz · Pull Request #1025 · hacl-star/hacl-star

msprotz · 2025-02-19T20:23:27Z

github-actions · 2025-02-19T20:23:59Z

[CI] Important!
The code in dist/gcc-compatible, dist/msvc-compatible, and dist/wasm
is tested on cryspen/hacl-packages.
dist is not automatically re-generated, be sure to do it manually.
(A fresh snapshot can also be downloaded from CI by going to the "artifacts" section of your run.)
Then check the following tests before merging this PR.
Always check the latest run, it corresponds to the most recent version of this branch.
All jobs are expected to be successful.
In some cases manual intervention is needed. Please ping the hacl-packages maintainers.

Build, Test, Benchmark: Build on Linux (x86, x64), Windows (x86, x64), MacOS (x64, arm64), s390x, Android (arm64) and test on Linux (x86, x64), Windows (x86, x64), MacOS (x64).
Performance Regression Tests: Navigate to the terminal output in “Run benchmarks”. The comparison with the main branch will be at the bottom. The run fails if the performance regresses too much.
OCaml bindings: Build & Tests
JS bindings: Build & Tests
Rust bindings: Build & Tests

chris-eibl

Most probably this is generated, but at least I marked the spots to #ifdef.

chris-eibl · 2025-02-27T20:21:07Z

+}
+Hacl_Streaming_MD_state_64;
+
+typedef struct Hacl_Streaming_Blake2_Types_two_vec128_s


Suggested change

typedef struct Hacl_Streaming_Blake2_Types_two_vec128_s

#if defined(HACL_CAN_COMPILE_VEC128)

typedef struct Hacl_Streaming_Blake2_Types_two_vec128_s

chris-eibl · 2025-02-27T20:21:39Z

+  Lib_IntVector_Intrinsics_vec128 *snd;
+}
+Hacl_Streaming_Blake2_Types_two_vec128;
+


Suggested change

#endif

chris-eibl · 2025-02-27T20:22:03Z

+}
+Hacl_Streaming_Blake2_Types_two_vec128;
+
+typedef struct Hacl_Streaming_Blake2_Types_two_vec256_s


Suggested change

typedef struct Hacl_Streaming_Blake2_Types_two_vec256_s

#if defined(HACL_CAN_COMPILE_VEC256)

typedef struct Hacl_Streaming_Blake2_Types_two_vec256_s

chris-eibl · 2025-02-27T20:22:16Z

+  Lib_IntVector_Intrinsics_vec256 *snd;
+}
+Hacl_Streaming_Blake2_Types_two_vec256;
+


Suggested change

#endif

chris-eibl · 2025-02-27T20:22:55Z

+}
+Hacl_Streaming_Blake2_Types_block_state_blake2b_32;
+
+typedef struct Hacl_Streaming_Blake2_Types_block_state_blake2b_256_s


Suggested change

typedef struct Hacl_Streaming_Blake2_Types_block_state_blake2b_256_s

#if defined(HACL_CAN_COMPILE_VEC256)

typedef struct Hacl_Streaming_Blake2_Types_block_state_blake2b_256_s

chris-eibl · 2025-02-27T20:23:13Z

+  Hacl_Streaming_Blake2_Types_two_vec256 f3;
+}
+Hacl_Streaming_Blake2_Types_block_state_blake2b_256;
+


Suggested change

#endif

chris-eibl · 2025-02-27T20:23:58Z

+}
+Hacl_Streaming_Blake2_Types_block_state_blake2s_32;
+
+typedef struct Hacl_Streaming_Blake2_Types_block_state_blake2s_128_s


Suggested change

typedef struct Hacl_Streaming_Blake2_Types_block_state_blake2s_128_s

#if defined(HACL_CAN_COMPILE_VEC128)

typedef struct Hacl_Streaming_Blake2_Types_block_state_blake2s_128_s

chris-eibl · 2025-02-27T20:24:23Z

+  Hacl_Streaming_Blake2_Types_two_vec128 f3;
+}
+Hacl_Streaming_Blake2_Types_block_state_blake2s_128;
+


Suggested change

#endif

chris-eibl · 2025-02-28T05:31:47Z

I think, libintvector.h can now be moved to internal, since the goal was to hide it.
Are there more candidates to be moved?

msprotz · 2025-03-03T19:18:04Z

Regarding the #ifdef: I think this doesn't work, because I still need these types in scope for Hacl_Streaming_HMAC.c to compile, since its agile type contains references to those types in any case (but with the new libintvector-shim.h that should not be a problem).

Regarding moving libintvector.h to internal: sadly there are other files in HACL* that do not have such a clean abstraction barrier (see e.g. Hacl_Hash_SHA3_Simd256.h) -- that latter file is used directly by other crypto implementations in other repositories, e.g. for SIMD ML-KEM.

I would like to fix that latter point, eventually.

msprotz · 2025-03-03T19:20:55Z

The windows CI error is a legitimate one -- I need to fix up an abstraction.

msprotz · 2025-03-03T23:46:30Z

Ok at this stage I feel confident that this is in the right shape for Python, modulo my comments above. I intend to merge, and fix things up as they arise during the Python integration process.

Thanks @chris-eibl for the feedback.

The Nix CI will come back red until I merge FStarLang/karamel#542

chris-eibl · 2025-03-04T06:05:26Z

Regarding the #ifdef: I think this doesn't work, because I still need these types in scope for Hacl_Streaming_HMAC.c to compile, since its agile type contains references to those types in any case (but with the new libintvector-shim.h that should not be a problem).

If my analysis is correct, this means, that

even though in the Python example blake2module.c does no longer need a compiler that supports the intrinsics without compiling for an AVX architecture (since the abstraction now hides the "problematic" intrinsics)
the intrinsics are needed for all HACL_*_.c files that include internal/Hacl_Streaming_Types.h, e.g. Hacl_Hash_SHA1.c. This was not the case, when Python last downstreamed (https://github.com/hacl-star/hacl-star/tree/f218923ef2417d963d7efc7951593ae6aef613f7)
IOW, a binary that does run on hosts which do not support AVX, can no longer be created with such compilers

Hopefully, I am mistaken?

msprotz · 2025-03-04T06:19:50Z

the intrinsics are needed for all HACL_*_.c files that include internal/Hacl_Streaming_Types.h, e.g. Hacl_Hash_SHA1.c. This was not the case, when Python last downstreamed

ok I did not realize about this side-effect, thanks for pointing it out

in my opinion then, the best option is to split the Hacl_Streaming_Types.h header into three files Hacl_Streaming_Types{,_Simd128,_Simd256} -- and then inclusion is more precise and does not have that unpleasant side effect

what do you think?

thanks again for your detailed review

chris-eibl · 2025-03-04T06:25:55Z

in my opinion then, the best option is to split the Hacl_Streaming_Types.h header into three files Hacl_Streaming_Types{,_Simd128,_Simd256} -- and then inclusion is more precise and does not have that unpleasant side effect

Sounds even better than my #ifdef approach. I just thought that would have been the easiest solution :)

thanks again for your detailed review

Thanks for all your efforts!

chris-eibl · 2025-03-04T17:00:36Z

Just a thought: include files with the same name only in different paths (e.g. Hacl_Streaming_Types.h and internal/Hacl_Streaming_Types.h) can be a root of trouble. Since most of the code is generated, would it be easily possible to e.g. postfix the internal ones with _internal (or whatever deems more appropriate)?

If this introduces churn or is not easily doable in the code generators - just forget about it :)

msprotz · 2025-03-04T19:51:16Z

@chris-eibl just pushed a change to avoid the issue you described with SHA1 -- the SIMD types are now in their own separate files, only included by the corresponding Blake2 modules.

Can you say more about the issue about the filenames? It's changeable, but I'm curious what issues you ran into.

chris-eibl · 2025-03-04T20:09:16Z

Can you say more about the issue about the filenames? It's changeable, but I'm curious what issues you ran into.

Oh sorry to have given that impression. I did not run into problems. Having the same filenames just can be a problem. If it is easy to avoid the same names - that would be just a "nice to have".

msprotz · 2025-03-04T21:05:07Z

Let me merge this first then make a note of the filename issue -- this PR has been open for a while and I'm kind of eager to get this going to see if it would solve Python's issues.

msprotz · 2025-03-04T21:23:44Z

I pushed one last simplification to the file structure that had become un-necessary with my latest changes to better support forward struct decls. Now the types that contains references to libintvector live in their respective Hacl_Hash_Blake2{b256,s128} files and are properly hidden behind the public header.

If you don't mind taking one last look and confirming that this is good for Python, I'll go ahead and merge.

chris-eibl · 2025-03-04T22:11:20Z

I've just had a quick look - sorry, it's late here and I am busy the next days.

AFAICT, when doing some find-in-files, etc, and quickly rushing over the last commits - this looks good to me.

Sorry that I don't have more time right now. Don't feel blocked - but if you're in doubt about merging, maybe you can just start off a PR in Python based on your last commit and during working on it switch over?

…-star into protz_abstract_struct

msprotz · 2025-03-07T01:55:00Z

I caught some incorrect cross-algorithm dependencies with e.g. Hacl_MAC_Poly1305 including Hacl_Blake2b_32.h, which I eventually fixed with FStarLang/karamel#550

With that, everything is now green and I feel confident about merging. Thanks everyone

chris-eibl · 2025-03-07T17:45:13Z

I did a draft PR based on 809c320 and can confirm that for clang-cl on Windows the issue is fixed 👍

Thank you so much for your efforts. @msprotz Maybe you can do a review there?

msprotz · 2025-03-07T17:53:09Z

for clang-cl on Windows the issue is fixed 👍

terrific news!

of course very happy to do a review there, cheers

mtzguido · 2025-03-07T18:48:35Z

  -add-include 'Hacl_P256:"lib_intrinsics.h"' \
  -add-include 'Hacl_Bignum:"lib_intrinsics.h"' \
-  -add-include 'Hacl_Bignum_Base:"lib_intrinsics.h"' \
+  -add-include 'Hacl_Bignum_Base.h:"lib_intrinsics.h"' \


This bit fixes the build (currently broken on main) after FStarLang/karamel#542. I can't really comment on the rest, the high-level idea makes sense to me but I'm not too familiar with the structure of the build here.

msprotz added 2 commits February 19, 2025 15:12

Refresh with C abstract struct

beb9452

Refresh with c abstract struct

b5292bf

msprotz requested a review from a team as a code owner February 19, 2025 20:23

msprotz mentioned this pull request Feb 24, 2025

gh-130213: POC let blake2module.c see far less internals python/cpython#130483

Closed

msprotz added 4 commits February 26, 2025 16:39

wip

c76a1ff

Invariant is on -- public headers shall not include libintvector.h

a0ca57a

WIP enforcing tight abstraction barriers

a5b82af

Bingo -- fix the last issue and have a clean abstration barrier

cc27ec4

chris-eibl reviewed Feb 27, 2025

View reviewed changes

One missing header inclusion

3d888ef

chris-eibl mentioned this pull request Feb 27, 2025

gh-130213: Check availability of Intel SIMD types python/cpython#130332

Closed

msprotz added 4 commits March 3, 2025 11:08

Refresh portable too, for testing

cf5ec66

Fix

2c0f68b

Fix

44f9cbc

Refresh msvc-compatible too

9d4d6ad

msprotz added 2 commits March 3, 2025 15:39

Fixup leaky abstraction by creating not(inline_for_extraction) variants

32c85cf

Refresh Windows dist

d997064

Isolate types that need libintvector.h into their own header

367c2c7

Missing files

e36de87

msprotz mentioned this pull request Mar 4, 2025

Consider renaming the internal headers FStarLang/karamel#546

Open

Simplify the file structure a bit

a712260

msprotz added 3 commits March 4, 2025 14:20

Merge branch 'main' into protz_abstract_struct

7d50eec

Refresh with latest krml changes

04f4dca

Merge branch 'protz_abstract_struct' of pro.github.com:hacl-star/hacl…

809c320

…-star into protz_abstract_struct

msprotz requested a review from R1kM March 7, 2025 01:55

chris-eibl mentioned this pull request Mar 7, 2025

gh-130213: update hacl_star_rev to 322f6d58290e0ed7f4ecb84fcce12917aa0f594b python/cpython#130960

Merged

mtzguido approved these changes Mar 7, 2025

View reviewed changes

chris-eibl mentioned this pull request Mar 7, 2025

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

Closed

Avoid name clashes that yield non-predictible user-facing names

7ff930c

R1kM approved these changes Mar 10, 2025

View reviewed changes

msprotz enabled auto-merge March 10, 2025 21:45

msprotz merged commit 322f6d5 into main Mar 10, 2025

msprotz deleted the protz_abstract_struct branch March 10, 2025 22:42

	typedef struct Hacl_Streaming_Blake2_Types_two_vec128_s
	#if defined(HACL_CAN_COMPILE_VEC128)
	typedef struct Hacl_Streaming_Blake2_Types_two_vec128_s

	typedef struct Hacl_Streaming_Blake2_Types_two_vec256_s
	#if defined(HACL_CAN_COMPILE_VEC256)
	typedef struct Hacl_Streaming_Blake2_Types_two_vec256_s

Conversation

msprotz commented Feb 19, 2025

Uh oh!

github-actions Bot commented Feb 19, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

chris-eibl left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

chris-eibl commented Feb 28, 2025

Uh oh!

msprotz commented Mar 3, 2025

Uh oh!

msprotz commented Mar 3, 2025

Uh oh!

msprotz commented Mar 3, 2025

Uh oh!

chris-eibl commented Mar 4, 2025

Uh oh!

msprotz commented Mar 4, 2025

Uh oh!

chris-eibl commented Mar 4, 2025

Uh oh!

chris-eibl commented Mar 4, 2025

Uh oh!

msprotz commented Mar 4, 2025

Uh oh!

chris-eibl commented Mar 4, 2025

Uh oh!

msprotz commented Mar 4, 2025

Uh oh!

msprotz commented Mar 4, 2025

Uh oh!

chris-eibl commented Mar 4, 2025

Uh oh!

msprotz commented Mar 7, 2025

Uh oh!

chris-eibl commented Mar 7, 2025

Uh oh!

msprotz commented Mar 7, 2025

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

github-actions Bot commented Feb 19, 2025 •

edited

Loading