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

Require Import Pip.Proof.Consistency Pip.Proof.DependentTypeLemmas Pip.Proof.Isolation
               Pip.Proof.InternalLemmas Pip.Proof.StateLib Pip.Proof.WeakestPreconditions.

Require Import Invariants UpdateMappedPageContent PropagatedProperties InitPEntryTable InitVEntryTable.

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


Lemma initFstShadowNewProperty table (nbL : level)(curidx : index):
{{ fun s ⇒ initFstShadowPreconditionToProveNewProperty nbL s table curidx }}
Internal.initFstShadow table nbL curidx
{{fun _ s ⇒ isWellFormedFstShadow nbL table s
  }}.

Lemma initFstShadowTablePropagateProperties1 nbL
table phyPDChild
       phySh1Child phySh2Child phyConfigPagesList phyDescChild (curidx : index) zero currentPart currentPD
 level ptRefChild descChild idxRefChild presentRefChild ptPDChild pdChild
 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 :
{{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)))/\
   zero = CIndex 0 ) ∧
  (∀ partition : page,
  In partition (getPartitions multiplexer s) →
  partition = table ∨ In table (getConfigPagesAux partition s) → False) ∧
  (Nat.eqb defaultPage table) = false
}}

initFstShadow table nbL curidx

{{ fun res 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)))/\
   zero = CIndex 0 ) }}.

Lemma initFstShadowPropagateProperties2 nbL accessibleChild accessibleSh1 accessibleSh2 accessibleList
partition va1 va2 idxVa1 idxVa2 (table1 table2 : page) phyPage1
      phyPage2 curidx 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 zero :
{{ fun s : state ⇒
   (propagatedProperties accessibleChild accessibleSh1 accessibleSh2 accessibleList
   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)))
∧ zero = CIndex 0) ∧
      
      (Nat.eqb defaultPage table1) = false ∧
      (Nat.eqb defaultPage table2) = false ∧
       nextEntryIsPP partition PDidx currentPD s ∧
      In partition (getPartitions multiplexer s) ∧
              
  ( ∀ idx, StateLib.readPhyEntry phyPage2 idx s.(memory) = Some defaultPage ∧
              StateLib.readPresent phyPage2 idx (memory s) = Some false )
              ∧
   
   
   (∀ partition : page,
    In partition (getPartitions multiplexer s) →
    partition = phyPage1 ∨ In phyPage1 (getConfigPagesAux partition s) → False) ∧
   ( (Nat.eqb defaultPage phyPage1) = false) ∧
   isEntryPage table1 idxVa1 phyPage1 s ∧
       isEntryPage table2 idxVa2 phyPage2 s ∧
       StateLib.getIndexOfAddr va1 fstLevel = idxVa1 ∧
       StateLib.getIndexOfAddr va2 fstLevel = idxVa2 ∧
       (∀ idx : index,
        StateLib.getIndexOfAddr va1 fstLevel = idx → isPE table1 idx s ∧
         getTableAddrRoot table1 PDidx partition va1 s) ∧
       (∀ idx : index,
        StateLib.getIndexOfAddr va2 fstLevel = idx →
        isPE table2 idx s ∧ getTableAddrRoot table2 PDidx partition va2 s) ∧
        Some level = StateLib.getNbLevel ∧
       false = StateLib.checkVAddrsEqualityWOOffset nbLevel va2 va1 level ∧
       entryPresentFlag table1 idxVa1 true s ∧ entryPresentFlag table2 idxVa2 true s

}}
 initFstShadow phyPage1 nbL curidx {{ fun _ (s : state) ⇒
 ( ∀ idx, StateLib.readPhyEntry phyPage2 idx s.(memory) = Some defaultPage ∧
              StateLib.readPresent phyPage2 idx (memory s) = Some false )
              }}.

Lemma initFstShadowPrepareHT lpred ptMMUTrdVA phySh2addr phySh1addr indMMUToPrepare ptMMUFstVA phyMMUaddr
      lastLLTable phyPDChild currentShadow2 phySh2Child currentPD ptSh1TrdVA ptMMUSndVA ptSh1SndVA ptSh1FstVA
      currentShadow1 descChildphy phySh1Child currentPart trdVA nextVA vaToPrepare sndVA fstVA nbLgen l idxFstVA idxSndVA idxTrdVA zeroI LLroot LLChildphy newLastLLable minFI indMMUToPreparebool:
{{ fun s : state ⇒
(propagatedPropertiesPrepare indMMUToPreparebool LLroot LLChildphy newLastLLable s ptMMUTrdVA phySh2addr phySh1addr indMMUToPrepare ptMMUFstVA phyMMUaddr
  lastLLTable phyPDChild currentShadow2 phySh2Child currentPD ptSh1TrdVA ptMMUSndVA ptSh1SndVA ptSh1FstVA
  currentShadow1 descChildphy phySh1Child currentPart trdVA nextVA vaToPrepare sndVA fstVA nbLgen l false
  false false true true true idxFstVA idxSndVA idxTrdVA zeroI minFI
∧ isPartitionFalseAll s ptSh1FstVA ptSh1TrdVA ptSh1SndVA idxFstVA idxSndVA idxTrdVA
∧ writeAccessibleRecPreparePostcondition currentPart phyMMUaddr s
∧ writeAccessibleRecPreparePostcondition currentPart phySh1addr s
∧ writeAccessibleRecPreparePostcondition currentPart phySh2addr s
∧ StateLib.Level.pred l = Some lpred)
∧ isWellFormedMMUTables phyMMUaddr s }} initFstShadow phySh1addr lpred zeroI
{{fun _ s ⇒ (propagatedPropertiesPrepare indMMUToPreparebool LLroot LLChildphy newLastLLable s ptMMUTrdVA phySh2addr phySh1addr indMMUToPrepare ptMMUFstVA phyMMUaddr
  lastLLTable phyPDChild currentShadow2 phySh2Child currentPD ptSh1TrdVA ptMMUSndVA ptSh1SndVA ptSh1FstVA
  currentShadow1 descChildphy phySh1Child currentPart trdVA nextVA vaToPrepare sndVA fstVA nbLgen l false
  false false true true true idxFstVA idxSndVA idxTrdVA zeroI minFI
∧ isPartitionFalseAll s ptSh1FstVA ptSh1TrdVA ptSh1SndVA idxFstVA idxSndVA idxTrdVA
∧ writeAccessibleRecPreparePostcondition currentPart phyMMUaddr s
∧ writeAccessibleRecPreparePostcondition currentPart phySh1addr s
∧ writeAccessibleRecPreparePostcondition currentPart phySh2addr s
∧ StateLib.Level.pred l = Some lpred)
∧ isWellFormedMMUTables phyMMUaddr s
∧ isWellFormedFstShadow lpred phySh1addr s }}.