Aseem Rastogi

I tried a windows build today, and it is also broken: ``` /home/aseemr/everest/hacl-star/dist/mozilla/Hacl_SHA3.c:93: undefined reference to `Lib_Memzero0_memzero' /usr/lib/gcc/x86_64-w64-mingw32/11/../../../../x86_64-w64-mingw32/bin/ld: /home/aseemr/everest/hacl-star/dist/mozilla/Hacl_SHA3.c:104: undefined reference to `Lib_Memzero0_memzero' /usr/lib/gcc/x86_64-w64-mingw32/11/../../../../x86_64-w64-mingw32/bin/ld: /home/aseemr/everest/hacl-star/dist/mozilla/Hacl_SHA3.c:121: undefined reference to `Lib_Memzero0_memzero' /usr/lib/gcc/x86_64-w64-mingw32/11/../../../../x86_64-w64-mingw32/bin/ld:...

See this for a wrapper over `HSL.Receive` as expected by `TLS.Handshake.Machine`: https://github.com/project-everest/mitls-fstar/blob/dev/src/tls/experiments/HSL.Receive.Wrapper.fst. It also contains an implementation of `buffer_received_fragment`. The way the invariant of this wrapper is structured, I think...

The support for the witnessed buffer lemma and dynamic regions is in F* master. Remaining tasks there: * Weaken the preconditions of existing `ralloc` and `ralloc_mm` functions to work on...

Looks like a `Pat_var` vs `Pat_wild` thing, any other name for the pattern bound variable in `f2` works.

Should `Pat_wild` unify with any pattern (the branches will anyway be compared after being opened with the pattern variables)?

Yes, makes sense.

This would also be useful to address issues like #1041.

Thanks for the PR @W95Psp! I have left some comments, the main one is for the AST change in `FStar.Syntax.Syntax`, wonder if we can do without it.

Your suggestion sounds good to me @tahina-pro. I would also be fine saying that our makefiles/scripts take care of the scenarios where F* is being used from binary packages or...

This looks good to me as well!