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

Require Import Pip.Proof.Isolation Pip.Proof.Consistency Pip.Proof.WeakestPreconditions Pip.Proof.StateLib.
Require Import Pip.Proof.DependentTypeLemmas Pip.Proof.Lib.
Require Import PropagatedProperties Invariants.

Require Import List Coq.Logic.ProofIrrelevance Lia Classical_Prop Compare_dec EqNat Lt Minus.

Import List.ListNotations.
Lemma inclGetIndirectionsAuxLe root s n m :
n ≤ m →
incl (getIndirectionsAux root s n) (getIndirectionsAux root s m).

Lemma getIndirectionStop1 s indirection x idxind va l:
StateLib.Level.eqb l fstLevel = false → indirection ≠ defaultPage →
lookup indirection idxind (memory s) beqPage beqIndex = Some (PE x) →
StateLib.getIndexOfAddr va l = idxind →
StateLib.getIndirection indirection va l 1 s = Some (pa x).

Lemma inNotInList :
∀ (l : list page) (a : page), In a l ∨ ¬ In a l.

Lemma getIndirectionStopS :
∀ stop (s : state) (nbL : level) nextind pd va indirection,
stop + 1 ≤ nbL → indirection ≠ defaultPage →
StateLib.getIndirection pd va nbL stop s = Some indirection→
StateLib.getIndirection indirection va (CLevel (nbL - stop)) 1 s = Some (pa nextind) →
StateLib.getIndirection pd va nbL (stop + 1) s = Some (pa nextind).
    Opaque StateLib.getIndirection.
          Opaque StateLib.getIndirection.
          Transparent StateLib.getIndirection.
Lemma getIndirectionProp :
∀ stop s nextind idxind indirection pd va (nbL : level),
stop +1 ≤ nbL → indirection ≠ defaultPage →
StateLib.Level.eqb (CLevel (nbL - stop)) fstLevel = false →
StateLib.getIndexOfAddr va (CLevel (nbL - stop)) = idxind →
lookup indirection idxind (memory s) beqPage beqIndex = Some (PE nextind)→
StateLib.getIndirection pd va nbL stop s = Some indirection →
StateLib.getIndirection pd va nbL (stop + 1) s = Some (pa nextind).

Lemma getIndirectionStopS1 :
∀ stop (s : state) (nbL : level) nextind pd va indirection,
stop + 1 ≤ nbL → indirection ≠ defaultPage →
StateLib.getIndirection pd va nbL stop s = Some indirection→
StateLib.getIndirection indirection va (CLevel (nbL - stop)) 1 s = Some (nextind) →
StateLib.getIndirection pd va nbL (stop + 1) s = Some (nextind).
    Opaque StateLib.getIndirection.
          Opaque StateLib.getIndirection.
          Transparent StateLib.getIndirection.
 Lemma getIndirectionRetNotDefaultLtNbLevel:
 ∀ (stop2 stop1 : nat) (nbL : level) (pd table1 table2 : page) (va : vaddr) (s : state),
 (Nat.eqb defaultPage pd) = false →
 stop1 ≤ stop2 →
 getIndirection pd va nbL stop1 s = Some table1 →
 getIndirection pd va nbL stop2 s = Some table2 →
 (Nat.eqb defaultPage table2) = false →
 (Nat.eqb defaultPage table1) = false.
Lemma fstIndirectionContainsValue_nbLevel_1 indirection idxroot s idx va l currentPart :
(idxroot = PDidx ∨ idxroot = sh1idx ∨ idxroot = sh2idx) →
dataStructurePdSh1Sh2asRoot idxroot s → In currentPart (getPartitions multiplexer s) →
StateLib.Level.eqb l fstLevel = true →
nextEntryIsPP currentPart idxroot indirection s →
StateLib.getIndexOfAddr va fstLevel = idx → indirection ≠ defaultPage →
Some l = StateLib.getNbLevel →
isVE indirection idx s ∧ idxroot = sh1idx ∨
isVA indirection idx s ∧ idxroot = sh2idx ∨
isPE indirection idx s ∧ idxroot = PDidx.

Lemma lastIndirectionContainsValueRec idxroot s l rootind indirection va idx currentPart:
StateLib.Level.eqb l fstLevel = true →
In currentPart (getPartitions multiplexer s) →
dataStructurePdSh1Sh2asRoot idxroot s →
 (idxroot = PDidx ∨ idxroot = sh1idx ∨ idxroot = sh2idx )->
 nextEntryIsPP currentPart idxroot rootind s →
rootind ≠ defaultPage →
(∃ (nbL : level) (stop : nat),
                 Some nbL = StateLib.getNbLevel ∧ stop ≤ nbL ∧
                 getIndirection rootind va nbL stop s = Some indirection ∧
                 indirection ≠ defaultPage ∧ l = CLevel (nbL - stop) ) →
StateLib.getIndexOfAddr va fstLevel = idx →
isVE indirection idx s ∧ idxroot = sh1idx ∨
isVA indirection idx s ∧ idxroot = sh2idx ∨
isPE indirection idx s ∧ idxroot = PDidx.

Lemma fstIndirectionContainsPENbLevelGT1 idxroot s l currentpd va idxind currentPart :
(idxroot = PDidx ∨ idxroot = sh1idx ∨ idxroot = sh2idx) →
 StateLib.Level.eqb l fstLevel = false →
dataStructurePdSh1Sh2asRoot idxroot s →
In currentPart (getPartitions multiplexer s) →
nextEntryIsPP currentPart idxroot currentpd s →
 currentpd ≠ defaultPage →
 Some l = StateLib.getNbLevel →
 StateLib.getIndexOfAddr va l = idxind →
isPE currentpd idxind s.

Lemma middleIndirectionsContainsPE idxroot s l rootind indirection va idxind currentPart:
 (idxroot = PDidx ∨ idxroot = sh1idx ∨ idxroot = sh2idx )->
StateLib.Level.eqb l fstLevel = false →
In currentPart (getPartitions multiplexer s) →
dataStructurePdSh1Sh2asRoot idxroot s →

rootind ≠ defaultPage →
(∃ (nbL : level) (stop : nat),
                 Some nbL = StateLib.getNbLevel ∧ stop ≤ nbL ∧
                 getIndirection rootind va nbL stop s = Some indirection ∧
                 indirection ≠ defaultPage ∧ l = CLevel (nbL - stop) ) →
nextEntryIsPP currentPart idxroot rootind s →
isPE indirection idxind s.

Lemma getIndirectionStopLevelGT s va p (l: nat) (level : level) (l0 : nat) p0:
l0 > level → l = level →
getIndirection p va level l s = Some p0 →
getIndirection p va level l0 s = Some p0.

Lemma getIndirectionStopLevelGT2 s va p (l: nat) (level : level) (l0 : nat) p0:
l0 > level → l = level →
getIndirection p va level l0 s = Some p0 →
getIndirection p va level l s = Some p0.

Lemma getIndirectionRetDefaultLtNbLevel l1 l0 (nbL :level) p va s:
l0 > 0 →
l0 < l1 →
l0 < nbL →
getIndirection p va nbL l0 s = Some defaultPage →
getIndirection p va nbL l1 s = Some defaultPage.

Lemma getIndirectionNbLevelEq (l1 l0 : nat) (nbL :level) p va s:
l0 > 0 →
l1 = nbL →
l0 ≤ nbL →
getIndirection p va nbL l0 s = Some defaultPage →
getIndirection p va nbL l1 s = Some defaultPage.

