Require Import Pip.Model.ADT Pip.Model.Hardware Pip.Model.MAL Pip.Model.Lib Pip.Model.IAL.
Require Import Pip.Proof.StateLib.
Require Import Lia List Compare_dec.
Lemma ret (A : Type) (a : A) (P : A → state → Prop) : {{ P a }} ret a {{ P }}.

Lemma bind (A B : Type) (m : LLI A) (f : A → LLI B) (P : state → Prop)( Q : A → state → Prop) (R : B → state → Prop) :
  (∀ a, {{ Q a }} f a {{ R }}) → {{ P }} m {{ Q }} → {{ P }} perform x := m in f x {{ R }}.

Lemma put (s : state) (P : unit → state → Prop) : {{ fun _ ⇒ P tt s }} put s {{ P }}.

Lemma get (P : state → state → Prop) : {{ fun s ⇒ P s s }} get {{ P }}.

Lemma undefined (A : Type)(a : nat) (P : A → state → Prop) : {{ fun s ⇒ False }} undefined a{{ P }}.

Lemma weaken (A : Type) (m : LLI A) (P Q : state → Prop) (R : A → state → Prop) :
  {{ Q }} m {{ R }} → (∀ s, P s → Q s) → {{ P }} m {{ R }}.
Lemma strengthen (A : Type) (m : LLI A) (P: state → Prop) (Q R: A → state → Prop) :
  {{ P }} m {{ R }} → (∀ s a, R a s → Q a s) → {{ P }} m {{ Q }}.

Lemma bindRev (A B : Type) (m : LLI A) (f : A → LLI B) (P : state → Prop)( Q : A → state → Prop) (R : B → state → Prop) :
  {{ P }} m {{ Q }} → (∀ a, {{ Q a }} f a {{ R }}) → {{ P }} perform x := m in f x {{ R }}.

Lemma modify f (P : unit → state → Prop) : {{ fun s ⇒ P tt (f s) }} modify f {{ P }}.

Lemma getCurPartition (P: page → state → Prop) :
{{wp P MAL.getCurPartition}} MAL.getCurPartition {{P}}.

Lemma getPDidx (P: index → state → Prop) :
{{ wp P getPDidx }} getPDidx {{ P }}.

Lemma getSh1idx (P: index → state → Prop) :
{{ wp P getSh1idx }} getSh1idx {{ P }}.
Lemma getSh2idx (P: index → state → Prop) :
{{ wp P getSh2idx }} getSh2idx {{ P }}.

Lemma getSh3idx (P: index → state → Prop) :
{{ wp P getSh3idx }} getSh3idx {{ P }}.

Lemma getPPRidx (P: index → state → Prop) :
{{ wp P getPPRidx }} getPPRidx {{ P }}.

Lemma getPRidx (P: index → state → Prop) :
{{ wp P getPRidx }} getPRidx {{ P }}.

Lemma getKidx (P : index → state → Prop) :
{{ wp P getKidx}} getKidx {{P}}.

Module Index.
Lemma eqb index1 index2 (P : bool → state → Prop):
{{ fun s : state ⇒ P (StateLib.Index.eqb index1 index2) s }}
  MALInternal.Index.eqb index1 index2 {{ fun s ⇒ P s}}.

Lemma gtb index1 index2 (P : bool → state → Prop):
{{ fun s : state ⇒ P (StateLib.Index.gtb index1 index2) s }}
  MALInternal.Index.gtb index1 index2 {{ fun s ⇒ P s}}.

Lemma ltb index1 index2 (P : bool → state → Prop):
{{ fun s : state ⇒ P (StateLib.Index.ltb index1 index2) s }}
  MALInternal.Index.ltb index1 index2 {{ fun s ⇒ P s}}.

Lemma leb index1 index2 (P : bool → state → Prop):
{{ fun s : state ⇒ P (StateLib.Index.leb index1 index2) s }}
  MALInternal.Index.leb index1 index2 {{ fun s ⇒ P s}}.

Lemma geb index1 index2 (P : bool → state → Prop):
{{ fun s : state ⇒ P (StateLib.Index.geb index1 index2) s }}
  MALInternal.Index.geb index1 index2 {{ fun s ⇒ P s}}.

Lemma succ (idx : index) (P: index → state → Prop) :
{{fun s ⇒ idx < (tableSize -1) ∧ ∀ l : idx + 1 < tableSize ,
    P {| i := idx + 1; Hi := MALInternal.Index.succ_obligation_1 idx l |} s}} MALInternal.Index.succ idx {{ P }}.
Lemma pred (idx : index) (P: index → state → Prop) :
{{ fun s : state ⇒ idx > 0 ∧ ∀ Hi : idx - 1 < tableSize,
                   P {| i := idx -1; Hi := Hi |} s }} MALInternal.Index.pred idx {{ P }}.
End Index.

