Require Import Pip.Model.ADT Pip.Model.Hardware Pip.Model.MAL Pip.Model.Lib.
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 PropagatedProperties Invariants UpdateMappedPageContent WriteIndex
               InsertEntryIntoLL.
Require Import Coq.Logic.ProofIrrelevance Lia List Bool Compare_dec EqNat.
Definition writeIndexInitLLPC phyConfigPagesList (curidx : index) zero maxidx maxidxminus1 eqbZero nullP nullV maxentries oneI twoI s:=

   ((((PeanoNat.Nat.Even curidx ∧
       (∀ idx : index,
        idx > CIndex 1 →
        idx < CIndex (tableSize - 2) →
        PeanoNat.Nat.Odd idx →
        idx < curidx →
        ∃ idxValue : index,
          StateLib.readIndex phyConfigPagesList idx (memory s) = Some idxValue) ∧
       (∀ idx : index,
        idx > CIndex 1 →
        idx < CIndex (tableSize - 2) →
        PeanoNat.Nat.Even idx →
        idx < curidx →
        StateLib.readVirtual phyConfigPagesList idx (memory s) = Some defaultVAddr) ∧
       zero = CIndex 0 ∧
       maxidx = CIndex (tableSize - 1) ∧
       StateLib.Index.pred maxidx = Some maxidxminus1 ∧
       true = StateLib.Index.geb curidx maxidxminus1 ∧
       eqbZero = StateLib.Index.eqb curidx zero ∧
       nullP = defaultPage ∧
       nullV = defaultVAddr ∧
       StateLib.readVirtual phyConfigPagesList maxidxminus1 (memory s) = Some nullV) ∧
      StateLib.readPhysical phyConfigPagesList maxidx (memory s) = Some nullP) ∧
     maxentries = {| i := Init.Nat.div2 tableSize - 2; Hi := MAL.maxFreeLL_obligation_1 |}) ∧
    StateLib.Index.succ zero = Some oneI) ∧ StateLib.Index.succ oneI = Some twoI .

Lemma readIndexUpdateLLIndex idx ptVaInCurPart table idxvaInCurPart s x:
ptVaInCurPart ≠ table ∨ idxvaInCurPart ≠ idx →
StateLib.readIndex ptVaInCurPart idxvaInCurPart (memory s) =
StateLib.readIndex ptVaInCurPart idxvaInCurPart
(memory {|
currentPartition := currentPartition s;
memory := add table idx (I x)
            (memory s) beqPage beqIndex |}).

Lemma writeIndexNbFI phyConfigPagesList (curidx : index) zero maxidx maxidxminus1 eqbZero nullP nullV maxentries oneI twoI :
{{fun s: state ⇒ writeIndexInitLLPC phyConfigPagesList (curidx : index) zero maxidx maxidxminus1 eqbZero nullP nullV maxentries oneI twoI s }}
MAL.writeIndex phyConfigPagesList oneI maxentries {{ fun (_ : unit) (s : state) ⇒
                                                 initConfigPagesListPostCondition
                                                     phyConfigPagesList s }}.

Lemma writeIndexFFI phyConfigPagesList (curidx : index) zero maxidx maxidxminus1 eqbZero nullP nullV maxentries oneI twoI:
{{ fun s : state ⇒ writeIndexInitLLPC phyConfigPagesList (curidx : index) zero maxidx maxidxminus1 eqbZero nullP nullV maxentries oneI twoI s }}
  MAL.writeIndex phyConfigPagesList zero twoI {{ fun _ s ⇒
  writeIndexInitLLPC phyConfigPagesList (curidx : index) zero maxidx maxidxminus1 eqbZero nullP nullV maxentries oneI twoI s }}.

Lemma initConfigPagesListNewProperty phyConfigPagesList (curidx : index):
{{ fun s : state ⇒ ( PeanoNat.Nat.Even curidx) ∧
                  (∀ idx : index, idx > (CIndex 1) → idx < CIndex (tableSize -2) → PeanoNat.Nat.Odd idx → idx < curidx →
                  ∃ idxValue, StateLib.readIndex phyConfigPagesList idx s.(memory) = Some idxValue) ∧
                 (∀ idx : index, idx > (CIndex 1) → idx < CIndex (tableSize -2) → PeanoNat.Nat.Even idx → idx < curidx →
                 StateLib.readVirtual phyConfigPagesList idx s.(memory) = Some defaultVAddr)}}
  Internal.initConfigPagesList phyConfigPagesList curidx
{{ fun _ s ⇒ initConfigPagesListPostCondition phyConfigPagesList s }}.

