Theory StartConfig

(*  Title:      JinjaThreads/Common/StartConfig.thy
    Author:     Andreas Lochbihler
*)

section ‹The initial configuration›

theory StartConfig
imports
  Exceptions
  Observable_Events
begin

definition initialization_list :: "cname list"
where
  "initialization_list = Thread # sys_xcpts_list"

context heap_base begin

definition create_initial_object :: "'heap × 'addr list × bool  cname  'heap × 'addr list × bool"
where
  "create_initial_object = 
  (λ(h, ads, b) C. 
     if b
     then let HA = allocate h (Class_type C)
          in if HA = {} then (h, ads, False)
             else let (h', a'') = SOME ha. ha  HA in (h', ads @ [a''], True)
     else (h, ads, False))"

definition start_heap_data :: "'heap × 'addr list × bool"
where
  "start_heap_data = foldl create_initial_object (empty_heap, [], True) initialization_list"

definition start_heap :: 'heap
where "start_heap = fst start_heap_data"

definition start_heap_ok :: bool
where "start_heap_ok = snd (snd (start_heap_data))"

definition start_heap_obs :: "('addr, 'thread_id) obs_event list"
where
  "start_heap_obs =
  map (λ(C, a). NewHeapElem a (Class_type C)) (zip initialization_list (fst (snd start_heap_data)))"

definition start_addrs :: "'addr list"
where "start_addrs = fst (snd start_heap_data)"

definition addr_of_sys_xcpt :: "cname  'addr"
where "addr_of_sys_xcpt C = the (map_of (zip initialization_list start_addrs) C)"

definition start_tid :: 'thread_id
where "start_tid = addr2thread_id (hd start_addrs)"

definition start_state :: "(cname  mname  ty list  ty  'm  'addr val list  'x)  'm prog  cname  mname  'addr val list  ('addr,'thread_id,'x,'heap,'addr) state"
where
  "start_state f P C M vs 
   let (D, Ts, T, m) = method P C M
   in (K$ None, ([start_tid  (f D M Ts T (the m) vs, no_wait_locks)], start_heap), Map.empty, {})"

lemma create_initial_object_simps:
  "create_initial_object (h, ads, b) C = 
   (if b 
    then let HA = allocate h (Class_type C)
         in if HA = {} then (h, ads, False)
            else let (h', a'') = SOME ha. ha  HA in (h', ads @ [a''], True)
    else (h, ads, False))"
unfolding create_initial_object_def by simp

lemma create_initial_object_False [simp]:
  "create_initial_object (h, ads, False) C = (h, ads, False)"
by(simp add: create_initial_object_simps)

lemma foldl_create_initial_object_False [simp]:
  "foldl create_initial_object (h, ads, False) Cs = (h, ads, False)"
by(induct Cs) simp_all

lemma NewHeapElem_start_heap_obs_start_addrsD:
  "NewHeapElem a CTn  set start_heap_obs  a  set start_addrs"
unfolding start_heap_obs_def start_addrs_def
by(auto dest: set_zip_rightD)

lemma shr_start_state: "shr (start_state f P C M vs) = start_heap"
by(simp add: start_state_def split_beta)

lemma start_heap_obs_not_Read: 
  "ReadMem ad al v  set start_heap_obs"
unfolding start_heap_obs_def by auto

lemma length_initialization_list_le_length_start_addrs:
  "length initialization_list  length start_addrs"
proof -
  { fix h ads xs
    have "length (fst (snd (foldl create_initial_object (h, ads, True) xs)))  length ads + length xs"
    proof(induct xs arbitrary: h ads)
      case Nil thus ?case by simp
    next
      case (Cons x xs)
      from this[of "fst (SOME ha. ha  allocate h (Class_type x))" "ads @ [snd (SOME ha. ha  allocate h (Class_type x))]"]
      show ?case by(clarsimp simp add: create_initial_object_simps split_beta)
    qed }
  from this[of empty_heap "[]" initialization_list]
  show ?thesis unfolding start_heap_def start_addrs_def start_heap_data_def by simp
qed

lemma (in -) distinct_initialization_list:
  "distinct initialization_list"
by(simp add: initialization_list_def sys_xcpts_list_def sys_xcpts_neqs Thread_neq_sys_xcpts)

