Hi Norrathep,

Norrathep Rattanavipanon wrote:
> I have been trying to generate Isabelle file from CapDL specification. But
> I run into an error when I'm running the command:
>
> ./parse-capDL --isabelle=out.thy --object-sizes=object_sizes.yaml
> example-arm.cdl
> 

We recently put in a major change to the Isabelle translator. The input
capDL file is now required to be pre-allocated, i.e. every object must
be placed in an untyped with a known physical address.

The existing example files date from before this change, and so they
don't meet the requirements to be translated into Isabelle.
Sorry that you got confusing error messages as a result. We plan to
make this more consistent in the near future.


> Is there any step I'm missing? Or does the tool not support the conversion
> to Isabelle?

The standard way is to build a CAmkES application with the option
`CAmkESCapDLStaticAlloc` enabled. This will generate a suitable capDL
file for proofs.

Based on your other question thread, you may be interested in our
README for CAmkES proofs:

  https://github.com/seL4/camkes-tool/tree/master/cdl-refine-tests

This generates proofs between the CAmkES high-level model and the capDL
system representation. However, we are not working on C glue code proofs
at the moment.


This is all work in progress, and quite rough around the edges.
Nevertheless, we're happy to try to answer any questions you might have.
It would help if we knew more about your work, so that we can give more
specific replies.

Cheers,
Japheth Lim
Proof Engineer, Trustworthy Systems