On 6 Aug 2019, at 05:04, Norrathep Rattanavipanon <nrattana@uci.edu> wrote:

I believe this has already made it into the public master branch, but I haven’t checked. If I remember correctly, the rest of the capDL tool chain has had this ability for quite some time, the result would just not pass wellformedness verification.

 

So does it have any implication if it fails wellformedness verification?

Yes, wellformedness is the precondition for the capDL-initialiser proof to apply. If it fails that, there is no proof that the initial system state conforms to the capDL spec. It will happen to conform anyway, but you’d have no proof. That said, shared frames should no longer fail wellformedness in capDL. 

i.e., would I still be able to extend the Camkes proof to prove functional correctness of the component's code?

You could still do that separately, but you wouldn’t be able to connect the capDL and the CAmkES proofs. These proofs are not connected at the moment anyway (although we are working towards that).

 Btw, how can I access generated Isabelle theorems from Camkes. I'm using Camkes from the public master branch. I think I could access generated glue code and capdl C specification (e.g., for hello-camkes-1 example, it's in hello-camkes-1_build/capdl_spec.c) but I couldnt find any generated RPC stub and system initialization theorems.

I think I should leave that part of the answer to Japheth or someone else from the team, because this is currently in flux. We’re busy extending the whole setup to be more flexible so that it applies to more systems (i.e. useful systems). This also slightly changes how everything works together, how things are generated etc.

Cheers,

Gerwin