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

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

Require Import Lia Bool Coq.Logic.ProofIrrelevance List Classical_Prop Compare_dec EqNat.
Import List.ListNotations.

Lemma getTablePagesUpdateCurrentPartition s rootStructure phyVA:
getTablePages rootStructure tableSize s =
getTablePages rootStructure tableSize {| currentPartition := phyVA; memory := memory s |}.

Lemma getIndirectionsUpdateCurrentPartition phyVA rootStructure s:
getIndirections rootStructure s =
getIndirections rootStructure {| currentPartition := phyVA; memory := memory s |}.

Lemma getIndirectionUpdateCurrentPartition p a l phyVA s:
getIndirection p a l (nbLevel - 1) s =
getIndirection p a l (nbLevel - 1) {| currentPartition := phyVA; memory := memory s |} .

Lemma getIndirectionUpdateCurrentPartition1 p a l phyVA stop s:
getIndirection p a l stop s =
getIndirection p a l stop {| currentPartition := phyVA; memory := memory s |} .

Lemma getMappedPageUpdateCurrentPartition phyVA p s a :
 getMappedPage p s a =
 getMappedPage p {| currentPartition := phyVA; memory := memory s |} a.

Lemma getAccessibleMappedPageUpdateCurrentPartition phyVA p s a :
 getAccessibleMappedPage p s a =
 getAccessibleMappedPage p {| currentPartition := phyVA; memory := memory s |} a.

Lemma getMappedPagesAuxUpdateCurrentPartition p l s phyVA :
getMappedPagesAux p l s = getMappedPagesAux p l {| currentPartition := phyVA; memory := memory s |}.

Lemma getAccessibleMappedPagesAuxUpdateCurrentPartition p l s phyVA :
getAccessibleMappedPagesAux p l s = getAccessibleMappedPagesAux p l {| currentPartition := phyVA; memory := memory s |}.

Lemma getMappedPagesUpdateCurrentPartition phyVA partition s:
getMappedPages partition s =
getMappedPages partition {| currentPartition := phyVA; memory := memory s |}.

Lemma getAccessibleMappedPagesUpdateCurrentPartition phyVA partition s:
getAccessibleMappedPages partition s =
getAccessibleMappedPages partition {| currentPartition := phyVA; memory := memory s |}.

Lemma getLLPagesUpdateCurrentPartition s:
∀ phyVA p2 : page,
getLLPages p2 s (nbPage+1) =
getLLPages p2 {| currentPartition := phyVA; memory := memory s |} (nbPage+1).

Lemma getconfigPagesUpdateCurrentDescriptor partition phyVA s:
getConfigPages partition s =
getConfigPages partition {| currentPartition := phyVA; memory := memory s |}.

Lemma getUsedPagesUpdateCurrentDescriptor s phyVA child1:
getUsedPages child1 s =
getUsedPages child1 {| currentPartition := phyVA; memory := memory s |}.

Lemma getPdsVAddrUpdateCurrentPartition phyVA parent lvl l s :
getPdsVAddr parent lvl l s =
getPdsVAddr parent lvl l{| currentPartition := phyVA; memory := memory s |}.

Lemma getChildrenUpdateCurrentDescriptor parent phyVA s :
getChildren parent s =
getChildren parent {| currentPartition := phyVA; memory := memory s |}.

Lemma getPartitionsUpdateCurrentDescriptor s phyVA partition :
getPartitions partition s =
getPartitions partition {| currentPartition := phyVA; memory := memory s |}.

Lemma dataStructurePdSh1Sh2asRootUpdateCurrentDescriptor idxroot phyVA s :
dataStructurePdSh1Sh2asRoot idxroot s →
dataStructurePdSh1Sh2asRoot idxroot {| currentPartition := phyVA; memory := memory s |}.

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

Lemma getPdsVAddrCheckChild partition descChild nbL s:
true = checkChild partition nbL s descChild →
In descChild getAllVAddrWithOffset0 →
List.In descChild (getPdsVAddr partition nbL getAllVAddrWithOffset0 s).

Lemma VAisChild phyVA partition nbL pd descChild (ptpd : page) s:
Some nbL = StateLib.getNbLevel →
(Nat.eqb defaultPage ptpd) = false →
nextEntryIsPP partition PDidx pd s →
true = checkChild partition nbL s descChild →
getTableAddrRoot ptpd PDidx partition descChild s →
isEntryPage ptpd (StateLib.getIndexOfAddr descChild fstLevel) phyVA s →
entryPresentFlag ptpd (StateLib.getIndexOfAddr descChild fstLevel) true s →
List.In phyVA (getChildren partition s).

Lemma getPDFlagUpdateCurrentPartition sh1 va phyVA s:
getPDFlag sh1 va {| currentPartition := phyVA; memory := memory s |} =
 getPDFlag sh1 va s.