Lemma checkVAddrsEqualityWOOffsetTrue' n va1 va2 (nbL predNbL : level) :
StateLib.checkVAddrsEqualityWOOffset n va1 va2 nbL = true →
predNbL ≤ nbL →
nbL < n →
StateLib.getIndexOfAddr va1 predNbL = StateLib.getIndexOfAddr va2 predNbL .

Lemma checkVAddrsEqualityWOOffsetTrue2 :
∀ (n : nat) (va1 va2 : vaddr) (nbL predNbL : level),
n ≤ nbLevel →
StateLib.checkVAddrsEqualityWOOffset n va1 va2 nbL = true →
nbL < n →
predNbL ≤ nbL →
StateLib.checkVAddrsEqualityWOOffset n va1 va2 predNbL = true.
Lemma checkVAddrsEqualityWOOffsetTrue va1 va2 (nbL predNbL : level):
StateLib.checkVAddrsEqualityWOOffset nbLevel va1 va2 nbL = true →
nbL < nbLevel →
predNbL ≤ nbL →
StateLib.checkVAddrsEqualityWOOffset nbLevel va1 va2 predNbL = true.

Lemma getIndirectionEq (nbL : level) va1 va2 pd stop s:
nbL < nbLevel →
StateLib.checkVAddrsEqualityWOOffset nbLevel va1 va2 nbL = true →
getIndirection pd va1 nbL stop s =
getIndirection pd va2 nbL stop s .

Lemma Index_eq_i (i1 i2 : index) : (ADT.i i1) = (ADT.i i2) → i1 = i2.

Lemma AllIndicesAll : ∀ idx : index, In idx getAllIndices.

Lemma VAddrEqVA (v1 v2: vaddr) : ADT.va v1 = ADT.va v2 → v1 = v2.

Lemma AllVAddrAll : ∀ v : vaddr, In v getAllVAddr.
 Lemma lengthRemoveLast(A :Type) :
     ∀ l : list A, ∀ n, length l = S n →length (removelast l) = n.
     Opaque removelast.
     Transparent removelast.
Lemma AllVAddrWithOffset0 :
∀ va, ∃ va1, In va1 getAllVAddrWithOffset0 ∧
StateLib.checkVAddrsEqualityWOOffset nbLevel va va1 ( CLevel (nbLevel -1) ) = true.

Lemma noDupAllVaddr : NoDup getAllVAddr.

Lemma filterOptionInIff l elt :
List.In elt (filterOption l) ↔ List.In (SomePage elt) l.

Lemma checkVAddrsEqualityWOOffsetEqFalse (nbL alevel : level):
∀ va1 va2,
Some nbL = StateLib.getNbLevel →
alevel ≤ nbL →
false = StateLib.checkVAddrsEqualityWOOffset nbLevel va1 va2 alevel →
va1 ≠ va2.

Lemma getMappedPageEq pd va1 va2 nbL s :
StateLib.getNbLevel = Some nbL →
StateLib.checkVAddrsEqualityWOOffset nbLevel va1 va2 nbL = true →
getMappedPage pd s va1 = getMappedPage pd s va2.

Lemma checkChildEq partition va1 va2 nbL s :
StateLib.getNbLevel = Some nbL →
StateLib.checkVAddrsEqualityWOOffset nbLevel va1 va2 nbL = true →
checkChild partition nbL s va1 = checkChild partition nbL s va2.

Lemma getPDFlagEq sh1 va1 va2 nbL s :
StateLib.getNbLevel = Some nbL →
StateLib.checkVAddrsEqualityWOOffset nbLevel va1 va2 nbL = true →
getPDFlag sh1 va1 s = getPDFlag sh1 va2 s.

Lemma getVirtualAddressSh1Eq sh1 va1 va2 nbL s :
StateLib.getNbLevel = Some nbL →
StateLib.checkVAddrsEqualityWOOffset nbLevel va1 va2 nbL = true →
getVirtualAddressSh1 sh1 s va1 = getVirtualAddressSh1 sh1 s va2.

Lemma checkVAddrsEqualityWOOffsetTrans :
∀ vaChild va1 a level,
StateLib.checkVAddrsEqualityWOOffset nbLevel vaChild va1
          level = true →
StateLib.checkVAddrsEqualityWOOffset nbLevel a va1 level =
      false →
StateLib.checkVAddrsEqualityWOOffset nbLevel vaChild a level = false.
Lemma checkVAddrsEqualityWOOffsetPermut va1 va2 level1 :
  StateLib.checkVAddrsEqualityWOOffset nbLevel va1 va2 level1 =
  StateLib.checkVAddrsEqualityWOOffset nbLevel va2 va1 level1.

Lemma checkVAddrsEqualityWOOffsetEqTrue descChild nbL :
StateLib.checkVAddrsEqualityWOOffset nbLevel descChild descChild nbL = true.
Lemma twoMappedPagesAreDifferent phy1 phy2 v1 v2 p nbL s:
getMappedPage p s v1 = SomePage phy1 →
getMappedPage p s v2 = SomePage phy2→
NoDup (filterOption (map (getMappedPage p s) getAllVAddrWithOffset0)) →
StateLib.getNbLevel = Some nbL →
StateLib.checkVAddrsEqualityWOOffset nbLevel v1 v2 nbL = false →
phy1 ≠ phy2.

Lemma eqMappedPagesEqVaddrs phy1 v1 v2 p s:
getMappedPage p s v1 = SomePage phy1 →
 In v1 getAllVAddrWithOffset0 →
 getMappedPage p s v2 = SomePage phy1→
In v2 getAllVAddrWithOffset0 →
NoDup (filterOption (map (getMappedPage p s) getAllVAddrWithOffset0)) →
v1 = v2.

Lemma getAccessibleMappedPageEq pd va1 va2 nbL s :
StateLib.getNbLevel = Some nbL →
StateLib.checkVAddrsEqualityWOOffset nbLevel va1 va2 nbL = true →
getAccessibleMappedPage pd s va1 = getAccessibleMappedPage pd s va2.

Lemma physicalPageIsAccessible (currentPart : page) (ptPDChild : page)
phyPDChild pdChild idxPDChild accessiblePDChild nbL presentPDChild
currentPD s:
 (Nat.eqb defaultPage ptPDChild ) = false →
accessiblePDChild = true →
presentPDChild = true →
StateLib.getIndexOfAddr pdChild fstLevel = idxPDChild →
nextEntryIsPP currentPart PDidx currentPD s →
Some nbL = StateLib.getNbLevel →
(∀ idx : index,
        StateLib.getIndexOfAddr pdChild fstLevel = idx →
        isPE ptPDChild idx s ∧ getTableAddrRoot ptPDChild PDidx currentPart pdChild s) →
entryPresentFlag ptPDChild idxPDChild presentPDChild s →
entryUserFlag ptPDChild idxPDChild accessiblePDChild s →
isEntryPage ptPDChild (StateLib.getIndexOfAddr pdChild fstLevel) phyPDChild s →
In currentPart (getPartitions multiplexer s) →
In phyPDChild (getAccessibleMappedPages currentPart s).

Lemma getIndirectionFstStep s root va (level1 : level) stop table :
level1 > 0 → stop > 0 → root ≠ defaultPage → table ≠ defaultPage →
getIndirection root va level1 stop s = Some table →
∃ pred page1,page1 ≠ defaultPage ∧ Some pred = StateLib.Level.pred level1 ∧
  StateLib.readPhyEntry root (StateLib.getIndexOfAddr va level1) (memory s) = Some page1 ∧
 getIndirection page1 va pred (stop -1) s = Some table.

