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.InternalLemmas
               Pip.Proof.Isolation Pip.Proof.StateLib Pip.Proof.WeakestPreconditions.
Require Import Invariants PropagatedProperties.
Require Import Coq.Logic.ProofIrrelevance Lia List Bool Logic.Classical_Prop Compare_dec.


Lemma inGetTrdShadowInConfigPagesAux partition LL table s:
partitionDescriptorEntry s →
In partition (getPartitions multiplexer s) →
In table (getLLPages LL s (nbPage + 1)) →
StateLib.getConfigTablesLinkedList partition (memory s) = Some LL →
In table (getConfigPagesAux partition s).

Lemma inGetTrdShadowInConfigPages partition LL table s:
partitionDescriptorEntry s →
In partition (getPartitions multiplexer s) →
In table (getLLPages LL s (nbPage + 1)) →
StateLib.getConfigTablesLinkedList partition (memory s) = Some LL →
In table (getConfigPages partition s).
Lemma LLtableNotPartition s LLtable partition LLroot :
In LLtable (getLLPages LLroot s (nbPage + 1))→
StateLib.getConfigTablesLinkedList partition (memory s) = Some LLroot →
In partition (getPartitions multiplexer s) →
In LLtable (getConfigPages partition s) →
configTablesAreDifferent s →
noDupConfigPagesList s →
noDupPartitionTree s →
partitionDescriptorEntry s →
¬ In LLtable (getPartitions multiplexer s).


Lemma getConfigTablesLinkedListUpdateLLCouplePPVA partition x table idx (s : state) entry :
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
partition≠table →
StateLib.getConfigTablesLinkedList partition
  (add table idx (PP x) (memory s) beqPage beqIndex) =
StateLib.getConfigTablesLinkedList partition (memory s).

Lemma getFstShadowUpdateLLCouplePPVA partition x
table idx (s : state) entry :
partition≠table →
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
StateLib.getFstShadow partition
  (add table idx (PP x) (memory s) beqPage beqIndex) =
StateLib.getFstShadow partition (memory s).

Lemma getSndShadowUpdateLLCouplePPVA partition x
table idx (s : state) entry :
partition≠table →
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
StateLib.getSndShadow partition
  (add table idx (PP x) (memory s) beqPage beqIndex) =
StateLib.getSndShadow partition (memory s).

Lemma getPdUpdateLLCouplePPVA partition x
table idx (s : state) entry :
partition≠table →
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
StateLib.getPd partition
  (add table idx (PP x) (memory s) beqPage beqIndex) =
StateLib.getPd partition (memory s).

Lemma getParentUpdateLLCouplePPVA partition x
table idx (s : state) entry :
partition≠table →
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
StateLib.getParent partition
  (add table idx (PP x) (memory s) beqPage beqIndex) =
StateLib.getParent partition (memory s).

Lemma getTablePagesUpdateLLCouplePPVA table idx entry size p (s : state) x:
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
getTablePages p size
 {|
currentPartition := currentPartition s;
memory := add table idx (PP x)
            (memory s) beqPage beqIndex |} =
getTablePages p size s.

Lemma getIndirectionsUpdateLLCouplePPVA table idx entry pd (s : state) x:
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
getIndirections pd
  {|
currentPartition := currentPartition s;
memory := add table idx (PP x)
            (memory s) beqPage beqIndex |} =
getIndirections pd s.

Lemma readPhysicalUpdateLLCouplePPVA idx1
table idx (s : state) p x:
table ≠ p ∨ idx ≠ idx1 →
StateLib.readPhysical p idx1
  (add table idx (PP x) (memory s) beqPage beqIndex) =
StateLib.readPhysical p idx1 (memory s).

Lemma getLLPagesUpdateLLCouplePPVA table idx p2 s x :
let s':= {|
currentPartition := currentPartition s;
memory := add table idx (PP x)
            (memory s) beqPage beqIndex |} in
StateLib.getMaxIndex ≠ Some idx →
getLLPages p2 s' (nbPage + 1) = getLLPages p2 s (nbPage + 1).

