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.

Require Import List Coq.Logic.ProofIrrelevance Lia Compare_dec Lt EqNat.

Lemma getTableAddr (indirection : page) (va : vaddr) (l : level) P currentPart idxroot:
{{fun s ⇒ P s ∧ consistency s ∧ In currentPart (getPartitions multiplexer s) ∧
            (idxroot = PDidx ∨ idxroot = sh1idx ∨ idxroot = sh2idx)/\
            ( ∃ (tableroot : page),
                nextEntryIsPP currentPart idxroot tableroot s∧
                tableroot ≠ defaultPage ∧
                ( (tableroot = indirection ∧ Some l = StateLib.getNbLevel ) ∨
                (∃ nbL stop, Some nbL = StateLib.getNbLevel ∧ stop ≤ nbL ∧
                StateLib.getIndirection tableroot va nbL stop s = Some indirection ∧
                indirection ≠ defaultPage ∧
                l = CLevel (nbL - stop)))) }}

getTableAddr indirection va l

{{fun (table : page) (s : state) ⇒ P s ∧
                 (getTableAddrRoot' table idxroot currentPart va s ∧ table = defaultPage ∨
                 (getTableAddrRoot table idxroot currentPart va s ∧ table≠ defaultPage ∧
                    ( ∀ idx, StateLib.getIndexOfAddr va fstLevel = idx →
                    ( (isVE table idx s ∧ idxroot = sh1idx) ∨
                      (isVA table idx s ∧ idxroot = sh2idx) ∨
                      (isPE table idx s ∧ idxroot = PDidx) ) ) ) )
 }}.