Hi seL4 devs,
I'm not sure whether this list is the right spot to ask about AutoCorres issues, but I gather you have some experience with that :-)
I'm currently working on proving that some CAmkES component behaves well wrt some higher- level specification. I want to prove this by simulation: Each step of my concrete CAmkES code corresponds to a step of some abstract machine. I've proven the behavioural lemmas as Hoare-triples using the validNF framework, and now want to lift the AutoCorres-generated executions to my higher-level representation.
I'm having issues with this however. Concretely, I want to be able to extract some resulting state after e.g. execution function f. For example:
I have the following triple:
{| P |} f {| Q |}!
Now given a state s such that P s is satisfied, I want to obtain some resulting state s' such that Q' _ s' holds. This is easy enough, as Isabelle has Hilbert's choice operator:
fun get_next_state where "get_next_state f s = SOME s'. s' : (snd ` fst (f s))"
Here is my problem: The choice operator only works when selecting from a non-empty set. I have a feeling that since I've shown that {P} f {Q} is a non-failing and valid hoare-triple this should somehow follow, but it doesn't. There is an easy counter-example:
{| top |} select {} {| toptop |}
This is a valid triple, however there are no valid executions for `select {}`. I have a feeling that this is the only counterexample though, since all other potential sources of empty executions are covered (namely nonterminating while loops, as they must always terminate in the validNF framework). If `select A` included a guard that A is non-empty, then I believe one could show that vaildNF P f Q implies exs_valid P f Q, although I'm not sure on this.
I've looked into the exs_valid framework, which proves exactly what I want. However, I have two issues with this:
1. I have already proven all the invariants I wanted in the validNF framework, and repeating these proofs seems redundant to me. 2. The exs_valid framework has very little utilities provided for use with the wp tool, which makes working with it more tedious than the validNF framework.
Another avenue I've looked at is using termination proofs from the SIMPL code: The AutoCorres ac_corres lemmas derived for my functions guarantee termination of the concrete SIMPL code if the abstract version does not fail, which I have proven. Since, as far as I understand it, the SIMPL layer has no problematic `select`-equivalent, termination should be sufficient to guarantee that a following state actually exists, and somehow lifting that guarantee to the AutoCorres layer. I haven't had success with this though.
Any help/pointers is appreciated. Thanks a lot in advance!
Cheers, Ben