Lemma readPhyEntryInGetTablePages s root:
∀ n : nat,
n ≤ tableSize →
∀ (idx : nat) (page1 : page),
idx < n →
page1 ≠ defaultPage →
StateLib.readPhyEntry root (CIndex idx) (memory s) = Some page1 →
In page1 (getTablePages root n s).

Lemma getIndirectionInGetIndirections1 (stop : nat) s:
(stop+1) ≤ nbLevel →
∀ (va : vaddr) (level1 : level) (table root : page) ,
getIndirection root va level1 stop s = Some table →
table ≠ defaultPage →
root ≠ defaultPage → In table (getIndirectionsAux root s (stop+1)).


Lemma getIndirectionInGetIndirections (n : nat) s:
n > 0 →
n ≤ nbLevel →
∀ (va : vaddr) (level1 : level) (table root : page) (stop : nat),
getIndirection root va level1 stop s = Some table →
table ≠ defaultPage →
level1 ≤ CLevel (n - 1) → root ≠ defaultPage → In table (getIndirectionsAux root s n).

Lemma AllPagesAll :
∀ p : page, In p getAllPages.

Lemma lengthNoDupPartitions :
∀ listPartitions : list page, NoDup listPartitions →
length listPartitions ≤ nbPage.

Lemma nextEntryIsPPgetParent partition pd s :
nextEntryIsPP partition PPRidx pd s ↔
StateLib.getParent partition (memory s) = Some pd.

Lemma nbPartition s:
noDupPartitionTree s →
length (getPartitions multiplexer s) < (nbPage+1).

Lemma childrenPartitionInPartitionList s phyVA parent:
noDupPartitionTree s →
In parent (getPartitions multiplexer s ) →
In phyVA (getChildren parent s) →
In phyVA (getPartitions multiplexer s).

Lemma nbPageLL fstLL s:
NoDup(getLLPages fstLL s (nbPage + 1)) →
length (getLLPages fstLL s (nbPage + 1)) <(nbPage + 1).

Lemma inGetLLPages s:
∀ fstLL LLChildphy lastLLTable,
NoDup(getLLPages fstLL s (nbPage + 1)) →
In LLChildphy (getLLPages fstLL s (nbPage + 1)) →
In lastLLTable (getLLPages LLChildphy s (nbPage + 1)) →
In lastLLTable (getLLPages fstLL s (nbPage + 1)).

Lemma verticalSharingRec n s :
NoDup (getPartitions multiplexer s) →
noCycleInPartitionTree s →
isParent s →
verticalSharing s →
∀ currentPart,
In currentPart (getPartitions multiplexer s) →
∀ partition, currentPart≠ partition →
In partition (getPartitionAux currentPart s (n + 1)) →
incl (getMappedPages partition s) (getMappedPages currentPart s).

   Lemma verticalSharingRec2 :
∀ (n : nat) (s : state), NoDup (getPartitions multiplexer s) → noCycleInPartitionTree s →
isParent s →
verticalSharing s →
∀ currentPart : page,
In currentPart (getPartitions multiplexer s) →
∀ partition : page,
currentPart ≠ partition →
In partition (getPartitionAux currentPart s (n + 1)) →
incl (getUsedPages partition s) (getMappedPages currentPart s).
           Lemma toApplyVerticalSharingRec s:
           consistency s →
           verticalSharing s →
           ∀ currentPart child1 closestAnc,
           currentPart ≠ child1 →
            In child1 (getChildren closestAnc s) →
            In closestAnc (getPartitions multiplexer s) →
             In currentPart (getPartitionAux child1 s nbPage) →
            incl (getMappedPages currentPart s) (getMappedPages child1 s).

  Lemma verticalSharing2 child parent s :
  incl (getUsedPages child s) (getMappedPages parent s) →
  incl (getMappedPages child s) (getMappedPages parent s).

Lemma getPartitionAuxMinus1 s :
NoDup (getPartitions multiplexer s) →
isParent s →
∀ n child parent ancestor,
In ancestor (getPartitions multiplexer s) →
StateLib.getParent child (memory s) = Some parent →
In child (flat_map (fun p : page ⇒ getPartitionAux p s n) (getChildren ancestor s)) →
In parent (getPartitionAux ancestor s n).

Lemma isAncestorTrans2 ancestor descParent currentPart s:
noDupPartitionTree s →
multiplexerWithoutParent s →
isParent s →
In currentPart (getPartitions multiplexer s) →
StateLib.getParent descParent (memory s) = Some ancestor →
In descParent (getAncestors currentPart s) →
In ancestor (getAncestors currentPart s).

Lemma getAncestorsProp1 s :
partitionDescriptorEntry s →
parentInPartitionList s →
∀ ancestor parent child ,
In parent (getPartitions multiplexer s) →
In ancestor (getAncestors child s) →
parent ≠ ancestor →
StateLib.getParent child (memory s) = Some parent →
In ancestor (getAncestors parent s).

Lemma isAncestorTrans3 s :
noDupPartitionTree s →
multiplexerWithoutParent s →
noCycleInPartitionTree s →
isParent s →
isChild s →
parentInPartitionList s →
∀ ancestor child x,
In x (getPartitions multiplexer s) →
In child (getPartitions multiplexer s) →
In ancestor (getPartitions multiplexer s) →
In ancestor (getAncestors child s) →
In x (getChildren child s) →

In ancestor (getAncestors x s).

Lemma noCycleInPartitionTree2 s :
noDupPartitionTree s →
multiplexerWithoutParent s →
isChild s →
parentInPartitionList s →
noCycleInPartitionTree s →
isParent s →
∀ n parent child,
In parent (getPartitions multiplexer s) →
In child (getChildren parent s) →
¬ In parent (getPartitionAux child s n).

Lemma accessiblePageIsNotPartitionDescriptor
phyPDChild pdChild idxPDChild accessiblePDChild currentPart nbL presentPDChild
currentPD (ptPDChild : page) s:
partitionsIsolation s →
kernelDataIsolation s →
 (Nat.eqb defaultPage ptPDChild ) = false →
accessiblePDChild = true →
presentPDChild = true →
StateLib.getIndexOfAddr pdChild fstLevel = idxPDChild →
nextEntryIsPP currentPart PDidx currentPD s →
Some nbL = StateLib.getNbLevel →
(∀ idx : index,
        StateLib.getIndexOfAddr pdChild fstLevel = idx →
        isPE ptPDChild idx s ∧ getTableAddrRoot ptPDChild PDidx currentPart pdChild s) →
entryPresentFlag ptPDChild idxPDChild presentPDChild s →
entryUserFlag ptPDChild idxPDChild accessiblePDChild s →
isEntryPage ptPDChild (StateLib.getIndexOfAddr pdChild fstLevel) phyPDChild s →
In currentPart (getPartitions multiplexer s) →
¬ In phyPDChild (getPartitionAux multiplexer s (nbPage + 1)).

Lemma getPdNextEntryIsPPEq partition pd1 pd2 s :
nextEntryIsPP partition PDidx pd1 s →
StateLib.getPd partition (memory s) = Some pd2 →
pd1 = pd2.

Lemma getSh1NextEntryIsPPEq partition pd1 pd2 s :
nextEntryIsPP partition sh1idx pd1 s →
StateLib.getFstShadow partition (memory s) = Some pd2 →
pd1 = pd2.

