Vincent Laporte

Indeed, it seems that `irmin` and `git` must be updated simultaneously.

However, fixing `git-unix` at the expenses of breaking `irmin-git` might be a good deal (i.e., updating `irmin`, `repr` and who knows what more can wait for a follow-up PR).

There is an update of `ligo` in #184394. Might be incorporated here.

I’ve just added the `ligo` and related updates from that other PR. cc @bezmuth.

Some time ago in Sophia, the `b` prefix was also considered. B stands for bits.

> I'm unsure if this is related to this https://github.com/jasmin-lang/jasmin/issues/67. I think it’s not related. Here the problem is about proving that an array is properly initialized; there it’s about...

Here are some details about sha512. Given enough time (a bit more than 30mn on my laptop) the analysis terminates and rises two alarms, both at line 291 of `sha512.jinc`....

The assertion failure is related to array copies (which should not be too hard to fix). See #308. There is some explanation about `-safetyparam` in the [wiki](https://github.com/jasmin-lang/jasmin/wiki/Safety-checker). Of course you...

With `-safetyparam "jade_xof_shake256_amd64_spec>output,input;output_length,input_length"`, the result is more precise (and as fast).

PR #312 should fix the assertion failures.