[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Axiom-developer] ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS

From: Tim Daly
Subject: [Axiom-developer] ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS
Date: Sun, 11 Nov 2018 19:09:53 -0500


This paper about ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS
is interesting. It seems to provide a "base case" for proving programs
correct. In particular, they seem to be able to generate proof code for
various provers, including Coq.

One of the criticisms about "proven programs" is that they tend to
ignore implementation details. But given a lisp variant, Milaw, that
is proven to the hardware instructions this new step is really important.

A proof of the machine instructions, a proof of milawa on top of those
instructions, a proof of lisp extensions on top of milawa, and a proof
of Axiom's spad language on top of lisp turns into a fully validated

It appears that all of this (and it is an impressive pile) can be developed
in Coq.

Also of interest, while I was part of the CMU CERT effort I developed
the ISA for the Intel 32 bit processor [0]. My program reads Intel binary
and generates "Conditional-Concurrent Assignment" semantics. I may
be able to re-target the back end to their Sail language which would
provide ISA semantics for Intel 32 in Coq.



Daly, Timothy Intel Instruction Semantics Generator SEI/CERT Research Report, March 2012

reply via email to

[Prev in Thread] Current Thread [Next in Thread]