Lemma accessibleVAIsNotPartitionDescriptorUpdateCurrentDescriptor phyVA s:
accessibleVAIsNotPartitionDescriptor s →
accessibleVAIsNotPartitionDescriptor {| currentPartition := phyVA; memory := memory s |}.

Lemma getVirtualAddressSh2UpdateCurrentPartition sh2 phyVA va s :
getVirtualAddressSh2 sh2 {| currentPartition := phyVA; memory := memory s |} va =
     getVirtualAddressSh2 sh2 s va.

Lemma isAccessibleMappedPageInParentUpdateCurrentPartition
 partition va accessiblePage s parent:
isAccessibleMappedPageInParent partition va accessiblePage
{| currentPartition := parent; memory := memory s |} =
isAccessibleMappedPageInParent partition va accessiblePage s.

Lemma noCycleInPartitionTreeUpdateCurrentPartition
parent s :
noCycleInPartitionTree s →
noCycleInPartitionTree
{| currentPartition := parent; memory := memory s |} .

Lemma configTablesAreDifferentUpdateCurrentPartition
parent s :
configTablesAreDifferent s → configTablesAreDifferent
{| currentPartition := parent; memory := memory s |} .

Lemma isChildUpdateCurrentPartition phyVA s :
isChild s →
isChild {| currentPartition := phyVA; memory := memory s |}.

Lemma getVirtualAddressSh1UpdateCurrentPartition sh1 phyVA va s :
getVirtualAddressSh1 sh1 s va =
getVirtualAddressSh1 sh1 {| currentPartition := phyVA; memory := memory s |} va.

Lemma isDerivedUpdateCurrentPartition parent va phyVA s :
isDerived parent va s =
isDerived parent va {| currentPartition := phyVA; memory := memory s |}.

Lemma physicalPageNotDerivedUpdateCurrentPartition phyVA s :
physicalPageNotDerived s →
physicalPageNotDerived {| currentPartition := phyVA; memory := memory s |}.

Lemma updateCurPartitionToChild descChild vaNotNulll currPart
root isMultiplexer nbL ptpd lastIndex phyVA pd:
{{ fun s : state ⇒((((((((((((partitionsIsolation s ∧ kernelDataIsolation s ∧ verticalSharing s ∧ consistency s) ∧
              beqVAddr defaultVAddr descChild = vaNotNulll) ∧ currPart = currentPartition s) ∧
            root = multiplexer) ∧ isMultiplexer = StateLib.Page.eqb currPart root) ∧
          Some nbL = StateLib.getNbLevel) ∧
         true = StateLib.checkChild currPart nbL s descChild) ∧
        nextEntryIsPP currPart PDidx pd s) ∧
       (getTableAddrRoot' ptpd PDidx currPart descChild s ∧ ptpd = defaultPage ∨
        getTableAddrRoot ptpd PDidx currPart descChild s ∧
        ptpd ≠ defaultPage ∧
        (∀ idx : index,
         StateLib.getIndexOfAddr descChild fstLevel = idx → isPE ptpd idx s))) ∧
      (Nat.eqb defaultPage ptpd) = false) ∧
     StateLib.getIndexOfAddr descChild fstLevel = lastIndex) ∧
    isEntryPage ptpd lastIndex phyVA s) ∧ entryPresentFlag ptpd lastIndex true s }} MAL.updateCurPartition phyVA {{ fun _ (s : state) ⇒
                       partitionsIsolation s ∧ kernelDataIsolation s ∧ verticalSharing s ∧ consistency s }}.
Lemma updateCurPartitionToParent parent currPart root descChild :
{{ fun s : state ⇒
   (((((partitionsIsolation s ∧ kernelDataIsolation s ∧ verticalSharing s ∧ consistency s) ∧ beqVAddr defaultVAddr descChild = true) ∧
      currPart = currentPartition s) ∧ root = multiplexer) ∧ false = StateLib.Page.eqb currPart root) ∧
   nextEntryIsPP currPart PPRidx parent s }}
  MAL.updateCurPartition parent {{ fun _ s ⇒ partitionsIsolation s∧ kernelDataIsolation s ∧ verticalSharing s ∧ consistency s }}.

Lemma getIndirectionActivate (newCurrentPartition : page) (va : vaddr) (s : state) :
let s' := {| currentPartition := newCurrentPartition; memory := memory s |} in
∀ (stop : nat) (pageDir : page) (l : level),
getIndirection pageDir va l stop s = getIndirection pageDir va l stop s'.

Lemma getMappedPagesActivate (newCurrentPartition : page) (somePartition : page) (s : state) :
let s' := {| currentPartition := newCurrentPartition; memory := memory s |} in
getMappedPages somePartition s = getMappedPages somePartition s'.

