On Mon, Aug 5, 2019 at 3:26 PM Klein, Gerwin (Data61, Kensington NSW) < [email protected]> wrote:
> > On 6 Aug 2019, at 05:04, Norrathep Rattanavipanon <[email protected]> > 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. > I look forward to knowing that. I'm also interested in the C refinement proof (of the initializer) in CapDL. I tried to look into l4v repo in: https://github.com/seL4/l4v/tree/master/proof/crefine and https://github.com/seL4/l4v/blob/master/sys-ini. But I couldnt find it. If anyone can give me a pointer, I'd really appreciate it. > > Cheers, > Gerwin > > -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine
_______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
