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.
Require Import Pip.Proof.StateLib Pip.Proof.DependentTypeLemmas Pip.Proof.InternalLemmas Pip.Proof.Lib.
Require Import PropagatedProperties Invariants.

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

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

 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 nextind →
StateLib.getIndirection pd va nbL (stop + 1) s = Some nextind.
    Opaque StateLib.getIndirection.
          Opaque StateLib.getIndirection.
          Transparent StateLib.getIndirection.
Lemma indirectionDescriptionInGetIndirections indirection pd partition vaToPrepare l s root:
(root=PDidx∨ root=sh1idx ∨ root=sh2idx) →
nextEntryIsPP partition root pd s →
indirectionDescription s partition indirection root vaToPrepare l →
In indirection (getIndirections pd s).

Lemma getIndirectionProp' :
∀ stop s nextind idxind indirection pd va (nbL : level) entry,
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 entry)→
isEntryPage indirection idxind nextind s →
StateLib.getIndirection pd va nbL stop s = Some indirection →
StateLib.getIndirection pd va nbL (stop + 1) s = Some nextind.

Lemma beq_nat_falseNot (tbl:page) :
(Nat.eqb defaultPage tbl) = false → tbl ≠ defaultPage.
Lemma getIndirectionEqStop :
∀ (stop : nat) (nbL : level) (va1 va2 : vaddr) (pd : page) (s : state),
stop ≤ nbL →
StateLib.checkVAddrsEqualityWOOffset stop va1 va2 nbL = true →
getIndirection pd va1 nbL stop s = getIndirection pd va2 nbL stop s.

Lemma noDupPreviousMMULevels s:
∀ m n pd,
NoDup(getIndirectionsAux pd s m) →
n ≤ m →
NoDup(getIndirectionsAux pd s n ).

Definition or3 idxroot:=
(idxroot=PDidx ∨ idxroot=sh1idx ∨ idxroot = sh2idx).

Definition or2 idxroot:=
(idxroot=PDidx ∨ idxroot = sh2idx).

Lemma indirectionNotInPreviousMMULevel' s (ptVaChildpd:page) idxvaChild
  pdChildphy
vaChild phyDescChild level root:
or3 root →
 partitionDescriptorEntry s →
 isPresentNotDefaultIff s →
 noDupConfigPagesList s →
configTablesAreDifferent s →



StateLib.getNbLevel = Some level →

In phyDescChild (getPartitions multiplexer s) →

 (Nat.eqb defaultPage ptVaChildpd) = false →
 StateLib.getIndexOfAddr vaChild fstLevel = idxvaChild →

nextEntryIsPP phyDescChild root pdChildphy s →
pdChildphy ≠ defaultPage →
getIndirection pdChildphy vaChild level (nbLevel - 1) s =
            Some ptVaChildpd →
            nbLevel -1 > 0 →
¬ In ptVaChildpd (getIndirectionsAux pdChildphy s (nbLevel - 1)).
Lemma indexDecOrNot :
∀ p1 p2 : index, p1 = p2 ∨ p1≠p2.
Lemma levelDecOrNot :
∀ p1 p2 : level, p1 = p2 ∨ p1≠p2.

Lemma checkVAddrsEqualityWOOffsetTrueLe :
∀ stop stopi vaToPrepare vavalue nbL,
stopi ≤ stop →
StateLib.checkVAddrsEqualityWOOffset stop vaToPrepare vavalue nbL = true →
StateLib.checkVAddrsEqualityWOOffset stopi vaToPrepare vavalue nbL = true.

Lemma indirectionNotInPreviousMMULevelAux vaChild s :
∀ (stop : nat) (pdChildphy : page) (level : level) (ptVaChildpd : page),
level > stop - 1 →
0 < stop →
pdChildphy ≠ defaultPage →
getIndirection pdChildphy vaChild level stop s = Some ptVaChildpd →
(Nat.eqb defaultPage ptVaChildpd) = false →
∃ prevtab : page,
  getIndirection pdChildphy vaChild level (stop - 1) s = Some prevtab ∧
  prevtab ≠ defaultPage ∧
  StateLib.readPhyEntry prevtab (StateLib.getIndexOfAddr vaChild (CLevel (level - (stop - 1)))) (memory s) = Some ptVaChildpd.
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 pageTablesAreDifferentMiddle stop0 s:

