spec+proof: use linked lists in the design spec

This models the ready queues in the design spec as linked lists
via the tcbSchedNext and tcbSchedPrev pointers of a TCB, as in the C.

Library functions to update these linked lists are introduced, and used
to perform all functions which modify the ready queues.

Refinement between the linked lists and the Isabelle lists in the
abstract spec is handled via the predicate `heap_ls`.

`invs'` has been significantly modified, with the introduction of
`valid_sched_pointers` and `sym_heap_sched_pointers`. The various
invariants related to the bitmaps have been collected in the invariant
`valid_bitmaps`.

This includes a major revision to Orphanage, which now uses the
tcbQueued field of a TCB to indicate a thread's membership in a
ready queue, rather than the previous formulation which used
membership in the set of the Isabelle list.

Co-authored-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Co-authored-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>

proof/crefine/AARCH64/ADT_C.thy

@@ -82,8 +82,8 @@ lemma Basic_sem_eq:
 
 lemma setTCBContext_C_corres:
   "\<lbrakk> ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t \<rbrakk> \<Longrightarrow>
-  corres_underlying rf_sr nf nf' dc (pspace_domain_valid and tcb_at' t) \<top>
-    (threadSet (\<lambda>tcb. tcb \<lparr> tcbArch := atcbContextSet tc (tcbArch tcb)\<rparr>) t) (setTCBContext_C tc' t')"
+   corres_underlying rf_sr nf nf' dc (pspace_domain_valid and tcb_at' t) \<top>
+     (threadSet (\<lambda>tcb. tcb \<lparr> tcbArch := atcbContextSet tc (tcbArch tcb)\<rparr>) t) (setTCBContext_C tc' t')"
   apply (simp add: setTCBContext_C_def exec_C_def Basic_sem_eq corres_underlying_def)
   apply clarsimp
   apply (simp add: threadSet_def bind_assoc split_def exec_gets)
@@ -112,8 +112,6 @@ lemma setTCBContext_C_corres:
   apply (simp add: map_to_ctes_upd_tcb_no_ctes map_to_tcbs_upd tcb_cte_cases_def
                    cvariable_relation_upd_const ko_at_projectKO_opt cteSizeBits_def)
   apply (simp add: cep_relations_drop_fun_upd)
-  apply (apply_conjunct \<open>match conclusion in \<open>cready_queues_relation _ _ _\<close> \<Rightarrow>
-         \<open>erule cready_queues_relation_not_queue_ptrs; rule ext; simp split: if_split\<close>\<close>)
   apply (drule ko_at_projectKO_opt)
   apply (erule (2) cmap_relation_upd_relI)
     apply (simp add: ctcb_relation_def carch_tcb_relation_def)
@@ -648,25 +646,51 @@ lemma tcb_queue_rel'_unique:
   apply (erule(2) tcb_queue_rel_unique)
   done
 
-definition
-  cready_queues_to_H
-  :: "(tcb_C ptr \<rightharpoonup> tcb_C) \<Rightarrow> (tcb_queue_C[num_tcb_queues]) \<Rightarrow> word8 \<times> word8 \<Rightarrow> machine_word list"
+
+definition tcb_queue_C_to_tcb_queue :: "tcb_queue_C \<Rightarrow> tcb_queue" where
+  "tcb_queue_C_to_tcb_queue q \<equiv>
+     TcbQueue (if head_C q = NULL then None else Some (ctcb_ptr_to_tcb_ptr (head_C q)))
+              (if end_C q = NULL then None else Some (ctcb_ptr_to_tcb_ptr (end_C q)))"
+
+definition cready_queues_to_H ::
+  "tcb_queue_C[num_tcb_queues] \<Rightarrow> (domain \<times> priority \<Rightarrow> ready_queue)"
   where
