Jonathan Protzenko

Yes, the check is because in Low\* you specify the number of *elements* you want to allocate, but unfortunately, if the elements are larger than a byte, you risk overflowing...

If this can be detected reliably via ifdefs, that's also totally fine by me!

what is the data model for these platforms?

Yes; for wasm I'd have to perform the alignment of allocation by hand (and the inlining by hand too).

try passing `-bundle WasmSupport`... I'm in the process of rewriting the tutorial to explain how to properly build a project without using kremlin as a compiler driver thanks for reminding...

Both of these examples can be fixed by marking `t_F` (and not `foo` itself) as `inline_for_extraction`. ``` inline_for_extraction type t_F (a:Type) = B.pointer a -> HST.St unit ``` However, I...

https://github.com/project-everest/hacl-star/pull/582 tests this patch on a large-scale, and I'm not sure inserting `(void)` casts is even worth it. Would it be more idiomatic in C to just not even insert...

@franziskuskiefer would love to have your thoughts

Looking at this again, my take is that if we want the HACL code to *not* look weird, we'll have to do `(void)` insertion along with a manual review to...

I thought `ppx_deriving` was supposed to be able to deal with these cases. Perhaps worth pinging the ppx_deriving folks to see if they're missing support for cross-compilation? In any case,...