Lemma getConfigPagesUpdateLLCouplePPVA s x table idx entry part:
part ≠ table →
StateLib.getMaxIndex ≠ Some idx →
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
 getConfigPages part {|
currentPartition := currentPartition s;
memory := add table idx (PP x)
            (memory s) beqPage beqIndex |} = getConfigPages part s.

Lemma getIndirectionUpdateLLCouplePPVA sh1 table idx s entry va nbL stop x:
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
getIndirection sh1 va nbL stop
  {|
currentPartition := currentPartition s;
memory := add table idx (PP x)
            (memory s) beqPage beqIndex |} =
getIndirection sh1 va nbL stop s .

Lemma readPresentUpdateLLCouplePPVA idx1
table idx (s : state) p entry x:
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
StateLib.readPresent p idx1
  (add table idx (PP x) (memory s) beqPage beqIndex) =
StateLib.readPresent p idx1 (memory s).

Lemma readAccessibleUpdateLLCouplePPVA
table idx (s : state) p idx1 entry x:
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
StateLib.readAccessible p idx1
  (add table idx (PP x) (memory s) beqPage beqIndex) =
StateLib.readAccessible p idx1 (memory s).

Lemma readPhyEntryUpdateLLCouplePPVA
table idx (s : state) p idx1 entry x:
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
StateLib.readPhyEntry p idx1
  (add table idx (PP x) (memory s) beqPage beqIndex) =
StateLib.readPhyEntry p idx1 (memory s).

Lemma readVirEntryUpdateLLCouplePPVA
table idx (s : state) p idx1 entry x:
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
StateLib.readVirEntry p idx1
  (add table idx (PP x) (memory s) beqPage beqIndex) =
StateLib.readVirEntry p idx1 (memory s).

Lemma readPDflagUpdateLLCouplePPVA idx1
table idx (s : state) p entry x:
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
StateLib.readPDflag p idx1
    (add table idx (PP x) (memory s) beqPage beqIndex) =
   StateLib.readPDflag p idx1 (memory s).

Lemma getMappedPageUpdateLLCouplePPVA root s x table idx va entry:
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
getMappedPage root {|
currentPartition := currentPartition s;
memory := add table idx (PP x)
            (memory s) beqPage beqIndex |} va = getMappedPage root s va.

Lemma getAccessibleMappedPageUpdateLLCouplePPVA root s x table idx va entry:
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
getAccessibleMappedPage root {|
currentPartition := currentPartition s;
memory := add table idx (PP x)
            (memory s) beqPage beqIndex |} va = getAccessibleMappedPage root s va.

Lemma getMappedPagesAuxUpdateLLCouplePPVA root s x table idx entry l:
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
getMappedPagesAux root l {|
currentPartition := currentPartition s;
memory := add table idx (PP x)
            (memory s) beqPage beqIndex |} =
getMappedPagesAux root l s.

Lemma getAccessibleMappedPagesAuxUpdateLLCouplePPVA root s x table idx entry l:
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
getAccessibleMappedPagesAux root l {|
currentPartition := currentPartition s;
memory := add table idx (PP x)
            (memory s) beqPage beqIndex |} =
getAccessibleMappedPagesAux root l s.

Lemma getMappedPagesUpdateLLCouplePPVA s x table idx entry part:
part ≠ table →
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
 getMappedPages part {|
currentPartition := currentPartition s;
memory := add table idx (PP x)
            (memory s) beqPage beqIndex |} = getMappedPages part s.

Lemma getAccessibleMappedPagesUpdateLLCouplePPVA s x table idx entry part:
part ≠ table →
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
getAccessibleMappedPages part {|
currentPartition := currentPartition s;
memory := add table idx (PP x)
            (memory s) beqPage beqIndex |} = getAccessibleMappedPages part s.

Lemma checkChildUpdateLLCouplePPVA s x table idx entry l va part:
part ≠ table →
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
checkChild part l {|
currentPartition := currentPartition s;
memory := add table idx (PP x)
            (memory s) beqPage beqIndex |} va = checkChild part l s va.