True →
∀ (n : nat) (root1 root2 table1 table2 : page) (level1 : level) (va1 va2 : vaddr) (stop : nat),
NoDup (getIndirectionsAux root1 s n) →
NoDup (getIndirectionsAux root2 s n) →
StateLib.checkVAddrsEqualityWOOffset (S stop0) va1 va2 level1 = false →
level1 = CLevel (n - 1) ∧ root1 = root2 ∨
level1 < CLevel (n - 1) ∧
(disjoint (getIndirectionsAux root1 s n) (getIndirectionsAux root2 s n) ∧ root1 ≠ root2 ∨ root1 = root2) →
table1 ≠ defaultPage →
table2 ≠ defaultPage →
getIndirection root1 va1 level1 (S stop0) s = Some table1 →
getIndirection root2 va2 level1 (S stop0) s = Some table2 →
S stop0 ≤ stop →
root1 ≠ defaultPage → root2 ≠ defaultPage → S stop0 ≤ level1 → n ≤ nbLevel → table1 ≠ table2.
Lemma pageTablesOrIndicesAreDifferentMiddle stop0 s:

True →
∀ (n : nat) (root1 root2 table1 table2 : page) (level1 : level) (va1 va2 : vaddr) ,
NoDup (getIndirectionsAux root1 s n) →
NoDup (getIndirectionsAux root2 s n) →
StateLib.checkVAddrsEqualityWOOffset (S stop0) va1 va2 level1 = false →
level1 = CLevel (n - 1) ∧ root1 = root2 ∨
level1 < CLevel (n - 1) ∧
(disjoint (getIndirectionsAux root1 s n) (getIndirectionsAux root2 s n) ∧ root1 ≠ root2 ∨ root1 = root2) →
table1 ≠ defaultPage →
table2 ≠ defaultPage →
getIndirection root1 va1 level1 stop0 s = Some table1 →
getIndirection root2 va2 level1 stop0 s = Some table2 →

root1 ≠ defaultPage → root2 ≠ defaultPage → S stop0 ≤ level1 → n ≤ nbLevel →
table1 ≠ table2 ∨
StateLib.getIndexOfAddr va1 (CLevel (level1 -stop0)) ≠ StateLib.getIndexOfAddr va2 (CLevel (level1 -stop0)) .
Lemma getIndirectionInGetIndirections2' (stop : nat) s
(va : vaddr) (level1 : level) (table root : page) :
(stop+1) ≤ nbLevel →
getIndirection root va level1 stop s = Some table →
NoDup (getIndirectionsAux root s (stop+1)) →
table ≠ defaultPage →
root ≠ defaultPage →
stop ≤ level1 →
stop > 0 →
¬ In table (getIndirectionsAux root s stop).

Lemma checkVAddrsEqualityWOOffsetPermut' n va1 va2 level1 :
  StateLib.checkVAddrsEqualityWOOffset n va1 va2 level1 =
  StateLib.checkVAddrsEqualityWOOffset n va2 va1 level1.

Lemma getIndirectionInGetIndirections2n:
  ∀ stopn (stop : nat) (s : state) (va : vaddr) (level1 : level) (table root : page),
  stop + 1 ≤ nbLevel →
  getIndirection root va level1 stop s = Some table →
  NoDup (getIndirectionsAux root s (stop+1)) →
  stopn ≤ stop →
  table ≠ defaultPage → root ≠ defaultPage → stop ≤ level1 → stop > 0 → ¬ In table (getIndirectionsAux root s stopn).

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

    Lemma CLevelIdentity' : ∀ l : level, CLevel (l - 0) = l.

