Library Pip.Proof.invariants.Collect

Summary

This file contains the invariant of collect. 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 collect (descChild : vaddr) (vaToCollect : vaddr) :
{{fun s ⇒ partitionsIsolation s ∧ kernelDataIsolation s ∧ verticalSharing s ∧ consistency s }}
collect descChild vaToCollect
{{fun _ s ⇒ partitionsIsolation s ∧ kernelDataIsolation s ∧ verticalSharing s ∧ consistency s }}.

TODO : To be proved