Library Pip.Proof.invariants.AddVAddr


Require Import Pip.Model.ADT Pip.Model.Hardware Pip.Model.Lib Pip.Model.MAL.
Require Import Pip.Core.Services.

Require Import Pip.Proof.Isolation Pip.Proof.Consistency Pip.Proof.WeakestPreconditions
Pip.Proof.StateLib Pip.Proof.InternalLemmas Pip.Proof.InternalLemmas2 Pip.Proof.DependentTypeLemmas.

Require Import Invariants GetTableAddr UpdateShadow2Structure UpdateShadow1Structure
               PropagatedProperties MapMMUPage.

Require Import Bool List EqNat.

Summary

This file contains the invariant of addVaddr. We prove that this PIP service preserves the isolation property

Lemma addVAddr (vaInCurrentPartition : vaddr) (descChild : vaddr)
(vaChild : vaddr) (r w e : bool) :
{{fun s ⇒ partitionsIsolation s ∧ kernelDataIsolation s ∧ verticalSharing s ∧ consistency s }}
addVAddr vaInCurrentPartition descChild vaChild r w e
{{fun _ s ⇒ partitionsIsolation s ∧ kernelDataIsolation s ∧ verticalSharing s ∧ consistency s }}.
compareVAddrToNull
comparePageToNull
checkKernelMap
checkRights
getCurPartition
getNbLevel
checkChild
getFstShadow
StateLib.getIndexOfAddr
getTableAddr
simplify the new precondition
comparePageToNull
end checkChild getFstShadow
getTableAddr
simplify the new precondition
StateLib.getIndexOfAddr
checkDerivation
readVirEntry
comparePageToNull
getPd
getTableAddr
simplify the new precondition
readAccessible
readPresent
getTableAddr : to return the physical page of the descChild
simplify the new precondition
StateLib.getIndexOfAddr
readPresent
readPhyEntry
getPd
descChild is a child
getTableAddr : to check if the virtual address is available to map a new page
simplify the new precondition
StateLib.getIndexOfAddr
readPresent
readPhyEntry
getSndShadow
getTableAddr : to access to the second shadow page table
simplify the new precondition
write virtual
writeVirEntry
writeVirEntry