Lemma getPdsVAddrUpdateLLCouplePPVA s x table idx entry l part:
part ≠ table →
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
 getPdsVAddr part l getAllVAddrWithOffset0 {|
currentPartition := currentPartition s;
memory := add table idx (PP x)
            (memory s) beqPage beqIndex |} = getPdsVAddr part l getAllVAddrWithOffset0 s.

Lemma getChildrenUpdateLLCouplePPVA s x table idx entry part:
part ≠ table →
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
getChildren part s =
getChildren part{|
currentPartition := currentPartition s;
memory := add table idx (PP x)
            (memory s) beqPage beqIndex |}.

Lemma getPartitionsUpdateLLCouplePPVA s x table idx entry:
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
¬In table (getPartitions multiplexer s) →
getPartitions multiplexer s = getPartitions multiplexer{|
currentPartition := currentPartition s;
memory := add table idx (PP x)
            (memory s) beqPage beqIndex |}.

Lemma nextEntryIsPPUpdateLLCouplePPVA table idx0 partition idx v x entry s :
lookup table idx0 (memory s) beqPage beqIndex = Some (I entry) →
table ≠ partition →
nextEntryIsPP partition idx v s ↔
nextEntryIsPP partition idx v
  {|
currentPartition := currentPartition s;
memory := add table idx0 (PP x)
            (memory s) beqPage beqIndex |}.

Lemma isVAUpdateLLCouplePPVA idx partition table entry idxroot s x:
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
isVA partition idxroot s →
isVA partition idxroot
  {|
currentPartition := currentPartition s;
memory := add table idx (PP x)
            (memory s) beqPage beqIndex |}.

Lemma isPEUpdateLLCouplePPVA idx partition table entry idxroot s x:
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
isPE partition idxroot s →
isPE partition idxroot
  {|
currentPartition := currentPartition s;
memory := add table idx (PP x)
            (memory s) beqPage beqIndex |}.

Lemma isVEUpdateLLCouplePPVA idx partition table entry idxroot s x:
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
isVE partition idxroot s →
isVE partition idxroot
  {|
currentPartition := currentPartition s;
memory := add table idx (PP x)
            (memory s) beqPage beqIndex |}.

Lemma entryUserFlagUpdateLLCouplePPVA idx ptVaInCurPartpd idxvaInCurPart table
 entry s x accessiblesrc:
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
entryUserFlag ptVaInCurPartpd idxvaInCurPart accessiblesrc s →
entryUserFlag ptVaInCurPartpd idxvaInCurPart accessiblesrc
  {|
currentPartition := currentPartition s;
memory := add table idx (PP x)
            (memory s) beqPage beqIndex |}.

Lemma entryPresentFlagUpdateLLCouplePPVA idx ptVaInCurPartpd idxvaInCurPart table
 entry s x accessiblesrc:
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
entryPresentFlag ptVaInCurPartpd idxvaInCurPart accessiblesrc s →
entryPresentFlag ptVaInCurPartpd idxvaInCurPart accessiblesrc
  {|
currentPartition := currentPartition s;
memory := add table idx (PP x)
            (memory s) beqPage beqIndex |}.

Lemma entryPDFlagUpdateLLCouplePPVA idx ptDescChild table idxDescChild entry s x flag:
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
entryPDFlag ptDescChild idxDescChild flag s →
entryPDFlag ptDescChild idxDescChild flag
  {|
currentPartition := currentPartition s;
memory := add table idx (PP x)
            (memory s) beqPage beqIndex |}.

Lemma isEntryVAUpdateLLCouplePPVA idx ptVaInCurPart table idxvaInCurPart entry s vainve x:
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
isEntryVA ptVaInCurPart idxvaInCurPart vainve s →
isEntryVA ptVaInCurPart idxvaInCurPart vainve
  {|
currentPartition := currentPartition s;
memory := add table idx (PP x)
            (memory s) beqPage beqIndex |}.

