coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Instruction Set Semantics

From: Peter Sewell <Peter.Sewell AT cl.cam.ac.uk>
To: coq-club AT inria.fr, Brian Campbell <Brian.Campbell AT ed.ac.uk>, Alastair Reid <Alastair.Reid AT arm.com>, Alasdair Armstrong <alasdair.armstrong AT cl.cam.ac.uk>, Thomas Bauereiss <Thomas.Bauereiss AT cl.cam.ac.uk>, Prashanth Mundkur <prashanth.mundkur AT sri.com>, Robert Norton <robert.norton AT cl.cam.ac.uk>
Subject: Re: [Coq-Club] Instruction Set Semantics
Date: Tue, 5 Jun 2018 14:27:21 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=p.m.sewell AT googlemail.com; spf=Pass smtp.mailfrom=p.m.sewell AT googlemail.com; spf=None smtp.helo=postmaster AT mail-wm0-f65.google.com
Ironport-phdr: 9a23:LoG/thIAy0/8rpiS3dmcpTZWNBhigK39O0sv0rFitYgXK/r7rarrMEGX3/hxlliBBdydt6oZzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlIiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0vRz+s87lkRwPpiCcfNj427mfXitBrjKlGpB6tvgFzz5LIbI2QMvdxeb7Tfc4BRWpZQMleSzBBDI27b4sKFeUBPOBYpJT5q1YBqRayAA+hD/7txDBVnH/7xa810+ohHw/I3wIuAswAv2jPodrvKKsfS/q4wLXUwTjBaf5dxDfz6JLPchAkufyCR6x/cdbPxkk1CgjLk0ufqIL7MDOR0uQGrm+W4fB+WuKzlWEnsRt9rCWxycYilIbJgoYVx0vY+iV92oo6Oce3SEthbdG+DJRcrTyaN4hvT84kXmpmtiE6yrgctp66eigH0Jsnxx/Da/yHboiH+QjvVOeWITtgi3Jlea6/hxav8Ue70OHzSs600FNMoyFYkdfMrmgA2h7c58SdV/dx4Ees1SyM2gzN8O1JIEA5mKzGIJA72LEwjIAcsUHbEy/2hkr2iKiWe10h+uey6uTnZqzqp5GZN4Nokw3+PKUjl8ylDeQ3NQgOWGeb+eCi27H54UL5R7BKguU3kqnfrp/aOdwWq6y2DgNPz4ov9RayAy2l3dgGh3UKLVJIdAqCj4fzOlHOJP74De24g1SpiDpr3+rKPrj7DpXWMHfCnqnufbJ560NHxwozytdf551QCr4fJfL8QE7xtNjCAhAlNAy0xv7rCM9h2YMGRWKPHqiZPbvOvl+P/+IjOvWDZIsIuDnmMPUl/P7vjXohmVAHZ6Wp3J0XaGq5Hvt8OUmZb2Ds0Z89FjIBuRN7R+j3gnWDVyRSbjC8ReZ0zCs6AYTuJo7GXoqghLjJiA2hH5RQIEtPD0iGHHPsX4iIHf4HLj+RdIspuzgNTqSoSpVp7xyvuEeu4r5uNfbd+zdej5/i2PB8/eiVnhY3o3g8JsCUyG2ETns8t3kNXCMs26Zw6Rh0zl6Y3aF5mbpRD9lI++lOVAgSPpqaxOV/Tdn5HB/CKJPBdFahR9y9SRs4U98rzt4VeA4pJ9WlixnYmQCjHrIPmr2QH7Q/9uTX1n23Ls071nWQkOEZlVA9QsJJKW3uo7N5+wvOHcadi1+QjKajc7gcmivQ8muA0HCmp1tZFgV3VPOBFUoYbEbMsZzf4VneSLnmXa4gOAZb1YiELbFWbdvBhlEAT/7mft3VJX+yzTSKCA6M14+LObLnZ2gHmh7QF0UAlygY+TCNPA14DyznvmGNIiZpEAfXbl/h66FFpWy2Skt8mzmHc0B7kYG45RMRgdSXT7UY17dCsSxntjYiTwX15M7fF9fV/1kpR65be95opQoejDOLh0lGJpWlaptaqBsbegVzsVnp0kwpWIpHlscuoXYjzQ40IqWdggoYK2GomKvoM7iSEVHcuQi1YveIiF7Z19mS96IG6fB+oFLm7lnwSxgStk5/2twQ6EOyo5XHCA1IDMD0W0czsgd///TUPHR76ITT2nlhd6Kzt22a1g==

Hi all,

as already communicated to Gregory - but perhaps useful to say more widely: we now have the 64-bit part of the public ARMv8-A specification from ARM and Alastair Reid automatically translated into well-typed Sail (our ISA specification language), and thence into Isabelle/HOL and HOL4; we're currently working on a Sail-to-Coq backend. This ARM spec is fairly complete as far as the sequential architecture goes - it includes address translation and suchlike, though not all the system registers and debug architecture. More details at https://github.com/rems-project/sail. We also have Sail ISA specifications for RISC-V, MIPS, and CHERI, and for modest user-mode fragments of x86 and POWER.

best,

Peter

On 1 June 2018 at 18:12, Gregory Malecha <gmalecha AT gmail.com> 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.

Thanks so much.
--
- gregory malecha
gmalecha.github.io

[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