The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

There has been plenty of other work with assembly languages in Coq contemporaneously and in the intervening years, including my original work on the Bedrock framework and our team's follow-on work with Bedrock2 and full-stack hardware-software proofs.

The later flavors are based around RISC-V, which I encourage everyone doing basic research to strongly consider switching to instead of x86 or ARM.  In my analysis, there is a pretty good chance that RISC-V is more popular among new system-building projects by 10 years from now.  Even if it doesn't win in the market to that level, its simplicity and openness make it much more fun as the foundation for basic research, at the same time as it has clearly already passed the threshold as one of the most important real-world instruction sets, e.g. recently added as one of the few officially supported by Android.

On 8/6/23 12:19 PM, Tadeusz Litak wrote:

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

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. It also seems that last commits seem more recent, relatively speaking, than those in the repo maintained by Nick Benton. However, it is not clear to me if the lofty goal of covering the amd64 instruction set has been fully achieved, therein or elsewhere.

Best,

t.

On 6/8/23 5:47 PM, Jason Gross wrote:

Probably you're looking for x86proved (Google suggests https://github.com/nbenton/x86proved), which is what we were all working on when I interned with Andrew Kennedy and Nick Benton at MSR around then.

On Sun, Aug 6, 2023, 04:31 mukesh tiwari <mukeshtiwari.iiitm AT gmail.com> wrote:

Also, if you want to reach out to Nick Benton, you can find his email [1].

[1] https://nickbenton.name/contact.html

On Sun, 6 Aug 2023 at 12:25, mukesh tiwari <mukeshtiwari.iiitm AT gmail.com> wrote:

Hi Frank,

I have also searched for the code of this paper and the closest I came was [1]. 

Best,

Mukesh 

[1] https://github.com/maximedenes/coq-amd64

On Sun, 6 Aug 2023 at 12:13, Frank Schwidom <schwidom AT gmx.net> wrote:

Hi,

I found this article:

https://www.microsoft.com/en-us/research/publication/coq-worlds-best-macro-assembler/?from=https://research.microsoft.com/en-us/um/people/nick/coqasm.pdf&type=exact

named "Coq: The world’s best macro assembler?". And I read the Publication

https://www.microsoft.com/en-us/research/wp-content/uploads/2016/12/coqasm.pdf

and I am very interested in the source code which I didn't manage to find anywhere.

My mails to the authors didn't make it to its destination. So my last chance lies in this mailing list.

Does anybody know how or where I can obtain a copy of this work?

Thanks in Advance,
Frank Schwidom