Lemma isIndexValueUpdateLLCouplePPVA idx ptVaInCurPart table idxvaInCurPart s vainve x:
ptVaInCurPart ≠ table ∨ idxvaInCurPart ≠ idx →
isIndexValue ptVaInCurPart idxvaInCurPart vainve s →
isIndexValue ptVaInCurPart idxvaInCurPart vainve
  {|
currentPartition := currentPartition s;
memory := add table idx (PP x)
            (memory s) beqPage beqIndex |}.

Lemma isVA'UpdateLLCouplePPVA idx ptVaInCurPart table idxvaInCurPart entry s vainve x:
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
isVA' ptVaInCurPart idxvaInCurPart vainve s →
isVA' ptVaInCurPart idxvaInCurPart vainve
  {|
currentPartition := currentPartition s;
memory := add table idx (PP x)
            (memory s) beqPage beqIndex |}.

Lemma isEntryPageUpdateLLCouplePPVA idx ptVaInCurPart table idxvaInCurPart entry s vainve x:
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
isEntryPage ptVaInCurPart idxvaInCurPart vainve s →
isEntryPage ptVaInCurPart idxvaInCurPart vainve
  {|
currentPartition := currentPartition s;
memory := add table idx (PP x)
            (memory s) beqPage beqIndex |}.

Lemma partitionsIsolationUpdateLLCouplePPVA s x table idx entry:
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
partitionsIsolation s →
¬ In table (getPartitions multiplexer s) →
StateLib.getMaxIndex ≠ Some idx →
noDupPartitionTree s →
partitionsIsolation {|
currentPartition := currentPartition s;
memory := add table idx (PP x)
            (memory s) beqPage beqIndex |}.

Lemma kernelDataIsolationUpdateLLCouplePPVA s x table idx entry:
StateLib.getMaxIndex ≠ Some idx →
¬ In table (getPartitions multiplexer s) →
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
kernelDataIsolation s →
kernelDataIsolation {|
currentPartition := currentPartition s;
memory := add table idx (PP x)
            (memory s) beqPage beqIndex |}.

Lemma verticalSharingUpdateLLCouplePPVA s x table idx entry:
StateLib.getMaxIndex ≠ Some idx →
¬ In table (getPartitions multiplexer s) →
noDupPartitionTree s →
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
verticalSharing s →
verticalSharing {|
currentPartition := currentPartition s;
memory := add table idx (PP x)
            (memory s) beqPage beqIndex |}.

Lemma isPPUpdateLLCouplePPVA table p idx idx0 x entry s:
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
isPP p idx0 s →
isPP p idx0 {|
      currentPartition := currentPartition s;
      memory := add table idx (PP x) (memory s) beqPage beqIndex |}.

Lemma dataStructurePdSh1Sh2asRootUpdateLLCouplePPVA s x table idx entry idxroot:
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
¬ In table (getPartitions multiplexer s) →
dataStructurePdSh1Sh2asRoot idxroot s →
dataStructurePdSh1Sh2asRoot idxroot {|
currentPartition := currentPartition s;
memory := add table idx (PP x)
            (memory s) beqPage beqIndex |}.

Lemma partitionDescriptorEntryUpdateLLCouplePPVA s x table idx entry:
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
¬ In table (getPartitions multiplexer s) →
partitionDescriptorEntry s →
partitionDescriptorEntry {|
currentPartition := currentPartition s;
memory := add table idx (PP x)
            (memory s) beqPage beqIndex |}.

Lemma currentPartitionInPartitionsListUpdateLLCouplePPVA s x table idx entry :
¬ In table (getPartitions multiplexer s) →
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
currentPartitionInPartitionsList s →
currentPartitionInPartitionsList {|
currentPartition := currentPartition s;
memory := add table idx (PP x)
            (memory s) beqPage beqIndex |}.

Lemma noDupMappedPagesListUpdateLLCouplePPVA s x table idx entry :
¬ In table (getPartitions multiplexer s) →
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
noDupMappedPagesList s →
noDupMappedPagesList {|
currentPartition := currentPartition s;
memory := add table idx (PP x)
            (memory s) beqPage beqIndex |}.

