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

Require Import Pip.Proof.WeakestPreconditions Pip.Proof.StateLib Pip.Proof.InternalLemmas
               Pip.Proof.DependentTypeLemmas.

Require Import Isolation Consistency Invariants GetTableAddr WriteAccessible WritePhyEntry
               PropagatedProperties WriteAccessibleRec InitConfigPagesList InitPEntryTable
               UpdateMappedPageContent UpdatePartitionDescriptor PropagatedProperties
               UpdateShadow1Structure InitFstShadow InitSndShadow UpdatePDFlagTrue.

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

Lemma andPreAndPost :
 ∀ (A : Type) (P: state → Prop)
 (Q1 Q2 : state → Prop) (m : LLI A),
{{fun s ⇒ P s ∧ Q1 s}} m {{fun _ ⇒ Q1}} →
{{fun s ⇒ P s ∧ Q2 s}} m {{fun _ ⇒ Q2}} →
{{fun s ⇒ P s ∧ Q1 s ∧ Q2 s}} m {{fun _ s ⇒ Q1 s ∧ Q2 s}}.
Lemma levelDecOrNot :
      ∀ p1 p2 : level, p1 ≠ p2 ∨ p1 = p2.

Lemma mapKernel table idx (P : unit → state → Prop) :
{{fun s ⇒ P tt {|
  currentPartition := currentPartition s;
  memory := add table idx
              (PE {| read := false; write := false; exec := false; present := false; user := false; pa := defaultPage |})
              (memory s) beqPage beqIndex |} }} MAL.writePhyEntry table idx defaultPage false false false false false {{P}}.

Lemma createPartition (descChild pdChild shadow1 shadow2 list : vaddr) :
{{fun s ⇒ partitionsIsolation s ∧ kernelDataIsolation s ∧ verticalSharing s ∧ consistency s }}
createPartition descChild pdChild shadow1 shadow2 list
{{fun _ s ⇒ partitionsIsolation s ∧ kernelDataIsolation s ∧ verticalSharing s ∧ consistency s }}.