rt crefine: update CRefine sorrying run to latest seL4

Update CRefine proof setup for RISCV64 to seL4 revision 4214775. Signed-off-by: Michael McInerney <[email protected]>
seL4 · Oct 19, 2023 · 4d1bd0e · 4d1bd0e
1 parent 6526a0e
commit 4d1bd0e
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 6 deletions.
diff --git a/proof/crefine/RISCV64/Invoke_C.thy b/proof/crefine/RISCV64/Invoke_C.thy
@@ -77,14 +77,14 @@ lemma setDomain_ccorres:
       apply simp
       apply wp
      apply (rule_tac Q="\<lambda>_. invs' and tcb_at' t and sch_act_simple
-                        and (\<lambda>s. rv = ksCurThread s)
+                        and (\<lambda>s. curThread = ksCurThread s)
                         and (\<lambda>s. \<forall>d p. distinct (ksReadyQueues s (d, p)))"
                   in hoare_strengthen_post)
        apply wp
       apply (fastforce simp: valid_pspace_valid_objs' weak_sch_act_wf_def
                       split: if_splits)
      apply (rule_tac Q="\<lambda>_. invs' and tcb_at' t and sch_act_simple
-                            and (\<lambda>s. rv = ksCurThread s \<and> (\<forall>p. t \<notin> set (ksReadyQueues s p)))
+                            and (\<lambda>s. curThread = ksCurThread s \<and> (\<forall>p. t \<notin> set (ksReadyQueues s p)))
                             and (\<lambda>s. \<forall>d p. distinct (ksReadyQueues s (d, p)))"
                   in hoare_strengthen_post)
       apply (wpsimp wp: threadSet_tcbDomain_update_invs')
@@ -2893,6 +2893,7 @@ lemma decodeUntypedInvocation_ccorres_helper:
                                   fromEnum_object_type_to_H
                                   object_type_from_H_def minSchedContextBits_def
                                   fromAPIType_def RISCV64_H.fromAPIType_def)
+sorry (* decodeUntypedInvocation_ccorres_helper: needs minSchedContextBits update
                 apply (rule syscall_error_throwError_ccorres_n)
                 apply (simp add: syscall_error_to_H_cases)
                apply (rule_tac xf'="nodeCap_'"
@@ -3365,7 +3366,7 @@ lemma decodeUntypedInvocation_ccorres_helper:
                          capCNodeRadix_CL_less_64s rf_sr_ksCurThread not_le
                   elim!: inl_inrE)
   apply (clarsimp simp: enum_object_type enum_apiobject_type word_le_nat_alt seL4_ObjectTypeCount_def)
-  done
+  done *)
 
 lemma decodeUntypedInvocation_ccorres:
 notes TripleSuc[simp]

diff --git a/proof/crefine/RISCV64/Recycle_C.thy b/proof/crefine/RISCV64/Recycle_C.thy
@@ -1113,7 +1113,7 @@ lemma coerce_memset_to_heap_update:
                           (NULL)
                           (seL4_Fault_C (FCP (\<lambda>x. 0)))
                           (lookup_fault_C (FCP (\<lambda>x. 0)))
-                            0 0 0 NULL NULL 0 NULL NULL NULL NULL NULL)"
+                            0 0 0 NULL NULL 0 NULL NULL NULL NULL)"
   apply (intro ext, simp add: heap_update_def)
   apply (rule_tac f="\<lambda>xs. heap_update_list x xs a b" for a b in arg_cong)
   apply (simp add: to_bytes_def size_of_def typ_info_simps tcb_C_tag_def)

diff --git a/proof/crefine/RISCV64/Retype_C.thy b/proof/crefine/RISCV64/Retype_C.thy
@@ -3311,8 +3311,7 @@ proof -
        tcbIPCBuffer_C := 0,
        tcbSchedNext_C := tcb_Ptr 0, tcbSchedPrev_C := tcb_Ptr 0,
        tcbEPNext_C := tcb_Ptr 0, tcbEPPrev_C := tcb_Ptr 0,
-       tcbBoundNotification_C := ntfn_Ptr 0,
-       tcbReply_C := reply_Ptr 0\<rparr>"
+       tcbBoundNotification_C := ntfn_Ptr 0\<rparr>"
   have fbtcb: "from_bytes (replicate (size_of TYPE(tcb_C)) 0) = ?tcb"
     apply (simp add: from_bytes_def)
     apply (simp add: typ_info_simps tcb_C_tag_def)