rt cspec: update gs_clear_region

Signed-off-by: Michael McInerney <[email protected]>
seL4 · Jul 21, 2022 · 1f6c6d8 · 1f6c6d8
1 parent f90f11e
commit 1f6c6d8
Showing 1 changed file with 7 additions and 5 deletions.
diff --git a/spec/cspec/RISCV64/Kernel_C.thy b/spec/cspec/RISCV64/Kernel_C.thy
@@ -29,11 +29,16 @@ type_synonym cghost_state =
   "(machine_word \<rightharpoonup> vmpage_size) * (machine_word \<rightharpoonup> nat) * ghost_assertions *
    (machine_word \<rightharpoonup> nat)"
 
+abbreviation gs_refill_buffer_lengths :: "cghost_state \<Rightarrow> (machine_word \<rightharpoonup> nat)" where
+  "gs_refill_buffer_lengths \<equiv> snd \<circ> snd \<circ> snd"
+
 definition
   gs_clear_region :: "addr \<Rightarrow> nat \<Rightarrow> cghost_state \<Rightarrow> cghost_state" where
   "gs_clear_region ptr bits gs \<equiv>
-   (%x. if x \<in> {ptr..+2 ^ bits} then None else fst gs x,
-    %x. if x \<in> {ptr..+2 ^ bits} then None else fst (snd gs) x, snd (snd gs))"
+   (\<lambda>x. if x \<in> {ptr..+2 ^ bits} then None else fst gs x,
+    \<lambda>x. if x \<in> {ptr..+2 ^ bits} then None else fst (snd gs) x,
+    fst (snd (snd gs)),
+    \<lambda>x. if x \<in> {ptr..+2 ^ bits} then None else gs_refill_buffer_lengths gs x)"
 
 definition
   gs_new_frames:: "vmpage_size \<Rightarrow> addr \<Rightarrow> nat \<Rightarrow> cghost_state \<Rightarrow> cghost_state"
@@ -53,9 +58,6 @@ definition
                      then Some sz
                      else fst (snd gs) x, snd (snd gs))"
 
-abbreviation gs_refill_buffer_lengths :: "cghost_state \<Rightarrow> (machine_word \<rightharpoonup> nat)" where
-  "gs_refill_buffer_lengths \<equiv> snd \<circ> snd \<circ> snd"
-
 abbreviation (input) refills_len :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
   "refills_len userSize struct_size refill_size \<equiv> (2 ^ userSize - struct_size) div refill_size"