Lemma getSh2NextEntryIsPPEq partition pd1 pd2 s :
nextEntryIsPP partition sh2idx pd1 s →
StateLib.getSndShadow partition (memory s) = Some pd2 →
pd1 = pd2.

Lemma getListNextEntryIsPPEq partition pd1 pd2 s :
nextEntryIsPP partition sh3idx pd1 s →
StateLib.getConfigTablesLinkedList partition (memory s) = Some pd2 →
pd1 = pd2.

Lemma getParentNextEntryIsPPEq partition pd1 pd2 s :
nextEntryIsPP partition PPRidx pd1 s →
StateLib.getParent partition (memory s) = Some pd2 →
pd1 = pd2.

Lemma nextEntryIsPPgetPd partition pd s :
nextEntryIsPP partition PDidx pd s ↔
StateLib.getPd partition (memory s) = Some pd.

Lemma nextEntryIsPPgetFstShadow partition sh1 s :
nextEntryIsPP partition sh1idx sh1 s ↔
StateLib.getFstShadow partition (memory s) = Some sh1.

Lemma nextEntryIsPPgetSndShadow partition sh2 s :
nextEntryIsPP partition sh2idx sh2 s ↔
StateLib.getSndShadow partition (memory s) = Some sh2.

Lemma nextEntryIsPPgetConfigList partition list s :
nextEntryIsPP partition sh3idx list s →
StateLib.getConfigTablesLinkedList partition (memory s) = Some list.

Lemma accessibleMappedPagesInMappedPages partition s :
incl (getAccessibleMappedPages partition s) (getMappedPages partition s).

Lemma inGetIndirectionsAuxLt pd s stop table bound:
¬ In table (getIndirectionsAux pd s bound) →
stop ≤ bound - 1 →
¬ In table (getIndirectionsAux pd s stop).

Lemma notConfigTableNotPdconfigTableLt partition pd table s stop :
stop < nbLevel - 1 →
partitionDescriptorEntry s →
In partition (getPartitions multiplexer s) →
¬ In table (getConfigPagesAux partition s) →
StateLib.getPd partition (memory s) = Some pd →
¬ In table (getIndirectionsAux pd s (S stop)).
Lemma inGetIndirectionsAuxInConfigPagesPD partition pd table s:
partitionDescriptorEntry s →
In partition (getPartitions multiplexer s) →
In table (getIndirectionsAux pd s nbLevel)→
StateLib.getPd partition (memory s) = Some pd →
In table (getConfigPagesAux partition s).

Lemma notConfigTableNotPdconfigTable partition pd table s :
partitionDescriptorEntry s →
In partition (getPartitions multiplexer s) →
¬ In table (getConfigPagesAux partition s) →
StateLib.getPd partition (memory s) = Some pd →
¬ In table (getIndirectionsAux pd s nbLevel).

Lemma notConfigTableNotSh1configTableLt partition sh1 table s stop :
stop < nbLevel - 1 →
partitionDescriptorEntry s →
In partition (getPartitions multiplexer s) →
¬ In table (getConfigPagesAux partition s) →
StateLib.getFstShadow partition (memory s) = Some sh1 →
¬ In table (getIndirectionsAux sh1 s (S stop)).

Lemma inGetIndirectionsAuxInConfigPagesSh1 partition pd table s:
partitionDescriptorEntry s →
In partition (getPartitions multiplexer s) →
In table (getIndirectionsAux pd s nbLevel)→
StateLib.getFstShadow partition (memory s) = Some pd →
In table (getConfigPagesAux partition s).
Lemma notConfigTableNotSh1configTable partition sh1 table s :
partitionDescriptorEntry s →
In partition (getPartitions multiplexer s) →
¬ In table (getConfigPagesAux partition s) →
StateLib.getFstShadow partition (memory s) = Some sh1 →
¬ In table (getIndirectionsAux sh1 s nbLevel).

Lemma notConfigTableNotSh2configTableLt partition sh2 table s stop :
stop < nbLevel - 1 →
partitionDescriptorEntry s →
In partition (getPartitions multiplexer s) →
¬ In table (getConfigPagesAux partition s) →
StateLib.getSndShadow partition (memory s) = Some sh2 →
¬ In table (getIndirectionsAux sh2 s (S stop)).

Lemma inGetIndirectionsAuxInConfigPagesSh2 partition pd table s:
partitionDescriptorEntry s →
In partition (getPartitions multiplexer s) →
In table (getIndirectionsAux pd s nbLevel)→
StateLib.getSndShadow partition (memory s) = Some pd →
In table (getConfigPagesAux partition s).

Lemma notConfigTableNotSh2configTable partition sh2 table s :
partitionDescriptorEntry s →
In partition (getPartitions multiplexer s) →
¬ In table (getConfigPagesAux partition s) →
StateLib.getSndShadow partition (memory s) = Some sh2 →
¬ In table (getIndirectionsAux sh2 s nbLevel).

Lemma notConfigTableNotListconfigTable partition sh3 table s :
partitionDescriptorEntry s →
In partition (getPartitions multiplexer s) →
¬ In table (getConfigPagesAux partition s) →
StateLib.getConfigTablesLinkedList partition (memory s) = Some sh3 →
¬ In table (getLLPages sh3 s (nbPage + 1)).


Lemma pdSh1Sh2ListExistsNotNull (s: state):
partitionDescriptorEntry s →
∀ partition, In partition (getPartitions multiplexer s) →
(∃ pd , StateLib.getPd partition (memory s) = Some pd ∧ pd ≠ defaultPage) ∧
(∃ sh1, StateLib.getFstShadow partition (memory s) = Some sh1 ∧ sh1 ≠ defaultPage) ∧
(∃ sh2, StateLib.getSndShadow partition (memory s) = Some sh2 ∧ sh2 ≠ defaultPage) ∧
(∃ list, StateLib.getConfigTablesLinkedList partition (memory s) = Some list ∧ list ≠ defaultPage).

Lemma isConfigTable descChild ptRefChild descParent s :
partitionDescriptorEntry s →
In descParent (getPartitions multiplexer s) →
(∀ idx : index,
StateLib.getIndexOfAddr descChild fstLevel = idx →
isPE ptRefChild idx s ∧ getTableAddrRoot ptRefChild PDidx descParent descChild s) →
(Nat.eqb defaultPage ptRefChild) = false →
In ptRefChild (getConfigPages descParent s).

Lemma isConfigTableSh2WithVA descChild ptRefChild descParent s :
partitionDescriptorEntry s →
In descParent (getPartitions multiplexer s) →
(∀ idx : index,
StateLib.getIndexOfAddr descChild fstLevel = idx →
isVA ptRefChild idx s ∧ getTableAddrRoot ptRefChild sh2idx descParent descChild s) →
(Nat.eqb defaultPage ptRefChild) = false →
In ptRefChild (getConfigPages descParent s).

Lemma isConfigTableSh2 descChild ptRefChild descParent s :
partitionDescriptorEntry s →
In descParent (getPartitions multiplexer s) →
getTableAddrRoot ptRefChild sh2idx descParent descChild s →
(Nat.eqb defaultPage ptRefChild) = false →
In ptRefChild (getConfigPages descParent s).
Lemma isConfigTableSh1WithVE descChild ptRefChild descParent s :
partitionDescriptorEntry s →
In descParent (getPartitions multiplexer s) →
(∀ idx : index,
StateLib.getIndexOfAddr descChild fstLevel = idx →
isVE ptRefChild idx s ∧ getTableAddrRoot ptRefChild sh1idx descParent descChild s) →
(Nat.eqb defaultPage ptRefChild) = false →
In ptRefChild (getConfigPages descParent s).

