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