Jonathan Protzenko

@Frosne any updates on @karthikbhargavan's question? Thanks!

@Frosne thanks for adding the motivations in the initial message. FYI, I don't think anyone gets a notification if the original message in the thread gets modified. If @polubelova @victor-dumitrescu...

Update: ran with `-n 5` as promised, here's a more precise count. This lists all of the files that ended up peaking above 2GB of memory. Surprisingly few of those!...

``` 2,172,040 Hacl.Impl.P256.LowLevel.fst 2,178,808 Vale.Curve25519.X64.FastMul.fst 2,234,952 Vale.AES.X64.AESGCM.fst 2,411,460 Vale.Poly1305.X64.fst 2,465,716 Spec.P256.MontgomeryMultiplication.PointAdd.fst 2,491,804 Hacl.Impl.SHA2.Core.fst 2,655,512 Hacl.Spec.K256.Field52.Lemmas3.fst 3,424,432 Vale.Wrapper.X64.GCMencryptOpt.fst 3,459,308 Vale.Curve25519.X64.FastUtil.fst 3,524,508 Vale.Wrapper.X64.GCMencryptOpt256.fst 3,678,088 Vale.Wrapper.X64.GCMdecryptOpt.fst 3,730,196 Vale.Wrapper.X64.GCMdecryptOpt256.fst 3,893,544 Vale.AES.X64.GCMdecryptOpt.fst 3,925,760 Vale.AES.X64.GCMencryptOpt.fst 3,936,032...

@karthikbhargavan your proof fixes undid the improvements that Aseem performed on that proof. The memory usage is now 9GB, down from the worst-case 12GB, but up from the Aseem-improved 2GB...

Closing since the file is now gone. @pnmadelaine you might find the commands interesting to monitor memory usage throughout the build; they're for OSX but can be easily adapted for...

Hi, and thanks for getting in touch. What you describe is an ambitious research project, and while we do have ideas and aspirations for verifying Rust programs, none of them...

I'm happy to consider changes to `kremlib.h` to make your life easier (it's a copy of the original file at https://github.com/FStarLang/kremlin/blob/master/kremlib/kremlib.h)... I'll ping you here when I have a revised...

I believe this is fixed by https://github.com/FStarLang/kremlin/commit/276bbd4ee67414109b5e88627cd7e2eda4eab73e

PascalCase = kremlin-generated file snake_case = hand-written there are two such files: the snake_case one is in include/kremlin, the PascalCase one is in dist/generic/* The correct fix is probably to...