Library Pip.Proof.rushby

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

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

Require Import GetTableAddr Invariants.

Require Import List Classical_Prop Lia EqNat.


Definition observation (partition : page) s: list page :=
getAccessibleMappedPages partition s.

Lemma MMUSimulation pd va l :
 translateAux nbLevel pd va l = getTableAddrAux nbLevel pd va l.

Lemma comparePageToNullEq :
MMU.comparePageToNull = Internal.comparePageToNull.

Lemma getIndexOfAddrEq :
MMU.getIndexOfAddr = MAL.getIndexOfAddr.

Lemma readPresentEq :
MMU.readPresent = MAL.readPresent.

Lemma readAccessibleEq :
MMU.readAccessible = MAL.readAccessible.
Lemma readPhyEntryEq :
MMU.readPhyEntry = MAL.readPhyEntry.

Lemma translateMappedPage :
∀ partition phypage va pd nbL s,
In partition (getPartitions multiplexer s) →
consistency s →
phypage ≠ defaultPage →
StateLib.getPd partition (memory s) = Some pd →
StateLib.getNbLevel = Some nbL →
runvalue (translate pd va nbL) s = Some (Some phypage) →
In phypage (observation partition s).

Definition select (s : state) (p : page) (i : index) :=
lookup p i s.(memory) beqPage beqIndex .


Definition isolatedPartitions partition1 partition2 s :=
¬ In partition1 (getPartitionAux partition2 s (nbPage+1)) ∧
¬ In partition2 (getPartitionAux partition1 s (nbPage+1)).

Fixpoint translateVaddrsAux valist nbL pd s:=
match valist with
|nil ⇒ nil
|va :: l ⇒
  match runvalue (translate pd va nbL) s with
  | Some pa ⇒ pa :: translateVaddrsAux l nbL pd s
  | _ ⇒ translateVaddrsAux l nbL pd s
  end
end.

Fixpoint filterOption1 (l : list (option page)) : list page :=
  match l with
  | nil ⇒ nil
  | Some a :: l1 ⇒ a :: filterOption1 l1
  | None :: l1 ⇒ filterOption1 l1
  end.

Definition translateVaddrs valist nbL pd s :=
filterOption1 (translateVaddrsAux valist nbL pd s).
Lemma filterOption1InIff l elt :
List.In elt (filterOption1 l) ↔ List.In (Some elt) l.

Definition UserFun (pdpartition: page)
                   (k: state → list page → value → state) nbL:
list vaddr → value → state → state :=
fun valist v s ⇒
k s (translateVaddrs valist nbL pdpartition s) v.

Definition UserFunWCond (k: state → list page → value → state) : Type :=
  ∀ (s:state) (listpage : list page) (p1:page) (v:value) (i : index),
    ¬In p1 listpage → select s p1 i = select (k s listpage v) p1 i.

Definition UserFunRCond (k: state → list page → value → state) : Type :=
  ∀ (s1 s2:state) (listpage :list page) (v:value) (i : index) (p : page),
  In p listpage →
  (∀ (i : index) , select s1 p i = select s2 p i )->
                select (k s1 listpage v) p i = select (k s2 listpage v) p i.
Lemma translateNotDefault partition1 s1 pd1 nbL obs a:
In partition1 (getPartitions multiplexer s1) →
consistency s1 →
StateLib.getPd partition1 (memory s1) = Some pd1 →
StateLib.getNbLevel = Some nbL →
runvalue (translate pd1 a nbL) s1 = Some (Some obs) →
obs ≠ defaultPage.
Lemma translatePagesInObservation partition1 s1 pd1 nbL valist:
In partition1 (getPartitions multiplexer s1) →
consistency s1 →
StateLib.getPd partition1 (memory s1) = Some pd1 →
StateLib.getNbLevel = Some nbL →
incl (translateVaddrs valist nbL pd1 s1) (observation partition1 s1).

Theorem weakStepConsistency :
∀ s1 s2 partition1,
consistency s1 →
consistency s2 →
In partition1 (getPartitions multiplexer s1) →
In partition1 (getPartitions multiplexer s2) →
∀ pd1 nbL pd2, StateLib.getPd partition1 (memory s1) = Some pd1 →
StateLib.getNbLevel = Some nbL →
StateLib.getPd partition1 (memory s2) = Some pd2 →
pd1 = pd2 →
∀ p, p ≠ defaultPage →
(∀ i, select s1 p i = select s2 p i) →
(∀ p, In p (observation partition1 s1) →
           ∀ i, select s1 p i = select s2 p i) →
observation partition1 s1 = observation partition1 s2 →
(∀ va , runvalue (translate pd1 va nbL) s1 = runvalue (translate pd1 va nbL) s2) →
∀ s1' s2' v valist k,
UserFunWCond k →
UserFunRCond k →
UserFun pd1 k nbL valist v s1 = s1' →
UserFun pd2 k nbL valist v s2 = s2' →
∀ i, select s1' p i = select s2' p i.

Theorem weakLocalRespect :
∀ s s' partition1 partition2,
isolatedPartitions partition1 partition2 s→
verticalSharing s →
isChild s →
currentPartitionInPartitionsList s →
noDupPartitionTree s →
consistency s →
isParent s →
partitionsIsolation s →
partition1 = (currentPartition s) →
In partition2 (getPartitions multiplexer s) →
partition1 ≠ partition2 →
∀ p k, In p (observation partition2 s) →
(∀ listpages (p1:page) (v:value) (i : index),
 ¬In p1 listpages → select s p1 i = select (k s listpages v) p1 i) →
∀ pd nbL valist v, StateLib.getPd partition1 (memory s) = Some pd →
StateLib.getNbLevel = Some nbL →
UserFun pd k nbL valist v s = s' →
∀ i, select s p i = select s' p i.