cakeml icon indicating copy to clipboard operation
cakeml copied to clipboard

Published 20 hours ago • verified publisher icon CakeML

Target official ARM semantics

Open xrchz opened this issue 6 years ago • 2 comments

A version of the ARM ISA in Sail has been made available here. This model originates with ARM, so has some form of legitimacy. This issue is to add this model of ARM as a target for CakeML (possibly replacing one or more of our existing ARM targets).

xrchz avatar Jan 14 '19 05:01 xrchz

Sounds good. A first step would be to get a HOL export from sail into HOL/examples.

myreen avatar Jan 22 '19 10:01 myreen

Just to link the issues: The following issue is related to defining the very large records included in the current ARM model: HOL-Theorem-Prover/HOL#713. Currently, it takes over two hours to define the large records in the model.

AndreasLoow avatar Jul 01 '19 11:07 AndreasLoow