Lemma getLLPagesActivate (newCurrentPartition : page) (s : state) :
let s' := {| currentPartition := newCurrentPartition; memory := memory s |} in
∀ (somePage : page),
getLLPages somePage s (nbPage + 1) = getLLPages somePage s' (nbPage + 1).

Lemma getTablePagesActivate (newCurrentPartition : page) (s : state) :
let s' := {| currentPartition := newCurrentPartition; memory := memory s |} in
∀ (somePage : page),
getTablePages somePage tableSize s = getTablePages somePage tableSize s'.

Lemma getIndirectionsActivate (newCurrentPartition : page) (s : state) :
let s' := {| currentPartition := newCurrentPartition; memory := memory s |} in
∀ somePage, getIndirections somePage s = getIndirections somePage s'.

Lemma getConfigPagesActivate (newCurrentPartition : page) (somePartition : page) (s : state) :
let s' := {| currentPartition := newCurrentPartition; memory := memory s |} in
getConfigPages somePartition s = getConfigPages somePartition s'.

Lemma getUsedPagesActivate (newCurrentPartition : page) (somePartition : page) (s : state) :
let s' := {| currentPartition := newCurrentPartition; memory := memory s |} in
getUsedPages somePartition s =
getUsedPages somePartition s'.

Lemma getPdActivate (newCurrentPartition : page) (s : state) :
let s' := {| currentPartition := newCurrentPartition; memory := memory s |} in
∀ (partDesc : page),
StateLib.getPd partDesc (memory s) = StateLib.getPd partDesc (memory s').

Lemma getChildrenActivate (newCurrentPartition : page) (s : state) :
let s' := {| currentPartition := newCurrentPartition; memory := memory s |} in
∀ (partDesc : page),
getChildren partDesc s = getChildren partDesc s'.

Lemma partitionTreeRemains (newCurrentPartition : page) (s : state) :
let s' := {| currentPartition := newCurrentPartition; memory := memory s |} in
∀ (root : page),
getPartitions root s = getPartitions root s'.

Lemma InPartDescGetChildrenActivate (newCurrentPartition : page) (s : state) :
let s' := {| currentPartition := newCurrentPartition; memory := memory s |} in
∀ (partDesc childPartDesc : page),
In childPartDesc (getChildren partDesc s) = In childPartDesc (getChildren partDesc s').

Lemma partitionsInPartitionTreeActivate (newCurrentPartition : page) (s : state) :
let s' := {| currentPartition := newCurrentPartition; memory := memory s |} in
∀ (partDesc : page),
In partDesc (getPartitions multiplexer s) = In partDesc (getPartitions multiplexer s').

Lemma partitionsIsolationActivate (partDesc : page) (s : state) :
let s' := {| currentPartition := partDesc; memory := memory s |} in
partitionsIsolation s → partitionsIsolation s'.

Lemma kernelDataIsolationActivate (partDesc : page) (s : state) :
let s' := {| currentPartition := partDesc; memory := memory s |} in
kernelDataIsolation s → kernelDataIsolation s'.

Lemma verticalSharingActivate (partDesc : page) (s : state) :
let s' := {| currentPartition := partDesc; memory := memory s |} in
verticalSharing s → verticalSharing s'.

Lemma nextEntryIsPPActivate (partDesc : page) (s : state) :
let s' := {| currentPartition := partDesc; memory := memory s |} in
∀ (partition entry : page) (idxroot : index),
nextEntryIsPP partition idxroot entry s =
nextEntryIsPP partition idxroot entry s'.

Lemma isVAActivate (partDesc : page) (s : state) :
let s' := {| currentPartition := partDesc; memory := memory s |} in
∀ (p : page) (idx : index),
isVA p idx s = isVA p idx s'.

Lemma isVEActivate (partDesc : page) (s : state) :
let s' := {| currentPartition := partDesc; memory := memory s |} in
∀ (p : page) (idx : index),
isVE p idx s = isVE p idx s'.

Lemma isPEActivate (partDesc : page) (s : state) :
let s' := {| currentPartition := partDesc; memory := memory s |} in
∀ (p : page) (idx : index),
isPE p idx s = isPE p idx s'.

Lemma getAncestorsActivate (partDesc : page) (s : state) :
let s' := {| currentPartition := partDesc; memory := memory s |} in
∀ (partition : page),
getAncestors partition s = getAncestors partition s'.

Lemma partitionDescriptorEntryActivate (partDesc : page) (s : state) :
let s' := {| currentPartition := partDesc; memory := memory s |} in
partitionDescriptorEntry s → partitionDescriptorEntry s'.

Lemma dataStructurePdSh1Sh2asRootActivate (partDesc : page) (s : state) :
let s' := {| currentPartition := partDesc; memory := memory s |} in
∀ idx : index,
dataStructurePdSh1Sh2asRoot idx s → dataStructurePdSh1Sh2asRoot idx s'.

Lemma currentPartitionInPartitionsListActivate (partDesc : page) (s : state) :
let s' := {| currentPartition := partDesc; memory := memory s |} in
currentPartitionInPartitionsList s ∧ In partDesc (getPartitions multiplexer s)
→ currentPartitionInPartitionsList s'.

Lemma noDupMappedPagesListActivate (partDesc : page) (s : state) :
let s' := {| currentPartition := partDesc; memory := memory s |} in
noDupMappedPagesList s → noDupMappedPagesList s'.

Lemma noDupConfigPagesListActivate (partDesc : page) (s : state) :
let s' := {| currentPartition := partDesc; memory := memory s |} in
noDupConfigPagesList s → noDupConfigPagesList s'.

Lemma parentInPartitionListActivate (partDesc : page) (s : state) :
let s' := {| currentPartition := partDesc; memory := memory s |} in
parentInPartitionList s → parentInPartitionList s'.

Lemma accessibleVAIsNotPartitionDescriptorActivate (partDesc : page) (s : state) :
let s' := {| currentPartition := partDesc; memory := memory s |} in
accessibleVAIsNotPartitionDescriptor s → accessibleVAIsNotPartitionDescriptor s'.

Lemma accessibleChildPageIsAccessibleIntoParentActivate (partDesc : page) (s : state) :
let s' := {| currentPartition := partDesc; memory := memory s |} in
accessibleChildPageIsAccessibleIntoParent s → accessibleChildPageIsAccessibleIntoParent s'.

Lemma noCycleInPartitionTreeActivate (partDesc : page) (s : state) :
let s' := {| currentPartition := partDesc; memory := memory s |} in
noCycleInPartitionTree s → noCycleInPartitionTree s'.

Lemma configTablesAreDifferentActivate (partDesc : page) (s : state) :
let s' := {| currentPartition := partDesc; memory := memory s |} in
configTablesAreDifferent s → configTablesAreDifferent s'.

Lemma isChildActivate (partDesc : page) (s : state) :
let s' := {| currentPartition := partDesc; memory := memory s |} in
isChild s → isChild s'.

Lemma physicalPageNotDerivedActivate (partDesc : page) (s : state) :
let s' := {| currentPartition := partDesc; memory := memory s |} in
physicalPageNotDerived s → physicalPageNotDerived s'.

Lemma isParentActivate (partDesc : page) (s : state) :
let s' := {| currentPartition := partDesc; memory := memory s |} in
isParent s → isParent s'.

Lemma noDupPartitionTreeActivate (partDesc : page) (s : state) :
let s' := {| currentPartition := partDesc; memory := memory s |} in
noDupPartitionTree s → noDupPartitionTree s'.

Lemma wellFormedFstShadowActivate (partDesc : page) (s : state) :
let s' := {| currentPartition := partDesc; memory := memory s |} in
wellFormedFstShadow s → wellFormedFstShadow s'.

Lemma wellFormedSndShadowActivate (partDesc : page) (s : state) :
let s' := {| currentPartition := partDesc; memory := memory s |} in
wellFormedSndShadow s → wellFormedSndShadow s'.

Lemma wellFormedShadowsActivate (partDesc : page) (s : state) :
let s' := {| currentPartition := partDesc; memory := memory s |} in
∀ (idx : index),
wellFormedShadows idx s → wellFormedShadows idx s'.

Lemma wellFormedFstShadowIfNoneActivate (partDesc : page) (s : state) :
let s' := {| currentPartition := partDesc; memory := memory s |} in
wellFormedFstShadowIfNone s → wellFormedFstShadowIfNone s'.

Lemma wellFormedFstShadowIfDefaultValuesActivate (partDesc : page) (s : state) :
let s' := {| currentPartition := partDesc; memory := memory s |} in
wellFormedFstShadowIfDefaultValues s → wellFormedFstShadowIfDefaultValues s'.

Lemma consistencyActivate (partDesc : page) (s : state) :
let s' := {| currentPartition := partDesc; memory := memory s |} in
consistency s ∧ In partDesc (getPartitions multiplexer s) ∧ partDesc ≠ defaultPage → consistency s'.

Lemma updateCurPartitionToPartition (partDesc : page) :
{{fun s ⇒ partitionsIsolation s ∧
           kernelDataIsolation s ∧
           verticalSharing s ∧
           consistency s ∧

           In partDesc (getPartitions multiplexer s) ∧
           partDesc ≠ defaultPage
}}
MAL.updateCurPartition partDesc
{{fun _ s' ⇒ partitionsIsolation s' ∧
            kernelDataIsolation s' ∧
            verticalSharing s' ∧
            consistency s'
}}.