theory Step_Prime
imports
Step_External
Misc_Aux
begin
section ‹Draft›
subsection ‹Dropping frames›
definition drop_frames where
"drop_frames k cs = update_frames (λfs. drop_tail k fs) cs"
subsection ‹Extending small_step›
context small_step
begin
lemmas simps =
run_instruction.simps
update_frames_stack.simps
update_frame.simps
terminate_frame_def
ret_from_frame.simps
call_function.simps
enter_frame.simps
definition terminate_frame' :: "terminator named ⇒ llvm_state error" where
"terminate_frame' t = do {
(case named_instruction t of
Ret (Some o1) ⇒ do {c ← operand_value o1;
error (ReturnValue c)}
| _ ⇒ terminate_frame t)}"
lemma terminate_frame':
assumes "∄o1. named_instruction t = Ret (Some o1)"
shows "terminate_frame' t = terminate_frame t"
using assms
by (auto simp add: terminate_frame'_def split: option.splits named.splits terminator.splits)
end
subsection ‹step relation with sum type instead of @{term llvm_state}}›
definition step_rel_e :: "llvm_prog ⇒ (stuck + llvm_state) rel" where
"step_rel_e prog = { (bef, aft) . bef ⤜ step prog = aft }"
lemma step_relation_step_rel_e:
assumes "(cs⇩1, cs⇩n) ∈ step_relation prog"
shows "(Inr cs⇩1, Inr cs⇩n) ∈ step_rel_e prog"
using assms unfolding step_relation_def step_rel_e_def by (auto simp del: step.simps)
lemma step_relation_step_rel_e_trancl:
assumes "(cs⇩1, cs⇩n) ∈ (step_relation prog)⇧+"
shows "(Inr cs⇩1, Inr cs⇩n) ∈ (step_rel_e prog)⇧+"
using assms by (induction cs⇩1 cs⇩n rule: trancl.induct)
(use step_relation_step_rel_e in ‹auto intro: trancl.intros›)
lemma step_relation_step_rel_e_rtrancl:
assumes "(cs⇩1, cs⇩n) ∈ (step_relation prog)⇧*"
shows "(Inr cs⇩1, Inr cs⇩n) ∈ (step_rel_e prog)⇧*"
using assms by (induction cs⇩1 cs⇩n rule: rtrancl.induct)
(use step_relation_step_rel_e in ‹auto intro: rtrancl.intros›)
subsection ‹step' semantics›
inductive step_call for prog s f fs n t g ps s' where
"step_call prog s f fs n t g ps s'"
if "small_step.call_external_function prog s f fs g ps n s'"
| "step_call prog s f fs n t g ps s'"
if "Inr f' = small_step.enter_frame prog f g ps"
"(Inr (update_frames (λ_. [f']) s), Inl (ReturnValue c)) ∈ (step_rel_e prog)⇧+"
"s' = small_step.update_frames_stack s f fs n (Inr c)"
definition step' :: "llvm_prog ⇒ llvm_state ⇒ llvm_state error ⇒ bool" where
"step' prog s s' = (case frames s of
(f#fs) ⇒
(case find_statement prog (frame.pos f)
of Inr (Terminator t) ⇒ s' = small_step.terminate_frame' prog s f fs t
| Inr (Instruction (Named n (Call t g ps))) ⇒ step_call prog s f fs n t g ps s'
| _ ⇒ s' = step prog s)
| [] ⇒ s' = step prog s)"
definition step'_relation :: "llvm_prog ⇒ llvm_state rel" where
"step'_relation prog = {(bef, aft) . step' prog bef (Inr aft)}"
subsection ‹Stack size›
definition stack_size where
"stack_size cs = length (frames cs)"
lemma stack_size_non_call:
assumes
"∄n t g ps. find_statement prog (frame.pos (hd (frames cs⇩1))) = Inr (Instruction (Named n (Call t g ps)))"
"step prog cs⇩1 = Inr cs⇩2"
shows
"stack_size cs⇩1 ≥ stack_size cs⇩2"
using assms by (auto split: list.splits option.splits action.splits named.splits instruction.splits
sum_bind_splits prod.splits terminator.splits sum.splits simp add: small_step.simps stack_size_def
elim!: option_to_sum.elims)
definition is_call where
"is_call prog s = (case frames s of
(f#fs) ⇒
(case find_statement prog (frame.pos f)
of Inr (Instruction (Named n (Call t g ps))) ⇒ True
| _ ⇒ False)
| [] ⇒ False)"
locale inf_run =
fixes cs :: "nat ⇒ llvm_state" and prog :: "llvm_prog"
assumes inf_run: "step prog (cs i) = Inr (cs (Suc i))"
begin
subsection ‹Stack size in an infinite chain of steps›
definition s⇩c⇩s where
"s⇩c⇩s x = stack_size (cs x)"
lemma stack_never_empty: "0 < s⇩c⇩s i"
using inf_run[of i] by (auto simp add: stack_size_def s⇩c⇩s_def)
definition min_stack_size where "min_stack_size = (LEAST i. i ∈ range s⇩c⇩s)"
lemma min_stack_size: "min_stack_size ≤ s⇩c⇩s i"
unfolding min_stack_size_def by (auto intro!: Least_le)
definition k⇩m⇩i⇩n where "k⇩m⇩i⇩n = (LEAST k. s⇩c⇩s k = min_stack_size)"
lemma k_min_stack_size: "s⇩c⇩s k⇩m⇩i⇩n = min_stack_size"
proof -
have "∃x. s⇩c⇩s x = min_stack_size"
by (smt LeastI comp_apply min_stack_size_def rangeE range_eqI)
then show ?thesis
unfolding k⇩m⇩i⇩n_def by (rule LeastI_ex)
qed
lemma stack_size_dec_inc:
"s⇩c⇩s (Suc i) ∈ {s⇩c⇩s i, s⇩c⇩s i + 1, s⇩c⇩s i - 1}"
proof -
show ?thesis
unfolding s⇩c⇩s_def
using inf_run[of i, symmetric]
by (auto split: list.splits option.splits action.splits named.splits
instruction.splits sum.splits llvm_fun.splits sum_bind_splits prod.splits terminator.splits
simp add: frames_simp small_step.simps stack_size_def elim!: option_to_sum.elims)
qed
lemma stack_size_IVT: "∃j ≤ l. s⇩c⇩s (k + j) = s⇩c⇩s k - 1" if "s⇩c⇩s (k + l) < s⇩c⇩s k"
using that proof (induction l)
case (Suc l)
consider "s⇩c⇩s (k + Suc l) = s⇩c⇩s (k + l)"
| "s⇩c⇩s (k + Suc l) = s⇩c⇩s (k + l) + 1"
| "s⇩c⇩s (k + Suc l) = s⇩c⇩s (k + l) - 1"
using stack_size_dec_inc by auto
then show ?case
proof cases
case 1
then show ?thesis
using Suc nat_less_le by fastforce
next
case 2
then show ?thesis
using Suc le_SucI add_lessD1 by (metis)
next
case 3
then consider "local.s⇩c⇩s (k + l) = local.s⇩c⇩s k" | "local.s⇩c⇩s (k + l) < local.s⇩c⇩s k"
using Suc by arith
then show ?thesis
using Suc 3 le_SucI by (cases) (auto, use le_SucI in blast)
qed
qed (auto)
lemma stack_size_eq_call:
assumes "is_call prog (cs j)" "j < k" "s⇩c⇩s k < s⇩c⇩s j"
shows "∃i. j < i ∧ i < k ∧ s⇩c⇩s j = s⇩c⇩s i"
proof -
have 1: "s⇩c⇩s (j + 1) = s⇩c⇩s j + 1"
unfolding s⇩c⇩s_def using inf_run[of j, symmetric] assms
by (auto split: list.splits option.splits action.splits named.splits
instruction.splits llvm_fun.splits sum_bind_splits sum.splits
simp add: is_call_def small_step.simps stack_size_def)
then have "local.s⇩c⇩s (j + 1 + (k - j - 1)) < local.s⇩c⇩s (j + 1)"
using assms by auto
then obtain i where i: "i≤k - j - 1" "s⇩c⇩s (j + 1 + i) = s⇩c⇩s (j + 1) - 1"
using stack_size_IVT by blast
then have "j < j + 1 + i" "j + 1 + i < k" "s⇩c⇩s (j + 1 + i) = s⇩c⇩s j"
using 1 assms nat_neq_iff by fastforce+
then show ?thesis
by metis
qed
subsection ‹Reindexing infinite chain of steps to infinite chain of step'›
fun r :: "nat ⇒ nat" where
"r 0 = k⇩m⇩i⇩n"
| "r (Suc i) = (
let j = r i in
if ¬ is_call prog (cs j)
then j + 1
else if (∀j' > j. stack_size (cs j) < stack_size (cs j'))
then j + 1
else (LEAST j'. j' > j ∧ stack_size (cs j) = stack_size (cs j')))"
subsection ‹Stack size only increases in @{term r}›
lemma i_leq_r_i: "i ≤ r i"
proof (induction i)
case (Suc i)
then have 1: ?case if "r i < j" "s⇩c⇩s j ≤ s⇩c⇩s (r i)" "is_call prog (cs (local.r i))" for j
proof -
let ?P = "λj'. r i < j' ∧ s⇩c⇩s (r i) = s⇩c⇩s j'"
have "?P (LEAST j. ?P j)"
by (rule LeastI_ex) (use stack_size_eq_call that in fastforce)
then show ?thesis
using that Suc unfolding s⇩c⇩s_def by (auto simp add: Let_def)
qed
moreover have "¬ (∀j'>local.r i. stack_size (cs (local.r i)) < stack_size (cs j'))"
if "r i < j" "s⇩c⇩s j ≤ s⇩c⇩s (r i)" "is_call prog (cs (local.r i))" for j
using that using leD unfolding s⇩c⇩s_def by (clarsimp) fastforce
ultimately show ?case
unfolding s⇩c⇩s_def using Suc by (auto simp add: Let_def split: if_splits)
qed (auto)
lemma r_strictly_monotone': "r i < r (Suc i)"
apply(auto simp add: Let_def)
using LeastI linorder_neqE_nat s⇩c⇩s_def stack_size_eq_call by smt
lemma r_strictly_monotone: "r i < r j" if "i < j"
using that by (induction j) (use Suc that lift_Suc_mono_less r_strictly_monotone' in blast)+
lemma s⇩c⇩s_inc:
assumes "i < j"
shows "s⇩c⇩s (r i) ≤ s⇩c⇩s (r j)"
using assms proof (induction i arbitrary: j)
case 0
then show ?case by (auto simp add: k_min_stack_size min_stack_size)
next
case (Suc i k)
define s where "s x = stack_size (cs (r x))" for x
define j where "j = r i"
let ?P = "(∀j' > j. stack_size (cs j) < stack_size (cs j'))"
have ?case if "is_call prog (cs j)" "?P"
proof -
have 1: "s (i + 1) = s i + 1"
proof -
have "s (i + 1) = stack_size (cs (j + 1))"
using that unfolding s_def j_def by (auto simp add: Let_def)
also have "… = stack_size (cs j) + 1"
using inf_run[of j, symmetric] that
by (auto split: list.splits option.splits action.splits named.splits
instruction.splits llvm_fun.splits sum_bind_splits sum.splits
simp add: is_call_def small_step.simps stack_size_def)
finally show ?thesis
unfolding s_def j_def s⇩c⇩s_def by simp
qed
show ?thesis
proof -
have "j < r k"
unfolding j_def
apply(rule r_strictly_monotone)
using Suc by simp
then have "stack_size (cs j) < stack_size (cs (r k))"
using that by blast
then show ?thesis
using 1 unfolding s_def j_def s⇩c⇩s_def by simp
qed
qed
moreover have ?case if "¬ is_call prog (cs j)"
proof -
have a: "local.r (i + 1) = j + 1"
using Suc_eq_plus1 j_def r.simps(2) that by presburger
have b: False if "frames (cs (r i)) = fs1 # fs2 # fs3"
"cs (Suc (r i)) = Llvm_state (update_pos inc_pos (small_step.update_stack fs2 n v) # fs3)"
for fs1 fs2 fs3 n v
proof -
have "length (frames (cs (Suc (local.r i)))) = Suc (length fs3)"
using that by simp
then show False
using that Suc(1)[of "Suc i"] a Suc_eq_plus1 Suc_n_not_le_n j_def length_nth_simps(2)
less_add_one s⇩c⇩s_def stack_size_def by (metis)
qed
then have "s (i + 1) = s i"
using that using inf_run[of j, symmetric]
unfolding s_def
by (auto split: list.splits option.splits action.splits named.splits
instruction.splits llvm_fun.splits sum_bind_splits prod.splits terminator.splits sum.splits
simp add: is_call_def stack_size_def s_def Let_def j_def small_step.simps
intro: named.exhaust)
(metis instruction.distinct named.exhaust)+
then show ?thesis
using Suc that unfolding s_def s⇩c⇩s_def by auto
qed
moreover have ?case if "is_call prog (cs j)" "¬ ?P"
proof -
have "s (i + 1) = s i"
using that unfolding s_def apply(auto simp add: Let_def j_def)
unfolding j_def[symmetric]
apply(rule LeastI_ex)
using stack_size_eq_call
by (metis (mono_tags, lifting) LeastI_ex nat_neq_iff s⇩c⇩s_def that(1))
then show ?thesis
using Suc that unfolding s_def s⇩c⇩s_def by auto
qed
ultimately show ?case
by blast
qed
subsection ‹No return statements encountered in reindexing›
lemma r_no_return:
assumes "find_statement prog (frame.pos (hd (frames (cs (r i))))) = Inr (Terminator x)"
"named_instruction x = Ret t"
shows False
proof -
have *: "r (Suc i) = Suc (r i)"
unfolding s⇩c⇩s_def using assms by (auto simp add: Let_def is_call_def split: list.splits)
have "s⇩c⇩s (r (Suc i)) = s⇩c⇩s (r i) - 1"
unfolding * s⇩c⇩s_def using inf_run[of "r i", symmetric] assms
by (auto simp del: r.simps split: list.splits option.splits sum_bind_splits
instruction.splits action.splits named.splits
simp add: small_step.simps stack_size_def elim!: option_to_sum.elims)
then show False
using s⇩c⇩s_inc[of i "Suc i"] unfolding s⇩c⇩s_def
by (auto simp del: r.simps) (metis less_irrefl_nat s⇩c⇩s_def stack_never_empty)
qed
lemma drop_frames_step:
assumes "k < stack_size cs⇩1" "k < stack_size cs⇩2" "step prog cs⇩1 = Inr cs⇩2"
shows "step prog (drop_frames k cs⇩1) = Inr (drop_frames k cs⇩2)"
using assms map_of_funs_name
apply (auto simp add: small_step.simps stack_size_def drop_frames_def drop_tail_def split: list.splits option.splits
action.splits named.splits terminator.splits instruction.splits prod.splits sum_bind_splits)
apply(auto split: sum.splits)
by (auto simp add: small_step.simps stack_size_def drop_frames_def drop_tail_def split: list.splits option.splits
action.splits llvm_fun.splits named.splits terminator.splits instruction.splits prod.splits sum_bind_splits)
lemma take_frames_step:
assumes "k < stack_size cs⇩1" "k < stack_size cs⇩2" "step prog cs⇩1 = Inr cs⇩2"
shows "take_tail k (frames cs⇩1) = take_tail k (frames cs⇩2)"
using assms
by (auto simp add: take_tail_Cons small_step.simps stack_size_def drop_frames_def drop_tail_def split: list.splits option.splits
action.splits llvm_fun.splits named.splits terminator.splits instruction.splits prod.splits sum_bind_splits sum.splits if_splits)
lemma drop_frames_step_plus:
assumes
"∀l < n. step prog (ds l) = Inr (ds (Suc l))"
"∀l ≤ n. k < stack_size (ds l)"
shows
"(drop_frames k (ds 0), drop_frames k (ds n)) ∈ (step_relation prog)⇧*"
using assms proof (induction n)
case 0
then show ?case
by simp
next
case (Suc n)
show ?case
apply(rule rtrancl.intros(2))
apply(rule Suc)
using Suc apply(simp)
using Suc apply(simp)
unfolding step_relation_def
apply(simp del: step.simps)
apply(rule drop_frames_step)
using Suc by (auto)
qed
lemma lower_frames_step:
assumes
"∀l < n. step prog (ds l) = Inr (ds (Suc l))"
"∀l ≤ n. k < stack_size (ds l)"
shows
"take_tail k (frames (ds 0)) = take_tail k (frames (ds n))"
using assms proof (induction n)
case 0
then show ?case
by simp
next
case (Suc n)
have "take_tail k (frames (ds n)) = take_tail k (frames (ds (Suc n)))"
using Suc take_frames_step by simp
then show ?case
using Suc by auto
qed
lemma inf_run_step': "step' prog (cs (r i)) (Inr (cs (r (Suc i))))"
proof -
define j where "j = r i"
obtain f fs where f_fs: "frames (cs j) = f#fs"
using inf_run[of j] by (auto split: list.splits)
define p where "p = frame.pos f"
have inf: "step prog (cs j) = (Inr (cs (Suc j)))"
using inf_run by simp
obtain c where c_def: "find_statement prog p = Inr c"
using inf unfolding p_def by (auto simp add: f_fs split: sum.splits)
let ?P = "(∀j' > j. stack_size (cs j) < stack_size (cs j'))"
consider (a) "¬ is_call prog (cs j)"
| (b) "is_call prog (cs j)" "?P"
| (c) "is_call prog (cs j)" "¬ ?P"
by fastforce
then show ?thesis
proof cases
case a
have 1: "r (Suc i) = Suc j"
using a j_def by (auto)
then show ?thesis
proof (cases "∃a x. c = Terminator a ∧ named_instruction a = Ret (Some x)")
case True
then show ?thesis
using r_no_return[of i] c_def unfolding p_def j_def[symmetric] f_fs
by (auto simp del: r.simps)
next
case False
show ?thesis
using j_def f_fs 1 apply(auto simp add: step'_def split: option.splits)
using inf apply(auto split: option.splits action.splits sum.splits named.splits instruction.splits)
apply(rule step_call.intros(1))
subgoal by (auto simp add: small_step.simps small_step.call_external_function_def split: llvm_fun.splits option.splits)
apply(subst small_step.terminate_frame')
defer apply(simp)
using False using c_def by (simp add: p_def)
qed
next
case b
have 1: "r (Suc i) = Suc j"
using b j_def by (auto)
then show ?thesis
using b j_def f_fs 1 apply(auto simp add: step'_def is_call_def split: option.splits sum.splits)
using inf by (auto intro!: step_call.intros(1)
simp add: small_step.call_external_function_def small_step.simps split: llvm_fun.splits option.splits action.splits named.splits instruction.splits)
next
case c
define l where "l = (LEAST j'. j' > j ∧ stack_size (cs j) = stack_size (cs j'))"
define c⇩0 where "c⇩0 = cs j"
define c⇩1 where "c⇩1 = cs (j + 1)"
define c⇩n where "c⇩n = cs l"
define c⇩n⇩1 where "c⇩n⇩1 = cs (l - 1)"
define s_s where "s_s = s⇩c⇩s j"
have 1: "r (Suc i) = (LEAST j'. j' > j ∧ stack_size (cs j) = stack_size (cs j'))"
using c j_def by (auto simp add: Let_def)
have "j < l ∧ stack_size (cs j) = stack_size (cs l)"
unfolding l_def
apply(rule LeastI_ex)
by (metis c(1) c(2) linorder_neqE_nat s⇩c⇩s_def stack_size_eq_call)
then have l: "j < l" "stack_size (cs j) = stack_size (cs l)"
by auto
have False if a: "s⇩c⇩s i ≤ s⇩c⇩s j" "j < i" "i < l" for i
proof (cases "s⇩c⇩s i = s⇩c⇩s j")
case True
have "l ≤ i"
unfolding l_def apply(rule Least_le)
using True that unfolding s⇩c⇩s_def by auto
then show ?thesis
using that by auto
next
case False
have 1: "s⇩c⇩s i < s⇩c⇩s j"
using that False by simp
then obtain k where k: "j < k" "k < i" "local.s⇩c⇩s j = local.s⇩c⇩s k"
using stack_size_eq_call a c by blast
then have "k < l"
using a by simp
moreover have "l ≤ k"
unfolding l_def apply(rule Least_le)
using k unfolding s⇩c⇩s_def by simp
ultimately show ?thesis
by simp
qed
then have 2: "s⇩c⇩s i > s⇩c⇩s j" if "j < i" "i < l" for i
using that leI by blast
have 21: "j < l - 1"
proof -
have False if "j = l - 1"
proof -
have "step prog (cs j) = Inr (cs l)"
using l inf_run[of j] that by (simp)
then show False
using l(2)[symmetric] c apply(auto split: list.splits option.splits action.splits named.splits instruction.splits
prod.splits sum.splits sum_bind_splits llvm_fun.splits terminator.splits
simp add: small_step.simps is_call_def stack_size_def)
by (metis length_Cons lessI less_irrefl_nat llvm_state.sel)
qed
then show ?thesis
using l by fastforce
qed
have 3: "step prog c⇩n⇩1 = Inr c⇩n"
unfolding c⇩n⇩1_def c⇩n_def using inf_run[of "l - 1"] l by auto
have 31: "stack_size c⇩1 = stack_size c⇩0 + 1"
using c inf_run[of j] unfolding c⇩1_def c⇩0_def
apply(auto split: list.splits option.splits action.splits named.splits instruction.splits
prod.splits sum_bind_splits llvm_fun.splits terminator.splits sum.splits
simp add: small_step.simps is_call_def)
by (metis (no_types, lifting) "2" "21" Nat.lessE One_nat_def Suc_mono Suc_pred ‹j < l ∧ stack_size (cs j) = stack_size (cs l)›
inf_run.s⇩c⇩s_def inf_run_axioms length_nth_simps(2) lessI less_irrefl_nat llvm_state.sel stack_size_def zero_less_Suc)+
have 4: "stack_size c⇩n⇩1 = stack_size c⇩n + 1"
proof -
have "stack_size c⇩n ∈ {stack_size c⇩n⇩1, stack_size c⇩n⇩1 + 1, stack_size c⇩n⇩1 - 1}"
using stack_size_dec_inc[of "l - 1"] l unfolding s⇩c⇩s_def c⇩n_def c⇩n⇩1_def by auto
moreover have "stack_size c⇩n < stack_size c⇩n⇩1"
using 2[of "l - 1"] 21 unfolding s⇩c⇩s_def c⇩n_def c⇩n⇩1_def l by auto
ultimately show ?thesis
by auto
qed
obtain f⇩n⇩1 fs⇩n⇩1 where 5: "frames c⇩n⇩1 = f⇩n⇩1#fs⇩n⇩1"
using 3 by (auto split: list.splits)
have 45: "∃t v. find_statement prog (frame.pos f⇩n⇩1) = Inr (Terminator t)
∧ named_instruction t = Ret (Some v)"
using 3 4 5 by (auto split: option.splits action.splits named.splits instruction.splits
prod.splits sum_bind_splits llvm_fun.splits terminator.splits sum.splits
simp add: small_step.simps stack_size_def)
have 55: "drop_frames s_s c⇩n⇩1 = Llvm_state [f⇩n⇩1]"
using 4
apply(simp add: drop_frames_def 5 stack_size_def s_s_def c⇩n_def s⇩c⇩s_def)
by (metis "5" drop_tail_except_first l(2) llvm_state.collapse stack_size_def update_frames.simps)
define ds where "ds x = j + 1 + x" for x
have 6: "(drop_frames s_s c⇩1, drop_frames s_s c⇩n⇩1) ∈ (step_relation prog)⇧*"
proof -
have "drop_frames s_s c⇩1 = drop_frames s_s (cs (ds 0))"
unfolding c⇩1_def ds_def by simp
moreover have "drop_frames s_s c⇩n⇩1 = drop_frames s_s (cs (ds (l - 2 - j)))"
proof -
have "l - 1 = j + 1 + (l - 2 - j)"
using 21 by (auto)
then show ?thesis
unfolding c⇩n⇩1_def ds_def by metis
qed
moreover have "(drop_frames s_s (cs (ds 0)), drop_frames s_s (cs (ds (l - 2 - j)))) ∈ (step_relation prog)⇧*"
apply(rule drop_frames_step_plus)
apply(auto simp add: ds_def simp del: step.simps)
using inf_run apply(simp)
unfolding s_s_def s⇩c⇩s_def apply(rule 2[unfolded s⇩c⇩s_def])
apply(simp)
using "21" by linarith
ultimately show ?thesis
unfolding c⇩1_def c⇩n⇩1_def l_def by simp
qed
have "∃c. step prog (drop_frames s_s c⇩n⇩1) = Inl (ReturnValue c)"
using 55 45 3 5 by (auto simp add: small_step.simps split: sum_bind_splits)
then obtain v where v: "step prog (drop_frames s_s c⇩n⇩1) = Inl (ReturnValue v)"
by blast
have "(Inr (drop_frames s_s c⇩1), Inl (ReturnValue v)) ∈ (step_rel_e prog)⇧*"
apply(rule rtrancl.intros(2)[of _ "Inr (drop_frames s_s c⇩n⇩1)"])
using 6 step_relation_step_rel_e_rtrancl apply(blast)
using v unfolding step_rel_e_def by simp
then have 601: "(Inr (drop_frames s_s c⇩1), Inl (ReturnValue v)) ∈ (step_rel_e prog)⇧+"
unfolding rtrancl_eq_or_trancl by auto
obtain f⇩1 fs⇩1 where f⇩1: "frames c⇩1 = f⇩1#fs⇩1"
using inf_run[of "Suc j"] unfolding c⇩1_def by (auto split: list.splits)
obtain f⇩0 fs⇩0 where f⇩0: "frames c⇩0 = f⇩0#fs⇩0"
using inf_run[of "j"] unfolding c⇩0_def by (auto split: list.splits)
obtain a fn t ps where
find_s: "find_statement prog (frame.pos f⇩0) = Inr (Instruction (Named a (Call fn t ps)))"
using c unfolding is_call_def using f⇩0 unfolding c⇩0_def
by (auto split: option.splits action.splits named.splits instruction.splits sum.splits)
have 61: "update_frames (λ_. [f⇩1]) c⇩0 = drop_frames s_s c⇩1"
proof -
have "update_frames (λ_. [f⇩1]) c⇩0 = Llvm_state [f⇩1]"
by (auto)
also have "… = drop_frames s_s c⇩1"
unfolding drop_frames_def
by (metis "31" Suc_eq_plus1 c⇩0_def drop_tail_except_first f⇩1 frames_simp inf_run.s⇩c⇩s_def
inf_run_axioms length_Cons nat.inject s_s_def stack_size_def)
finally show ?thesis
by simp
qed
have 7: "Inr f⇩1 = small_step.enter_frame prog f⇩0 t ps"
using inf_run[of j] f⇩0 f⇩1 find_s map_of_funs_name unfolding c⇩0_def c⇩1_def
apply(auto elim!: simp add: map_of_funs_name small_step.simps split: llvm_fun.splits option.splits sum_bind_splits)
using map_of_funs_name apply(fastforce)
using map_of_funs_name by (metis list.inject llvm_fun.inject(1) llvm_state.sel option.inject sum.inject(2))
have 8: "(Inr (update_frames (λ_. [f⇩1]) (cs (local.r i))), Inl (ReturnValue v)) ∈ (step_rel_e prog)⇧+"
using 61 601 unfolding c⇩0_def j_def by auto
have 85: "fs⇩n⇩1 = f⇩0#fs⇩0"
proof -
have "f⇩0#fs⇩0 = fs⇩1"
using inf_run[of j, symmetric] f⇩0 f⇩1 c unfolding c⇩0_def c⇩1_def
by (auto split: option.splits action.splits named.splits instruction.splits
prod.splits sum.splits sum_bind_splits llvm_fun.splits terminator.splits
simp add: small_step.simps is_call_def)
also have "… = take_tail s_s (frames c⇩1)"
unfolding f⇩1 apply(rule take_tail_except_first[symmetric])
using 31 unfolding s_s_def s⇩c⇩s_def stack_size_def f⇩1 c⇩0_def by simp
also have "c⇩1 = cs (ds 0)"
unfolding ds_def c⇩1_def by simp
also have "take_tail s_s (frames (cs (ds 0))) = take_tail s_s (frames (cs (ds (l - 2 - j))))"
apply(rule lower_frames_step)
apply(auto simp add: ds_def simp del: step.simps)
using inf_run apply(simp)
unfolding s_s_def s⇩c⇩s_def apply(rule 2[unfolded s⇩c⇩s_def])
apply(simp)
using "21" by linarith
also have "cs (ds (l - 2 - j)) = c⇩n⇩1"
proof -
have "l - 1 = j + 1 + (l - 2 - j)"
using 21 by (auto)
then show ?thesis
unfolding c⇩n⇩1_def ds_def by metis
qed
also have "take_tail s_s (frames c⇩n⇩1) = fs⇩n⇩1"
unfolding 5 apply(rule take_tail_except_first)
using 4 unfolding stack_size_def 5 s_s_def
using c⇩n_def l(2) s⇩c⇩s_def stack_size_def by force
finally show ?thesis
by simp
qed
have 9: "Inr (cs l) = small_step.update_frames_stack (cs (local.r i)) f⇩0 fs⇩0 a (Inr v)"
using 3[symmetric] 5 45 85 v find_s by (fastforce simp add: 55 small_step.simps c⇩n_def
small_step.update_stack.simps split: prod.splits sum_bind_splits
action.splits named.splits instruction.splits option.splits Option.bind_splits
list.splits intro!: frame.expand elim!: option_to_sum.elims)
show ?thesis
unfolding 1 l_def[symmetric]
using c 1 find_s f⇩0 unfolding c⇩0_def j_def
apply(auto simp add: step'_def is_call_def j_def split: list.splits option.splits
action.splits named.splits terminator.splits instruction.splits
simp del: r.simps)
apply(rule step_call.intros(2)[of f⇩1, where c = v])
using 7 8 9 by auto
qed
qed
end
end