address PR comments squash

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
seL4 · Feb 12, 2025 · c58bb64 · c58bb64
1 parent 66590fb
commit c58bb64
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 4 deletions.
diff --git a/proof/refine/RISCV64/TcbAcc_R.thy b/proof/refine/RISCV64/TcbAcc_R.thy
@@ -2371,10 +2371,6 @@ lemma threadSet_heap_ls_other:
   apply (wpsimp wp: threadSet_wp)
   by (fastforce dest: heap_path_heap_upd_not_in)
 
-lemma heap_path_not_Nil:
-  "heap_ls hp (Some st) ls \<Longrightarrow> ls \<noteq> []"
-  by fastforce
-
 lemma threadSet_prev_queue_head_other:
   "\<lbrace>\<lambda>s. prev_queue_head q (tcbSchedPrevs_of s)
         \<and> (\<exists>ls. heap_ls (tcbSchedNexts_of s) (tcbQueueHead q) ls \<and> t \<notin> set ls)\<rbrace>

diff --git a/spec/haskell/src/SEL4/Kernel/Thread.lhs b/spec/haskell/src/SEL4/Kernel/Thread.lhs
@@ -854,3 +854,5 @@ Kernel init will created a initial thread whose tcbPriority is max priority.
 >         new_queue <- tcbQueueRemove releaseQueue tcbPtr
 >         setReleaseQueue new_queue
 >         threadSet (\t -> t { tcbInReleaseQueue = False }) tcbPtr
+
+%