Jonathan Protzenko

icon indicating a website link https://jonathan.protzenko.fr

icon company Microsoft icon location Redmond, WA icon location This is my professional GitHub account to record my contributions with my @Microsoft (MS) employee hat on. My open-source work is done with the @protz hat on

Results 404 comments of Jonathan Protzenko

Custom setup using Cygwin and Ocaml Issue

I myself almost invariably encounter the same problem, FWIW

Guard against the pitfalls found in Darren's setup

Also should suggest the tip at the end of https://github.com/protz/ocaml-installer/wiki for /etc/nsswitch.conf that everyone on the corporate microsoft network seems to have

Makefiles reference incorrect Make installation on Mac

Unfortunately, on OSX, hacl-star is known to unreliably build owing to OSX-specific Z3 behavior. We do not have OSX CI at the current time which makes these problems very hard...

Some utility functions need to be refactored into TCP.fst either in Record/Test clients

@ad-l says bugs in the TCP server, need to write tests

Externally-implemented modules for Catala

Filling out the "Interpreter" part after the design discussion for this issue. There are essentially two steps to this process. The first one is to i) go over the types...

Progress on Section 121

I think it'd be good to merge this. But I'm unclear why CI failed.

Update exponentiation

I would precompute it by reducing the spec-level functions at compile-time. What is the pure equivalent of this stateful function?

Update exponentiation

@polubelova I'm happy for you to land this at any point -- let me know if you want me to hold off onto anything I have so that you can...

Check maximum length is not exceeded for incremental hashing.

Note that as a drive-by change I: - fixed a notoriously flaky proof - ditched those uu_ functions from EverCrypt_Error

Check maximum length is not exceeded for incremental hashing.

@hacl-star/maintainers need an approving review on this, thanks!