Added signature of cap_invalidate_preserves_value to abstract class

rems-project · Feb 20, 2024 · 957bba3 · 957bba3
1 parent 5daaeb8
commit 957bba3
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/theories/Common/Capabilities.v b/theories/Common/Capabilities.v
@@ -329,4 +329,6 @@ Module Type CAPABILITY
 
   Parameter cap_invalidate_invalidates: forall c, cap_is_valid (cap_invalidate c) = false.
 
+  Parameter cap_invalidate_preserves_value: forall c, cap_get_value c = cap_get_value (cap_invalidate c).
+
 End CAPABILITY.