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
I've made some progress on this. I have decided to go with the below approach.
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.
This works great: The f'_ac_corres theorems which are derived from the f_body Simpl definition are exactly what I need. Together with hoaret_from_ac_corres I can derive a termination guarantee for f_body, which in turn implies the existence of a successor state (assuming non-failure of an abstract hoare triple {P} f {Q}).
However, this only works for functions without parameters. In Simpl, calling functions works by setting the arguments of the global state to the function's input parameters, running the function, and then restoring the global context. The AutoCorres-generated theorems only prove the termination of the actual `Call f` body, not the setup/teardown of the global state. Hence we get, for a function f with 0 parameters, returning int:
ac_corres (lift_global_heap ∘ globals) True Γ (sint ∘ ret__int_') ((λs. True) and (λx. True) ∘ lift_global_heap ∘ globals) (liftE controller_mut_lock') (Call controller_mut_lock_'proc)
thm hoaret_from_ac_corres[OF f'_ac_corres] ⦃?P⦄ liftE f' ⦃?Q⦄, ⦃λrv s. True⦄! ⟹ (⋀s. ?P ((lift_global_heap ∘ globals) s) ⟹ ((λs. True) and (λx. True) ∘ lift_global_heap ∘ globals) s) ⟹ True ⟹ Γ,?Θ⊢⇩t⇘/?F⇙ {s. ?P ((lift_global_heap ∘ globals) s)} Call f'proc {s. ?Q ((sint ∘ ret__int_') s) ((lift_global_heap ∘ globals) s)},?E
which trivially provable for some hoare triple {P} f {Q}!
However, for a function g with one parameter (returning nothing) we get:
ac_corres (lift_global_heap ∘ globals) True Γ (const ()) ((λs. x_' s = ?x') and (λx. abs_var ?x id ?x') ∘ lift_global_heap ∘ globals) (liftE (g' ?x)) (Call g'proc)
thm hoaret_from_ac_corres[OF g'_ac_corres] ⦃?P⦄ liftE (g' ?x) ⦃?Q⦄, ⦃λrv s. True⦄! ⟹ (⋀s. ?P ((lift_global_heap ∘ globals) s) ⟹ ((λs. x_' s = ?x'1) and (λx. abs_var ?x id ?x'1) ∘ lift_global_heap ∘ globals) s) ⟹ True ⟹ Γ,?Θ⊢⇩t⇘/?F⇙ {s. ?P ((lift_global_heap ∘ globals) s)} Call g'proc {s. ?Q () ((lift_global_heap ∘ globals) s)},?E
which leaves us with the following proof obligation after simplifying:
⋀s. ?P (lift_global_heap (globals s)) ⟹ x_' s = ?x
which is unprovable. If we on the other hand had this ac_corres theorem:
lemma i_wish_i_had_this: "ac_corres (lift_global_heap ∘ globals) True Γ (λs. ()) (const True) (liftE (g' x)) (CALL g(x))" sorry
then we can neatly derive termination for g, again given some abstract valid Hoare triple {P} g {Q}!
thm hoaret_from_ac_corres[OF i_wish_i_had_this] ⦃?P⦄ liftE (g' ?x) ⦃?Q⦄, ⦃λrv s. True⦄! ⟹ (⋀s. ?P ((lift_global_heap ∘ globals) s) ⟹ True) ⟹ True ⟹ Γ,?Θ⊢⇩t⇘/?F⇙ {s. ?P ((lift_global_heap ∘ globals) s)} CALL g'proc(?x) {s. ?Q () ((lift_global_heap ∘ globals) s)},?E
which simplifies neatly.
I have attempted reasoning about the CALL macro (?), however the reasoning tools for ac_corres are not fleshed out as well as the underlying ones, and I believe there would be some effort required to make it work. Additionally, each function may require a different unfolding, since the CALL notation handily hides the implementation differences of functions and procedures in the Simpl language. Since the AutoCorres layer has access to each function's implementation details, I believe this could be an easily automated step in addition to the function translation.
For now, I will sidestep the problem by rewriting my functions to not take any parameters, however I believe this will be helpful to end-users who aren't familiar with the AutoCorres/Simpl internals. Sadly, I don't see myself having enough time to implement this during the rest of my Master's thesis.
Anyway, I hope this helped anybody having the same problem as me.
Cheers, Ben
-
Ben Fiedler