Isabelle2018: DSpec

spec/capDL/CNode_D.thy

@@ -27,7 +27,7 @@ definition
       cdl_cnode_intent \<Rightarrow> cdl_cnode_invocation except_monad"
 where
   "decode_cnode_invocation target target_ref caps intent \<equiv> case intent of
-     (* Copy a cap to anther capslot, without modifying the cap. *)
+       \<comment> \<open>Copy a cap to anther capslot, without modifying the cap.\<close>
        CNodeCopyIntent dest_index dest_depth src_index src_depth rights \<Rightarrow>
          doE
            (src_root, _) \<leftarrow> throw_on_none $ get_index caps 0;

spec/capDL/CSpace_D.thy

@@ -521,7 +521,7 @@ where
   "resolve_address_bits cnode_cap cap_ptr remaining_size = doE
     unlessE (is_cnode_cap cnode_cap) $ throw;
 
-    (* Fetch the next level CNode. *)
+    \<comment> \<open>Fetch the next level CNode.\<close>
     cnode \<leftarrow> liftE $ get_cnode $ cap_object cnode_cap;
     radix_size \<leftarrow> returnOk $ cdl_cnode_size_bits cnode;
     guard_size \<leftarrow> returnOk $ cap_guard_size cnode_cap;
@@ -529,14 +529,14 @@ where
     level_size \<leftarrow> returnOk (radix_size + guard_size);
     assertE (level_size \<noteq> 0);
 
-    (* Ensure the guard matches up. *)
+    \<comment> \<open>Ensure the guard matches up.\<close>
     guard \<leftarrow> returnOk $ (cap_ptr >> (remaining_size-guard_size)) && (mask guard_size);
     unlessE (guard_size \<le> remaining_size \<and> guard = cap_guard) $ throw;
 
-    (* Ensure we still enough unresolved bits left in our CPTR. *)
+    \<comment> \<open>Ensure we still enough unresolved bits left in our CPTR.\<close>
     whenE (level_size > remaining_size) $ throw;
 
-    (* Find the next slot. *)
+    \<comment> \<open>Find the next slot.\<close>
     offset \<leftarrow> returnOk $ (cap_ptr >> (remaining_size-level_size)) && (mask radix_size);
     slot \<leftarrow> returnOk (cap_object cnode_cap, unat offset);
     size_left \<leftarrow> returnOk (remaining_size - level_size);

spec/capDL/KHeap_D.thy

@@ -120,7 +120,7 @@ definition
 where
   "slots_of obj_id \<equiv> \<lambda>s.
   case opt_object obj_id s of
-    None \<Rightarrow> empty
+    None \<Rightarrow> Map.empty
   | Some obj \<Rightarrow> object_slots obj"
 
 (* The cap at the given cap_ref. None if object or cap does not exist *)

spec/capDL/Types_D.thy

@@ -460,7 +460,7 @@ where
   | CNode x \<Rightarrow> cdl_cnode_caps x
   | Tcb x \<Rightarrow> cdl_tcb_caps x
   | IRQNode x \<Rightarrow> cdl_irq_node_caps x
-  | _ \<Rightarrow> empty"
+  | _ \<Rightarrow> Map.empty"
 
 definition
   update_slots :: "cdl_cap_map \<Rightarrow> cdl_object \<Rightarrow> cdl_object"