coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Instruction Set Semantics

From: Clément Pit-Claudel <cpitclaudel AT gmail.com>
To: coq-club AT inria.fr
Cc: Thomas E Bourgeat <bthom AT csail.mit.edu>
Subject: Re: [Coq-Club] Instruction Set Semantics
Date: Fri, 1 Jun 2018 15:04:00 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=cpitclaudel AT gmail.com; spf=Pass smtp.mailfrom=cpitclaudel AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt0-f178.google.com
Ironport-phdr: 9a23:68uErh/JhpckNP9uRHKM819IXTAuvvDOBiVQ1KB30OgcTK2v8tzYMVDF4r011RmVBdids6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+553ebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMNboRr4oRzut86ZrSAfpiCgZMT457HrXgdF0gK5CvR6tuwBzz4vSbYqINvRxY7ndcMsHS2RfUMZfVy9PDI2yYIQADeUOIelWopLhp1YMtxayGRWgCe3txzJOm3T43bc60+MkEQzewgEgG8gJsHHKo9XzKKcdSfq7zKjUzTnacf5W3S3y6JXVfR8/pfGHQLV9ftbJyUkuCwPKklGQppb4PzyIyOsNt3OW7+VlVe21im4nrxt9rSSoxscpk4TEgJ8exF7D9SV82ok1JNu4RVZ0Yd6lDJtQtzyaOJBsTsw+RGFovSA3waAFt56jZCUG1ogryhrFZ/GEc4WE+AzvWPuQLDtimX5oerGyiw6v/UWj0OHwSMi53ExUoiZfj9XAqH4A2hrO4cadUPR95F2u2TOX2gDT9O5EJUc0mLLeK5E7w74wkoMfsV3fHiPqgUn2grKae0cn9+Sy5OTnZbLmppCYN4BqkA3xLqMumsmnDeQ5NAgBQXSb9Pyi2LH/+UD1WrZHg/0snqXHrZzXJN4XqrO7DgJWyooj7gywDzai0NQWh3kHK1dFdQqbgIjxOlHOPOz3DfOljFSxjThk2fTGM6buApXINHfDkbPhcaxh5E5bzQo/1cpf6I5MCrEdPPLzXVf8u8DfDh8gKgC73+LnCMhm2Y4FQmKOAqqZMLvIvlOS5+IvJfOMZI4PtzrnJfgl/a2msXhsklgEOKKtwJE/aXaiH/0gLV/KT2Drh4IqFeYPswwie9TrlBipVTdOa3u2F/Y3/jAnA4avEIvOQqiihbWA2GGwGZgANTMOMUyFDXq9L9bMYPwLci/HZ5Y5ymVVB4jkcJco0FSVjCG/zrNmKuTO/ShB7MDs0dF046vYkhRgrGUoXfTY6HmESiRPpk1NXyU/hfktrkl0y1PF2q990aQBSI5joshRWwJ/Dqbyiux3D9eoBFDEd9aNDU+6GpCoWG5hCN02xNAKbgB2HNDw1h0=

On 2018-06-01 13:12, Gregory Malecha wrote:
> Hello --
>
> I am wondering if anyone knows of a formalization of the ARMv8 (or other
> instruction set) in Coq that is open source. I'm looking for as complete of
> an instruction set as possible since I am working with low-level systems
> programs.
CCing Thomas, whose spec of RISCV (written in Haskell and translated to Coq)
is currently being used to verify compilers to RISCV (for now only the
machine mode part of the spec has been translated, IIUC). See
https://github.com/mit-plv/riscv-semantics and
https://github.com/samuelgruetter/riscv-coq

[Coq-Club] Instruction Set Semantics, Gregory Malecha, 06/01/2018
- Re: [Coq-Club] Instruction Set Semantics, Clément Pit-Claudel, 06/01/2018
- Re: [Coq-Club] Instruction Set Semantics, Frédéric Blanqui, 06/04/2018
- Re: [Coq-Club] Instruction Set Semantics, Peter Sewell, 06/05/2018