EverCrypr.Hash.alloca: remove strict_on_args attribute

[mtzguido]

Proposed changes

FStarLang/FStar#3107 changes the behavior of strict_on_args slightly. Previously, if a strict_on_args function f appeared by itself, without any arguments, it could be unfolded (according to delta rules as usual). That PR fixes that problem, preventing the unfolding, which raises a compilation failure for libevercrypt:

Warning 2: in the arguments to EverCrypt.Hash.alloca, in the definition of tmp_block_state, after the definition of buf_1, in the last element of the sequence, after the definition of uu___, in top-level declaration EverCrypt.Hash.Incremental.digest_md5, in file EverCrypt_Hash: Reference to EverCrypt.Hash.alloca has no corresponding implementation; please provide a C implementation
Warning 2 is fatal, exiting.
gmake[1]: *** [Makefile:859: dist/wasm/Makefile.basic] Error 255

My understanding is that now some standalone occurrence of alloca remains, and since it doesn't have an implementation, the build fails. My "fix" in this PR is just removing the attribute for this definition. Looking at it again, I guess removing the noextract may be more sensible.. I'll update this bit with whether that works too.

Does this make sense?

Full error here: https://sprunge.us/xQxQsv

Types of changes

What types of changes does your code introduce to HACL*?
Put an x in the boxes that apply

• Proof maintenance (non-breaking change which fixes a proof regression)
• Bugfix (non-breaking change which fixes an issue)
• New algorithm or feature (non-breaking change which adds functionality)
• Improved performance (fix or feature that would improve performance of some algorithm on some platform)
• Breaking change (fix or feature that would cause existing functionality to not work as expected)
• Documentation Update (if none of the other choices apply)

Checklist

Put an x in the boxes that apply. You can also fill these out after creating the PR. If you're unsure about any of them, don't hesitate to ask. We're here to help! This is simply a reminder of what we are going to look for before merging your code.

• I have read the CODE_OF_CONDUCT.md doc
• I have read and agree to submit my changes under the LICENSE
• I have added necessary documentation (if appropriate)
• I have edited CHANGES.md (if appropriate)

[github-actions]

[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

[msprotz]

The noextract should remain -- this function cannot be compiled safely to C.

Note that the commit that added the strict on args is

commit bb981031e609b37e4a5fd63b040357eb16ab9277
Author: Guido Martínez <mtzguido@gmail.com>
Date:   Sat Jun 10 17:00:23 2023 -0700

    EverCrypt.Hash: use @@strict_on_arguments for efficiency

the error stems from line 1674 in Hacl.Streaming.Functor.fst and at first glance this does look like the argument should be constant

[msprotz]

Do you think you could try to dump either an OCaml, or use krml's -dmonomorphization for the WASM target (make dist/wasm/Makefile.basic) to figure out what the arguments to this particular call to alloca are?

[mtzguido]

Note that the commit that added the strict on args is

Haha, what a genius, somehow I thought it was a different one. Thanks for the pointers, I'll take a deeper look and report back.

[msprotz]

Can I help with this in any way?