Lemma mappedPageIsNotPTable (table1 table2 currentPart root : page)
F idxroot va idx1 (s : state):
 (idxroot = PDidx ∨ idxroot = sh1idx ∨ idxroot = sh2idx) →
(∀ partition : page,
          In partition (getPartitions multiplexer s) →
          partition = table2 ∨ In table2 (getConfigPagesAux partition s) → False) →
In currentPart (getPartitions multiplexer s) →
partitionDescriptorEntry s →
nextEntryIsPP currentPart idxroot root s →
StateLib.getIndexOfAddr va fstLevel = idx1 →
(∀ idx : index,
        StateLib.getIndexOfAddr va fstLevel = idx →
       F table1 idx s ∧
        getTableAddrRoot table1 idxroot currentPart va s) →
(Nat.eqb defaultPage table1) = false →
table2 ≠ table1.

Lemma entryPresentFlagReadPresent s table idx flag:
entryPresentFlag table idx flag s →
StateLib.readPresent table idx (memory s) = Some flag.

Lemma entryPresentFlagReadPresent' s table idx flag:
entryPresentFlag table idx flag s ↔
StateLib.readPresent table idx (memory s) = Some flag.

Lemma entryUserFlagReadAccessible s table idx flag:
entryUserFlag table idx flag s ↔
StateLib.readAccessible table idx (memory s) = Some flag.

Lemma isEntryPageLookupEq table idx entry phy s:
lookup table idx (memory s) beqPage beqIndex = Some (PE entry) →
isEntryPage table idx phy s →
pa entry = phy.

Lemma isEntryPageReadPhyEntry table idx entry s:
isEntryPage table idx (pa entry) s →
StateLib.readPhyEntry table idx (memory s) = Some (pa entry).

Lemma isEntryPageReadPhyEntry1 table idx p s:
isEntryPage table idx p s →
StateLib.readPhyEntry table idx (memory s) = Some p.
Lemma isAccessibleMappedPage pdChild currentPD (ptPDChild : page) entry s :
(Nat.eqb defaultPage ptPDChild ) = false →
entryPresentFlag ptPDChild (StateLib.getIndexOfAddr pdChild fstLevel) true s →
entryUserFlag ptPDChild (StateLib.getIndexOfAddr pdChild fstLevel) true s →
lookup ptPDChild (StateLib.getIndexOfAddr pdChild fstLevel) (memory s) beqPage beqIndex =
    Some (PE entry) →
 nextEntryIsPP (currentPartition s) PDidx currentPD s →
(∀ idx : index,
StateLib.getIndexOfAddr pdChild fstLevel = idx →
isPE ptPDChild idx s ∧ getTableAddrRoot ptPDChild PDidx (currentPartition s) pdChild s ) →
getAccessibleMappedPage currentPD s pdChild = SomePage (pa entry).
Lemma isAccessibleMappedPage2 partition pdChild currentPD (ptPDChild : page) phypage s :
(Nat.eqb defaultPage ptPDChild ) = false →
entryPresentFlag ptPDChild (StateLib.getIndexOfAddr pdChild fstLevel) true s →
entryUserFlag ptPDChild (StateLib.getIndexOfAddr pdChild fstLevel) true s →
isEntryPage ptPDChild (StateLib.getIndexOfAddr pdChild fstLevel) phypage s →
 nextEntryIsPP partition PDidx currentPD s →
(∀ idx : index,
StateLib.getIndexOfAddr pdChild fstLevel = idx →
isPE ptPDChild idx s ∧ getTableAddrRoot ptPDChild PDidx partition pdChild s ) →
getAccessibleMappedPage currentPD s pdChild = SomePage phypage.

Lemma getPDFlagReadPDflag currentShadow1 pdChild (ptPDChildSh1 : page)
idxPDChild currentPart s:
(Nat.eqb ptPDChildSh1 defaultPage) = false →
nextEntryIsPP currentPart sh1idx currentShadow1 s →
getPDFlag currentShadow1 pdChild s = false →
StateLib.getIndexOfAddr pdChild fstLevel = idxPDChild →
(∀ idx : index,
   StateLib.getIndexOfAddr pdChild fstLevel = idx →
   isVE ptPDChildSh1 idx s ∧
   getTableAddrRoot ptPDChildSh1 sh1idx currentPart pdChild s) →
StateLib.readPDflag ptPDChildSh1 idxPDChild (memory s) = Some false ∨
StateLib.readPDflag ptPDChildSh1 idxPDChild (memory s) = None .

Lemma isVaInParent s va descParent (ptsh2 : page) vaInAncestor sh2 :
(Nat.eqb defaultPage ptsh2) = false →
(∀ idx : index,
StateLib.getIndexOfAddr va fstLevel = idx →
isVA ptsh2 idx s ∧ getTableAddrRoot ptsh2 sh2idx descParent va s) →
isVA' ptsh2 (StateLib.getIndexOfAddr va fstLevel) vaInAncestor s →
nextEntryIsPP descParent sh2idx sh2 s →
getVirtualAddressSh2 sh2 s va = Some vaInAncestor.

Lemma disjointUsedPagesDisjointMappedPages partition1 partition2 s:
disjoint (getUsedPages partition1 s) (getUsedPages partition2 s) →
disjoint (getMappedPages partition1 s) (getMappedPages partition2 s).

Lemma inGetMappedPagesGetIndirection descParent entry vaInDescParent pdDesc (pt : page) nbL1 s:
entryPresentFlag pt (StateLib.getIndexOfAddr vaInDescParent fstLevel) true s →
(Nat.eqb defaultPage pt) = false →
Some nbL1 = StateLib.getNbLevel →
nextEntryIsPP descParent PDidx pdDesc s →
getIndirection pdDesc vaInDescParent nbL1 (nbL1 + 1) s = Some pt →
isEntryPage pt (StateLib.getIndexOfAddr vaInDescParent fstLevel) (pa entry) s →
In (pa entry) (getMappedPages descParent s).

Lemma getMappedPageGetIndirection ancestor phypage newVA pdAncestor
 (ptAncestor : page) L s:
StateLib.readPresent ptAncestor (StateLib.getIndexOfAddr newVA fstLevel)
 (memory s) = Some true →
(Nat.eqb defaultPage ptAncestor) = false →
 Some L = StateLib.getNbLevel →
nextEntryIsPP ancestor PDidx pdAncestor s →
getIndirection pdAncestor newVA L (nbLevel - 1) s = Some ptAncestor →
StateLib.readPhyEntry ptAncestor (StateLib.getIndexOfAddr newVA fstLevel)
 (memory s) = Some phypage →
getMappedPage pdAncestor s newVA = SomePage phypage.

Lemma getMappedPageGetTableRoot ptvaInAncestor ancestor phypage pdAncestor vaInAncestor s :
( ∀ idx : index,
      StateLib.getIndexOfAddr vaInAncestor fstLevel = idx →
      isPE ptvaInAncestor idx s ∧
      getTableAddrRoot ptvaInAncestor PDidx ancestor vaInAncestor s) →
(Nat.eqb defaultPage ptvaInAncestor) = false →
 isEntryPage ptvaInAncestor (StateLib.getIndexOfAddr vaInAncestor fstLevel)
 phypage s →
 entryPresentFlag ptvaInAncestor (StateLib.getIndexOfAddr vaInAncestor fstLevel) true s
  →