Lemma noDupConfigPagesListUpdateLLCouplePPVA s x table idx entry :
StateLib.getMaxIndex ≠ Some idx →
¬ In table (getPartitions multiplexer s) →
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
noDupConfigPagesList s →
noDupConfigPagesList
  {|
  currentPartition := currentPartition s;
  memory := add table idx (PP x) (memory s) beqPage
              beqIndex |}.

Lemma parentInPartitionListUpdateLLCouplePPVA s x table idx entry :
¬ In table (getPartitions multiplexer s) →
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
parentInPartitionList s →
parentInPartitionList
  {|
  currentPartition := currentPartition s;
  memory := add table idx (PP x) (memory s) beqPage
              beqIndex |}.

Lemma getPDFlagUpdateLLCouplePPVA s x table idx entry sh1 va:
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
getPDFlag sh1 va
  {|
  currentPartition := currentPartition s;
  memory := add table idx (PP x) (memory s) beqPage
              beqIndex |} = getPDFlag sh1 va s.

Lemma accessibleVAIsNotPartitionDescriptorUpdateLLCouplePPVA s x table idx entry :
¬ In table (getPartitions multiplexer s) →
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
accessibleVAIsNotPartitionDescriptor s →
accessibleVAIsNotPartitionDescriptor
  {|
  currentPartition := currentPartition s;
  memory := add table idx (PP x) (memory s) beqPage
              beqIndex |}.

Lemma readVirtualUpdateLLCouplePPVA table1 table2 idx1 idx2 x entry s :

lookup table2 idx2 (memory s) beqPage beqIndex = Some (I entry) →
 StateLib.readVirtual table1 idx1
         (add table2 idx2 (PP x) (memory s) beqPage
     beqIndex) =
 StateLib.readVirtual table1 idx1 (memory s).

Lemma wellFormedShadowsUpdateLLCouplePPVA s vaInCurrentPartition table idx entry idxroot:
¬ In table (getPartitions multiplexer s) →
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
wellFormedShadows idxroot s →
wellFormedShadows idxroot
  {|
  currentPartition := currentPartition s;
  memory := add table idx (PP vaInCurrentPartition) (memory s) beqPage
              beqIndex |}.

Lemma getTableAddrRootUpdateLLCouplePPVA s vaInCurrentPartition table idx entry idxroot
ptDescChild descChild currentPart:
table ≠ currentPart →
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
getTableAddrRoot ptDescChild idxroot currentPart descChild s→
getTableAddrRoot ptDescChild idxroot currentPart descChild
  {|
  currentPartition := currentPartition s;
  memory := add table idx (PP vaInCurrentPartition) (memory s)
              beqPage beqIndex |}.

Lemma getAncestorsUpdateLLCouplePPVA s x table idx entry partition:
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
table ≠ partition →
¬ In table (getAncestors partition s) →
getAncestors partition
  {|
  currentPartition := currentPartition s;
  memory := add table idx (PP x) (memory s)
              beqPage beqIndex |} =
                      getAncestors partition s.

Lemma noCycleInPartitionTreeUpdateLLCouplePPVA s vaInCurrentPartition table idx entry :
¬ In table (getPartitions multiplexer s) →
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
parentInPartitionList s →
isChild s →
noCycleInPartitionTree s →
noCycleInPartitionTree
  {|
  currentPartition := currentPartition s;
  memory := add table idx (PP vaInCurrentPartition) (memory s) beqPage
              beqIndex |}.

Lemma configTablesAreDifferentUpdateLLCouplePPVA s vaInCurrentPartition table idx entry :
StateLib.getMaxIndex ≠ Some idx →
¬ In table (getPartitions multiplexer s) →
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
configTablesAreDifferent s →
configTablesAreDifferent
  {|
  currentPartition := currentPartition s;
  memory := add table idx (PP vaInCurrentPartition) (memory s) beqPage
              beqIndex |}.