Module Level.
Lemma pred (level1 : level) (P: level → state → Prop) :
{{ fun s : state ⇒ level1 > 0 ∧ ∀ Hl : level1 - 1 < nbLevel,
                   P {| l := level1 -1; Hl := Hl |} s }} MALInternal.Level.pred level1 {{ P }}.

Lemma gtb level1 level2 (P : bool → state → Prop):
{{ fun s : state ⇒ P (StateLib.Level.gtb level1 level2) s }}
  MALInternal.Level.gtb level1 level2 {{ fun s ⇒ P s}}.

Lemma eqb level1 level2 (P : bool → state → Prop):
{{ fun s : state ⇒ P (StateLib.Level.eqb level1 level2) s }}
  MALInternal.Level.eqb level1 level2 {{ fun s ⇒ P s}}.
End Level.

Module Page.
Lemma eqb page1 page2 (P : bool → state → Prop):
{{ fun s : state ⇒ P (StateLib.Page.eqb page1 page2) s }}
  MALInternal.Page.eqb page1 page2 {{ fun s ⇒ P s}}.
End Page.

Module VAddr.
Lemma eqbList(vaddr1 : vaddr) (vaddr2 : vaddr) (P : bool → state → Prop) :
{{ fun s : state ⇒ P (StateLib.VAddr.eqbList vaddr1 vaddr2) s }}
  MALInternal.VAddr.eqbList vaddr1 vaddr2 {{ fun s ⇒ P s}}.
End VAddr.

Lemma readPhyEntry table idx (P : page → state → Prop) :
{{fun s ⇒ ∃ entry, lookup table idx s.(memory) beqPage beqIndex = Some (PE entry) ∧
             P entry.(pa) s }} MAL.readPhyEntry table idx {{P}}.
Lemma readVirEntry table idx (P : vaddr → state → Prop) :
{{fun s ⇒ ∃ entry, lookup table idx s.(memory) beqPage beqIndex = Some ( VE entry) ∧
             P entry.(va) s }} MAL.readVirEntry table idx {{P}}.

Lemma readVirtual table idx (P : vaddr → state → Prop) :
{{fun s ⇒ ∃ entry : vaddr, lookup table idx s.(memory) beqPage beqIndex = Some ( VA entry) ∧
             P entry s }} MAL.readVirtual table idx {{P}}.

Lemma readVirtualUser table idx (P : vaddr → state → Prop) :
{{fun s ⇒ match lookup table idx s.(memory) beqPage beqIndex with
| Some ( VA a) ⇒ P a s
| _ ⇒ P defaultVAddr s
end }} MAL.readVirtualUser table idx {{P}}.

Lemma writePhyEntry table idx (addr : page) (p u r w e : bool) (P : unit → state → Prop) :
{{fun s ⇒ P tt {|
  currentPartition := currentPartition s;
  memory := add table idx
              (PE {| read := r; write := w; exec := e; present := p; user := u; pa := addr |})
              (memory s) beqPage beqIndex |} }} writePhyEntry table idx addr p u r w e {{P}}.

Lemma writeVirtual table idx (addr : vaddr) (P : unit → state → Prop) :
{{fun s ⇒ P tt {|
  currentPartition := currentPartition s;
  memory := add table idx (VA addr) (memory s) beqPage beqIndex |} }} writeVirtual table idx addr {{P}}.

Lemma writeVirEntry table idx (addr : vaddr) (P : unit → state → Prop) :
{{fun s ⇒ P tt {|
  currentPartition := currentPartition s;
  memory := add table idx (VE {| pd := false; va := addr |} ) (memory s) beqPage beqIndex |} }} writeVirEntry table idx addr {{P}}.

Lemma writePhysical table idx (addr : page) (P : unit → state → Prop) :
{{fun s ⇒ P tt {|
  currentPartition := currentPartition s;
  memory := add table idx
              (PP addr )
              (memory s) beqPage beqIndex |} }} writePhysical table idx addr {{P}}.

Lemma writeIndex table idx (indexValue : index) (P : unit → state → Prop) :
{{fun s ⇒ P tt {|
  currentPartition := currentPartition s;
  memory := add table idx
              (I indexValue )
              (memory s) beqPage beqIndex |} }} writeIndex table idx indexValue {{P}}.

Lemma writeAccessible (table : page) (idx : index) (flag : bool) (P : unit → state → Prop) :
{{fun s ⇒ ∃ entry , lookup table idx s.(memory) beqPage beqIndex = Some (PE entry) ∧
P tt {|
  currentPartition := currentPartition s;
  memory := add table idx
              (PE {| read := entry.(read); write :=entry.(write); exec := entry.(exec);
                     present := entry.(present); user := flag; pa := entry.(pa) |})
              (memory s) beqPage beqIndex |} }} writeAccessible table idx flag {{P}}.