lemma (in -) wf_syscls_initialization_list_is_class:
  " wf_syscls P; C  set initialization_list   is_class P C"
by(auto simp add: initialization_list_def sys_xcpts_list_def wf_syscls_is_class_xcpt)

lemma start_addrs_NewHeapElem_start_heap_obsD:
  "a  set start_addrs  CTn. NewHeapElem a CTn  set start_heap_obs"
using length_initialization_list_le_length_start_addrs
unfolding start_heap_obs_def start_addrs_def
by(force simp add: set_zip in_set_conv_nth intro: rev_image_eqI)

lemma in_set_start_addrs_conv_NewHeapElem:
  "a  set start_addrs  (CTn. NewHeapElem a CTn  set start_heap_obs)"
by(blast dest: start_addrs_NewHeapElem_start_heap_obsD intro: NewHeapElem_start_heap_obs_start_addrsD)


subsection @{term preallocated}

definition preallocated :: "'heap  bool"
where "preallocated h  C  sys_xcpts. typeof_addr h (addr_of_sys_xcpt C) = Class_type C"

lemma typeof_addr_sys_xcp: 
  " preallocated h; C  sys_xcpts   typeof_addr h (addr_of_sys_xcpt C) = Class_type C"
by(simp add: preallocated_def)

lemma typeof_sys_xcp:
  " preallocated h; C  sys_xcpts   typeof⇘h(Addr (addr_of_sys_xcpt C)) = Class C"
by(simp add: typeof_addr_sys_xcp)

lemma addr_of_sys_xcpt_start_addr:
  " start_heap_ok; C  sys_xcpts   addr_of_sys_xcpt C  set start_addrs"
unfolding start_heap_ok_def start_heap_data_def initialization_list_def sys_xcpts_list_def 
  preallocated_def start_heap_def start_addrs_def
apply(simp split: prod.split_asm if_split_asm add: create_initial_object_simps)
apply(erule sys_xcpts_cases)
apply(simp_all add: addr_of_sys_xcpt_def start_addrs_def start_heap_data_def initialization_list_def sys_xcpts_list_def create_initial_object_simps)
done

lemma [simp]:
  assumes "preallocated h"
  shows typeof_ClassCast: "typeof_addr h (addr_of_sys_xcpt ClassCast) = Some(Class_type ClassCast)"
  and typeof_OutOfMemory: "typeof_addr h (addr_of_sys_xcpt OutOfMemory) = Some(Class_type OutOfMemory)" 
  and typeof_NullPointer: "typeof_addr h (addr_of_sys_xcpt NullPointer) = Some(Class_type NullPointer)" 
  and typeof_ArrayIndexOutOfBounds: 
  "typeof_addr h (addr_of_sys_xcpt ArrayIndexOutOfBounds) = Some(Class_type ArrayIndexOutOfBounds)" 
  and typeof_ArrayStore: "typeof_addr h (addr_of_sys_xcpt ArrayStore) = Some(Class_type ArrayStore)" 
  and typeof_NegativeArraySize: "typeof_addr h (addr_of_sys_xcpt NegativeArraySize) = Some(Class_type NegativeArraySize)" 
  and typeof_ArithmeticException: "typeof_addr h (addr_of_sys_xcpt ArithmeticException) = Some(Class_type ArithmeticException)" 
  and typeof_IllegalMonitorState: "typeof_addr h (addr_of_sys_xcpt IllegalMonitorState) = Some(Class_type IllegalMonitorState)"
  and typeof_IllegalThreadState: "typeof_addr h (addr_of_sys_xcpt IllegalThreadState) = Some(Class_type IllegalThreadState)" 
  and typeof_InterruptedException: "typeof_addr h (addr_of_sys_xcpt InterruptedException) = Some(Class_type InterruptedException)"
using assms
by(simp_all add: typeof_addr_sys_xcp)

lemma cname_of_xcp [simp]:
  " preallocated h; C  sys_xcpts   cname_of h (addr_of_sys_xcpt C) = C"
by(drule (1) typeof_addr_sys_xcp)(simp add: cname_of_def)

lemma preallocated_hext:
  " preallocated h; h  h'   preallocated h'"
by(auto simp add: preallocated_def dest: hext_objD)