Lemma isChildUpdateLLCouplePPVA s vaInCurrentPartition table idx entry :
¬ In table (getPartitions multiplexer s) →
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
parentInPartitionList s →
isChild s →
isChild
  {|
  currentPartition := currentPartition s;
  memory := add table idx (PP vaInCurrentPartition) (memory s) beqPage
              beqIndex |}.

Lemma isPresentNotDefaultIffUpdateLLCouplePPVA s vaInCurrentPartition table idx entry :
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
isPresentNotDefaultIff s →
isPresentNotDefaultIff
  {|
  currentPartition := currentPartition s;
  memory := add table idx (PP vaInCurrentPartition) (memory s) beqPage
              beqIndex |}.

Lemma getVirtualAddressSh1UpdateLLCouplePPVA s vaInCurrentPartition table idx entry p va:
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
getVirtualAddressSh1 p s va =
getVirtualAddressSh1 p {|
    currentPartition := currentPartition s;
    memory := add table idx (PP vaInCurrentPartition) (memory s) beqPage
                beqIndex |} va.

Lemma getVirtualAddressSh2UpdateLLCouplePPVA s vaInCurrentPartition table idx entry p va:
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
getVirtualAddressSh2 p s va =
getVirtualAddressSh2 p {|
    currentPartition := currentPartition s;
    memory := add table idx (PP vaInCurrentPartition) (memory s) beqPage
                beqIndex |} va.

Lemma isDerivedUpdateLLCouplePPVA s vaInCurrentPartition table idx entry parent va:
¬ In table (getPartitions multiplexer s) →
In parent (getPartitions multiplexer s) →
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
isDerived parent va s → isDerived parent va {|
       currentPartition := currentPartition s;
       memory := add table idx (PP vaInCurrentPartition) (memory s) beqPage
                   beqIndex |}
       .

Lemma physicalPageNotDerivedUpdateLLCouplePPVA s vaInCurrentPartition table idx entry :
¬ In table (getPartitions multiplexer s) →
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
noDupPartitionTree s →
physicalPageNotDerived s →
physicalPageNotDerived
  {|
  currentPartition := currentPartition s;
  memory := add table idx (PP vaInCurrentPartition) (memory s) beqPage
              beqIndex |}.

Lemma multiplexerWithoutParentUpdateLLCouplePPVA s vaInCurrentPartition table idx entry :
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
¬ In table (getPartitions multiplexer s) →
multiplexerWithoutParent s →
multiplexerWithoutParent
  {|
  currentPartition := currentPartition s;
  memory := add table idx (PP vaInCurrentPartition) (memory s) beqPage
              beqIndex |}.

Lemma isParentUpdateLLCouplePPVA s vaInCurrentPartition table idx entry :
¬ In table (getPartitions multiplexer s) →
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
noDupPartitionTree s →
isParent s →
isParent
  {|
  currentPartition := currentPartition s;
  memory := add table idx (PP vaInCurrentPartition) (memory s) beqPage
              beqIndex |}.

Lemma noDupPartitionTreeUpdateLLCouplePPVA s vaInCurrentPartition table idx entry :
¬ In table (getPartitions multiplexer s) →
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
noDupPartitionTree s →
noDupPartitionTree
  {|
  currentPartition := currentPartition s;
  memory := add table idx (PP vaInCurrentPartition) (memory s) beqPage
              beqIndex |}.

Lemma wellFormedFstShadowUpdateLLCouplePPVA s vaInCurrentPartition table idx entry :
¬ In table (getPartitions multiplexer s) →
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
wellFormedFstShadow s →
wellFormedFstShadow
  {|
  currentPartition := currentPartition s;
  memory := add table idx (PP vaInCurrentPartition) (memory s) beqPage
              beqIndex |}.

Lemma wellFormedSndShadowUpdateLLCouplePPVA s vaInCurrentPartition table idx entry :
¬ In table (getPartitions multiplexer s) →
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
wellFormedSndShadow s →
wellFormedSndShadow
  {|
  currentPartition := currentPartition s;
  memory := add table idx (PP vaInCurrentPartition) (memory s) beqPage
              beqIndex |}.

