Theory ModifiesProofs
theory ModifiesProofs
imports CLanguage
begin
definition
modifies_inv_refl :: "('a ⇒ 'a set) ⇒ bool"
where
"modifies_inv_refl P ≡ ∀x. x ∈ P x"
definition
modifies_inv_incl :: "('a ⇒ 'a set) ⇒ bool"
where
"modifies_inv_incl P ≡ ∀x y. y ∈ P x ⟶ P y ⊆ P x"
definition
modifies_inv_prop :: "('a ⇒ 'a set) ⇒ bool"
where
"modifies_inv_prop P ≡ modifies_inv_refl P ∧ modifies_inv_incl P"
lemma modifies_inv_prop:
"modifies_inv_refl P ⟹ modifies_inv_incl P ⟹ modifies_inv_prop P"
by (simp add: modifies_inv_prop_def)
named_theorems modifies_inv_intros
locale modifies_assertion =
fixes P :: "'s ⇒ 's set"
assumes p: "modifies_inv_prop P"
begin
lemmas modifies_inv_prop' =
p[unfolded modifies_inv_prop_def modifies_inv_refl_def modifies_inv_incl_def]
lemma modifies_inv_prop_lift:
assumes c: "⋀σ. Γ,Θ⊢⇘/F⇙ {σ} c (P σ),(P σ)"
shows "Γ,Θ⊢⇘/F⇙ (P σ) c (P σ),(P σ)"
using modifies_inv_prop' by (fastforce intro: c hoarep.Conseq)
lemma modifies_inv_prop_lower:
assumes c: "⋀σ. Γ,Θ⊢⇘/F⇙ (P σ) c (P σ),(P σ)"
shows "Γ,Θ⊢⇘/F⇙ {σ} c (P σ),(P σ)"
using modifies_inv_prop' by (fastforce intro: c hoarep.Conseq)
text ‹Note that the C-Parser associates sequential composition to the right. So the first statement
is typically already an 'atomic' statement (or at least no further sequential composition)
that can be solved. We place it as the second precondition because the modifies-tactic follows the
canonical order of tactical reasoning and solves the subgoals from the back.
So \<^term>‹c1› is already solved before further decomposing \<^term>‹c2›. This keeps
the number of subgoals (and thus the overall goal-state) small.
›
lemma modifies_inv_Seq [modifies_inv_intros]:
assumes c: "⋀σ. Γ,Θ⊢⇘/F⇙ {σ} c2 (P σ),(P σ)" "⋀σ. Γ,Θ⊢⇘/F⇙ {σ} c1 (P σ),(P σ)"
shows "Γ,Θ⊢⇘/F⇙ {σ} c1 ;; c2 (P σ),(P σ)"
by (intro modifies_inv_prop_lower HoarePartial.SeqSwap[OF c[THEN modifies_inv_prop_lift]])
lemma modifies_inv_Cond [modifies_inv_intros]:
assumes c: "⋀σ. Γ,Θ⊢⇘/F⇙ {σ} c1 (P σ),(P σ)" "⋀σ. Γ,Θ⊢⇘/F⇙ {σ} c2 (P σ),(P σ)"
shows "Γ,Θ⊢⇘/F⇙ {σ} Cond b c1 c2 (P σ),(P σ)"
by (auto intro: HoarePartial.Cond c)
lemma modifies_inv_Guard_strip [modifies_inv_intros]:
assumes c: "⋀σ. Γ,Θ⊢⇘/UNIV⇙ {σ} c (P σ),(P σ)"
shows "Γ,Θ⊢⇘/UNIV⇙ {σ} Guard f b c (P σ),(P σ)"
by (rule HoarePartial.GuardStrip[OF subset_refl c UNIV_I])
lemma modifies_inv_Skip [modifies_inv_intros]:
shows "Γ,Θ⊢⇘/F⇙ {σ} SKIP (P σ),(P σ)"
using modifies_inv_prop' by (auto intro: modifies_inv_prop_lift HoarePartial.Skip)
lemma modifies_inv_Skip' [modifies_inv_intros]:
shows "Γ,Θ⊢⇘/F⇙ {σ} SKIP (P σ)"
using modifies_inv_prop' by (auto intro: modifies_inv_prop_lift HoarePartial.Skip)
lemma modifies_inv_whileAnno [modifies_inv_intros]:
assumes c: "⋀σ. Γ,Θ⊢⇘/F⇙ {σ} c (P σ),(P σ)"
shows "Γ,Θ⊢⇘/F⇙ {σ} whileAnno b I V c (P σ),(P σ)"
apply (rule HoarePartial.reannotateWhileNoGuard[where I="P σ"])
by (intro HoarePartial.While hoarep.Conseq;
fastforce simp: modifies_inv_prop' intro: modifies_inv_prop_lift c)
lemma modifies_inv_While [modifies_inv_intros]:
assumes c: "⋀σ. Γ,Θ⊢⇘/F⇙ {σ} c (P σ),(P σ)"
shows "Γ,Θ⊢⇘/F⇙ {σ} While b c (P σ),(P σ)"
by (intro modifies_inv_whileAnno[unfolded whileAnno_def] c)
lemma modifies_inv_Throw [modifies_inv_intros]:
shows "Γ,Θ⊢⇘/F⇙ {σ} THROW (P σ),(P σ)"
using modifies_inv_prop' by (auto intro: modifies_inv_prop_lift HoarePartial.Throw)
lemma modifies_inv_Catch [modifies_inv_intros]:
assumes c: "⋀σ. Γ,Θ⊢⇘/F⇙ {σ} c1 (P σ),(P σ)"
"⋀σ. Γ,Θ⊢⇘/F⇙ {σ} c2 (P σ),(P σ)"
shows "Γ,Θ⊢⇘/F⇙ {σ} TRY c1 CATCH c2 END (P σ),(P σ)"
by (intro modifies_inv_prop_lower HoarePartial.Catch[OF c[THEN modifies_inv_prop_lift]])
lemma modifies_inv_Catch_all [modifies_inv_intros]:
assumes 1: "⋀σ. Γ,Θ⊢⇘/F⇙ {σ} c1 (P σ),(P σ)"
assumes 2: "⋀σ. Γ,Θ⊢⇘/F⇙ {σ} c2 (P σ)"
shows "Γ,Θ⊢⇘/F⇙ {σ} TRY c1 CATCH c2 END (P σ)"
apply (intro HoarePartial.Catch[OF 1] hoarep.Conseq, clarsimp)
apply (metis modifies_inv_prop' 2 singletonI)
done
lemma modifies_inv_switch_Nil [modifies_inv_intros]:
shows "Γ,Θ⊢⇘/F⇙ {σ} switch v [] (P σ),(P σ)"
by (auto intro: modifies_inv_Skip)
lemma modifies_inv_switch_Cons [modifies_inv_intros]:
assumes c: "⋀σ. Γ,Θ⊢⇘/F⇙ {σ} c (P σ),(P σ)"
"⋀σ. Γ,Θ⊢⇘/F⇙ {σ} switch p vcs (P σ),(P σ)"
shows "Γ,Θ⊢⇘/F⇙ {σ} switch p ((v,c) # vcs) (P σ),(P σ)"
by (auto intro: c modifies_inv_Cond)
end
locale modifies_state_assertion = modifies_assertion P for
P :: "('g, 'l, 'e, 'x) state_scheme ⇒ ('g, 'l, 'e, 'x) state_scheme set" +
assumes p: "modifies_inv_prop P"
begin
lemma modifies_inv_creturn [modifies_inv_intros]:
assumes c: "⋀σ. Γ,Θ⊢⇘/F⇙ {σ} Basic (λs. xfu (λ_. v s) s) (P σ),(P σ)"
"⋀σ. Γ,Θ⊢⇘/F⇙ {σ} Basic (rtu (λ_. Return)) (P σ),(P σ)"
shows "Γ,Θ⊢⇘/F⇙ {σ} creturn rtu xfu v (P σ),(P σ)"
unfolding creturn_def by (intro p c modifies_inv_intros)
lemma modifies_inv_creturn_void [modifies_inv_intros]:
assumes c: "⋀σ. Γ,Θ⊢⇘/F⇙ {σ} Basic (rtu (λ_. Return)) (P σ),(P σ)"
shows "Γ,Θ⊢⇘/F⇙ {σ} creturn_void rtu (P σ),(P σ)"
unfolding creturn_void_def by (intro p c modifies_inv_intros)
lemma modifies_inv_cbreak [modifies_inv_intros]:
assumes c: "⋀σ. Γ,Θ⊢⇘/F⇙ {σ} Basic (rtu (λ_. Break)) (P σ),(P σ)"
shows "Γ,Θ⊢⇘/F⇙ {σ} cbreak rtu (P σ),(P σ)"
unfolding cbreak_def by (intro p c modifies_inv_intros)
lemma modifies_inv_ccatchbrk [modifies_inv_intros]:
shows "Γ,Θ⊢⇘/F⇙ {σ} ccatchbrk rt (P σ),(P σ)"
unfolding ccatchbrk_def by (intro p modifies_inv_intros)
lemma modifies_inv_cgoto [modifies_inv_intros]:
assumes c: "⋀σ. Γ,Θ⊢⇘/F⇙ {σ} Basic (rtu (λ_. Goto l)) (P σ),(P σ)"
shows "Γ,Θ⊢⇘/F⇙ {σ} cgoto l rtu (P σ),(P σ)"
unfolding cgoto_def by (intro p c modifies_inv_intros)
lemma modifies_inv_ccatchgoto [modifies_inv_intros]:
shows "Γ,Θ⊢⇘/F⇙ {σ} ccatchgoto l rt (P σ),(P σ)"
unfolding ccatchgoto_def by (intro p modifies_inv_intros)
lemma modifies_inv_ccatchreturn [modifies_inv_intros]:
shows "Γ,Θ⊢⇘/F⇙ {σ} ccatchreturn rt (P σ),(P σ)"
unfolding ccatchreturn_def by (intro p modifies_inv_intros)
end
lemma On_Exit_wp:
assumes cleanup: "Γ,Θ⊢⇘/F⇙ R cleanup Q, A"
assumes cleanup_catch: "Γ,Θ⊢⇘/F⇙ B cleanup A, A"
assumes c: "Γ,Θ⊢⇘/F⇙ P c R, B"
shows "Γ,Θ⊢⇘/F⇙ P On_Exit c cleanup Q, A"
unfolding On_Exit_def
apply (rule HoarePartial.SeqSwap [where R=R])
apply (rule HoarePartial.conseq_no_aux)
apply (rule cleanup)
apply simp
apply (rule HoarePartial.Catch)
apply (rule c)
apply (rule HoarePartial.SeqSwap )
apply (rule HoarePartial.Throw)
apply (rule subset_refl)
apply (rule cleanup_catch)
done
lemma DynCom_fix_pre: "∀s ∈ P. Γ,Θ⊢⇘/F⇙ {s} (c s) Q,A
⟹
Γ,Θ⊢⇘/F⇙ P (DynCom c) Q,A"
by (smt (verit, best) HoarePartial.conseq_exploit_pre Int_insert_left_if1 hoarep.DynCom inf_bot_left singletonD)
lemma "Γ,Θ⊢⇘/F ⇙{s. (∀t. (s, t) ∈ r ⟶ t ∈ Q) ∧ (∃t. (s, t) ∈ r)} Spec r Q,A"
by (rule hoarep.Spec)
lemma hoarep_Spec_fixed: "(∃t. (s, t) ∈ r) ⟹ Γ,Θ⊢⇘/F⇙{s} Spec r {t. (s, t) ∈ r},A"
by (simp add: HoarePartial.Spec)
context stack_heap_state
begin
lemma With_Fresh_Stack_Ptr_tight:
assumes c: "⋀s p d vs bs. s ∈ P ⟹ vs ∈ init s ⟹ length vs = n ⟹ length bs = n * size_of TYPE('a) ⟹
(p, d) ∈ stack_allocs n 𝒮 TYPE('a::mem_type) (htd s) ⟹
Γ,Θ⊢⇘/F⇙{hmem_upd (fold (λi. heap_update_padding (p +⇩p int i) (vs!i) (take (size_of TYPE('a)) (drop (i * size_of TYPE('a)) bs))) [0..<n]) (htd_upd (λ_. d) s)}
(c p)
{t. ∀bs. length bs = n * size_of TYPE('a) ⟶ hmem_upd (heap_update_list (ptr_val p) bs) (htd_upd (stack_releases n p) t) ∈ Q},
{t. ∀bs. length bs = n * size_of TYPE('a) ⟶ hmem_upd (heap_update_list (ptr_val p) bs) (htd_upd (stack_releases n p) t) ∈ A}"
assumes no_overflow: "StackOverflow ∈ F"
shows "Γ,Θ⊢⇘/F⇙ P With_Fresh_Stack_Ptr n init c Q, A"
unfolding With_Fresh_Stack_Ptr_def
apply (rule hoarep.Guarantee [OF no_overflow])
apply (rule DynCom_fix_pre)
apply (rule ballI)
apply clarsimp
apply (rule HoarePartial.Seq)
apply (rule hoarep_Spec_fixed)
apply clarsimp
subgoal using Ex_list_of_length
by (metis equals0I old.prod.exhaust)
apply clarsimp
apply (rule DynCom_fix_pre)
apply (rule ballI)
apply clarsimp
apply (rule On_Exit_wp)
apply (rule HoarePartial.Spec)
apply (rule subset_refl)
apply (rule HoarePartial.Spec)
apply (rule subset_refl)
subgoal premises prems for s vs p d' vsa bs
proof -
have eq1: "length vs = n" using prems by simp
have eq2:"(allocated_ptrs n 𝒮 TYPE('a) (htd s) d') = p" using prems by (simp add: stack_allocs_allocated_ptrs)
show ?thesis
apply (simp add: eq1 eq2 Ex_list_of_length)
apply (rule HoarePartialDef.conseqPost [OF c [where s1=s and vs1=vsa and d1=d' and p1=p]])
using prems
apply auto
done
qed
done
lemma With_Fresh_Stack_Ptr_tight_wp:
assumes conseq: "⋀s p d vs bs. s ∈ P ⟹ vs ∈ init s ⟹ length vs = n ⟹ length bs = n * size_of TYPE('a) ⟹
(p, d) ∈ stack_allocs n 𝒮 TYPE('a::mem_type) (htd s) ⟹
(hmem_upd (fold (λi. heap_update_padding (p +⇩p int i) (vs!i) (take (size_of TYPE('a)) (drop (i * size_of TYPE('a)) bs))) [0..<n]) (htd_upd (λ_. d) s)) ∈ R s p d vs"
assumes c: "⋀s p d vs bs. s ∈ P ⟹ vs ∈ init s ⟹ length vs = n ⟹ length bs = n * size_of TYPE('a) ⟹
(p, d) ∈ stack_allocs n 𝒮 TYPE('a::mem_type) (htd s) ⟹
(hmem_upd (fold (λi. heap_update_padding (p +⇩p int i) (vs!i) (take (size_of TYPE('a)) (drop (i * size_of TYPE('a)) bs))) [0..<n]) (htd_upd (λ_. d) s)) ∈ R s p d vs ⟹
Γ,Θ⊢⇘/F⇙(R s p d vs) (c p)
{t. ∀bs. length bs = n * size_of TYPE('a) ⟶ hmem_upd (heap_update_list (ptr_val p) bs) (htd_upd (stack_releases n p) t) ∈ Q},
{t. ∀bs. length bs = n * size_of TYPE('a) ⟶ hmem_upd (heap_update_list (ptr_val p) bs) (htd_upd (stack_releases n p) t) ∈ A}"
assumes no_overflow: "StackOverflow ∈ F"
shows "Γ,Θ⊢⇘/F⇙ P With_Fresh_Stack_Ptr n init c Q, A"
apply (rule With_Fresh_Stack_Ptr_tight [OF _ no_overflow])
subgoal for s p d vs bs
apply (rule HoarePartial.conseq)
apply (rule allI)
apply (rule c[where s1=s and vs1=vs and d1=d])
apply assumption
apply assumption
apply assumption
apply assumption
apply assumption
apply (rule conseq)
apply assumption
apply assumption
apply assumption
apply assumption
apply clarsimp
subgoal premises prems
proof -
from prems have eq: "length vs = n" by simp
show ?thesis
apply (simp add: eq)
apply (rule conseq)
using prems by auto
qed
done
done
text ‹Caution: this WP-setup was developed to solve the modified clauses. It might not be the
best fit for WP-style reasoning in general. Also note that it is currently not
invoked by the automatic modifies-proofs triggerd by the C-parser as \<^const>‹With_Fresh_Stack_Ptr› is
first decomposed by the @{thm modifies_inv_intros} (see the rule below).›
declaration ‹fn phi =>
let
val rule = Morphism.thm phi @{thm With_Fresh_Stack_Ptr_tight}
fun tac cont_tac ctxt mode i =
resolve_tac ctxt [rule] i THEN
SOLVED_verbose "no_overflow" ctxt (simp_tac ctxt) (i + 1) THEN
cont_tac true i
in
Hoare.add_hoare_tacs [("With_Fresh_Stack_Ptr_tac", tac)]
end
›
end
locale modifies_assertion_stack_heap_state =
modifies_assertion P + stack_heap_state htd htd_upd hmem hmem_upd 𝒮
for P::"'s ⇒ 's set" and
htd:: "'s ⇒ heap_typ_desc" and
htd_upd:: "(heap_typ_desc ⇒ heap_typ_desc) ⇒ 's ⇒ 's" and
hmem:: "'s ⇒ heap_mem" and
hmem_upd:: "(heap_mem ⇒ heap_mem) ⇒ 's ⇒ 's" and
𝒮::"addr set" +
assumes hmem_upd_inv: "⋀σ m. hmem_upd m σ ∈ (P σ)"
assumes htd_upd_inv: "⋀σ d. htd_upd d σ ∈ (P σ)"
begin
lemma modifies_With_Fresh_Stack_Ptr [modifies_inv_intros]:
assumes no_overflow: "StackOverflow ∈ F"
assumes c: "⋀σ p. Γ,Θ⊢⇘/F⇙ {σ} (c (p::'a::mem_type ptr)) (P σ),(P σ)"
shows "Γ,Θ⊢⇘/F⇙ {σ} With_Fresh_Stack_Ptr n init c (P σ), (P σ)"
apply (rule With_Fresh_Stack_Ptr_tight_wp [where R = "λ s p d v. P s"])
subgoal for s p d vs bs
proof -
have "(htd_upd (λ_. d) s) ∈ P s" by (rule htd_upd_inv)
moreover have "hmem_upd (fold (λi. heap_update_padding (p +⇩p int i) (vs!i) (take (size_of TYPE('a)) (drop (i * size_of TYPE('a)) bs))) [0..<n]) (htd_upd (λ_. d) s) ∈ P (htd_upd (λ_. d) s)"
by (rule hmem_upd_inv)
ultimately
show "hmem_upd (fold (λi. heap_update_padding (p +⇩p int i) (vs!i) (take (size_of TYPE('a)) (drop (i * size_of TYPE('a)) bs))) [0..<n]) (htd_upd (λ_. d) s) ∈ P s"
using modifies_inv_prop' p by blast
qed
subgoal for s p d v
apply (rule HoarePartial.conseq [where P'=P and Q'=P and A'=P])
apply (rule allI)
subgoal for Z
apply (rule modifies_inv_prop_lift)
apply (rule c)
done
using modifies_inv_prop' hmem_upd_inv htd_upd_inv
by (smt (verit, best) mem_Collect_eq singletonD subset_eq)
apply (rule no_overflow)
done
end
locale modifies_assertion_stack_heap_raw_state =
modifies_assertion P + stack_heap_raw_state t_hrs t_hrs_update 𝒮
for P::"'s ⇒ 's set" and
t_hrs:: "'s ⇒ heap_raw_state" and
t_hrs_update:: "(heap_raw_state ⇒ heap_raw_state) ⇒ 's ⇒ 's" and
𝒮::"addr set" +
assumes hrs_upd_inv: "⋀σ m. t_hrs_update m σ ∈ (P σ)"
begin
sublocale modifies_assertion_stack_heap_state
P
"λs. hrs_htd (t_hrs s)" "λupd. t_hrs_update (hrs_htd_update upd)"
"λs. hrs_mem (t_hrs s)" "λupd. t_hrs_update (hrs_mem_update upd)"
"𝒮"
using hrs_upd_inv by unfold_locales auto
end
end