-  "cready_queues_to_H h_tcb cs \<equiv> \<lambda>(qdom, prio). if ucast minDom \<le> qdom \<and> qdom \<le> ucast maxDom
-              \<and> ucast seL4_MinPrio \<le> prio \<and> prio \<le> ucast seL4_MaxPrio
-   then THE aq. let cqueue = index cs (cready_queues_index_to_C qdom prio)
-    in sched_queue_relation' h_tcb aq (head_C cqueue) (StateRelation_C.end_C cqueue)
-   else []"
+  "cready_queues_to_H cs \<equiv>
+     \<lambda>(qdom, prio).
+       if qdom \<le> maxDomain \<and> prio \<le> maxPriority
+       then let cqueue = index cs (cready_queues_index_to_C qdom prio)
+             in tcb_queue_C_to_tcb_queue cqueue
+       else TcbQueue None None"
 
 lemma cready_queues_to_H_correct:
-  "cready_queues_relation (clift s) cs as \<Longrightarrow>
-   cready_queues_to_H (clift s) cs = as"
-  apply (clarsimp simp: cready_queues_to_H_def cready_queues_relation_def
-                   fun_eq_iff)
-  apply (rule the_equality)
-   apply simp
-  apply (clarsimp simp: Let_def)
-  apply (rule_tac hp="clift s" in tcb_queue_rel'_unique, simp_all add: lift_t_NULL)
+  "\<lbrakk>cready_queues_relation (ksReadyQueues s) (ksReadyQueues_' ch);
+    no_0_obj' s; ksReadyQueues_asrt s; pspace_aligned' s; pspace_distinct' s\<rbrakk>
+   \<Longrightarrow> cready_queues_to_H (ksReadyQueues_' ch) = ksReadyQueues s"
+  apply (clarsimp simp: cready_queues_to_H_def cready_queues_relation_def Let_def)
+  apply (clarsimp simp: fun_eq_iff)
+  apply (rename_tac d p)
+  apply (drule_tac x=d in spec)
+  apply (drule_tac x=p in spec)
+  apply (clarsimp simp: ready_queue_relation_def ksReadyQueues_asrt_def)
+  apply (drule_tac x=d in spec)
+  apply (drule_tac x=p in spec)
+  apply clarsimp
+  apply (frule (3) obj_at'_tcbQueueHead_ksReadyQueues)
+  apply (frule (3) obj_at'_tcbQueueEnd_ksReadyQueues)
+  apply (frule tcbQueueHead_iff_tcbQueueEnd)
+  apply (rule conjI)
+   apply (clarsimp simp: tcb_queue_C_to_tcb_queue_def ctcb_queue_relation_def option_to_ctcb_ptr_def)
+   apply (case_tac "tcbQueueHead (ksReadyQueues s (d, p)) = None")
+    apply (clarsimp simp: tcb_queue.expand)
+   apply clarsimp
+   apply (rename_tac queue_head queue_end)
+   apply (prop_tac "tcb_at' queue_head s", fastforce simp: tcbQueueEmpty_def obj_at'_def)
+   apply (prop_tac "tcb_at' queue_end s", fastforce simp: tcbQueueEmpty_def obj_at'_def)
+   apply (drule tcb_at_not_NULL)+
+   apply (fastforce simp: tcb_queue.expand kernel.ctcb_ptr_to_ctcb_ptr)
+  apply (clarsimp simp: tcbQueueEmpty_def ctcb_queue_relation_def option_to_ctcb_ptr_def
+                 split: option.splits;
+         metis tcb_queue.exhaust_sel word_not_le)
   done
 
 (* showing that cpspace_relation is actually unique >>>*)
@@ -820,17 +844,20 @@ lemma cthread_state_rel_imp_eq:
   apply (cases y, simp_all add: ThreadState_defs)+
   done
 
-lemma ksPSpace_valid_objs_tcbBoundNotification_nonzero:
-  "\<exists>s. ksPSpace s = ah \<and> no_0_obj' s \<and> valid_objs' s
-     \<Longrightarrow> map_to_tcbs ah p = Some tcb \<Longrightarrow> tcbBoundNotification tcb \<noteq> Some 0"
+lemma map_to_tcbs_Some_refs_nonzero:
+  "\<lbrakk>map_to_tcbs (ksPSpace s) p = Some tcb; no_0_obj' s; valid_objs' s\<rbrakk>
+   \<Longrightarrow> tcbBoundNotification tcb \<noteq> Some 0
+       \<and> tcbSchedPrev tcb \<noteq> Some 0
+       \<and> tcbSchedNext tcb \<noteq> Some 0"
+  supply word_neq_0_conv[simp del]
   apply (clarsimp simp: map_comp_def split: option.splits)
-  apply (erule(1) valid_objsE')
-  apply (clarsimp simp: valid_obj'_def valid_tcb'_def)
+  apply (erule (1) valid_objsE')
+  apply (fastforce simp: valid_obj'_def valid_tcb'_def)
   done
 
 lemma ksPSpace_valid_objs_atcbVCPUPtr_nonzero:
-  "\<exists>s. ksPSpace s = ah \<and> no_0_obj' s \<and> valid_objs' s
-     \<Longrightarrow> map_to_tcbs ah p = Some tcb \<Longrightarrow> atcbVCPUPtr (tcbArch tcb) \<noteq> Some 0"
+  "\<lbrakk> no_0_obj' s; valid_objs' s \<rbrakk> \<Longrightarrow>
+   map_to_tcbs (ksPSpace s) p = Some tcb \<Longrightarrow> atcbVCPUPtr (tcbArch tcb) \<noteq> Some 0"
   apply (clarsimp simp: map_comp_def split: option.splits)
   apply (erule(1) valid_objsE')
   apply (clarsimp simp: valid_obj'_def valid_tcb'_def valid_arch_tcb'_def)
@@ -855,36 +882,77 @@ lemma carch_tcb_relation_imp_eq:
   apply (case_tac vcpuptr2 ; simp)
   done
 
+lemma tcb_ptr_to_ctcb_ptr_inj:
+  "tcb_ptr_to_ctcb_ptr x = tcb_ptr_to_ctcb_ptr y \<Longrightarrow> x = y"
+  by (auto simp: tcb_ptr_to_ctcb_ptr_def ctcb_offset_def)
+
+lemma
+  assumes "pspace_aligned' as" "pspace_distinct' as" "valid_tcb' atcb as"
+  shows tcb_at'_tcbBoundNotification:
+    "bound (tcbBoundNotification atcb) \<longrightarrow> ntfn_at' (the (tcbBoundNotification atcb)) as"
+  and tcb_at'_tcbSchedPrev:
+    "tcbSchedPrev atcb \<noteq> None \<longrightarrow> tcb_at' (the (tcbSchedPrev atcb)) as"
+  and tcb_at'_tcbSchedNext:
+    "tcbSchedNext atcb \<noteq> None \<longrightarrow> tcb_at' (the (tcbSchedNext atcb)) as"
+  using assms
+  by (clarsimp simp: valid_tcb'_def obj_at'_def)+
+
 lemma cpspace_tcb_relation_unique:
-  assumes tcbs: "cpspace_tcb_relation ah ch" "cpspace_tcb_relation ah' ch"
-      and   vs: "\<exists>s. ksPSpace s = ah \<and> no_0_obj' s \<and> valid_objs' s"
-      and   vs': "\<exists>s. ksPSpace s = ah' \<and> no_0_obj' s \<and> valid_objs' s"
-  assumes ctes: " \<forall>tcb tcb'. (\<exists>p. map_to_tcbs ah p = Some tcb \<and>
-                                  map_to_tcbs ah' p = Some tcb') \<longrightarrow>
-                  (\<forall>x\<in>ran tcb_cte_cases. fst x tcb' = fst x tcb)"
-  shows "map_to_tcbs ah' = map_to_tcbs ah"
+  assumes tcbs: "cpspace_tcb_relation (ksPSpace as) ch" "cpspace_tcb_relation (ksPSpace as') ch"
+  assumes   vs: "no_0_obj' as" "valid_objs' as"
+  assumes  vs': "no_0_obj' as'" "valid_objs' as'"
+  assumes   ad: "pspace_aligned' as" "pspace_distinct' as"
+  assumes  ad': "pspace_aligned' as'" "pspace_distinct' as'"
+  assumes ctes: "\<forall>tcb tcb'. (\<exists>p. map_to_tcbs (ksPSpace as) p = Some tcb \<and>
+                                 map_to_tcbs (ksPSpace as') p = Some tcb') \<longrightarrow>
+                 (\<forall>x\<in>ran tcb_cte_cases. fst x tcb' = fst x tcb)"
+  shows "map_to_tcbs (ksPSpace as') = map_to_tcbs (ksPSpace as)"
   using tcbs(2) tcbs(1)
   apply (clarsimp simp add: cmap_relation_def)
   apply (drule inj_image_inv[OF inj_tcb_ptr_to_ctcb_ptr])+
   apply (simp add: tcb_ptr_to_ctcb_ptr_def[abs_def] ctcb_offset_def)
   apply (rule ext)
-  apply (case_tac "x:dom (map_to_tcbs ah)")
+  apply (case_tac "x \<in> dom (map_to_tcbs (ksPSpace as))")
    apply (drule bspec, assumption)+
    apply (simp add: dom_def Collect_eq, drule_tac x=x in spec)
    apply clarsimp
    apply (rename_tac p x y)
    apply (cut_tac ctes)
    apply (drule_tac x=x in spec, drule_tac x=y in spec, erule impE, fastforce)
-   apply (frule ksPSpace_valid_objs_tcbBoundNotification_nonzero[OF vs])
-   apply (frule ksPSpace_valid_objs_tcbBoundNotification_nonzero[OF vs'])
+   apply (frule map_to_tcbs_Some_refs_nonzero[OF _ vs])
+   apply (frule map_to_tcbs_Some_refs_nonzero[OF _ vs'])
    apply (frule ksPSpace_valid_objs_atcbVCPUPtr_nonzero[OF vs])
    apply (frule ksPSpace_valid_objs_atcbVCPUPtr_nonzero[OF vs'])
+   apply (rename_tac atcb atcb')
+   apply (prop_tac "valid_tcb' atcb as")
+    apply (fastforce intro: vs ad map_to_ko_atI tcb_ko_at_valid_objs_valid_tcb')
+   apply (prop_tac "valid_tcb' atcb' as'")
+    apply (fastforce intro: vs' ad' map_to_ko_atI tcb_ko_at_valid_objs_valid_tcb')
+   apply (frule tcb_at'_tcbSchedPrev[OF ad])
+   apply (frule tcb_at'_tcbSchedPrev[OF ad'])
+   apply (frule tcb_at'_tcbSchedNext[OF ad])
+   apply (frule tcb_at'_tcbSchedNext[OF ad'])
    apply (thin_tac "map_to_tcbs x y = Some z" for x y z)+
-   apply (case_tac x, case_tac y, case_tac "the (clift ch (tcb_Ptr (p+0x400)))")
+   apply (case_tac "the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))")
    apply (clarsimp simp: ctcb_relation_def ran_tcb_cte_cases)
-   apply (clarsimp simp: option_to_ptr_def option_to_0_def split: option.splits)
-   apply (auto simp: cfault_rel_imp_eq cthread_state_rel_imp_eq carch_tcb_relation_imp_eq
-                     ccontext_relation_imp_eq up_ucast_inj_eq ctcb_size_bits_def)
+   apply (clarsimp simp: option_to_ctcb_ptr_def option_to_ptr_def option_to_0_def)
+   apply (rule tcb.expand)
+   apply clarsimp
+   apply (intro conjI)
+        apply (simp add: cthread_state_rel_imp_eq)
+       apply (simp add: cfault_rel_imp_eq)
+      apply (case_tac "tcbBoundNotification atcb'", case_tac "tcbBoundNotification atcb"; clarsimp)
+      apply (clarsimp split: option.splits)
+     apply (case_tac "tcbSchedPrev atcb'"; case_tac "tcbSchedPrev atcb"; clarsimp)
+       apply (force dest!: tcb_at_not_NULL)
+      apply (force dest!: tcb_at_not_NULL)
+     apply (force simp: tcb_ptr_to_ctcb_ptr_inj)
+    apply (case_tac "tcbSchedNext atcb'"; case_tac "tcbSchedNext atcb"; clarsimp)
+      apply (force dest!: tcb_at_not_NULL)
+     apply (force dest!: tcb_at_not_NULL)
+    apply (force simp: tcb_ptr_to_ctcb_ptr_inj)
+   apply (clarsimp simp: carch_tcb_relation_imp_eq)
+  apply auto
   done
 
 lemma tcb_queue_rel_clift_unique:
@@ -916,10 +984,6 @@ lemma is_aligned_no_overflow_0:
 abbreviation
   "is_aligned_opt x n \<equiv> case x of None \<Rightarrow> True | Some y \<Rightarrow> is_aligned y n"
 
-lemma tcb_ptr_to_ctcb_ptr_inj:
-  "tcb_ptr_to_ctcb_ptr x = tcb_ptr_to_ctcb_ptr y \<Longrightarrow> x = y"
-  by (auto simp: tcb_ptr_to_ctcb_ptr_def ctcb_offset_def)
-
 lemma option_to_ctcb_ptr_inj:
   "\<lbrakk> is_aligned_opt a tcbBlockSizeBits; is_aligned_opt b tcbBlockSizeBits \<rbrakk>
     \<Longrightarrow> (option_to_ctcb_ptr a = option_to_ctcb_ptr b) = (a = b)"
@@ -1218,8 +1282,8 @@ proof -
       apply (rule valid_objs'_aligned_vcpuTCB [OF valid_objs])
      apply (rule valid_objs'_aligned_vcpuTCB [OF valid_objs'])
     apply (drule (1) cpspace_tcb_relation_unique)
-       apply (fastforce intro: no_0_objs no_0_objs' valid_objs valid_objs')
-      apply (fastforce intro: no_0_objs no_0_objs' valid_objs valid_objs')
+       apply (fastforce intro: no_0_objs no_0_objs' valid_objs valid_objs')+
+      apply (fastforce intro: aligned distinct aligned' distinct')+
      apply (intro allI impI,elim exE conjE)
      apply (rule_tac p=p in map_to_ctes_tcb_ctes, assumption)
       apply (frule (1) map_to_ko_atI[OF _ aligned distinct])
@@ -1427,7 +1491,7 @@ where
     ksDomSchedule = cDomSchedule_to_H kernel_all_global_addresses.ksDomSchedule,
     ksCurDomain = ucast (ksCurDomain_' s),
     ksDomainTime = ksDomainTime_' s,
-    ksReadyQueues = cready_queues_to_H (clift (t_hrs_' s)) (ksReadyQueues_' s),
+    ksReadyQueues = cready_queues_to_H (ksReadyQueues_' s),
     ksReadyQueuesL1Bitmap = cbitmap_L1_to_H (ksReadyQueuesL1Bitmap_' s),
     ksReadyQueuesL2Bitmap = cbitmap_L2_to_H (ksReadyQueuesL2Bitmap_' s),
     ksCurThread = ctcb_ptr_to_tcb_ptr (ksCurThread_' s),
@@ -1449,27 +1513,27 @@ lemma trivial_eq_conj: "B = C \<Longrightarrow> (A \<and> B) = (A \<and> C)"
 lemma cstate_to_H_correct:
   assumes valid: "valid_state' as"
   assumes cstate_rel: "cstate_relation as cs"
+  assumes rdyqs: "ksReadyQueues_asrt as"
   shows "cstate_to_H cs = as \<lparr>ksMachineState:=  observable_memory (ksMachineState as) (user_mem' as)\<rparr>"
   apply (subgoal_tac "cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as)")
    apply (rule kernel_state.equality, simp_all add: cstate_to_H_def)
-                      apply (rule cstate_to_pspace_H_correct)
+                    apply (rule cstate_to_pspace_H_correct)
                      using valid
                      apply (simp add: valid_state'_def)
                     using cstate_rel valid
                     apply (clarsimp simp: cstate_relation_def cpspace_relation_def Let_def
-                      observable_memory_def valid_state'_def
-                      valid_pspace'_def)
+                                          observable_memory_def valid_state'_def valid_pspace'_def)
                    using cstate_rel
                    apply (clarsimp simp: cstate_relation_def cpspace_relation_def Let_def prod_eq_iff)
                   using cstate_rel
                   apply (clarsimp simp: cstate_relation_def cpspace_relation_def  Let_def prod_eq_iff)
                  using valid cstate_rel
                  apply (rule mk_gsUntypedZeroRanges_correct)
                 subgoal
-                using cstate_rel
-                by (fastforce simp: cstate_relation_def cpspace_relation_def
-                                    Let_def ghost_size_rel_def unat_eq_0
-                            split: if_split)
+                  using cstate_rel
+                  by (fastforce simp: cstate_relation_def cpspace_relation_def
+                                      Let_def ghost_size_rel_def unat_eq_0
+                              split: if_split)
                using valid cstate_rel
                apply (rule cDomScheduleIdx_to_H_correct)
                using cstate_rel
@@ -1483,8 +1547,13 @@ lemma cstate_to_H_correct:
             using cstate_rel
             apply (clarsimp simp: cstate_relation_def Let_def)
            apply (rule cready_queues_to_H_correct)
-           using cstate_rel
-           apply (clarsimp simp: cstate_relation_def Let_def)
+               using cstate_rel rdyqs
+               apply (fastforce intro!: cready_queues_to_H_correct
+                                  simp: cstate_relation_def Let_def)
+              using valid apply (fastforce simp: valid_state'_def)
+             using rdyqs apply fastforce
+            using valid apply (fastforce simp: valid_state'_def)
+           using valid apply (fastforce simp: valid_state'_def)
           using cstate_rel
           apply (clarsimp simp: cstate_relation_def Let_def)
           using cstate_rel

proof/crefine/AARCH64/ArchMove_C.thy

@@ -292,9 +292,6 @@ lemma asUser_getRegister_discarded:
                         return_def fail_def stateAssert_def)
   done
 
-crunches Arch.switchToThread
-  for valid_queues'[wp]: valid_queues'
-  (simp: crunch_simps wp: hoare_drop_imps crunch_wps getASID_wp)
 crunches switchToIdleThread
   for ksCurDomain[wp]: "\<lambda>s. P (ksCurDomain s)"
 
@@ -312,10 +309,6 @@ lemma updateASIDPoolEntry_valid_pspace'[wp]:
   unfolding updateASIDPoolEntry_def valid_pspace'_def getPoolPtr_def
   by (wpsimp wp: getASID_wp)
 
-crunches switchToIdleThread, switchToThread
-  for valid_pspace'[wp]: valid_pspace'
-  (simp: whenE_def crunch_simps wp: crunch_wps hoare_drop_imps)
-
 lemma getMessageInfo_less_4:
   "\<lbrace>\<top>\<rbrace> getMessageInfo t \<lbrace>\<lambda>rv s. msgExtraCaps rv < 4\<rbrace>"
   including no_pre
@@ -454,8 +447,6 @@ lemma ko_at_vcpu_at'D:
 crunch pred_tcb_at'2[wp]: doMachineOp "\<lambda>s. P (pred_tcb_at' a b p s)"
   (simp: crunch_simps)
 
-crunch valid_queues'[wp]: readVCPUReg "\<lambda>s. valid_queues s"
-
 crunch valid_objs'[wp]: readVCPUReg "\<lambda>s. valid_objs' s"
 
 crunch sch_act_wf'[wp]: readVCPUReg "\<lambda>s. P (sch_act_wf (ksSchedulerAction s) s)"