Aymeric Fromherz

Permanent link for the code mentioned above: https://github.com/hacl-star/hacl-star/blob/8bc5b21f26917ab27cce93cab29270259524ff7b/dist/gcc-compatible/Hacl_Hash_SHA3.c#L307

Relevant F* code: The call to update_multi in the generic functor implementation: https://github.com/hacl-star/hacl-star/blob/90a3b50041511871b607ae13025bb8738d83c78e/code/streaming/Hacl.Streaming.Functor.fst#L1361 The update_multi instantiation for Keccak: https://github.com/hacl-star/hacl-star/blob/37f0d971631736481b27010368ae29a5eb7cd425/code/streaming/Hacl.Streaming.Keccak.fst#L177

@msprotz and myself are working this week on significant improvements to the codebase (especially related to the pervasive use of mutable borrows). The version currently on the branch is still...

I like the idea of using attributes, as this also paves the way towards more expressive "effects". Regarding your idea of simplifying through micro-passes in the pure model, wouldn't you...

Sure. From a slightly smaller file, I'm getting the following: ``` ;;; Started F* interactive: ("fstar.exe" "/home/aymeric/everest/hacl-star/vale/code/arch/Arch.Types.fsti" "--ide" "--smt" "z3" "--smt" "/home/aymeric/everest/z3/bin/z3" "--include" "/home/aymeric/everest/hacl-star/specs/" "--include" "/home/aymeric/everest/hacl-star/obj/" "--include" "/home/aymeric/everest/hacl-star/vale/specs/interop" "--include" "/home/aymeric/everest/hacl-star/vale/code/crypto/sha"...

This is weird, even by adding this (both on my local and remote F* versions), I still only get "Json parsing failed." without any more information

I'm not sure, I'm simply running `make` in the FStar directory to get an executable

Btw, I have a simple workaround for this (running emacs with ssh -X instead of over TRAMP), so there is no need to spend a huge amount of time debugging...

I think you were right, it was using the recompiled version, but apparently the OCaml one for which the F# change wasn't propagated. Below is the output for the file...

I'm using `/sshx:`/