nextEntryIsPP ancestor PDidx pdAncestor s →
getMappedPage pdAncestor s vaInAncestor = SomePage phypage.
Lemma getVirtualAddressSh2GetTableRoot:
∀ (ptsh2 descParent sh2 : page)
    (vaInAncestor va: vaddr) (s : state) L,
(∀ idx : index,
  StateLib.getIndexOfAddr va fstLevel = idx →
   isVA ptsh2 idx s ∧ getTableAddrRoot ptsh2 sh2idx descParent va s) →
(Nat.eqb defaultPage ptsh2) = false →
isVA' ptsh2 (StateLib.getIndexOfAddr va fstLevel) vaInAncestor s →
StateLib.getSndShadow descParent (memory s) = Some sh2 →
Some L = StateLib.getNbLevel →
getVirtualAddressSh2 sh2 s va = Some vaInAncestor.

Lemma getMappedPageNotAccessible
ptvaInAncestor ancestor phypage pdAncestor vaInAncestor s :
( ∀ idx : index,
      StateLib.getIndexOfAddr vaInAncestor fstLevel = idx →
      isPE ptvaInAncestor idx s ∧
      getTableAddrRoot ptvaInAncestor PDidx ancestor vaInAncestor s) →
(Nat.eqb defaultPage ptvaInAncestor) = false →
 isEntryPage ptvaInAncestor (StateLib.getIndexOfAddr vaInAncestor fstLevel)
 phypage s →
 entryPresentFlag ptvaInAncestor (StateLib.getIndexOfAddr vaInAncestor fstLevel) true s →
entryUserFlag ptvaInAncestor (StateLib.getIndexOfAddr vaInAncestor fstLevel) false s →
nextEntryIsPP ancestor PDidx pdAncestor s →
getAccessibleMappedPage pdAncestor s vaInAncestor = NonePage.

Lemma getAccessibleMappedPageNotPresent
ptvaInAncestor ancestor pdAncestor vaInAncestor s :
( ∀ idx : index,
      StateLib.getIndexOfAddr vaInAncestor fstLevel = idx →
      isPE ptvaInAncestor idx s ∧
      getTableAddrRoot ptvaInAncestor PDidx ancestor vaInAncestor s) →
(Nat.eqb defaultPage ptvaInAncestor) = false →
 entryPresentFlag ptvaInAncestor (StateLib.getIndexOfAddr vaInAncestor fstLevel) false s →
nextEntryIsPP ancestor PDidx pdAncestor s →
getAccessibleMappedPage pdAncestor s vaInAncestor = NonePage.

Lemma getMappedPageNotPresent
ptvaInAncestor ancestor pdAncestor vaInAncestor s :
( ∀ idx : index,
      StateLib.getIndexOfAddr vaInAncestor fstLevel = idx →
      isPE ptvaInAncestor idx s ∧
      getTableAddrRoot ptvaInAncestor PDidx ancestor vaInAncestor s) →
(Nat.eqb defaultPage ptvaInAncestor) = false →
 entryPresentFlag ptvaInAncestor (StateLib.getIndexOfAddr vaInAncestor fstLevel) false s →
nextEntryIsPP ancestor PDidx pdAncestor s →
getMappedPage pdAncestor s vaInAncestor = SomeDefault.

Lemma inGetMappedPagesGetTableRoot va pt descParent phypage pdParent s :
(∀ idx : index,
StateLib.getIndexOfAddr va fstLevel = idx →
isPE pt idx s ∧ getTableAddrRoot pt PDidx descParent va s) →
(Nat.eqb defaultPage pt) = false →
isEntryPage pt(StateLib.getIndexOfAddr va fstLevel) phypage s →
entryPresentFlag pt (StateLib.getIndexOfAddr va fstLevel) true s →
nextEntryIsPP descParent PDidx pdParent s →
In phypage (getMappedPages descParent s).

Lemma pageDecOrNot :
∀ p1 p2 : page, p1 = p2 ∨ p1≠p2.

Lemma isAncestorTrans ancestor descParent currentPart s:
parentInPartitionList s →
noCycleInPartitionTree s→
isParent s →
noDupPartitionTree s →
multiplexerWithoutParent s →
In currentPart (getPartitions multiplexer s) →
StateLib.getParent descParent (memory s) = Some ancestor →
isAncestor currentPart descParent s →
isAncestor currentPart ancestor s.

Lemma parentIsAncestor partition ancestor s:
nextEntryIsPP partition PPRidx ancestor s →
In ancestor (getAncestors partition s).

Lemma phyPageNotDefault table idx phyPage s :
isPresentNotDefaultIff s →
entryPresentFlag table idx true s →
isEntryPage table idx phyPage s →
(Nat.eqb defaultPage phyPage) = false.

Lemma phyPageIsPresent table idx entry s :
isPresentNotDefaultIff s →
 lookup table idx (memory s) beqPage beqIndex = Some (PE entry) →
(Nat.eqb defaultPage (pa entry)) = false →
present entry = true.

Lemma accessiblePAgeIsMapped pd s va accessiblePage :
getAccessibleMappedPage pd s va = SomePage accessiblePage →
getMappedPage pd s va = SomePage accessiblePage.
Import List.ListNotations.
Lemma getIndirectionsOnlyPD pd s:
(∀ idx : index,
        StateLib.readPhyEntry pd idx (memory s) = Some defaultPage ∧
        StateLib.readPresent pd idx (memory s) = Some false) →
  getIndirections pd s = [pd].

Lemma getIndirectionsOnlySh1 sh1 level s:
Some level =StateLib.getNbLevel →
 isWellFormedFstShadow level sh1 s →
  getIndirections sh1 s = [sh1].

Lemma getIndirectionsOnlySh2 sh2 level s:
Some level =StateLib.getNbLevel →
 isWellFormedSndShadow level sh2 s →
  getIndirections sh2 s = [sh2].

Lemma getLLPagesOnlyRoot root s:
initConfigPagesListPostCondition root s →
 getLLPages root s (nbPage+1) =
[root].

Require Import Coq.Sorting.Permutation.

Lemma getIndirectionGetTableRoot (s : state) currentShadow1 currentPart ptRefChildFromSh1 descChild
nbL :
StateLib.getFstShadow currentPart (memory s) = Some currentShadow1 →
StateLib.getNbLevel = Some nbL →
(∀ idx : index,
  StateLib.getIndexOfAddr descChild fstLevel = idx →
  isVE ptRefChildFromSh1 idx s ∧
  getTableAddrRoot ptRefChildFromSh1 sh1idx currentPart descChild s)
  →
getIndirection currentShadow1 descChild nbL (nbLevel - 1) s = Some ptRefChildFromSh1.

Lemma getIndirectionGetTableRoot1 (s : state) pd currentPart pt va
nbL :
StateLib.getPd currentPart (memory s) = Some pd →
StateLib.getNbLevel = Some nbL →
(∀ idx : index,
  StateLib.getIndexOfAddr va fstLevel = idx →
  isPE pt idx s ∧
  getTableAddrRoot pt PDidx currentPart va s)
  →
getIndirection pd va nbL (nbLevel - 1) s = Some pt.

Lemma readPhyEntryInGetIndirectionsAux s root n:
∀ page1,page1 ≠ defaultPage →
In page1 (getTablePages root tableSize s) →
n> 1 →
In page1 (getIndirectionsAux root s n) .

Lemma nodupLevelMinus1 root s (n0 : nat) idx:
∀ p , p≠ defaultPage →
StateLib.readPhyEntry root idx (memory s) = Some p →
NoDup (getIndirectionsAux root s n0 ) →
 n0 ≤ nbLevel →