Lemma initConfigPagesListPropagateProperties
(curidx:index) pdChild currentPart currentPD level ptRefChild descChild idxRefChild
      presentRefChild ptPDChild idxPDChild presentPDChild ptSh1Child shadow1 idxSh1 presentSh1
      ptSh2Child shadow2 idxSh2 presentSh2 ptConfigPagesList idxConfigPagesList
      presentConfigPagesList currentShadow1 ptRefChildFromSh1 derivedRefChild ptPDChildSh1
      derivedPDChild ptSh1ChildFromSh1 derivedSh1Child childSh2 derivedSh2Child childListSh1
      derivedRefChildListSh1 list pzero phyPDChild phySh1Child phySh2Child phyConfigPagesList
      phyDescChild:
presentRefChild = true ∧ presentPDChild = true ∧
              presentConfigPagesList = true ∧ presentSh1 = true ∧ presentSh2 = true
               →
{{ fun s : state ⇒
  (((propagatedProperties false false false false pdChild currentPart currentPD level ptRefChild
        descChild idxRefChild presentRefChild ptPDChild idxPDChild presentPDChild ptSh1Child shadow1
        idxSh1 presentSh1 ptSh2Child shadow2 idxSh2 presentSh2 ptConfigPagesList idxConfigPagesList
        presentConfigPagesList currentShadow1 ptRefChildFromSh1 derivedRefChild ptPDChildSh1
        derivedPDChild ptSh1ChildFromSh1 derivedSh1Child childSh2 derivedSh2Child childListSh1
        derivedRefChildListSh1 list phyPDChild phySh1Child phySh2Child phyConfigPagesList
        phyDescChild s /\((((∀ partition : page,
          In partition (getAncestors currentPart s) →
          ¬ In phyPDChild (getAccessibleMappedPages partition s)) ∧
         (∀ partition : page,
          In partition (getAncestors currentPart s) →
          ¬ In phySh1Child (getAccessibleMappedPages partition s))) ∧
        (∀ partition : page,
         In partition (getAncestors currentPart s) →
         ¬ In phySh2Child (getAccessibleMappedPages partition s))) ∧
       (∀ partition : page,
        In partition (getAncestors currentPart s) →
        ¬ In phyConfigPagesList (getAccessibleMappedPages partition s)) ∧
       (∀ partition : page,
        In partition (getAncestors currentPart s) →
        ¬ In phyDescChild (getAccessibleMappedPages partition s))) ∧ pzero = CIndex 0) ∧ isWellFormedSndShadow level phySh2Child s) ∧
    isWellFormedFstShadow level phySh1Child s) ∧
   (∀ idx : index,
    StateLib.readPhyEntry phyPDChild idx (memory s) = Some defaultPage ∧
    StateLib.readPresent phyPDChild idx (memory s) = Some false) ∧
   (PeanoNat.Nat.Even curidx)
    }}

  Internal.initConfigPagesList phyConfigPagesList curidx
  
  {{ fun _ s ⇒
  (((propagatedProperties false false false false pdChild currentPart currentPD level ptRefChild
        descChild idxRefChild presentRefChild ptPDChild idxPDChild presentPDChild ptSh1Child shadow1
        idxSh1 presentSh1 ptSh2Child shadow2 idxSh2 presentSh2 ptConfigPagesList idxConfigPagesList
        presentConfigPagesList currentShadow1 ptRefChildFromSh1 derivedRefChild ptPDChildSh1
        derivedPDChild ptSh1ChildFromSh1 derivedSh1Child childSh2 derivedSh2Child childListSh1
        derivedRefChildListSh1 list phyPDChild phySh1Child phySh2Child phyConfigPagesList
        phyDescChild s ∧ ((((∀ partition : page,
          In partition (getAncestors currentPart s) →
          ¬ In phyPDChild (getAccessibleMappedPages partition s)) ∧
         (∀ partition : page,
          In partition (getAncestors currentPart s) →
          ¬ In phySh1Child (getAccessibleMappedPages partition s))) ∧
        (∀ partition : page,
         In partition (getAncestors currentPart s) →
         ¬ In phySh2Child (getAccessibleMappedPages partition s))) ∧
       (∀ partition : page,
        In partition (getAncestors currentPart s) →
        ¬ In phyConfigPagesList (getAccessibleMappedPages partition s)) ∧
       (∀ partition : page,
        In partition (getAncestors currentPart s) →
        ¬ In phyDescChild (getAccessibleMappedPages partition s))) ∧pzero = CIndex 0) ∧ isWellFormedSndShadow level phySh2Child s) ∧
    isWellFormedFstShadow level phySh1Child s) ∧
   (∀ idx : index,
    StateLib.readPhyEntry phyPDChild idx (memory s) = Some defaultPage ∧
    StateLib.readPresent phyPDChild idx (memory s) = Some false)
   }}.