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
_______________________________________________
Devel mailing list -- [email protected]
To unsubscribe send an email to [email protected]