Lemma checkVAddrsEqualityWOOffsetFalseS:
∀ stop vaToPrepare vavalue , ∀ (nbL:level),
StateLib.getIndexOfAddr vaToPrepare (CLevel (nbL - stop)) =
StateLib.getIndexOfAddr vavalue (CLevel (nbL - stop)) →
StateLib.checkVAddrsEqualityWOOffset (stop + 1) vaToPrepare vavalue nbL = false →
StateLib.checkVAddrsEqualityWOOffset stop vaToPrepare vavalue nbL = false.

Lemma levelPredMinus1Nat:
  ∀ l0 l' : level,
  StateLib.Level.eqb l0 fstLevel = false → StateLib.Level.pred l0 = Some l' → l0 - 1 = l'.

Lemma CLevelIdentity2 :
∀ x, x < nbLevel → x = CLevel (x).


Lemma getIndirectionStopSRead :
∀ 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 pd va nbL (stop + 1) s = Some ( nextind) →
StateLib.readPhyEntry indirection (StateLib.getIndexOfAddr va (CLevel (nbL - stop))) (memory s) = Some ( nextind).


Lemma inGetChildren child part s (level:level) (currentPD ptDescChildpd ptDescChild currentShadow:page)(descChild:vaddr):
isPE ptDescChildpd (StateLib.getIndexOfAddr descChild fstLevel) s →
getTableAddrRoot ptDescChildpd PDidx part descChild s →
(Nat.eqb defaultPage ptDescChildpd) = false →
isEntryPage ptDescChildpd (StateLib.getIndexOfAddr descChild fstLevel) child s →
entryPresentFlag ptDescChildpd (StateLib.getIndexOfAddr descChild fstLevel) true s →
nextEntryIsPP part PDidx currentPD s →
nextEntryIsPP part sh1idx currentShadow s →
(Nat.eqb defaultPage ptDescChild) = false →
 entryPDFlag ptDescChild (StateLib.getIndexOfAddr descChild fstLevel) true s →
  Some level = StateLib.getNbLevel →
isVE ptDescChild (StateLib.getIndexOfAddr descChild fstLevel) s →
getTableAddrRoot ptDescChild sh1idx part descChild s →
In child (getChildren part s).
    Lemma childIsNotParent (parent phyDescChild:page) s:
    isParent s →
    noCycleInPartitionTree s →
    noDupPartitionTree s →
    In parent (getPartitions multiplexer s) →
    In phyDescChild (getChildren parent s) →
    parent ≠ phyDescChild.
  Lemma levelPredSn nbL l n :
   StateLib.Level.eqb nbL fstLevel = false →
   StateLib.Level.pred nbL = Some l →
   l - n = nbL - S n.
 Lemma getIndirectionMiddle max:
 ∀ pd va nbL s last stop,
 getIndirection pd va nbL max s = Some last →
 last ≠ defaultPage →
 max ≥ stop →
 (∃ middle, getIndirection pd va nbL stop s = Some middle ∧
 getIndirection middle va (CLevel (nbL - stop)) (max-stop) s = Some last).

Lemma getIndirectionMiddle2 stop:
 ∀ pd va nbL s last max middle,
 last ≠ defaultPage →
 max ≥ stop →
 getIndirection pd va nbL stop s = Some middle →
 getIndirection middle va (CLevel (nbL - stop)) (max-stop) s = Some last →
  middle ≠ defaultPage →
 getIndirection pd va nbL max s = Some last.

Lemma nodupLevelMinusN :
∀(m n: nat) p root s va l, p≠ defaultPage →
NoDup (getIndirectionsAux root s (n+m) ) →
n+m ≤ nbLevel →
getIndirection root va l n s = Some p →
NoDup (getIndirectionsAux p s m).

 Lemma LLPartNotNone phyDescChild s:
