Theory KPL_soundness

(*
Title:       KPL_soundness.thy
Author:      John Wickerson
Date:        6 April 2014
Description: 
  This theory file accompanies the article "The Design and 
  Implementation of a Verification Technique for GPU Kernels" 
  by Adam Betts, Nathan Chong, Alastair F. Donaldson, Jeroen
  Ketema, Shaz Qadeer, Paul Thomson and John Wickerson. It
  gives an outline proof of Theorem 4.2, which states that 
  the two-thread reduction using equality-abstraction is sound. 

  There are several "sorry" statements in the file, which
  mark the places where the proof is completed "by hand".

  The theory builds on the entry "GPU_Kernel_PL" in the Archive
  of Formal Proofs, which can be downloaded from
  {http://afp.sf.net/entries/GPU_Kernel_PL.shtml}.
*)

theory KPL_soundness imports
  "$AFP/GPU_Kernel_PL/KPL_wellformedness"
  "$AFP/GPU_Kernel_PL/KPL_execution_kernel"
begin

section {* Soundness of the two-thread reduction using equality-abstraction *}

(* Holds if the K_Open rule can be applied *)
fun K_Open_applies :: "kernel_state => bool"
where
  "K_Open_applies (_,ss,_) = (∃ e S p. 
  hd ss = (While e S, p))"

(* Holds if the K_Done rule can be applied *)
fun K_Done_applies 
  :: "threadset => kernel_state => bool"
where
  "K_Done_applies (G,T) (κ,ss,_) = (∃ e S p.
  hd ss = (WhileDyn e S, p) ∧ 
  (∀i ∈ G. ∀j ∈ the (T i).
  ¬ (eval_bool (p ∧* e) (the ((the (κ i))⇩t⇩s j)))))" 

(* Holds if the K_Iter rule can be applied, but all of the
   threads in the threadset (G',T') are disabled *)
fun K_Iter_applies_but 
  :: "threadset => threadset => kernel_state => bool"