Lemma wellFormedFstShadowIfNoneUpdateLLCouplePPVA s vaInCurrentPartition table idx entry :
¬ In table (getPartitions multiplexer s) →
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
wellFormedFstShadowIfNone s →
wellFormedFstShadowIfNone
  {|
  currentPartition := currentPartition s;
  memory := add table idx (PP vaInCurrentPartition) (memory s) beqPage
              beqIndex |}.

Lemma wellFormedFstShadowIfDefaultValuesUpdateLLCouplePPVA s vaInCurrentPartition table idx entry :
¬ In table (getPartitions multiplexer s) →
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
wellFormedFstShadowIfDefaultValues s →
wellFormedFstShadowIfDefaultValues
  {|
  currentPartition := currentPartition s;
  memory := add table idx (PP vaInCurrentPartition) (memory s) beqPage
              beqIndex |}.

Lemma isAccessibleMappedPageInParentUpdateSh2 s entry v table idx parent va pg:
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
¬In table (getAncestors parent s) →
parent ≠ table →
isAccessibleMappedPageInParent parent va pg s =
isAccessibleMappedPageInParent parent va pg
   {|
  currentPartition := currentPartition s;
  memory := add table idx (PP v) (memory s) beqPage beqIndex |}.

Lemma accessibleChildPageIsAccessibleIntoParentUpdateSh2 s entry v table nextFFI:
lookup table nextFFI (memory s) beqPage beqIndex = Some (I entry) →
¬ In table (getPartitions multiplexer s) →
parentInPartitionList s →
isChild s →
accessibleChildPageIsAccessibleIntoParent s →
accessibleChildPageIsAccessibleIntoParent
   {|
  currentPartition := currentPartition s;
  memory := add table nextFFI (PP v) (memory s) beqPage beqIndex |}.

Lemma consistencyUpdateLLCouplePPVA newLastLLable nextFFI v entry s:
StateLib.getMaxIndex ≠ Some nextFFI →
lookup newLastLLable nextFFI (memory s) beqPage beqIndex = Some (I entry)→
¬ In newLastLLable (getPartitions multiplexer s) →
consistency s → consistency {|
  currentPartition := currentPartition s;
  memory := add newLastLLable nextFFI (PP v) (memory s) beqPage beqIndex |}.

Lemma isEntryVAExistsUpdateLLCouplePPVA idx ptVaInCurPart table idxvaInCurPart entry s x:
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
(∃ va : vaddr,
       isEntryVA ptVaInCurPart idxvaInCurPart va s∧
        beqVAddr defaultVAddr va = false)
 → ∃ va : vaddr,
isEntryVA ptVaInCurPart idxvaInCurPart va
  {|
currentPartition := currentPartition s;
memory := add table idx (PP x)
            (memory s) beqPage beqIndex |}∧
        beqVAddr defaultVAddr va = false.
Lemma indirectionDescriptionUpdateLLCouplePPVA l descChildphy x idx table entry
phyPDChild vaToPrepare idxroot s:
let s':= {|
currentPartition := currentPartition s;
memory := add table idx (PP x)
            (memory s) beqPage beqIndex |} in
lookup table idx (memory s) beqPage beqIndex = Some (I entry) →
table ≠ descChildphy →
indirectionDescription s descChildphy phyPDChild idxroot vaToPrepare l →
indirectionDescription s' descChildphy phyPDChild idxroot vaToPrepare l.

Lemma initPEntryTablePreconditionToPropagatePreparePropertiesUpdateLLCouplePPVA pg
 table idx x v0 s:
let s':= {|
currentPartition := currentPartition s;
memory := add table idx (PP x)
            (memory s) beqPage beqIndex |} in
StateLib.getMaxIndex ≠ Some idx →
lookup table idx (memory s) beqPage beqIndex = Some (I v0) →
¬ In table (getPartitions multiplexer s) →
initPEntryTablePreconditionToPropagatePrepareProperties s pg →

initPEntryTablePreconditionToPropagatePrepareProperties s' pg.

Lemma writeAccessibleRecPreparePostconditionUpdateLLCouplePPVA desc pg
 table idx x v0 s:
let s':= {|
currentPartition := currentPartition s;
memory := add table idx (PP x)
            (memory s) beqPage beqIndex |} in
lookup table idx (memory s) beqPage beqIndex = Some (I v0) →
¬ In table (getAncestors desc s) →
table ≠ desc →

writeAccessibleRecPreparePostcondition desc pg s →
writeAccessibleRecPreparePostcondition desc pg s'.

Lemma isWellFormedMMUTablesUpdateLLCouplePPVA pg
 table idx x v0 s:
let s':= {|
currentPartition := currentPartition s;
memory := add table idx (PP x)
            (memory s) beqPage beqIndex |} in
lookup table idx (memory s) beqPage beqIndex = Some (I v0) →
isWellFormedMMUTables pg s → isWellFormedMMUTables pg s'.

Lemma isWellFormedFstShadowTablesUpdateLLCouplePPVA s nbL phySh1addr x table idx v0:
let s':= {|
currentPartition := currentPartition s;
memory := add table idx (PP x)
            (memory s) beqPage beqIndex |} in
lookup table idx (memory s) beqPage beqIndex = Some (I v0) →

isWellFormedFstShadow nbL phySh1addr s→ isWellFormedFstShadow nbL phySh1addr s'.

Lemma isWellFormedSndShadowTablesUpdateLLCouplePPVA s pg idx v0 l table x:
let s':= {|
currentPartition := currentPartition s;
memory := add table idx (PP x)
            (memory s) beqPage beqIndex |} in
lookup table idx (memory s) beqPage beqIndex = Some (I v0) →
isWellFormedSndShadow l pg s → isWellFormedSndShadow l pg s'.

Lemma newIndirectionsAreNotAccessibleUpdateLLCouplePPVA s idx v0 table x phyMMUaddr phySh1addr phySh2addr:
let s':= {|
currentPartition := currentPartition s;
memory := add table idx (PP x)
            (memory s) beqPage beqIndex |} in
¬ In table (getPartitions multiplexer s)→
lookup table idx (memory s) beqPage beqIndex = Some (I v0) →
newIndirectionsAreNotAccessible s phyMMUaddr phySh1addr phySh2addr →
newIndirectionsAreNotAccessible s' phyMMUaddr phySh1addr phySh2addr.

Lemma newIndirectionsAreNotMappedInChildrenUpdateLLCouplePPVA s idx v0 table x curpart newIndirection:
let s':= {|
currentPartition := currentPartition s;
memory := add table idx (PP x)
            (memory s) beqPage beqIndex |} in
newIndirectionsAreNotMappedInChildren s curpart newIndirection →
noDupPartitionTree s →
In curpart (getPartitions multiplexer s)→
¬ In table (getPartitions multiplexer s)→
lookup table idx (memory s) beqPage beqIndex = Some (I v0) →
newIndirectionsAreNotMappedInChildren s' curpart newIndirection.

Lemma insertEntryIntoLLPCUpdateLLCouplePPVA 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 idxFstVA idxSndVA idxTrdVA
      zeroI lpred newLastLLable nextFFI entry fstLL LLChildphy pgvalue minFI FFI indMMUToPreparebool:
isIndexValue newLastLLable (CIndex 0) FFI s →
StateLib.Index.succ FFI = Some nextFFI →
lookup newLastLLable nextFFI (memory s) beqPage beqIndex = Some (I entry) →
StateLib.getMaxIndex ≠ Some nextFFI →
insertEntryIntoLLPC 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 idxFstVA idxSndVA idxTrdVA
      zeroI lpred fstLL LLChildphy newLastLLable minFI indMMUToPreparebool→
insertEntryIntoLLPC {|
  currentPartition := currentPartition s;
  memory := add newLastLLable nextFFI (PP pgvalue) (memory s) beqPage beqIndex |} 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 lpred fstLL LLChildphy newLastLLable minFI indMMUToPreparebool.