Require Import Pip.Model.ADT Pip.Model.Hardware Pip.Model.Lib Pip.Model.MAL.
Require Import Pip.Core.Internal.
Require Import Pip.Proof.Isolation Pip.Proof.Consistency Pip.Proof.WeakestPreconditions
               Pip.Proof.StateLib Pip.Proof.DependentTypeLemmas Pip.Proof.InternalLemmas.
Require Import Invariants GetTableAddr.

Require Import List Coq.Logic.ProofIrrelevance Lia EqNat Compare_dec.

Lemma checkChild (parent : page) (va : vaddr) (nbL : level) (P : state → Prop) :
{{fun s ⇒ P s ∧ consistency s ∧ parent = currentPartition s ∧ Some nbL = StateLib.getNbLevel}}
Internal.checkChild parent nbL va
{{fun isChild s ⇒ P s ∧ isChild = StateLib.checkChild parent nbL s va}}.

Lemma checkChildInv vaInCurrentPartition vaChild currentPart descChild level:
{{ fun s : state ⇒ ((((partitionsIsolation s ∧
    kernelDataIsolation s ∧
    verticalSharing s ∧
    consistency s) ∧
    (Nat.eqb Kidx
       (List.nth (length vaInCurrentPartition - (nbLevel - 1 + 2)) vaInCurrentPartition defaultIndex))
       = false) ∧
    (Nat.eqb Kidx
       (List.nth (length vaChild - (nbLevel - 1 + 2)) vaChild defaultIndex))
       = false) ∧
    currentPart = currentPartition s) ∧
    Some level = StateLib.getNbLevel
}}
  Internal.checkChild currentPart level descChild
{{
  fun res s ⇒
     (res = false ∧
        partitionsIsolation s ∧
        kernelDataIsolation s ∧
        verticalSharing s ∧
        consistency s
     )
  ∨ (res = true ∧
        ∃ currentShadow1 idxRefChild ptRefChild,
          partitionsIsolation s ∧
          kernelDataIsolation s ∧
          verticalSharing s ∧
          consistency s ∧

          (Nat.eqb
             Kidx
             (List.nth (length vaInCurrentPartition - (nbLevel - 1 + 2)) vaInCurrentPartition defaultIndex)
          ) = false ∧
          (Nat.eqb
             Kidx
             (List.nth (length vaChild - (nbLevel - 1 + 2)) vaChild defaultIndex)
          ) = false ∧

          currentPart = currentPartition s ∧
          Some level = StateLib.getNbLevel ∧

          nextEntryIsPP currentPart sh1idx currentShadow1 s ∧
          StateLib.getIndexOfAddr descChild fstLevel = idxRefChild ∧
          (getTableAddrRoot' ptRefChild sh1idx currentPart descChild s ∧
             ptRefChild = defaultPage ∨
             (∀ idx : index,
                StateLib.getIndexOfAddr descChild fstLevel = idx →
                  isVE ptRefChild idx s ∧
                  getTableAddrRoot ptRefChild sh1idx currentPart descChild s
             )
          ) ∧
          (Nat.eqb defaultPage ptRefChild) = false
     )
}}.

Lemma childInPartTree (childPartDesc parentPartDesc parentPageDir childLastMMUPage : page)
                      (s : state)
                      (nbL : level)
                      (childPartDescVAddr : vaddr)
                      (idxChildPartDesc : index) :
 Some nbL = StateLib.getNbLevel
 → nextEntryIsPP parentPartDesc PDidx parentPageDir s
 → currentPartition s = parentPartDesc
 → isPE childLastMMUPage (StateLib.getIndexOfAddr childPartDescVAddr fstLevel) s
 → getTableAddrRoot childLastMMUPage PDidx parentPartDesc childPartDescVAddr s
 → defaultPage ≠ childLastMMUPage
 → StateLib.getIndexOfAddr childPartDescVAddr fstLevel = idxChildPartDesc
 → isEntryPage childLastMMUPage idxChildPartDesc childPartDesc s
 → entryPresentFlag childLastMMUPage idxChildPartDesc true s
 → true = StateLib.checkChild parentPartDesc nbL s childPartDescVAddr
 → consistency s
 → In childPartDesc (getPartitions multiplexer s).