Jonathan Protzenko

Thanks for your comment, Greg. Some related thoughts. - We have support for all of the algorithms in hashlib (md5, sha1, sha2, sha3, blake2). So there is a clear pathway...

I would say: at least machine integers and buffers. Unclear about HST... maybe.

Maybe rename it Machine then? From the discussion with @kaepora, the goal was to group modules that "belong together" under a common namespace. It feels to me like machine integers,...

@kaepora can you suggest a consistent naming scheme for the modules in ulib? happy to implement any good suggestions

Now that we have universes we could theoretically implement a perfectly dependent printf, except that the normalizer would have to be able to reduce functions on strings.

I think the root issue is that with universes, both `t₁ * t₂` and `t₁ × t₂` are valid... the former is a tuple (i.e. `Prims.tuple2 t₁ t₂`) and the...

More specifically, the parser doesn't distinguish between types and terms; there's a cascade of precedence levels, and somewhere in the cascade is `tmTuple`. The relevant bits are: ``` 603 typ:...

Z3 4.8.5 segfaults on arm64. It returns "Killed" as its only output, but then F* cannot deal with that, raises a fatal exception. Then, F* synthesizes an incorrect backtrace and...

> So, the ALL_ML_FILES variable emitted in .depend DOES respect the module selector setting given by the --extract option. The ALL_KRML_FILES does not. Correct. > For HACL* purposes, it seems...

> E.g., --extract "OCaml:A,B; Kremlin:A,B,C; FSharp:A" etc. with our current version of extract interpreted as a uniform module selector for all codegen targets. So, in short, this is a fine...