Library Pip.Proof.Consistency

Summary

This file contains the formalization of the consistency properties : for each one we summarize the description of its definition

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

Require Import Pip.Proof.Lib Pip.Proof.Isolation Pip.Proof.StateLib.

Require Import List Coq.Logic.ProofIrrelevance.
Import List.ListNotations.

The dataStructurePdSh1Sh2asRoot property defines the type of different values

stored into the page directory structure, the first shadow structure and the second shadow structure. Configuation tables of the last level must contain :

Physical entries (the type PEntry is already definded in Model.ADT) for the page directory data structure
Virtual entries (the type VEntry is already definded in Model.ADT ) for the first shadow data structure
Virtual addresses (the type vaddr is already definded in Model.ADT) for the second shadow data structure

The other tables contain Physical entries idxroot should be PDidx, sh1idx or sh2idx. (1)

Definition dataStructurePdSh1Sh2asRoot (idxroot : index) (s : state) :=
∀ (partition : page),
In partition (getPartitions multiplexer s) →
∀ entry, nextEntryIsPP partition idxroot entry s →
∀ va : vaddr,
True → ∀ level stop , Some level = getNbLevel →
∀ indirection idx, getIndirection entry va level stop s = Some indirection →
( indirection = defaultPage ∨
(( ( stop < level ∧ isPE indirection idx s )\/
   ( stop ≥ level ∧ ( (isVE indirection idx s ∧ idxroot = sh1idx ) ∨
                       (isVA indirection idx s ∧ idxroot = sh2idx ) ∨
                       (isPE indirection idx s ∧ idxroot = PDidx ) ) ))
                       ∧
  indirection ≠ defaultPage )) .

Definition wellFormedFstShadow (s : state) :=
∀ partition,
In partition (getPartitions multiplexer s) →
∀ va pg pd sh1,
StateLib.getPd partition (memory s) = Some pd →
StateLib.getFstShadow partition (memory s) = Some sh1 →
getMappedPage pd s va = SomePage pg →
∃ vainparent , getVirtualAddressSh1 sh1 s va = Some vainparent.

Definition wellFormedSndShadow (s : state) :=
∀ partition,
In partition (getPartitions multiplexer s) →
partition ≠ multiplexer →
∀ va pg pd sh2,
StateLib.getPd partition (memory s) = Some pd →
StateLib.getSndShadow partition (memory s) = Some sh2 →
getMappedPage pd s va = SomePage pg →
∃ vainparent , getVirtualAddressSh2 sh2 s va = Some vainparent ∧
beqVAddr defaultVAddr vainparent = false .

Definition wellFormedShadows (idxroot : index) (s : state) :=
∀ (partition : page),
In partition (getPartitions multiplexer s) →
∀ pdroot ,
StateLib.getPd partition (memory s) = Some pdroot →
∀ structroot, nextEntryIsPP partition idxroot structroot s →
∀ nbL stop , Some nbL = getNbLevel →
∀ indirection1 va b,
getIndirection pdroot va nbL stop s = Some indirection1 →
(Nat.eqb defaultPage indirection1 ) = b →
(∃ indirection2 ,
getIndirection structroot va nbL stop s = Some indirection2 ∧
(Nat.eqb defaultPage indirection2 ) = b ).

The currentPartitionInPartitionsList property specifies that the

current partition must be into the list of partitions retrieved from the first created partition (multiplexer) (2)

Definition currentPartitionInPartitionsList (s : state) :=
In (currentPartition s) (getPartitions multiplexer s).

The currentPartitionIsNotDefaultPage t property specifies that the

current partition is not a default physical page (2)

Definition currentPartitionIsNotDefaultPage (s : state) :=
(currentPartition s ) ≠ defaultPage.

The parentInPartitionList property specifies that the parent of a given

partition should be into the list of partitions retrieved from the first created partition (multiplexer) (3)

Definition parentInPartitionList (s : state) :=
∀ partition, In partition (getPartitions multiplexer s) →
∀ parent, nextEntryIsPP partition PPRidx parent s →
In parent (getPartitions multiplexer s).

The partitionDescriptorEntry defines some properties of the partition descriptor.

A partition descriptor is a table containing virtual addresses and physical pages.
Indecie PDidx, sh1idx, sh2idx, PPRidx and PRidx should be less than ("tableSize" - 1) and contain virtual addresses.
The successors of these indices contain physical pages which should not be equal to "defaultPage".

(4)