NoDup (getIndirectionsAux p s (n0 - 1)).

Lemma inclGetIndirectionsAuxMinus1 n root idx p s:
StateLib.readPhyEntry root idx (memory s) = Some p →
(Nat.eqb defaultPage p) = false →
n> 1 →
incl (getIndirectionsAux p s (n - 1)) (getIndirectionsAux root s n).

Lemma notInFlatMapNotInGetIndirection k l ( p0: page) s x:
In p0 l →
¬ In x (flat_map (fun p : page ⇒ getIndirectionsAux p s k) l) →
¬ In x (getIndirectionsAux p0 s k).

Lemma disjointGetIndirectionsAuxMiddle n (p p0 : page) root (idx1 idx2 : index) s:
p0 ≠ p →
n > 1 →
(Nat.eqb defaultPage p) = false →
(Nat.eqb defaultPage p0) = false →
NoDup (getIndirectionsAux root s n) →
StateLib.readPhyEntry root idx1 (memory s) = Some p0 →
StateLib.readPhyEntry root idx2 (memory s) = Some p →
disjoint (getIndirectionsAux p s (n - 1)) (getIndirectionsAux p0 s (n - 1)).

Lemma getIndirectionInGetIndirectionAuxMinus1 table (p: page) s n va1 pred n1 (level1 : level):
level1> 0 →
(Nat.eqb defaultPage p) = false →
level1 ≤ CLevel (n -1) →
StateLib.Level.pred level1 = Some pred →
table ≠ defaultPage →
n ≤ nbLevel →
n > 1 →
getIndirection p va1 pred n1 s = Some table →
In table (getIndirectionsAux p s (n - 1)).

Lemma getTablePagesNoDup root (p p0 : page) idx1 idx2 s:
idx1 < tableSize → idx2 < tableSize →
NoDup (getTablePages root tableSize s) →
StateLib.readPhyEntry root (CIndex idx1) (memory s) = Some p0 →
StateLib.readPhyEntry root (CIndex idx2) (memory s) = Some p →
(Nat.eqb idx1 idx2) = false →
(Nat.eqb p defaultPage) = false →
(Nat.eqb defaultPage p0) = false →
p0 ≠ p.

Lemma getTablePagesNoDupFlatMap s n k root:
n > 0 →
NoDup
(flat_map (fun p : page ⇒ getIndirectionsAux p s n)
(getTablePages root k s)) →
NoDup (getTablePages root k s).

   Lemma getIndirectionGetTableRoot2 (s : state) sh2 currentPart pt va
nbL :
StateLib.getSndShadow currentPart (memory s) = Some sh2 →
StateLib.getNbLevel = Some nbL →
(∀ idx : index,
  StateLib.getIndexOfAddr va fstLevel = idx →
  isVA pt idx s ∧
  getTableAddrRoot pt sh2idx currentPart va s)
  →
getIndirection sh2 va nbL (nbLevel - 1) s = Some pt.

Lemma pageTablesOrIndicesAreDifferent (root1 root2 table1 table2 : page )
(va1 va2 : vaddr) (level1 : level) (stop : nat) s:
root1 ≠ defaultPage → root2 ≠ defaultPage →
NoDup (getIndirections root1 s) →
NoDup (getIndirections root2 s) →
StateLib.checkVAddrsEqualityWOOffset stop va1 va2 level1 = false →
( (level1 = CLevel (nbLevel -1) ∧ root1 = root2) ∨ (level1 < CLevel (nbLevel -1) /\(
(disjoint (getIndirections root1 s) (getIndirections root2 s)∧ root1 ≠ root2) ∨ root1 = root2 )) )->
table1 ≠ defaultPage →
table2 ≠ defaultPage →

getIndirection root1 va1 level1 stop s = Some table1→
getIndirection root2 va2 level1 stop s = Some table2 →
table1 ≠ table2 ∨ StateLib.getIndexOfAddr va1 fstLevel ≠ StateLib.getIndexOfAddr va2 fstLevel.
Lemma noDupConfigPagesListNoDupGetIndirections s:
partitionDescriptorEntry s →
∀ (partition : page),
In partition (getPartitions multiplexer s) →
NoDup (getConfigPages partition s) →
∀ root idxroot, (idxroot = PDidx ∨ idxroot = sh1idx ∨ idxroot = sh2idx) →
nextEntryIsPP partition idxroot root s→
 NoDup (getIndirections root s).

Lemma toApplyPageTablesOrIndicesAreDifferent idx1 idx2 va1 va2 (table1 table2 : page)
currentPart root idxroot level1 F s:
(idxroot = PDidx ∨ idxroot = sh1idx ∨ idxroot = sh2idx) →
(Nat.eqb defaultPage table1) = false → (Nat.eqb defaultPage table2) = false →
false = StateLib.checkVAddrsEqualityWOOffset nbLevel va1 va2 level1 →
currentPart = currentPartition s →
consistency s →
StateLib.getIndexOfAddr va1 fstLevel = idx1 →
StateLib.getIndexOfAddr va2 fstLevel = idx2 →
(∀ idx : index,
StateLib.getIndexOfAddr va1 fstLevel = idx →
F table1 idx s ∧ getTableAddrRoot table1 idxroot currentPart va1 s) →
(∀ idx : index,
StateLib.getIndexOfAddr va2 fstLevel = idx →
F table2 idx s ∧ getTableAddrRoot table2 idxroot currentPart va2 s) →
nextEntryIsPP currentPart idxroot root s →
Some level1 = StateLib.getNbLevel →
table1 ≠ table2 ∨ idx1 ≠ idx2.

Lemma getMappedPagesAuxConsSome :
∀ pd va phyVa listva s,
getMappedPage pd s va = SomePage phyVa →
 (getMappedPagesAux pd (va :: listva) s) =
 phyVa :: (getMappedPagesAux pd listva) s.

Lemma getMappedPagesAuxConsNone :
 ∀ pd va listva s,
getMappedPage pd s va = NonePage →
 (getMappedPagesAux pd (va :: listva) s) =(getMappedPagesAux pd listva) s.

Lemma getMappedPagesAuxConsDefault :
 ∀ pd va listva s,
getMappedPage pd s va = SomeDefault →
 (getMappedPagesAux pd (va :: listva) s) =(getMappedPagesAux pd listva) s.

Lemma childIsMappedPage partition child s :
In partition (getPartitions multiplexer s) →
In child (getChildren partition s) →
In child (getMappedPages partition s).

Lemma ancestorInPartitionTree s:
parentInPartitionList s →
isChild s →
∀ partition ancestor ,
In partition (getPartitions multiplexer s) →
In ancestor (getAncestors partition s) →
In ancestor (getPartitions multiplexer s).

Lemma getPartitionAuxSn s :
isChild s →
∀ n child parent ancestor,
In child (getPartitions multiplexer s) →
StateLib.getParent child (memory s) = Some parent →
In parent (getPartitionAux ancestor s n) →
In child (flat_map (fun p : page ⇒ getPartitionAux p s n) (getChildren ancestor s)).

Lemma getPartitionAuxSbound s bound :
∀ partition1 partition2, In partition1 (getPartitionAux partition2 s bound) →
In partition1 (getPartitionAux partition2 s (bound+1)).

Lemma idxSh2idxSh1notEq : sh2idx ≠ sh1idx.

Lemma idxPDidxSh1notEq :
PDidx ≠ sh1idx.

