The Coq mailing list

[Pierre-Evariste Dagand <pierre AT evr.ist>]

Hi folks,

> Several years ago, I discussed this paper with one of its coauthors, namely
> Pierre-Évariste Dagand (two plausible email addresses in the cc). He said
> that he would find it interesting to port this work to the amd64 instruction
> set, using Iris as a framework for separation logic. Or, in general, port it
> to a more modern separation logic framework and prevent further bitrot.
> However, he added that the amount of engineering work required would call
> for a decent scientific motivation.

Yep, I still believe this to be true.


Note that, in the meantime, Intel has released Xed

  https://intelxed.github.io/

which can be used to obtain the encoding/decoding of instructions from
Intel's declarative specification. A few years back, a student of mine
"kind of almost" extracted all AVX-512 instructions as a Coq datatype,
through a hacky Python script.


Alternatively, one could have a look at "high-level assembly
languages", such as Jasmin

  https://github.com/jasmin-lang/jasmin

> Hope that Pierre-Évariste is fine with this public summary of his
> stance back then; not sure if it has changed since.

No problem. I only take issue when you rob me of the last slice of
chocolate cake at a conference. Only then do I hold a grudge forever
after :)

> Now, what I find interesting is that the git repo maintained by Maxime Dénès
> (also cc'd) found by Mukesh actually does mention amd64, at least in its
> title.

Andrew Kennedy had started a 64-bit version. However, there were some
significant performance issues with instruction decoding, so it
remains very partial wrt. full amd64.


If I can be of any help, don't hesitate to ping me.


Regards,

--
Pierre