Lemma readPhysical table idx (P : page → state → Prop) :
{{fun s ⇒ ∃ p1, lookup table idx s.(memory) beqPage beqIndex = Some (PP p1) ∧
             P p1 s }} MAL.readPhysical table idx {{P}}.

Lemma readPresent table idx (P : bool → state → Prop) :
{{fun s ⇒ ∃ entry, lookup table idx s.(memory) beqPage beqIndex = Some (PE entry) ∧
             P entry.(present) s }} MAL.readPresent table idx {{P}}.
   Lemma writePDflag table idx (flag: bool) (P : unit → state → Prop) :
{{fun s ⇒ ∃ v , lookup table idx (memory s) beqPage beqIndex = Some (VE v) ∧
P tt {|
         currentPartition := currentPartition s;
         memory := add table idx (VE {| pd := flag; va := va v |})
                     (memory s) beqPage beqIndex |} }} writePDflag table idx flag {{P}}.

Lemma readAccessible table idx (P : bool → state → Prop) :
{{fun s ⇒ ∃ entry, lookup table idx s.(memory) beqPage beqIndex = Some (PE entry) ∧
             P entry.(user) s }} MAL.readAccessible table idx {{P}}.

Lemma getNbLevel (P : level → state → Prop) :
{{fun s ⇒ nbLevel > 0 ∧ (∀ H, P {|
           l := nbLevel -1;
           Hl := MAL.getNbLevel_obligation_1 H
           |} s) }}
MAL.getNbLevel
{{P}}.

Lemma getIndexOfAddr (va : vaddr) (level1 : level) (P: index → state → Prop) :
{{ fun s ⇒ P (nth (length va - (level1+ 2)) va defaultIndex) s }}
   MAL.getIndexOfAddr va level1
{{P}}.

Lemma getMultiplexer (P : page → state → Prop) :
{{ wp P getMultiplexer}} getMultiplexer {{P}}.

Lemma readPDflag table idx (P : bool → state → Prop) :
{{fun s ⇒ ∃ entry, lookup table idx s.(memory) beqPage beqIndex = Some (VE entry) ∧
             P entry.(pd) s }} MAL.readPDflag table idx {{P}}.
Lemma readIndex table idx (P : index → state → Prop) :
{{fun s ⇒ ∃ ivalue : index, lookup table idx s.(memory) beqPage beqIndex = Some ( I ivalue) ∧
             P ivalue s }} MAL.readIndex table idx {{P}}.

Lemma updateCurPartition (partitionDescriptor : page) (P : unit → state → Prop) :
{{fun s ⇒ P tt {|
  currentPartition := partitionDescriptor;
  memory := memory s |} }}updateCurPartition partitionDescriptor {{P}}.

Lemma checkIndexPropertyLTB (userIndex : userValue) (P : bool → state → Prop) :
{{fun s ⇒ P (Nat.ltb userIndex tableSize) s }} checkIndexPropertyLTB userIndex {{P}}.

Lemma updateMMURoot (MMURoot : page) (P : unit → state → Prop) :
{{fun s ⇒ P tt s }}
updateMMURoot MMURoot
{{ P }}.

Lemma userValueToIndex (userIndex : userValue) (P : index → state → Prop) :
{{fun s ⇒ userIndex < tableSize ∧ P (CIndex userIndex) s}}
  userValueToIndex userIndex
{{P}}.

Lemma readInterruptMask (calleeVidt : page) (P : interruptMask → state → Prop) :
{{ fun s ⇒ P int_mask_d s}}
readInterruptMask calleeVidt
{{P}}.

Lemma isInterruptMasked (interruptMask : interruptMask) (targetInterrupt : index) (P : bool → state → Prop) :
{{fun s ⇒ P false s}}
isInterruptMasked interruptMask targetInterrupt
{{P}}.


Lemma getNthVAddrFrom (va : vaddr) (n : nat) (P : vaddr → state → Prop):
{{fun s ⇒ P (getNthVAddrFromAux va n) s}}
IAL.getNthVAddrFrom va n
{{P}}.

Lemma firstVAddrGreaterThanSecond (first second : vaddr) (P : bool → state → Prop):
{{fun s ⇒ P (firstVAddrGreaterThanSecondAux first second (IAL.firstVAddrGreaterThanSecond_obligation_1 first second)) s}}
firstVAddrGreaterThanSecond first second
{{P}}.

Lemma writeContext (callingContextAddr : contextAddr) (contextSaveAddr : vaddr) (flagsOnWake : interruptMask)
(P : unit → state → Prop) :
{{fun s ⇒ P tt s}}
writeContext callingContextAddr contextSaveAddr flagsOnWake
{{P}}.

Lemma setInterruptMask (mask : interruptMask)
(P : unit → state → Prop) :
{{fun s ⇒ P tt s}}
setInterruptMask mask
{{P}}.