where
  "K_Iter_applies_but (G,T) (G',T') K = (∃ e S κ' ss p vs.
  K = (κ', (WhileDyn e S, p) # ss, vs)
  ∧ (∃i ∈ G. ∃j ∈ the (T i). 
    eval_bool (p ∧* e) (the ((the (κ' i))⇩t⇩s j))) 
  ∧ (∀i ∈ G'. ∀j ∈ the (T' i). 
    ¬ (eval_bool (p ∧* e) (the ((the (κ' i))⇩t⇩s j)))))"

(* Executions (can start from any state) *)
definition executions
  :: "abs_level => proc list => threadset 
     => kernel_state list set"
where
  "executions a fs GT ≡ { Ks :: kernel_state list. Ks ≠ [] ∧
  (∀n < length Ks - 1. 
  step_k a fs GT (Ks ! n) (Some (Ks ! (n + 1))))}"

(* The singleton sequence is trivially an execution *)
lemma executions_singleton:
  "[K] ∈ executions a fs GT"
by (auto simp add: executions_def)

(* Lengthening an execution at its head *)
lemma executions_consI:
  "[| Ks ∈ executions a fs GT ; step_k a fs GT K (Some (Ks ! 0)) |] ==>
  (K # Ks) ∈ executions a fs GT"
apply (auto simp add: executions_def)
apply (case_tac n)
apply auto
done

(* Removing the first state from an execution *)
lemma executions_consD:
  "[| (K # Ks) ∈ executions a fs GT ; Ks ≠ [] |] ==> Ks ∈ executions a fs GT"
apply (auto simp add: executions_def)
apply (metis drop_0 drop_Suc length_drop nth_Cons_Suc tl_drop zero_less_diff)
done

(* Well-founded execution = execution starting from a valid initial state *)
definition wf_executions 
  :: "abs_level => stmt => proc list => threadset 
     => kernel_state list set"
where
  "wf_executions a S fs GT ≡ { Ks :: kernel_state list. 
  valid_initial_kernel_state S GT (Ks ! 0) ∧
  Ks ∈ executions a fs GT}"

(* Faulting execution = well-founded execution leading to an error *)
definition faulting_executions
  :: "abs_level => stmt => proc list => threadset 
     => kernel_state list set"
where
  "faulting_executions a S fs GT ≡ { Ks :: kernel_state list.
  Ks ∈ wf_executions a S fs GT ∧
  step_k a fs GT (last Ks) None }"

(* Holds if no well-founded execution leads to an error *)
definition error_free 
  :: "abs_level => stmt => proc list => threadset => bool"
where
  "error_free a S fs GT ≡ faulting_executions a S fs GT = {}"

(* The reductions of a threadset (G,T) are all the threadsets (G',T') that 
   consist of exactly two threads from (G,T) *)
fun reductions :: "threadset => threadset set"
where
  "reductions (G,T) = {(G',T') | G' T'. 
    ((∃i. G' = {i} ∧ card (the (T' i)) = 2) ∨ 
    (∃i1 i2. i1 ≠ i2 ∧ G' = {i1,i2} ∧ card (the (T' i1)) = 1 ∧ card (the (T' i2)) = 1)) 
    ∧ G' ⊆ G ∧ (∀i ∈ G'. the (T' i) ⊆ the (T i))}"

(* Projection function for group states *)
fun proj_g :: "lid set => group_state => group_state"
where
  "proj_g T' γ = γ (| 
    thread_states := (thread_states γ) |` T',
    R_group := {r ∈ R_group γ . fst r ∈ T'} ,
    W_group := {w ∈ W_group γ . fst w ∈ T'} |)" 

(* Projection function for group state maps *)
fun proj_k :: "threadset => (gid \<rightharpoonup> group_state) => (gid \<rightharpoonup> group_state)"
where
  "proj_k (G',T') κ = (λ i. if i ∈ G' then Some (proj_g (the (T' i)) (the (κ i))) else None)" 

(* Projection function for kernel states *)
fun proj :: "threadset => kernel_state => kernel_state"
where 
  "proj GT' (κ,ss,vs) = (proj_k GT' κ, ss, vs)"

(* If there are no group races in the threadset (G,T), and
   (G',T') is a reduction of (G,T), then there are no 
   group races in (G',T'). *)
lemma reduction_preserves_no_group_race:
  assumes "¬ (group_race (the (T i)) ((the (κ i))⇩t⇩s))"
  assumes "(G', T') ∈ reductions (G, T)"
  assumes "i ∈ G'"
  shows "¬ (group_race (the (T' i)) ((the (proj_k (G', T') κ i))⇩t⇩s))"
using assms
apply (unfold group_race_def)
apply clarify
apply (subgoal_tac "j ∈ the (T i)")
apply (subgoal_tac "k ∈ the (T i)")
apply auto
done

(* If there are no kernel races in the threadset (G,T), and
   (G',T') is a reduction of (G,T), then there are no 
   kernel races in (G',T'). *)
lemma reduction_preserves_no_kernel_race:
  assumes "¬ kernel_race G κ"
  assumes "(G', T') ∈ reductions (G, T)"
  shows "¬ kernel_race G' (proj_k (G', T') κ)"
using assms
apply (unfold kernel_race_def)
apply clarify
apply (subgoal_tac "i ∈ G")
apply (subgoal_tac "j ∈ G")
apply simp
apply (fold atomize_ball)
apply (subgoal_tac "snd ` W_group (the (κ i)) ∩
  (snd ` R_group (the (κ j)) 
  ∪ snd ` W_group (the (κ j))) = {}")
apply auto[1]
apply (metis (hide_lams, no_types))
apply auto
done

(* The reduction respects updates to the R_group field *)
lemma reduction_preserves_reads:
  assumes "i ∈ G'"
  assumes "(G',T') ∈ reductions (G,T)"
  assumes "R_group (the (κ' i)) = 
    R_group (the (κ i)) 
    ∪ (\<Union>j∈the (T i). {j} × R (the ((the (κ' i))⇩t⇩s j)))"
  shows "R_group (the (proj_k (G', T') κ' i)) =
    R_group (the (proj_k (G', T') κ i)) 
    ∪ (\<Union>j∈the (T' i). {j} × 
      R (the ((the (proj_k (G', T') κ' i))⇩t⇩s j)))"
using assms by auto

(* The reduction respects updates to the W_group field *)
lemma reduction_preserves_writes:
  assumes "i ∈ G'"
  assumes "(G', T') ∈ reductions (G, T)"
  assumes "W_group (the (κ' i)) = 
    W_group (the (κ i)) 
    ∪ (\<Union>j∈the (T i). {j} × W (the ((the (κ' i))⇩t⇩s j)))"
  shows "W_group (the (proj_k (G', T') κ' i)) =
    W_group (the (proj_k (G', T') κ i)) 
    ∪ (\<Union>j∈the (T' i). {j} × 
      W (the ((the (proj_k (G', T') κ' i))⇩t⇩s j)))"
using assms by auto

(* The reduction preserves the step_t relation. That is:
   If τ can step to τ' in the non-abstracted semantics, then the
   projected version of τ can step to the projected version of
   τ' in the equality-abstracted semantics. *)
lemma reduced_step_t:
  "[| step_t a τbp τ' ; 
     a = No_Abst ; 
     τbp = (the ((the (κ i))⇩t⇩s j), b, p) ;
     τ' = the ((the (κ' i))⇩t⇩s j) ; i ∈ G' ; 
     γ' = the (proj_k (G', T') κ' i) ;
     j ∈ the (T' i) |] ==> 
  step_t Eq_Abst (the ((the (proj_k (G', T') κ i))⇩t⇩s j), b, p)
        (the (γ' ⇩t⇩s j))"
apply (induct rule: step_t.induct)
apply (auto simp add: step_t.T_Disabled T_Assign_helper T_Read_helper T_Write_helper)
done

(* The reduction preserves the step_g relation. That is:
   If γ can step to γ' in the non-abstracted semantics, then the
   projected version of γ can step to the projected version of
   γ' in the equality-abstracted semantics. *)
lemma reduced_step_g:
  "[| step_g a i T γbp γo ; γo = Some (the (κ' i)) ;
    (G',T') ∈ reductions (G,T) ; γbp = (the (κ i), S, p) ; 
    i ∈ G' ; a = No_Abst |] ==> 
  step_g Eq_Abst i T' (the (proj_k (G', T') κ i), S, p)
    (Some (the (proj_k (G',T') κ' i)))"
proof (induct rule: step_g.induct)
  case (G_Basic T i a γ s pa γ')
  thus ?case
  apply clarify
  apply (rule step_g.G_Basic)
  apply (intro ballI)
  apply (fold atomize_ball)[1]
  apply (rule_tac a=No_Abst and τbp="(the ((the (κ i))⇩t⇩s j), s, p)" 
    and τ'="(the ((the (κ' i))⇩t⇩s j))" and κ=κ and i=i and j=j 
    and b=s and p=p and κ'=κ' and T'=T' and G'=G' in reduced_step_t) 
  apply (subgoal_tac "j ∈ the (T i)")
  apply auto[8]
  apply (rule reduction_preserves_no_group_race[of T i κ' G' T' G])
  apply auto[3]
  apply (rule reduction_preserves_reads, assumption+)
  apply (rule reduction_preserves_writes, assumption+)
  done
next
  case (G_No_Op T i pa γ a)
  thus ?case 
  apply clarify
  apply (rule G_No_Op_helper)
  apply auto
  done
next
  case (G_Sync T i pa γ γ' P)
  thus ?case  
  apply clarify
  apply (rule step_g.G_Sync_Eq)
  apply (intro ballI)
  apply (auto simp del: reductions.simps)[1]
  apply (subgoal_tac "j ∈ the (T i)")
  apply auto[2]
  apply (auto simp del: reductions.simps)[1]
  apply (subgoal_tac "j ∈ the (T i)")
  apply auto[2]
  done
qed auto

(* The reduction preserves errors in the step_g relation. That is:
   If γ can step to Error in the non-abstracted semantics, then the
   projected version of γ can step to Error in the equality-
   abstracted semantics. *)
lemma reduced_step_g_error:
  "[| step_g a i T γbp γo ; γo = None ;
    (G',T') ∈ reductions (G,T) ; γbp = (the (κ i), S, p) ; 
    i ∈ G' ; a = No_Abst |] ==> 
  step_g Eq_Abst i T' (the (proj_k (G', T') κ i), S, p) None"
proof (induct rule: step_g.induct)
  case (G_Race T i a γ s p' γ')
  thus ?case
  sorry (* This is probably not
  provable without augmenting the operational 
  semantics to tag the Error state with the identities
  of the threads causing the error. *)
next
  case (G_Divergence j k T i p' γ a)
  thus ?case
  sorry (* As above *)
qed auto

(* The reduction preserves the step_k relation. That is:
   If K can step to K' in the non-abstracted semantics, then the
   projected version of K can step to the projected version of
   K' in the equality-abstracted semantics. *)
lemma reduced_step_k: 
  "[| step_k a fs (G,T) K Ko ; 
     (G',T') ∈ reductions (G,T) ; 
     a = No_Abst ; Ko = Some K' ;
     ¬ K_Iter_applies_but (G,T) (G',T') K |] ==>
   step_k Eq_Abst fs (G',T') (proj (G',T') K) (Some (proj (G',T') K'))"
proof (induct rule: step_k.induct)
  case (K_Basic G a T κ b p κ' fs ss vs)
  thus ?case
  apply clarify
  apply (unfold proj.simps)
  apply (rule step_k.K_Basic)
  prefer 2  
  apply (rule reduction_preserves_no_kernel_race[of G κ' G' T' T])
  apply (assumption)+
  apply (intro ballI)
  apply (subgoal_tac "i ∈ G")
  apply (drule_tac x=i in bspec, assumption)
  apply (rule_tac a=No_Abst and i=i and T=T 
    and γbp="(the (κ i), Basic b, p)" 
    and γo="Some (the (κ' i))" in reduced_step_g)
  apply auto
  done
next
  case (K_Sync G a T κ p κ' fs ss vs)
  thus ?case
  apply clarify
  apply (unfold proj.simps)
  apply (rule step_k.K_Sync)
  prefer 2  
  apply (rule reduction_preserves_no_kernel_race[of G κ' G' T' T])
  apply assumption+
  apply (intro ballI)
  apply (subgoal_tac "i ∈ G")
  apply (drule_tac x=i in bspec, assumption)
  apply (rule_tac a=No_Abst and i=i and T=T 
    and γbp="(the (κ i), Barrier, p)" 
    and γo="Some (the (κ' i))" in reduced_step_g)
  apply auto
  done
next
  case (K_Iter i G j T p e κ u vs v a fs S ss)
  thus ?case
  apply (unfold option.inject)  
  apply clarify
  apply (unfold proj.simps)
  apply (unfold K_Iter_applies_but.simps)
  apply (auto simp del: eval_bool.simps reductions.simps proj_k.simps)
  apply (rule step_k.K_Iter)
  apply auto
  done
next
  case (K_Done G T p e κ a fs S ss vs)
  thus ?case
  apply clarify
  apply (unfold proj.simps)
  apply (rule step_k.K_Done)
  apply fastforce
  done
qed (auto simp add: step_k.K_Seq step_k.K_Var step_k.K_If step_k.K_Open step_k.K_Call)

(* The reduction preserves errors in the step_k relation. That is:
   If K can step to Error in the non-abstracted semantics, then the
   projected version of K can step to Error in the equality-
   abstracted semantics. *)
lemma reduced_step_k_error: 
  "[| step_k a fs (G,T) K Ko ; 
     (G',T') ∈ reductions (G,T) ; 
     ¬ K_Iter_applies_but (G,T) (G',T') K ;
     Ko = None ; a = No_Abst |] ==>
   step_k Eq_Abst fs (G',T') (proj (G',T') K) None"
proof (induct rule: step_k.induct)
  case (K_Inter_Group_Race G a T κ b p κ' P fs ss vs)
  thus ?case sorry (* This is probably not
  provable without augmenting the operational 
  semantics to tag the Error state with the identities
  of the threads causing the error. *)
next
  case (K_Intra_Group_Race i G a T κ s p fs ss vs)
  thus ?case sorry (* As above. *)
next
  case (K_Divergence i G a T κ p fs ss vs) 
  thus ?case sorry (* As above. *)
qed (auto)

definition endOfLoop :: "threadset => kernel_state => kernel_state => bool"
where
  "endOfLoop GT K K' ≡ K_Done_applies GT K' ∧ snd3 K' = snd3 K"

fun dropUntil :: "('a => bool) => 'a list => 'a list"
where
  "dropUntil P [] = []"
| "dropUntil P (x # xs) = (if P x then xs else dropUntil P xs)"

lemma length_dropUntil_le: 
  "length (dropUntil P xs) ≤ length xs"
by (induct xs, auto)

lemma executions_consD2:
  "[| Ks ∈ executions a fs GT ; dropUntil P Ks ≠ [] |] ==> dropUntil P Ks ∈ executions a fs GT"
proof (induct Ks)
  case (Cons K Ks)
  thus ?case
  apply (cases "P K")
  apply (metis dropUntil.simps(2) executions_consD)
  apply (metis dropUntil.simps executions_consD)
  done
qed (auto)

function process 
  :: "threadset => threadset => kernel_state list => kernel_state list"
where
  "process GT GT' [] = []"
| "process GT GT' (K # Ks) = (
    if K_Iter_applies_but GT GT' K then 
      proj GT' K # process GT GT' (dropUntil (endOfLoop GT K) Ks) 
    else 
      proj GT' K # process GT GT' Ks)"
by pat_completeness auto
termination
apply (relation "measure(λ(_,_,xs). length xs)")
apply (auto)
apply (smt length_dropUntil_le)
done

lemma reduction_preserves_valid_initial_kernel_state:
  "[| valid_initial_kernel_state S (G, T) K0 ; 
     (G',T') ∈ reductions (G, T) |]
  ==> valid_initial_kernel_state S (G', T') (proj (G', T') K0)"
sorry (* This should be provable, but the complexity
  of the predicates involved causes Isabelle's higher-
  order unification algorithm to diverge, making the 
  lemma very hard to work with! *)

lemma must_leave_loop:
  "[| Ks ∈ executions No_Abst (procs P) GT ;
     step_k No_Abst fs GT (last Ks) None ;
     K_Iter_applies_but GT GT' Ks_head ;
     Ks = Ks_head # Ks_tail |] ==>
  dropUntil (endOfLoop GT Ks_head) Ks_tail ≠ []"
sorry
(* This is likely missing some assumption  
   like "(G',T') ∈ reductions (G,T)". It's not
   provable in its current form because we need
   to track the fact that it is exactly those
   two threads in (G',T') that are causing the
   error. This is not possible without 
   augmenting the operational semantics. *)

lemma last_dropUntil:
  "dropUntil P xs ≠ [] ==> last (dropUntil P xs) = last xs"
by (induct xs, auto)

lemma process_not_empty: 
  "Ks ≠ [] ==> process GT GT' Ks ≠ []"
by (case_tac Ks, auto)

(* Soundness theorem for the equality-abstraction (Theorem 4.2). *)
theorem Eq_Soundness:
  assumes "wf_kernel P"
  assumes "∀(G',T') ∈ reductions (G,T). error_free Eq_Abst (main P) (procs P) (G',T')"
  assumes "G = {0..<(groups P)}"
  assumes "T = [G |=> {0..<(threads P)}]"
  shows "error_free No_Abst (main P) (procs P) (G,T)"
proof (rule ccontr)

  assume "¬ (error_free No_Abst (main P) (procs P) (G,T))"

  then obtain Ks where 
    "Ks ∈ faulting_executions No_Abst (main P) (procs P) (G,T)"
  by (auto simp add: error_free_def)
  
  hence
    1: "Ks ∈ wf_executions No_Abst (main P) (procs P) (G,T)" and 
    2: "step_k No_Abst (procs P) (G,T) (last Ks) None"
  by (auto simp add: faulting_executions_def)
  
  hence 
    3: "Ks ∈ executions No_Abst (procs P) (G,T)" and
    4: "valid_initial_kernel_state (main P) (G,T) (Ks ! 0)"
  by (auto simp add: wf_executions_def)

  hence "Ks ≠ []" by (auto simp add: executions_def)

  from 2 obtain s t where "s ≠ t" and "s ∈ tids (G,T)" and "t ∈ tids (G,T)" 
  sorry (* This is currently not provable. One would need
    to augment the operational semantics so that the Error
    state is tagged with the two threads responsible for
    the error. *)

  def G' ≡ "{fst s, fst t}"
  def T' ≡ "if fst s = fst t then [fst s \<mapsto> {snd s, snd t}] 
            else [fst s \<mapsto> {snd s}, fst t \<mapsto> {snd t}]"

  have 5: "(G', T') ∈ reductions (G, T)"
  apply (simp)
  apply (intro conjI) 
  apply (case_tac "fst s = fst t")
  apply (intro disjI1)
  apply (rule_tac x="fst s" in exI)
  apply (intro conjI)
  apply (simp add: G'_def)
  apply (case_tac "snd s = snd t")
  apply (metis `s ≠ t` prod_eqI)
  apply (simp add: T'_def)
  apply (intro disjI2)
  apply (rule_tac x="fst s" in exI)
  apply (rule_tac x="fst t" in exI)
  apply (intro conjI)
  apply assumption
  apply (simp add: G'_def)
  apply (simp add: T'_def)
  apply (simp add: T'_def)  
  apply (simp add: G'_def)
  apply (intro conjI)
  apply (insert `s ∈ tids (G,T)`) [1]
  apply (case_tac s, simp)
  apply (insert `t ∈ tids (G,T)`) [1]
  apply (case_tac t, simp)  
  apply (simp add: G'_def T'_def)
  apply (intro conjI impI)
  apply (insert `s ∈ tids (G,T)`) [1]
  apply (case_tac s, simp)
  apply (insert `t ∈ tids (G,T)`) [1]
  apply (case_tac t, simp)
  apply (insert `s ∈ tids (G,T)`) [1]
  apply (case_tac s, simp)
  apply (insert `t ∈ tids (G,T)`) [1]
  apply (case_tac t, simp)
  done

  def Ks' ≡ "process (G,T) (G',T') Ks"

  {
    fix n :: nat
    have 
      "!!Ks. [| length Ks = n ; 
        Ks ∈ executions No_Abst (procs P) (G,T) ; 
        step_k No_Abst (procs P) (G,T) (last Ks) None |] ==>
      process (G,T) (G',T') Ks ∈ executions Eq_Abst (procs P) (G',T')"
    proof (induct n rule: less_induct)
      case (less n Ks)
      hence "Ks ≠ []" and "n > 0" by (auto simp add: executions_def)
      then obtain rest κ ss vs where 
        Ks_def: "Ks = (κ,ss,vs) # rest" 
      by (case_tac Ks, auto)
      { 
        assume 8: "¬ K_Iter_applies_but (G,T) (G',T') (κ, ss, vs)"
        have ?case
        apply (subst Ks_def)
        apply (subst process.simps)
        apply (subst if_not_P)
        apply (rule 8)
        apply (case_tac rest)
        apply (simp add: executions_singleton)
        apply (rename_tac K' rest')
        apply (rule executions_consI)
        apply (cut_tac y="n - 1" and Ks=rest in less.hyps)
        apply (simp add: `n > 0`)
        apply (insert `length Ks = n` Ks_def, auto)[1]
        apply (insert less.prems(2))[1]
        apply (subst (asm) Ks_def)
        apply (erule executions_consD)
        apply simp
        apply (insert less.prems(3) Ks_def)[1]
        apply simp
        apply assumption
        apply (insert 8)
        apply (simp del: K_Iter_applies_but.simps proj.simps)
        apply (rule reduced_step_k)
        apply (insert less.prems(2) Ks_def executions_def)[1]
        apply auto[1]
        apply (rule 5)
        apply simp+
        done
      } 
      moreover 
      { 
        assume 8: "K_Iter_applies_but (G,T) (G',T') (κ, ss, vs)"
        have ?case
        apply (subst Ks_def)
        apply (subst process.simps)
        apply (subst if_P)
        apply (rule 8)
        apply (case_tac rest)
        apply simp
        apply (rule executions_singleton)
        apply (case_tac 
          "dropUntil (endOfLoop (G, T) (κ, ss, vs)) rest = []")
        apply (simp add: executions_singleton)
        apply (rename_tac K' rest')
        apply (rule executions_consI)
        apply (cut_tac 
          y="length (dropUntil (endOfLoop (G, T) (κ, ss, vs)) rest)" and 
          Ks="dropUntil (endOfLoop (G,T) (κ, ss, vs)) rest" in less.hyps) 
        apply (subst `length Ks = n`[symmetric])
        apply (subst Ks_def)
        apply (subst list.size(4))
        apply (thin_tac "?x")
        apply (thin_tac "?x")
        apply (auto simp add: length_dropUntil_le less_Suc_eq_le)[1]
        apply simp
        apply (insert less.prems(2))[1]
        apply (subst (asm) Ks_def)
        apply (rule executions_consD2)
        apply (rule executions_consD)
        apply assumption
        apply simp
        apply (rule must_leave_loop)
        apply assumption
        apply (subst Ks_def[symmetric])
        apply (rule less.prems(3))
        apply (rule 8)
        apply simp
        defer 1
        apply assumption
        defer 1
        apply (insert less.prems(3))[1] 
        apply (unfold Ks_def)[1]
        apply (unfold last.simps)
        apply (subst (asm) if_not_P)
        apply simp
        apply (subst last_dropUntil)
        apply simp
        apply simp
        (* remaining to prove: can take a 
           K-Done step to exit the loop *)
        sorry
      }
      ultimately show ?case 
      by (cases "K_Iter_applies_but (G,T) (G',T') (κ, ss, vs)", auto)
    qed
  }
  hence "Ks' ∈ executions Eq_Abst (procs P) (G', T')"
  by (auto simp add: 2 3 Ks'_def)

  moreover
  { 
    fix n
    have "!!Ks. [| length Ks = n ; 
        Ks ∈ executions No_Abst (procs P) (G,T) ; 
        step_k No_Abst (procs P) (G,T) (last Ks) None |] ==>
      step_k Eq_Abst (procs P) (G',T') (last (process (G,T) (G',T') Ks)) None"
    proof (induct n rule: less_induct)
      case (less n Ks)
      hence "Ks ≠ []" and "n > 0" by (auto simp add: executions_def)
      then obtain rest κ ss vs where 
        Ks_def: "Ks = (κ,ss,vs) # rest" 
      by (case_tac Ks, auto)
      { 
        assume 8: "¬ K_Iter_applies_but (G,T) (G',T') (κ, ss, vs)"
        have ?case
        apply (subst Ks_def)
        apply (subst process.simps)
        apply (subst if_not_P)
        apply (rule 8)
        apply (case_tac "rest = []")
        apply (insert less.prems(3))
        apply (subst (asm) Ks_def)
        apply (simp del: proj.simps)
        apply (rule reduced_step_k_error)
        apply assumption
        apply (rule 5)
        apply (rule 8)
        apply simp
        apply simp
        apply (unfold Ks_def)
        apply (subgoal_tac "process (G, T) (G', T') rest ≠ []")
        apply (simp del: proj.simps)
        apply (rule less.hyps[where y="n - 1" and Ks="rest"])
        apply (simp add: `n > 0`)
        apply (insert `length Ks = n`)[1]
        apply (simp add: Ks_def)
        defer 1
        apply assumption
        apply (case_tac rest, simp, simp)
        apply (metis Ks_def less.prems(2) executions_consD)
        done
      } 
      moreover 
      { 
        assume 8: "K_Iter_applies_but (G,T) (G',T') (κ, ss, vs)"
        have ?case
        apply (subst Ks_def)
        apply (subst process.simps)
        apply (subst if_P)
        apply (rule 8)
        apply (case_tac "dropUntil (endOfLoop (G, T) (κ, ss, vs)) rest = []")
        apply (subgoal_tac "dropUntil (endOfLoop (G, T) (κ, ss, vs)) rest ≠ []")
        apply simp
        apply (rule must_leave_loop)
        prefer 4
        apply simp
        apply (fold Ks_def)
        apply (metis 8 Ks_def less.prems(2) less.prems(3) must_leave_loop)
        apply (metis 8 Ks_def less.prems(2) less.prems(3) must_leave_loop)
        apply (rule 8)
        apply (subgoal_tac "process (G, T) (G', T') (
          dropUntil (endOfLoop (G, T) (κ, ss, vs)) rest) ≠ []")
        apply (subst last.simps)
        apply (subst if_not_P, assumption)
        apply (rule less.hyps)
        prefer 2
        apply blast
        apply (insert `length Ks = n`)[1]
        apply (auto simp add: Ks_def)[1]
        apply (smt length_dropUntil_le)
        apply (rule executions_consD2)
        apply (rule executions_consD)
        apply (insert less.prems(2))[1]
        apply (simp add: Ks_def)
        apply fastforce
        apply assumption 
        apply (metis Ks_def dropUntil.simps(1) last.simps last_dropUntil less.prems(3))
        apply (rule process_not_empty)
        apply assumption
        done
      }
      ultimately show ?case 
      by (cases "K_Iter_applies_but (G,T) (G',T') (κ, ss, vs)", auto)
    qed
  }
  hence "step_k Eq_Abst (procs P) (G',T') (last Ks') None"
  by (auto simp add: 2 3 Ks'_def)
  
  moreover have 
    "valid_initial_kernel_state (main P) (G',T') (Ks' ! 0)"
  apply (unfold Ks'_def)
  apply (case_tac Ks)
  apply (simp add: `Ks ≠ []`)
  apply (rename_tac K0 rest)
  apply (simp del: valid_initial_kernel_state.simps K_Iter_applies_but.simps)
  apply (rule reduction_preserves_valid_initial_kernel_state)
  apply (insert 4, simp)[1]
  apply (rule 5)
  done  
 
  ultimately have 
    "Ks' ∈ faulting_executions Eq_Abst (main P) (procs P) (G',T')"
  by (metis (lifting) wf_executions_def faulting_executions_def mem_Collect_eq)
  
  hence "¬ error_free Eq_Abst (main P) (procs P) (G',T')"
  by (metis elem_set error_free_def not_None_eq set_empty_eq)
  
  with 5 and assms(2) show False by auto
qed

end