Library Pip.Proof.invariants.DeletePartition
Summary
This file contains the invariant of deletePartition. We prove that this PIP service preserves the isolation property
Require Import Pip.Model.ADT Pip.Model.Hardware.
Require Import Pip.Core.Services.
Require Import Isolation Consistency.
Lemma deletePartition (descChild : vaddr) :
{{fun s ⇒ partitionsIsolation s ∧ kernelDataIsolation s ∧ verticalSharing s ∧ consistency s }}
deletePartition descChild
{{fun _ s ⇒ partitionsIsolation s ∧ kernelDataIsolation s ∧ verticalSharing s ∧ consistency s }}.
Require Import Pip.Core.Services.
Require Import Isolation Consistency.
Lemma deletePartition (descChild : vaddr) :
{{fun s ⇒ partitionsIsolation s ∧ kernelDataIsolation s ∧ verticalSharing s ∧ consistency s }}
deletePartition descChild
{{fun _ s ⇒ partitionsIsolation s ∧ kernelDataIsolation s ∧ verticalSharing s ∧ consistency s }}.