Library Pip.Proof.invariants.mapInChild
Require Import Pip.Model.ADT Pip.Model.Hardware Pip.Model.Lib Pip.Model.MAL.
Require Import Pip.Core.Services.
Require Import Pip.Proof.Consistency Pip.Proof.DependentTypeLemmas Pip.Proof.InternalLemmas
Pip.Proof.Isolation Pip.Proof.StateLib Pip.Proof.WeakestPreconditions.
Require Import Invariants GetTableAddr.
Require Import Bool List EqNat.
Summary
This file contains the invariant of addVaddr. We prove that this PIP service preserves the isolation propertyLemma mappedInChild (vaChild : vaddr) :
{{fun s ⇒ partitionsIsolation s ∧ kernelDataIsolation s ∧ verticalSharing s ∧ consistency s }}
mappedInChild vaChild
{{fun _ s ⇒ partitionsIsolation s ∧ kernelDataIsolation s ∧ verticalSharing s ∧ consistency s }}.
getCurPartition
getNbLevel
getPd
getTableAddr
simplify the new precondition
StateLib.getIndexOfAddr
getFstShadow
getTableAddr : to check if the virtual address is available to map a new page
simplify the new precondition
StateLib.getIndexOfAddr
readVirEntry
ret