end

context heap begin

lemma preallocated_heap_ops:
  assumes "preallocated h"
  shows preallocated_allocate: "a. (h', a)  allocate h hT  preallocated h'"
  and preallocated_write_field: "heap_write h a al v h'  preallocated h'"
using preallocated_hext[OF assms, of h']
by(blast intro: hext_heap_ops)+

lemma not_empty_pairE: " A  {}; a b. (a, b)  A  thesis   thesis"
by auto

lemma allocate_not_emptyI: "(h', a)  allocate h hT  allocate h hT  {}"
by auto

lemma allocate_Eps:
  " (h'', a'')  allocate h hT; (SOME ha. ha  allocate h hT) = (h', a')   (h', a')  allocate h hT"
by(drule sym)(auto intro: someI)

lemma preallocated_start_heap:
  " start_heap_ok; wf_syscls P   preallocated start_heap"
unfolding start_heap_ok_def start_heap_data_def initialization_list_def sys_xcpts_list_def 
  preallocated_def start_heap_def start_addrs_def
apply(clarsimp split: prod.split_asm if_split_asm simp add: create_initial_object_simps)
apply(erule not_empty_pairE)+
apply(drule (1) allocate_Eps)
apply(drule (1) allocate_Eps)
apply(drule (1) allocate_Eps)
apply(drule (1) allocate_Eps)
apply(drule (1) allocate_Eps)
apply(drule (1) allocate_Eps)
apply(drule (1) allocate_Eps)
apply(drule (1) allocate_Eps)
apply(drule (1) allocate_Eps)
apply(drule (1) allocate_Eps)
apply(drule (1) allocate_Eps)
apply(rotate_tac 13)
apply(frule allocate_SomeD, simp add: wf_syscls_is_class_xcpt, frule hext_allocate, rotate_tac 1)
apply(frule allocate_SomeD, simp add: wf_syscls_is_class_xcpt, frule hext_allocate, rotate_tac 1)
apply(frule allocate_SomeD, simp add: wf_syscls_is_class_xcpt, frule hext_allocate, rotate_tac 1)
apply(frule allocate_SomeD, simp add: wf_syscls_is_class_xcpt, frule hext_allocate, rotate_tac 1)
apply(frule allocate_SomeD, simp add: wf_syscls_is_class_xcpt, frule hext_allocate, rotate_tac 1)
apply(frule allocate_SomeD, simp add: wf_syscls_is_class_xcpt, frule hext_allocate, rotate_tac 1)
apply(frule allocate_SomeD, simp add: wf_syscls_is_class_xcpt, frule hext_allocate, rotate_tac 1)
apply(frule allocate_SomeD, simp add: wf_syscls_is_class_xcpt, frule hext_allocate, rotate_tac 1)
apply(frule allocate_SomeD, simp add: wf_syscls_is_class_xcpt, frule hext_allocate, rotate_tac 1)
apply(frule allocate_SomeD, simp add: wf_syscls_is_class_xcpt, frule hext_allocate, rotate_tac 1)
apply(frule allocate_SomeD, simp add: wf_syscls_is_class_xcpt, frule hext_allocate, rotate_tac 1)
apply(erule sys_xcpts_cases)
apply(simp_all add: addr_of_sys_xcpt_def initialization_list_def sys_xcpts_list_def sys_xcpts_neqs Thread_neq_sys_xcpts start_heap_data_def start_addrs_def create_initial_object_simps allocate_not_emptyI split del: if_split)
apply(assumption|erule typeof_addr_hext_mono)+
done

lemma start_tid_start_addrs:
  " wf_syscls P; start_heap_ok   thread_id2addr start_tid  set start_addrs"
unfolding start_heap_ok_def start_heap_data_def initialization_list_def sys_xcpts_list_def 
  preallocated_def start_heap_def start_addrs_def
apply(simp split: prod.split_asm if_split_asm add: create_initial_object_simps addr_of_sys_xcpt_def start_addrs_def start_tid_def start_heap_data_def initialization_list_def sys_xcpts_list_def)
apply(erule not_empty_pairE)+
apply(drule (1) allocate_Eps)
apply(rotate_tac -1)
apply(drule allocate_SomeD, simp)
apply(auto intro: addr2thread_id_inverse)
done

lemma
  assumes "wf_syscls P"
  shows dom_typeof_addr_start_heap: "set start_addrs  dom (typeof_addr start_heap)"
  and distinct_start_addrs: "distinct start_addrs"
proof -
  { fix h ads b and Cs xs :: "cname list"
    assume "set ads  dom (typeof_addr h)" and "distinct (Cs @ xs)" and "length Cs = length ads"
      and "C a. (C, a)  set (zip Cs ads)  typeof_addr h a = Class_type C"
      and "C. C  set xs  is_class P C"
    hence "set (fst (snd (foldl create_initial_object (h, ads, b) xs))) 
             dom (typeof_addr (fst (foldl create_initial_object (h, ads, b) xs)))  
           (distinct ads  distinct (fst (snd (foldl create_initial_object (h, ads, b) xs))))"
      (is "?concl xs h ads b Cs")
    proof(induct xs arbitrary: h ads b Cs)
      case Nil thus ?case by auto
    next
      case (Cons x xs)
      note ads = set ads  dom (typeof_addr h)
      note dist = distinct (Cs @ x # xs)
      note len = length Cs = length ads
      note type = C a. (C, a)  set (zip Cs ads)  typeof_addr h a = Class_type C
      note is_class = C. C  set (x # xs)  is_class P C
      show ?case
      proof(cases "b  allocate h (Class_type x)  {}")
        case False thus ?thesis
          using ads len by(auto simp add: create_initial_object_simps zip_append1)
      next
        case [simp]: True
        obtain h' a' where h'a': "(SOME ha. ha  allocate h (Class_type x)) = (h', a')"
          by(cases "SOME ha. ha  allocate h (Class_type x)")
        with True have new_obj: "(h', a')  allocate h (Class_type x)"
          by(auto simp del: True intro: allocate_Eps)
        hence hext: "h  h'" by(rule hext_allocate)
        with ads new_obj have ads': "set ads  dom (typeof_addr h')"
          by(auto dest: typeof_addr_hext_mono[OF hext_allocate])
        moreover {
          from new_obj ads' is_class[of x]
          have "set (ads @ [a'])  dom (typeof_addr h')"
            by(auto dest: allocate_SomeD)
          moreover from dist have "distinct ((Cs @ [x]) @ xs)" by simp
          moreover have "length (Cs @ [x]) = length (ads @ [a'])" using len by simp
          moreover {
            fix C a
            assume "(C, a)  set (zip (Cs @ [x]) (ads @ [a']))"
            hence "typeof_addr h' a = Class_type C"
              using hext new_obj type[of C a] len is_class
              by(auto dest: allocate_SomeD hext_objD) }
          note type' = this
          moreover have is_class': "C. C  set xs  is_class P C" using is_class by simp
          ultimately have "?concl xs h' (ads @ [a']) True (Cs @ [x])" by(rule Cons)
          moreover have "a'  set ads"
          proof
            assume a': "a'  set ads"
            then obtain C where "(C, a')  set (zip Cs ads)" "C  set Cs"
              using len unfolding set_zip in_set_conv_nth by auto
            hence "typeof_addr h a' = Class_type C" by-(rule type)
            with hext have "typeof_addr h' a' = Class_type C" by(rule typeof_addr_hext_mono)
            moreover from new_obj is_class
            have "typeof_addr h' a' = Class_type x" by(auto dest: allocate_SomeD)
            ultimately have "C = x" by simp
            with dist C  set Cs show False by simp
          qed
          moreover note calculation }
        ultimately show ?thesis by(simp add: create_initial_object_simps new_obj h'a')
      qed
    qed }
  from this[of "[]" empty_heap "[]" initialization_list True]
    distinct_initialization_list wf_syscls_initialization_list_is_class[OF assms]
  show "set start_addrs  dom (typeof_addr start_heap)"
    and "distinct start_addrs"
    unfolding start_heap_def start_addrs_def start_heap_data_def by auto
qed

lemma NewHeapElem_start_heap_obsD:
  assumes "wf_syscls P"
  and "NewHeapElem a hT  set start_heap_obs"
  shows "typeof_addr start_heap a = hT"
proof -
  show ?thesis
  proof(cases hT)
    case (Class_type C)
    { fix h ads b xs Cs
      assume "(C, a)  set (zip (Cs @ xs) (fst (snd (foldl create_initial_object (h, ads, b) xs))))"
        and "(C, a)  set (zip Cs ads). typeof_addr h a = Class_type C"
        and "length Cs = length ads"
        and "C  set xs. is_class P C"
      hence "typeof_addr (fst (foldl create_initial_object (h, ads, b) xs)) a = Class_type C"
      proof(induct xs arbitrary: h ads b Cs)
        case Nil thus ?case by auto
      next
        case (Cons x xs)
        note inv = (C, a)  set (zip Cs ads). typeof_addr h a = Class_type C
          and Ca = (C, a)  set (zip (Cs @ x # xs) (fst (snd (foldl create_initial_object (h, ads, b) (x # xs)))))
          and len = length Cs = length ads
          and is_class = C  set (x # xs). is_class P C
        show ?case
        proof(cases "b  allocate h (Class_type x)  {}")
          case False thus ?thesis
            using inv Ca len by(auto simp add: create_initial_object_simps zip_append1 split: if_split_asm)
        next
          case [simp]: True
          obtain h' a' where h'a': "(SOME ha. ha  allocate h (Class_type x)) = (h', a')"
            by(cases "SOME ha. ha  allocate h (Class_type x)")
          with True have new_obj: "(h', a')  allocate h (Class_type x)"
            by(auto simp del: True intro: allocate_Eps)
          hence hext: "h  h'" by(rule hext_allocate)

          have "(C, a)  set (zip ((Cs @ [x]) @ xs) (fst (snd (foldl create_initial_object (h', ads @ [a'], True) xs))))"
            using Ca new_obj by(simp add: create_initial_object_simps h'a')
          moreover have "(C, a)set (zip (Cs @ [x]) (ads @ [a'])).  typeof_addr h' a = Class_type C"
          proof(clarify)
            fix C a
            assume "(C, a)  set (zip (Cs @ [x]) (ads @ [a']))"
            thus "typeof_addr h' a = Class_type C"
              using inv len hext new_obj is_class by(auto dest: allocate_SomeD typeof_addr_hext_mono)
          qed
          moreover have "length (Cs @ [x]) = length (ads @ [a'])" using len by simp
          moreover have "C  set xs. is_class P C" using is_class by simp
          ultimately have "typeof_addr (fst (foldl create_initial_object (h', ads @ [a'], True) xs)) a = Class_type C"
            by(rule Cons)
          thus ?thesis using new_obj by(simp add: create_initial_object_simps h'a')
        qed
      qed }
    from this[of "[]" initialization_list empty_heap "[]" True] assms wf_syscls_initialization_list_is_class[of P] 
    show ?thesis by(auto simp add: start_heap_obs_def start_heap_data_def start_heap_def Class_type)
  next
    case Array_type thus ?thesis using assms
      by(auto simp add: start_heap_obs_def start_heap_data_def start_heap_def)
  qed
qed

end


subsection ‹Code generation›

definition pick_addr :: "('heap × 'addr) set  'heap × 'addr"
where "pick_addr HA = (SOME ha. ha  HA)"

lemma pick_addr_code [code]:
  "pick_addr (set [ha]) = ha"
by(simp add: pick_addr_def)

lemma (in heap_base) start_heap_data_code:
  "start_heap_data = 
   (let 
     (h, ads, b) = foldl 
        (λ(h, ads, b) C. 
           if b then
             let HA = allocate h (Class_type C)
             in if HA = {} then (h, ads, False)
                else let (h', a'') = pick_addr HA in (h', a'' # ads, True)
           else (h, ads, False)) 
        (empty_heap, [], True) 
        initialization_list 
    in (h, rev ads, b))"
unfolding start_heap_data_def create_initial_object_def pick_addr_def
by(rule rev_induct)(simp_all add: split_beta)

lemmas [code] =
  heap_base.start_heap_data_code
  heap_base.start_heap_def
  heap_base.start_heap_ok_def
  heap_base.start_heap_obs_def
  heap_base.start_addrs_def
  heap_base.addr_of_sys_xcpt_def
  heap_base.start_tid_def
  heap_base.start_state_def

end