Check stack memory allocation

[franziskuskiefer]

As noted in hacl-star/hacl-star#446 it looks like KRML_CHECK_SIZE isn't doing the right thing.
It checks for SIZE_MAX, not what can be allocated on the stack. I'm not entirely sure what the original intention was behind it. But it's used for stack allocations in hacl. So I think we should change it to check for the stack allocation limits.

https://github.com/FStarLang/kremlin/blob/6e60e33aac1551c1ae20e4e02cb66a188935990b/include/kremlin/internal/target.h#L89

On Windows the default stack size appears to be 1MB ("For ARM, x86 and x64 machines, the default stack size is 1 MB." /STACK). On Linux and macOS I get 8192K for ulimit -a (and that's what most of the internet says).

@msprotz what do you think about just checking those limits?

[msprotz]

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 size_t with a wraparound on 32-bit systems. So KRML_CHECK_SIZE prevents against this kind of attacks.

I am fine with adding another macro called KRML_CHECK_STACK_SIZE that would do KRML_CHECK_SIZE + check that size does not exceed e.g. 8MB (to keep things simple). Would that work for you?

Thanks!

[franziskuskiefer]

Ok, makes sense.
Maybe there should also be a different mechanisms for Low* to prevent large stack allocations. But having a macro in kremlin could be a start. But I'm not sure I'd go for a general 8MB limit because we'd see different errors on Windows than on Linux and mac.

[msprotz]

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