Lemma rootStructNotNull root part s idxroot:
idxroot = PDidx ∨
idxroot = sh1idx ∨
idxroot = sh2idx ∨ idxroot = sh3idx ∨ idxroot = PPRidx ∨ idxroot = PRidx →
partitionDescriptorEntry s →
nextEntryIsPP part idxroot root s →
In part (getPartitions multiplexer s) →
root ≠ defaultPage.
 Lemma checkVAddrsEqualityWOOffsetTrue1 s phyDescChild vaChild va level:
      In va (getPdsVAddr phyDescChild level getAllVAddr s) →
StateLib.checkVAddrsEqualityWOOffset nbLevel vaChild va level = true →
StateLib.getNbLevel = Some level →
In vaChild (getPdsVAddr phyDescChild level getAllVAddr s).

Lemma pdPartNotNull phyDescChild pdChildphy s:
In phyDescChild (getPartitions multiplexer s) →
nextEntryIsPP phyDescChild PDidx pdChildphy s →
partitionDescriptorEntry s →
pdChildphy ≠ defaultPage.
Lemma sh1PartNotNull phyDescChild pdChildphy s:
In phyDescChild (getPartitions multiplexer s) →
nextEntryIsPP phyDescChild sh1idx pdChildphy s →
partitionDescriptorEntry s →
pdChildphy ≠ defaultPage.

Lemma sh2PartNotNull phyDescChild pdChildphy s:
In phyDescChild (getPartitions multiplexer s) →
nextEntryIsPP phyDescChild sh2idx pdChildphy s →
partitionDescriptorEntry s →
pdChildphy ≠ defaultPage.

Lemma getConfigTablesRootNotNone phyDescChild s:
In phyDescChild (getPartitions multiplexer s) →
partitionDescriptorEntry s →
StateLib.getConfigTablesLinkedList phyDescChild (memory s) = None → False.

 Lemma sh2PartNotNone phyDescChild s:
In phyDescChild (getPartitions multiplexer s) →
partitionDescriptorEntry s →
StateLib.getSndShadow phyDescChild (memory s) = None → False.

 Lemma sh1PartNotNone phyDescChild s:
In phyDescChild (getPartitions multiplexer s) →
partitionDescriptorEntry s →
StateLib.getFstShadow phyDescChild (memory s) = None → False.
 Lemma configNotDefault s stop:
∀ pd ,
pd≠ defaultPage →
(stop+1) ≤ nbLevel →
  ¬ In defaultPage (getIndirectionsAux pd s stop).

Lemma getIndirectionInGetIndirections2 (stop : nat) s prevtable
(va : vaddr) (level1 : level) (table root : page) :
(stop+1) ≤ nbLevel →
getIndirection root va level1 (stop-1) s = Some prevtable →
StateLib.readPhyEntry prevtable ( StateLib.getIndexOfAddr va (CLevel (level1 - (stop-1))))
         (memory s) = Some table →
NoDup (getIndirectionsAux root s (stop+1)) →
table ≠ defaultPage →
root ≠ defaultPage →
stop ≤ level1 →
prevtable ≠ defaultPage →
¬ In table (getIndirectionsAux root s stop).

Lemma indirectionNotInPreviousMMULevel s ptVaChildpd idxvaChild phyVaChild
  pdChildphy currentPart
presentvaChild vaChild phyDescChild level entry:
 partitionDescriptorEntry s →
 isPresentNotDefaultIff s →
 noDupConfigPagesList s →
configTablesAreDifferent s →
In currentPart (getPartitions multiplexer s) →
In phyVaChild (getAccessibleMappedPages currentPart s) →
lookup ptVaChildpd idxvaChild (memory s) beqPage beqIndex = Some (PE entry) →
StateLib.getNbLevel = Some level →
negb presentvaChild = true →
In phyDescChild (getPartitions multiplexer s) →
 isPE ptVaChildpd (StateLib.getIndexOfAddr vaChild fstLevel) s →
 getTableAddrRoot ptVaChildpd PDidx phyDescChild vaChild s →
 (Nat.eqb defaultPage ptVaChildpd) = false →
 StateLib.getIndexOfAddr vaChild fstLevel = idxvaChild →
 entryPresentFlag ptVaChildpd idxvaChild presentvaChild s →
nextEntryIsPP phyDescChild PDidx pdChildphy s →
pdChildphy ≠ defaultPage →
getIndirection pdChildphy vaChild level (nbLevel - 1) s =
            Some ptVaChildpd →
            nbLevel -1 > 0 →
¬ In ptVaChildpd (getIndirectionsAux pdChildphy s (nbLevel - 1)).
Lemma vaNotDerived currentPart shadow1 (ptSh1ChildFromSh1 : page) s :
consistency s →
In currentPart (getPartitions multiplexer s) →
(Nat.eqb defaultPage ptSh1ChildFromSh1) = false →
(∃ va : vaddr,
isEntryVA ptSh1ChildFromSh1 (StateLib.getIndexOfAddr shadow1 fstLevel) va s ∧
beqVAddr defaultVAddr va = true) →
(∀ idx : index,
StateLib.getIndexOfAddr shadow1 fstLevel = idx →
isVE ptSh1ChildFromSh1 idx s ∧ getTableAddrRoot ptSh1ChildFromSh1 sh1idx currentPart shadow1 s) →
¬ isDerived currentPart shadow1 s .
Lemma phyNotDerived currentPart phySh1Child currentPD shadow1 (ptSh1Child : page)s :
(Nat.eqb defaultPage ptSh1Child) = false →
¬ isDerived currentPart shadow1 s →
consistency s →
In currentPart (getPartitions multiplexer s) →
nextEntryIsPP currentPart PDidx currentPD s →
(∀ idx : index,
StateLib.getIndexOfAddr shadow1 fstLevel = idx →
isPE ptSh1Child idx s ∧ getTableAddrRoot ptSh1Child PDidx currentPart shadow1 s) →
isEntryPage ptSh1Child (StateLib.getIndexOfAddr shadow1 fstLevel) phySh1Child s →
entryPresentFlag ptSh1Child (StateLib.getIndexOfAddr shadow1 fstLevel) true s →
∀ child : page,
In child (getChildren currentPart s) → ¬ In phySh1Child (getMappedPages child s).

Lemma noDupAllVAddrWithOffset0 :
 NoDup getAllVAddrWithOffset0.

Lemma checkVAddrsEqualityWOOffsetFalseEqOffset nbL a descChild:
StateLib.getNbLevel = Some nbL →
a ≠ descChild →
checkOffset0 descChild = true →
checkOffset0 a = true →
StateLib.checkVAddrsEqualityWOOffset nbLevel a descChild nbL = false.

Lemma getPDFlagGetPdsVAddr' sh1Childphy vaChild phyDescChild level s:
 nextEntryIsPP phyDescChild sh1idx sh1Childphy s →
  getPDFlag sh1Childphy vaChild s = false →
  StateLib.getNbLevel = Some level →
  StateLib.getFstShadow phyDescChild (memory s) = Some sh1Childphy →
  ¬ In vaChild (getPdsVAddr phyDescChild level getAllVAddr s).

Lemma isEntryPageReadPhyEntry2 table idx entry s:
StateLib.readPhyEntry table idx (memory s) = Some (pa entry) →
isEntryPage table idx (pa entry) s.

   Lemma isPresentNotDefaultIffTrue (s :state):
   ∀ (table : page) (idx : index) ,
   isPresentNotDefaultIff s →
StateLib.readPresent table idx (memory s) = Some true →
StateLib.readPhyEntry table idx (memory s) ≠ Some defaultPage.