Updating for new F* build

[mtzguido]

Preparing for F* PR FStarLang/FStar#3637

I'm not sure how to properly update the hacl-star-snapshot, I just copied over some files from a HACL* build.. is there a script?

[TWal]

Thanks guido!

No, I don't ever update HACL* actually, so I think we shouldn't update it (unless new F* packaging requires to?)

[mtzguido]

No, I don't ever update HACL* actually, so I think we shouldn't update it (unless new F* packaging requires to?)

The new library split does make this need a patch. Trying to build the current status (make check) gives:

File "hacl-star-snapshot/haclml/Vale_X64_QuickCodes.ml", line 10, characters 52-71:
10 | type ('r, 'msg, 'p) labeled_wrap = (unit, unit, 'p) FStar_Range.labeled
                                                         ^^^^^^^^^^^^^^^^^^^
Error: Unbound module FStar_Range

since FStar_Range now only exists in the pluginlib (it points to an internal type, that of ranges). Replacing fstar.lib for fstar.pluginlib gives a bunch of:

Error: Unbound module Prims
File "hacl-star-snapshot/haclml/Vale_X64_Memory_Sems.ml", line 1, characters 5-10:
1 | open Prims
         ^^^^^
Error: Unbound module Prims
File "hacl-star-snapshot/haclml/Primitives.mli", line 6, characters 17-35:
6 | type bytes = int FStar_Seq_Base.seq
                     ^^^^^^^^^^^^^^^^^^
Error: Unbound module FStar_Seq_Base

since the plugin library is wrapped, and requires an open Fstar_pluginlib at the top.

I could try to find a smaller patch the current one, but the easiest is probably just regenerating everything.

[TWal]

Thinking more about it, I don't think regeneration is the best thing to do because we actually hand-edited these files (!) so that instead of executing the specifications we instead execute the C HACL* bindings so that tests run quickly. See e.g. 1b2874e#diff-baa58c6d8e41452182989d5d62b3de7cac0f8f81488594c73b1b38b46e0af095

This is a bit nasty and the clean thing to do be that the great HACL* developers provide an F* API that binds to the C code, but well, I guess they have more interesting things to do.
I will try to find a hacky solution by myself then, and come back to you if I have problems.

[mtzguido]

Makes sense, I think maybe just adding open Fstar_pluginlib at the top of the files that were extracted with --codegen Plugin would be enough, plus a module renaming or two perhaps.

[TWal]

I went for the hacky solution of defining a minimal FStar_Range.ml, it seems to be doing the job.

[mtzguido]

Sounds good! F* master is now updated btw.