Library Pip.Model.Hardware
Summary
This file contains the monad state and Hoare logic formalization. + State monad formalization :The type constructor "LLI"
Two operations : "bind" to compose a sequence of monadic functions
and "ret" to create monadic values. + We use state monad to simulate side effects like state updates so we define the following functions:"get" to get back the current state
"put" to update the current state
+ The state contains mainly the physical memory. In our Hardware model, physical memory is an associaton list that keeps only relevent data. Its key is a the physical address and the value is the data to store into physical memory. + Hoare logic formalization : " P m Q ""m" is a monadic function
"P" is the precondition of the function "m", it is an unary predicate
which depends on the state"Q" is the postcondition of the function "m", it is a binary predicate
which depends on the new state and the return value We define some lemmas like "weaken" and "bindWP" to facilitate Hoare logic and monad manipulation.
Require Import Pip.Model.ADT.
Require Import FunctionalExtensionality Arith.
Record Pentry : Type:=
{read :bool;
write : bool ;
exec : bool;
present : bool;
user : bool;
pa : page
}.
Record Ventry : Type:=
{
pd : bool;
va : vaddr
}.
Definition unsafe := nat.
Inductive value : Type :=
|PE : Pentry → value
|VE : Ventry → value
|PP : page → value
|VA : vaddr → value
|I : index → value
|U : userValue → value.
Record state : Type := {
currentPartition : page;
memory : list (paddr × value)
}.
Inductive yield_checks : Type :=
| FAIL_INVALID_INT_LEVEL_Cons
| FAIL_INVALID_CTX_SAVE_INDEX_Cons
| FAIL_CALLER_CONTEXT_SAVE_Cons
| FAIL_UNAVAILABLE_TARGET_VIDT_Cons
| FAIL_UNAVAILABLE_TARGET_CTX_Cons
| FAIL_UNAVAILABLE_CALLER_VIDT_Cons
| FAIL_ROOT_CALLER_Cons
| FAIL_INVALID_CHILD_Cons
| FAIL_MASKED_INTERRUPT_Cons
| SUCCESS_Cons.
Inductive result (A : Type) : Type :=
| val : A → result A
| undef : nat → state → result A.
Definition LLI (A :Type) : Type := state → result (A × state).
Definition ret {A : Type} (a : A) : LLI A :=
fun s ⇒ val (a , s) .
Definition bind {A B : Type} (m : LLI A)(f : A → LLI B) : LLI B :=
fun s ⇒ match m s with
| val (a, s') ⇒ f a s'
| undef a s' ⇒ undef a s'
end.
Definition put (s : state) : LLI unit :=
fun _ ⇒ val (tt, s).
Definition get : LLI state :=
fun s ⇒ val (s, s).
Definition undefined {A : Type} (code : nat ): LLI A :=
fun s ⇒ undef code s.
Definition runvalue {A : Type} (m : LLI A) (s : state) : option A :=
match m s with
|undef _ _⇒ None
| val (a, _) ⇒ Some a
end.
Definition runstate {A : Type} (m : LLI A) (s : state) : option state :=
match m s with
|undef _ _⇒ None
| val (_, s') ⇒ Some s'
end.
Notation "'perform' x ':=' m 'in' e" := (bind m (fun x ⇒ e))
(at level 60, x name, m at level 200, e at level 60, format "'[v' '[' 'perform' x ':=' m 'in' ']' '/' '[' e ']' ']'") : state_scope.
Notation "m1 ;; m2" := (bind m1 (fun _ ⇒ m2)) (at level 60, right associativity) : state_scope.
Open Scope state_scope.
Definition modify (f : state → state) : LLI unit :=
perform s := get in put (f s).
Definition hoareTriple {A : Type} (P : state → Prop) (m : LLI A) (Q : A → state → Prop) : Prop :=
∀ s, P s → match m s with
| val (a, s') ⇒ Q a s'
| undef _ _⇒ False
end.
Notation "{{ P }} m {{ Q }}" := (hoareTriple P m Q)
(at level 90, format "'[' '[' {{ P }} ']' '/ ' '[' m ']' '[' {{ Q }} ']' ']'") : state_scope.
Lemma conjProp (A : Type ) (P R : state → Prop) (Q : A → state → Prop) m :
{{ P }} m {{ Q}} → {{R}} m {{fun _ ⇒ R}} → {{fun s ⇒ P s∧ R s}} m {{fun a s ⇒ Q a s∧ R s}}.
Definition wp {A : Type} (P : A → state → Prop) (m : LLI A) :=
fun s ⇒ match m s with val (a, s') ⇒ P a s' | Err ⇒ False end.
Lemma wpIsPrecondition {A : Type} (P : A → state → Prop) (m : LLI A) :
{{ wp P m }} m {{ P }}.
Lemma wpIsWeakestPrecondition
(A : Type) (P : A → state → Prop) (Q : state → Prop) (m : LLI A) :
{{ Q }} m {{ P }} → ∀ s, Q s → (wp P m) s.
Lemma assoc (A B C : Type)(m : LLI A)(f : A → LLI B)(g : B → LLI C) :
perform y :=
perform x := m in
f x in
g y =
perform x := m in
perform y := f x in
g y.
Lemma postAnd :
∀ (A : Type) (P : state → Prop) (Q R : A → state → Prop) (m : LLI A),
{{ P }} m {{ Q }} → {{ P }} m {{ R }} → {{ P }} m {{ fun a s ⇒ Q a s ∧ R a s }}.
Lemma preOr :
∀ (A : Type) (P Q : state → Prop) (R : A → state → Prop) (m : LLI A),
{{ P }} m {{ R }} → {{ Q }} m {{ R }} → {{ fun s ⇒ P s ∨ Q s }} m {{ R }}.
Lemma preAndPost :
∀ (A : Type) (P1 Q1 : state → Prop) (P2 : A → state → Prop) (m : LLI A),
{{P1}} m {{P2}} →
{{fun s ⇒ P1 s ∧ Q1 s}} m {{fun a ⇒ Q1 }} →
{{fun s ⇒ P1 s ∧ Q1 s}} m {{fun a s ⇒ P2 a s ∧ Q1 s}}.
Lemma andAssocHT :
∀ (A : Type) (P1 P2 P3 : state → Prop) (R : A → state → Prop) (m : LLI A),
{{ fun s ⇒ (P1 s ∧ P2 s) ∧ P3 s}} m {{ R}} ↔ {{ fun s ⇒ P1 s ∧ P2 s ∧ P3 s }} m {{ R}}.
Lemma permutHT :
∀ (A : Type) (P1 P2 P3 : state → Prop) (R : A → state → Prop) (m : LLI A),
{{ fun s ⇒ P1 s ∧ P2 s ∧ P3 s}} m {{ R}} ↔ {{ fun s ⇒ P1 s ∧ P3 s ∧ P2 s }} m {{ R}}.
Lemma permutHT1 :
∀ (A : Type) (P1 P2 P3 : state → Prop) (R : A → state → Prop) (m : LLI A),
{{ fun s ⇒ P1 s ∧ P2 s ∧ P3 s}} m {{ R}} ↔ {{ fun s ⇒P3 s ∧ P1 s ∧ P2 s ∧ P3 s}} m {{ R}}.
Lemma preAnd:
∀ (A : Type) (P1 Q : state → Prop) (P2 : A → state → Prop) (m : LLI A),
{{P1}} m {{P2}} → {{fun s ⇒ P1 s ∧ Q s}} m {{P2}}.
Lemma conjPrePost :
∀ (A : Type) (P1 Q1 : state → Prop) (P2 Q2 : A → state → Prop) (m : LLI A),
{{P1}} m {{P2}} →
{{Q1}} m {{Q2}} →
{{fun s ⇒ P1 s ∧ Q1 s}} m {{fun a s ⇒ P2 a s ∧ Q2 a s}}.
Require Import FunctionalExtensionality Arith.
Record Pentry : Type:=
{read :bool;
write : bool ;
exec : bool;
present : bool;
user : bool;
pa : page
}.
Record Ventry : Type:=
{
pd : bool;
va : vaddr
}.
Definition unsafe := nat.
Inductive value : Type :=
|PE : Pentry → value
|VE : Ventry → value
|PP : page → value
|VA : vaddr → value
|I : index → value
|U : userValue → value.
Record state : Type := {
currentPartition : page;
memory : list (paddr × value)
}.
Inductive yield_checks : Type :=
| FAIL_INVALID_INT_LEVEL_Cons
| FAIL_INVALID_CTX_SAVE_INDEX_Cons
| FAIL_CALLER_CONTEXT_SAVE_Cons
| FAIL_UNAVAILABLE_TARGET_VIDT_Cons
| FAIL_UNAVAILABLE_TARGET_CTX_Cons
| FAIL_UNAVAILABLE_CALLER_VIDT_Cons
| FAIL_ROOT_CALLER_Cons
| FAIL_INVALID_CHILD_Cons
| FAIL_MASKED_INTERRUPT_Cons
| SUCCESS_Cons.
Inductive result (A : Type) : Type :=
| val : A → result A
| undef : nat → state → result A.
Definition LLI (A :Type) : Type := state → result (A × state).
Definition ret {A : Type} (a : A) : LLI A :=
fun s ⇒ val (a , s) .
Definition bind {A B : Type} (m : LLI A)(f : A → LLI B) : LLI B :=
fun s ⇒ match m s with
| val (a, s') ⇒ f a s'
| undef a s' ⇒ undef a s'
end.
Definition put (s : state) : LLI unit :=
fun _ ⇒ val (tt, s).
Definition get : LLI state :=
fun s ⇒ val (s, s).
Definition undefined {A : Type} (code : nat ): LLI A :=
fun s ⇒ undef code s.
Definition runvalue {A : Type} (m : LLI A) (s : state) : option A :=
match m s with
|undef _ _⇒ None
| val (a, _) ⇒ Some a
end.
Definition runstate {A : Type} (m : LLI A) (s : state) : option state :=
match m s with
|undef _ _⇒ None
| val (_, s') ⇒ Some s'
end.
Notation "'perform' x ':=' m 'in' e" := (bind m (fun x ⇒ e))
(at level 60, x name, m at level 200, e at level 60, format "'[v' '[' 'perform' x ':=' m 'in' ']' '/' '[' e ']' ']'") : state_scope.
Notation "m1 ;; m2" := (bind m1 (fun _ ⇒ m2)) (at level 60, right associativity) : state_scope.
Open Scope state_scope.
Definition modify (f : state → state) : LLI unit :=
perform s := get in put (f s).
Definition hoareTriple {A : Type} (P : state → Prop) (m : LLI A) (Q : A → state → Prop) : Prop :=
∀ s, P s → match m s with
| val (a, s') ⇒ Q a s'
| undef _ _⇒ False
end.
Notation "{{ P }} m {{ Q }}" := (hoareTriple P m Q)
(at level 90, format "'[' '[' {{ P }} ']' '/ ' '[' m ']' '[' {{ Q }} ']' ']'") : state_scope.
Lemma conjProp (A : Type ) (P R : state → Prop) (Q : A → state → Prop) m :
{{ P }} m {{ Q}} → {{R}} m {{fun _ ⇒ R}} → {{fun s ⇒ P s∧ R s}} m {{fun a s ⇒ Q a s∧ R s}}.
Definition wp {A : Type} (P : A → state → Prop) (m : LLI A) :=
fun s ⇒ match m s with val (a, s') ⇒ P a s' | Err ⇒ False end.
Lemma wpIsPrecondition {A : Type} (P : A → state → Prop) (m : LLI A) :
{{ wp P m }} m {{ P }}.
Lemma wpIsWeakestPrecondition
(A : Type) (P : A → state → Prop) (Q : state → Prop) (m : LLI A) :
{{ Q }} m {{ P }} → ∀ s, Q s → (wp P m) s.
Lemma assoc (A B C : Type)(m : LLI A)(f : A → LLI B)(g : B → LLI C) :
perform y :=
perform x := m in
f x in
g y =
perform x := m in
perform y := f x in
g y.
Lemma postAnd :
∀ (A : Type) (P : state → Prop) (Q R : A → state → Prop) (m : LLI A),
{{ P }} m {{ Q }} → {{ P }} m {{ R }} → {{ P }} m {{ fun a s ⇒ Q a s ∧ R a s }}.
Lemma preOr :
∀ (A : Type) (P Q : state → Prop) (R : A → state → Prop) (m : LLI A),
{{ P }} m {{ R }} → {{ Q }} m {{ R }} → {{ fun s ⇒ P s ∨ Q s }} m {{ R }}.
Lemma preAndPost :
∀ (A : Type) (P1 Q1 : state → Prop) (P2 : A → state → Prop) (m : LLI A),
{{P1}} m {{P2}} →
{{fun s ⇒ P1 s ∧ Q1 s}} m {{fun a ⇒ Q1 }} →
{{fun s ⇒ P1 s ∧ Q1 s}} m {{fun a s ⇒ P2 a s ∧ Q1 s}}.
Lemma andAssocHT :
∀ (A : Type) (P1 P2 P3 : state → Prop) (R : A → state → Prop) (m : LLI A),
{{ fun s ⇒ (P1 s ∧ P2 s) ∧ P3 s}} m {{ R}} ↔ {{ fun s ⇒ P1 s ∧ P2 s ∧ P3 s }} m {{ R}}.
Lemma permutHT :
∀ (A : Type) (P1 P2 P3 : state → Prop) (R : A → state → Prop) (m : LLI A),
{{ fun s ⇒ P1 s ∧ P2 s ∧ P3 s}} m {{ R}} ↔ {{ fun s ⇒ P1 s ∧ P3 s ∧ P2 s }} m {{ R}}.
Lemma permutHT1 :
∀ (A : Type) (P1 P2 P3 : state → Prop) (R : A → state → Prop) (m : LLI A),
{{ fun s ⇒ P1 s ∧ P2 s ∧ P3 s}} m {{ R}} ↔ {{ fun s ⇒P3 s ∧ P1 s ∧ P2 s ∧ P3 s}} m {{ R}}.
Lemma preAnd:
∀ (A : Type) (P1 Q : state → Prop) (P2 : A → state → Prop) (m : LLI A),
{{P1}} m {{P2}} → {{fun s ⇒ P1 s ∧ Q s}} m {{P2}}.
Lemma conjPrePost :
∀ (A : Type) (P1 Q1 : state → Prop) (P2 Q2 : A → state → Prop) (m : LLI A),
{{P1}} m {{P2}} →
{{Q1}} m {{Q2}} →
{{fun s ⇒ P1 s ∧ Q1 s}} m {{fun a s ⇒ P2 a s ∧ Q2 a s}}.