Library Pip.Proof.invariants.CountToMap
Summary
This file contains the invariant of countToMap. 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 countToMap (descChild : vaddr) (vaToMap : vaddr) :
{{fun s ⇒ partitionsIsolation s ∧ kernelDataIsolation s ∧ verticalSharing s ∧ consistency s }}
countToMap descChild vaToMap
{{fun _ s ⇒ partitionsIsolation s ∧ kernelDataIsolation s ∧ verticalSharing s ∧ consistency s }}.
Require Import Pip.Core.Services.
Require Import Isolation Consistency.
Lemma countToMap (descChild : vaddr) (vaToMap : vaddr) :
{{fun s ⇒ partitionsIsolation s ∧ kernelDataIsolation s ∧ verticalSharing s ∧ consistency s }}
countToMap descChild vaToMap
{{fun _ s ⇒ partitionsIsolation s ∧ kernelDataIsolation s ∧ verticalSharing s ∧ consistency s }}.
TODO : To be proved