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
_______________________________________________
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems
