Require Import Pip.Model.ADT Pip.Model.Hardware Pip.Model.Lib Pip.Model.MAL.
Require Import Pip.Core.Services.
Require Import Pip.Proof.Consistency Pip.Proof.DependentTypeLemmas Pip.Proof.InternalLemmas
Pip.Proof.InternalLemmas2 Pip.Proof.Isolation Pip.Proof.StateLib Pip.Proof.WeakestPreconditions.
Require Import Invariants Lib GetTableAddr MapMMUPage PropagatedProperties WriteAccessible .
Import Arith Bool Classical_Prop Coq.Logic.ProofIrrelevance Lia List.


Definition nextIndirectionsOR (indirection nextIndirection phyPDChild phyMMUaddr phySh1Child phySh1addr phySh2Child phySh2addr: page) idxroot:=
(indirection = phyPDChild ∧ nextIndirection = phyMMUaddr ∧ idxroot = PDidx) ∨
(indirection = phySh1Child∧ nextIndirection = phySh1addr ∧ idxroot = sh1idx ) ∨
(indirection = phySh2Child∧ nextIndirection = phySh2addr ∧ idxroot = sh2idx).

 Lemma getIndirectionMapMMUPage11' s a (phyVaChild ptVaChildpd pd:page) e r w entry nbL stop1 a1 (li : level):
  (∀ (stop : nat) (tbl : page) ,
        getIndirection pd a nbL stop s = Some tbl → (defaultPage =? tbl) = false →
        tbl ≠ ptVaChildpd ∨ ( tbl = ptVaChildpd ∧ (StateLib.getIndexOfAddr a (CLevel (nbL-stop)) ≠ StateLib.getIndexOfAddr a1 li))) →
       lookup ptVaChildpd (StateLib.getIndexOfAddr a1 li) (memory s) beqPage beqIndex = Some (PE entry) →
       pd ≠ defaultPage →
       getIndirection pd a nbL stop1 s =
       getIndirection pd a nbL stop1
         {|
         currentPartition := currentPartition s;
         memory := add ptVaChildpd (StateLib.getIndexOfAddr a1 li)
                     (PE {| read := r; write := w; exec := e; present := true; user := true; pa := phyVaChild |})
                     (memory s) beqPage beqIndex |}.

 Lemma getIndirectionMapMMUPage11xx s a (phyVaChild ptVaChildpd pd:page) e r w entry nbL stop1 a1 (li : level):
let s':= {|
         currentPartition := currentPartition s;
         memory := add ptVaChildpd (StateLib.getIndexOfAddr a1 li)
                     (PE {| read := r; write := w; exec := e; present := true; user := true; pa := phyVaChild |})
                     (memory s) beqPage beqIndex |} in
  (∀ (stop : nat) (tbl : page) ,
        getIndirection pd a nbL stop s' = Some tbl → (defaultPage =? tbl) = false →
        tbl ≠ ptVaChildpd ∨ ( tbl = ptVaChildpd ∧ (StateLib.getIndexOfAddr a (CLevel (nbL-stop)) ≠ StateLib.getIndexOfAddr a1 li))) →
       lookup ptVaChildpd (StateLib.getIndexOfAddr a1 li) (memory s) beqPage beqIndex = Some (PE entry) →
       pd ≠ defaultPage →
       getIndirection pd a nbL stop1 s =
       getIndirection pd a nbL stop1 s'.

     Lemma getIndirectionAddIndirectionEq stop :
      ∀ s pd indirection phyMMUaddr e w r va entry idx level,
     lookup indirection idx
            (memory s) beqPage beqIndex = Some (PE entry) →
     ¬ In indirection (getIndirectionsAux pd s stop) →
     getIndirection pd va level stop {|
      currentPartition := currentPartition s;
      memory := add indirection idx
                  (PE
                     {| read := r; write := w; exec := e; present := true; user := true; pa := phyMMUaddr |})
                  (memory s) beqPage beqIndex |} =getIndirection pd va level stop s.

Lemma readPhyEntryAddIndirectionSameTable indirection idx pg r w e p s:
StateLib.readPhyEntry indirection idx
(add indirection idx
(PE {| read := r; write := w; exec := e; present := p; user := true; pa := pg |})
(memory s) beqPage beqIndex) = Some pg.

Lemma isWellFormedMMUTablesAddIndirection nextIndirection indirection idx entry s r w e:
lookup indirection idx
      (memory s) beqPage beqIndex = Some (PE entry) →
nextIndirection ≠ indirection →
isWellFormedMMUTables nextIndirection s →
isWellFormedMMUTables nextIndirection {|
currentPartition := currentPartition s;
memory := add indirection idx
            (PE
               {|
               read := r;
               write := w;
               exec := e;
               present := true;
               user := true;
               pa := nextIndirection |}) (memory s) beqPage beqIndex |}.

Lemma isWellFormedFstShadowTablesAddIndirection nextIndirection indirection entry vaToPrepare l lpred s e w r:
lookup indirection (StateLib.getIndexOfAddr vaToPrepare l)
      (memory s) beqPage beqIndex = Some (PE entry) →
nextIndirection ≠ indirection →
isWellFormedFstShadow lpred nextIndirection s →
isWellFormedFstShadow lpred nextIndirection
  {|
  currentPartition := currentPartition s;
  memory := add indirection (StateLib.getIndexOfAddr vaToPrepare l)
              (PE {| read := r; write := w; exec := e; present := true; user := true; pa := nextIndirection |})
              (memory s) beqPage beqIndex |}.

Lemma isWellFormedSndShadowTablesAddIndirection nextIndirection indirection entry vaToPrepare l lpred s e w r:
lookup indirection (StateLib.getIndexOfAddr vaToPrepare l)
      (memory s) beqPage beqIndex = Some (PE entry) →
nextIndirection ≠ indirection →
isWellFormedSndShadow lpred nextIndirection s →
isWellFormedSndShadow lpred nextIndirection
  {|
  currentPartition := currentPartition s;
  memory := add indirection (StateLib.getIndexOfAddr vaToPrepare l)
              (PE {| read := r; write := w; exec := e; present := true; user := true; pa := nextIndirection |})
              (memory s) beqPage beqIndex |}.

Lemma getIndirectionAddIndirectionCheckVaddrsFalse vapg l indirection vaToPrepare nextIndirection p pg entry partition s r e w:
let s' := {|
      currentPartition := currentPartition s;
      memory := add indirection (StateLib.getIndexOfAddr vaToPrepare l)
                  (PE
                     {|
                     read := r;
                     write := w;
                     exec := e;
                     present := true;
                     user := true;
                     pa := nextIndirection |}) (memory s) beqPage beqIndex |} in
 
 getIndirection indirection vapg l (nbLevel - 1) s' = Some p →
 (defaultPage =? p) = false →
 Some l = StateLib.getNbLevel →
 false = StateLib.Level.eqb l fstLevel →

lookup indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) beqPage beqIndex =
          Some (PE entry) →
nextEntryIsPP partition PDidx indirection s →
indirection ≠ defaultPage →

StateLib.readPhyEntry indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) = Some defaultPage →
(defaultPage =? nextIndirection) = false →
 isWellFormedMMUTables nextIndirection s →
 nextIndirection ≠ indirection →
pg ≠ defaultPage →
noDupConfigPagesList s →
StateLib.readPresent p (StateLib.getIndexOfAddr vapg fstLevel) (memory s') = Some true →
StateLib.readPhyEntry p (StateLib.getIndexOfAddr vapg fstLevel) (memory s') = Some pg →


partitionDescriptorEntry s →
In partition (getPartitions multiplexer s) →
               
 getIndirection indirection vapg l (nbLevel - 1) s =
 getIndirection indirection vapg l (nbLevel - 1) s'.

Lemma getMappedPageSomeAddIndirectionSamePartSSI1 s (indirection nextIndirection :page) vaToPrepare entry vavalue pd pg partition l
 r w e:
partitionDescriptorEntry s →
In partition (getPartitions multiplexer s) →
noDupConfigPagesList s →
isPresentNotDefaultIff s →
configTablesAreDifferent s →
lookup indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) beqPage beqIndex = Some (PE entry) →
nextEntryIsPP partition PDidx pd s →

StateLib.readPhyEntry indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) = Some defaultPage →
(defaultPage =? nextIndirection) = false →
indirectionDescription s partition indirection PDidx vaToPrepare l →
getMappedPage pd s vavalue = SomePage pg →
false = StateLib.Level.eqb l fstLevel →
 getMappedPage pd {|
  currentPartition := currentPartition s;
  memory := add indirection (StateLib.getIndexOfAddr vaToPrepare l)
              (PE
                 {|
                 read := r;
                 write := w;
                 exec := e;
                 present := true;
                 user := true;
                 pa := nextIndirection |}) (memory s) beqPage beqIndex |} vavalue = SomePage pg.

Lemma getAccessibleMappedPageAddIndirectionSh1Sh2 nbLgen pd s vapg indirection vaToPrepare partition
idxroot l r w e nextIndirection root entry:
let s':= {|
      currentPartition := currentPartition s;
      memory := add indirection (StateLib.getIndexOfAddr vaToPrepare l)
                  (PE
                     {| read := r; write := w; exec := e; present := true; user := true; pa := nextIndirection |})
                  (memory s) beqPage beqIndex |} in
Some nbLgen = StateLib.getNbLevel →
partitionDescriptorEntry s →
 idxroot = sh1idx ∨ idxroot = sh2idx →

lookup indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) beqPage beqIndex =
          Some (PE entry) →
In indirection (getIndirections root s) →
nextEntryIsPP partition idxroot root s →
In partition (getPartitions multiplexer s) →
nextEntryIsPP partition PDidx pd s→
noDupConfigPagesList s →
getAccessibleMappedPage pd s vapg = getAccessibleMappedPage pd s' vapg.

Lemma getAccessibleMappedPageSomeAddIndirectionSamePartSSI1 s (indirection nextIndirection :page) vaToPrepare entry vavalue pd pg partition l lpred r w e
idxroot rootx
phyPDChild phyMMUaddr phySh1Child phySh1addr phySh2Child phySh2addr :
nextIndirectionsOR indirection nextIndirection phyPDChild phyMMUaddr phySh1Child phySh1addr phySh2Child phySh2addr idxroot →
isWellFormedFstShadow lpred phySh1addr s →
StateLib.Level.pred l = Some lpred →
or3 idxroot →
nextEntryIsPP partition idxroot rootx s →
In indirection (getIndirections rootx s) →
partitionDescriptorEntry s →
In partition (getPartitions multiplexer s) →
noDupConfigPagesList s →
isPresentNotDefaultIff s →
configTablesAreDifferent s →
lookup indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) beqPage beqIndex = Some (PE entry) →
nextEntryIsPP partition PDidx pd s →
StateLib.readPhyEntry indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) = Some defaultPage →
(defaultPage =? nextIndirection) = false →
indirectionDescription s partition indirection idxroot vaToPrepare l →
getAccessibleMappedPage pd s vavalue = SomePage pg →
false = StateLib.Level.eqb l fstLevel →
 getAccessibleMappedPage pd {|
  currentPartition := currentPartition s;
  memory := add indirection (StateLib.getIndexOfAddr vaToPrepare l)
              (PE
                 {|
                 read := r;
                 write := w;
                 exec := e;
                 present := true;
                 user := true;
                 pa := nextIndirection |}) (memory s) beqPage beqIndex |} vavalue = SomePage pg.

Lemma getMappedPageAddIndirectionSh1Sh2 nbLgen pd s vapg indirection vaToPrepare partition
idxroot l r w e nextIndirection root entry:
let s':= {|
      currentPartition := currentPartition s;
      memory := add indirection (StateLib.getIndexOfAddr vaToPrepare l)
                  (PE
                     {| read := r; write := w; exec := e; present := true; user := true; pa := nextIndirection |})
                  (memory s) beqPage beqIndex |} in
Some nbLgen = StateLib.getNbLevel →
partitionDescriptorEntry s →
 idxroot = sh1idx ∨ idxroot = sh2idx →

lookup indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) beqPage beqIndex =
          Some (PE entry) →
In indirection (getIndirections root s) →
nextEntryIsPP partition idxroot root s →
In partition (getPartitions multiplexer s) →
nextEntryIsPP partition PDidx pd s→
noDupConfigPagesList s →
getMappedPage pd s vapg = getMappedPage pd s' vapg.

Lemma getMappedPagesAuxAddIndirectionSSI1 s indirection nextIndirection entry nbLgen valist pd pg vaToPrepare partition l r w e root idxroot
phyPDChild phyMMUaddr phySh1Child phySh1addr phySh2Child phySh2addr:
or3 idxroot →
nextIndirectionsOR indirection nextIndirection phyPDChild phyMMUaddr phySh1Child phySh1addr phySh2Child phySh2addr idxroot →
lookup indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) beqPage beqIndex = Some (PE entry) →
Some nbLgen = StateLib.getNbLevel →
indirectionDescription s partition indirection idxroot vaToPrepare l →

StateLib.readPhyEntry indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) = Some defaultPage →
isWellFormedMMUTables phyMMUaddr s →
false = StateLib.Level.eqb l fstLevel →
noDupConfigPagesList s →
partitionDescriptorEntry s →
nextEntryIsPP partition idxroot root s →
In indirection (getIndirections root s) →

In pg (getMappedPagesAux pd valist s) →
In partition (getPartitions multiplexer s) →
isPresentNotDefaultIff s →
configTablesAreDifferent s →
(defaultPage =? nextIndirection) = false →
nextEntryIsPP partition PDidx pd s →
nextIndirection ≠ indirection →

 In pg (getMappedPagesAux pd valist {|
  currentPartition := currentPartition s;
  memory := add indirection (StateLib.getIndexOfAddr vaToPrepare l)
              (PE
                 {|
                 read := r;
                 write := w;
                 exec := e;
                 present := true;
                 user := true;
                 pa := nextIndirection |}) (memory s) beqPage beqIndex |}).
 Lemma isPresentNotDefaultIffMapMMUPage s phyVaChild ptVaChildpd idxvaChild r w e
     
entry
:
lookup ptVaChildpd idxvaChild (memory s) beqPage beqIndex = Some (PE entry) →

phyVaChild ≠ defaultPage →
isPresentNotDefaultIff s →
isPresentNotDefaultIff {|
      currentPartition := currentPartition s;
      memory := add ptVaChildpd idxvaChild
                  (PE
                     {|
                     read := r;
                     write := w;
                     exec := e;
                     present := true;
                     user := true;
                     pa := phyVaChild |}) (memory s) beqPage beqIndex |}.
Lemma getIndirectionMapMMUPage11Stoplt:
∀ (stop1 : nat) (s : state) (a : vaddr) (phyVaChild ptVaChildpd pd : page) (e r w : bool) (idxvaChild : index)
   (entry : Pentry) (level : level) ,
 (∀ (stop : nat) (tbl : page),
  getIndirection pd a level stop s = Some tbl → (defaultPage =? tbl) = false → stop1> stop → tbl ≠ ptVaChildpd) →
 lookup ptVaChildpd idxvaChild (memory s) beqPage beqIndex = Some (PE entry) →
 pd ≠ defaultPage →
 getIndirection pd a level stop1 s =
 getIndirection pd a level stop1
   {|
   currentPartition := currentPartition s;
   memory := add ptVaChildpd idxvaChild
               (PE {| read := r; write := w; exec := e; present := true; user := true; pa := phyVaChild |})
               (memory s) beqPage beqIndex |}.

Lemma getMappedPageSomeAddIndirectionSSI2 s indirection nextIndirection vapg entry nbLgen pd pg indMMUToPrepare vaToPrepare partition l r w e root idxroot
phyPDChild phyMMUaddr phySh1Child phySh1addr phySh2Child phySh2addr:
or3 idxroot →
nextIndirectionsOR indirection nextIndirection phyPDChild phyMMUaddr phySh1Child phySh1addr phySh2Child phySh2addr idxroot →
isPresentNotDefaultIff s →
lookup indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) beqPage beqIndex = Some (PE entry) →
Some nbLgen = StateLib.getNbLevel →
indirectionDescription s partition indirection idxroot vaToPrepare l →
isEntryPage indirection (StateLib.getIndexOfAddr vaToPrepare l) indMMUToPrepare s →
(defaultPage =? indMMUToPrepare) = true →
isWellFormedMMUTables phyMMUaddr s →
false = StateLib.Level.eqb l fstLevel →
noDupConfigPagesList s →


indirectionDescription s partition indirection idxroot vaToPrepare l →
getMappedPage pd {|
  currentPartition := currentPartition s;
  memory := add indirection (StateLib.getIndexOfAddr vaToPrepare l)
              (PE
                 {|
                 read := r;
                 write := w;
                 exec := e;
                 present := true;
                 user := true;
                 pa := nextIndirection |}) (memory s) beqPage beqIndex |} vapg = SomePage pg →
nextEntryIsPP partition idxroot root s →
partitionDescriptorEntry s →
In partition (getPartitions multiplexer s) →
isPresentNotDefaultIff s →
configTablesAreDifferent s →
(defaultPage =? nextIndirection) = false →
nextEntryIsPP partition PDidx pd s →
nextIndirection ≠ indirection →
getMappedPage pd s vapg = SomePage pg.

Lemma getAccessibleMappedPageSomeAddIndirectionSSI2 s indirection nextIndirection
vapg entry nbLgen pd pg vaToPrepare partition l r w e root idxroot
phyPDChild phyMMUaddr phySh1Child phySh1addr phySh2Child phySh2addr:
or3 idxroot →
nextIndirectionsOR indirection nextIndirection phyPDChild phyMMUaddr phySh1Child phySh1addr phySh2Child phySh2addr idxroot →
isPresentNotDefaultIff s →
lookup indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) beqPage beqIndex = Some (PE entry) →
Some nbLgen = StateLib.getNbLevel →
indirectionDescription s partition indirection idxroot vaToPrepare l →

StateLib.readPhyEntry indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) = Some defaultPage →
isWellFormedMMUTables phyMMUaddr s →
false = StateLib.Level.eqb l fstLevel →
noDupConfigPagesList s →
getAccessibleMappedPage pd {|
  currentPartition := currentPartition s;
  memory := add indirection (StateLib.getIndexOfAddr vaToPrepare l)
              (PE
                 {|
                 read := r;
                 write := w;
                 exec := e;
                 present := true;
                 user := true;
                 pa := nextIndirection |}) (memory s) beqPage beqIndex |} vapg = SomePage pg →
nextEntryIsPP partition idxroot root s →
In indirection (getIndirections root s) →

partitionDescriptorEntry s →
In partition (getPartitions multiplexer s) →
isPresentNotDefaultIff s →
configTablesAreDifferent s →
(defaultPage =? nextIndirection) = false →
nextEntryIsPP partition PDidx pd s →
nextIndirection ≠ indirection →
getAccessibleMappedPage pd s vapg = SomePage pg.

Lemma getMappedPagesAuxAddIndirectionSSI2 s indirection nextIndirection entry nbLgen valist pd pg vaToPrepare partition l r w e idxroot root
phyPDChild phyMMUaddr phySh1Child phySh1addr phySh2Child phySh2addr:
or3 idxroot →
nextIndirectionsOR indirection nextIndirection phyPDChild phyMMUaddr phySh1Child phySh1addr phySh2Child phySh2addr idxroot →

isPresentNotDefaultIff s →
lookup indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) beqPage beqIndex = Some (PE entry) →
Some nbLgen = StateLib.getNbLevel →
indirectionDescription s partition indirection idxroot vaToPrepare l →

StateLib.readPhyEntry indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) = Some defaultPage →
isWellFormedMMUTables phyMMUaddr s →
false = StateLib.Level.eqb l fstLevel →
noDupConfigPagesList s →
 In pg (getMappedPagesAux pd valist {|
  currentPartition := currentPartition s;
  memory := add indirection (StateLib.getIndexOfAddr vaToPrepare l)
              (PE
                 {|
                 read := r;
                 write := w;
                 exec := e;
                 present := true;
                 user := true;
                 pa := nextIndirection |}) (memory s) beqPage beqIndex |}) →

nextEntryIsPP partition idxroot root s →
In indirection (getIndirections root s) →
partitionDescriptorEntry s →
In partition (getPartitions multiplexer s) →
isPresentNotDefaultIff s →