In phyDescChild (getPartitions multiplexer s) →
partitionDescriptorEntry s →
StateLib.getConfigTablesLinkedList phyDescChild (memory s) = None → False.
 Lemma disjointPartitionDataStructure tbl1 tbl2 root1 root2 idxroot1 idxroot2 partition s:
 or3 idxroot1 →
 or3 idxroot2 →
 idxroot1≠ idxroot2 →
nextEntryIsPP partition idxroot1 root1 s →
nextEntryIsPP partition idxroot2 root2 s →
consistency s →
In partition (getPartitions multiplexer s) →
In tbl1 (getIndirections root1 s) →
In tbl2 (getIndirections root2 s) →
NoDup (getConfigPagesAux partition s) → tbl1 ≠ tbl2.

Lemma indirectionDescriptionNotDefault s partition indirection idxroot vaToPrepare l:
indirectionDescription s partition indirection idxroot vaToPrepare l →
indirection ≠ defaultPage.

Lemma inGetIndirectionsAuxInConfigPages partition pd table idxroot s:
or3 idxroot →
partitionDescriptorEntry s →
In partition (getPartitions multiplexer s) →
In table (getIndirectionsAux pd s nbLevel)→
 nextEntryIsPP partition idxroot pd s →
In table (getConfigPagesAux partition s).

Lemma MMUindirectionIsPE partition pd indirection idx vaToPrepare l s:
pd ≠ defaultPage →
dataStructurePdSh1Sh2asRoot PDidx s →
nextEntryIsPP partition PDidx pd s →
In partition (getPartitions multiplexer s) →
( pd = indirection ∧ Some l = StateLib.getNbLevel ∨
(∃ (nbL : ADT.level) (stop : nat),
   Some nbL = StateLib.getNbLevel ∧
   stop ≤ nbL ∧
   getIndirection pd vaToPrepare nbL stop s = Some indirection ∧
   indirection ≠ defaultPage ∧ l = CLevel (nbL - stop))) →
isPE indirection idx s.
Lemma sh1indirectionIsVE partition pd indirection vaToPrepare s:
pd ≠ defaultPage →
dataStructurePdSh1Sh2asRoot sh1idx s →
nextEntryIsPP partition sh1idx pd s →
In partition (getPartitions multiplexer s) →
∀ (nbL : ADT.level) (stop : nat),
 Some nbL = StateLib.getNbLevel →
 stop ≤ nbL →
 getIndirection pd vaToPrepare nbL stop s = Some indirection →
 indirection ≠ defaultPage →
( ∀ idx,
( stop < nbL ∧ isPE indirection idx s ∨
stop ≥ nbL ∧
isVE indirection idx s)).
Lemma readPhyEntryIsPE table idx p s:
StateLib.readPhyEntry table idx (memory s) = Some p →
isPE table idx s.
Lemma readVirEntryIsPE table idx p s:
StateLib.readVirEntry table idx (memory s) = Some p →
isVE table idx s.

Lemma fstLevelIs0 :
0 = fstLevel.

      Lemma sh2indirectionIsVA partition pd indirection vaToPrepare s:
pd ≠ defaultPage →
dataStructurePdSh1Sh2asRoot sh2idx s →
nextEntryIsPP partition sh2idx pd s →
In partition (getPartitions multiplexer s) →
∀ (nbL : ADT.level) (stop : nat),
 Some nbL = StateLib.getNbLevel →
 stop ≤ nbL →
 getIndirection pd vaToPrepare nbL stop s = Some indirection →
 indirection ≠ defaultPage →
( ∀ idx,
( stop < nbL ∧ isPE indirection idx s ∨
stop ≥ nbL ∧
isVA indirection idx s)).
Lemma readVirtualIsVA table idx p s:
StateLib.readVirtual table idx (memory s) = Some p →
isVA table idx s.

Lemma updateCurPartAndActivate (partDesc pageDir : page)
(P : unit → state → Prop) :
{{ fun s ⇒ P tt {|
  currentPartition := partDesc;
  memory := memory s |} }}
updateCurPartAndActivate partDesc pageDir
{{P}}.