Hi Norrathep, 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. There is currently no C-level proof of the initialiser, the proof is on the model level (model = spec of the initialiser) only. The initial plan was indeed to perform a refinement down towards C, but we have in the meantime changed plans and are looking into getting that implementation in CakeML instead, which comes with its own compiler proof and is hopefully much easier to connect to the initialiser semantics in Isabelle. This is ongoing work. Cheers, Gerwin
_______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
