karthikbhargavan

I am happy to try re-fixing this proof, but it would be useful to get some guidance on what blows up memory usage here, so that I or others don't...

printf and exit are not used in the crypto code, they are primarily used for testing. so this should not affect verification. editing kremlib to remove these and defining htolen64...

Thanks! We will need a review from the vale team.

This has been sitting around for a while and is out-of-date with master. Is there new work in this direction that we should update with, or shall we close this...

If this is working now, maybe we can close this?

How about we introduce a new function of the form: ``` let ignore_st (x:'a) : ST unit (requires (fun _ -> True)) (ensures fun h0 _ h1 -> h0 ==...

Good point, we do not do this yet, because the code is designed to be super general.

What is the status on this? It looks very useful!

Spec equivalence is mostly done, it needs some help from HACL* experts to push it over the line.

We did a detailed in-person review of the code with Mamone. We have a strategy for reducing the inlined code which Mamone is executing. Mamone will also fix the test...