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