Set Implicit Arguments.
Unset Strict Implicit.
Require Import Arith.
Require Import Omega.
General definitions |
Inductive optionT (A : Type) : Type :=
| SomeT : A -> optionT A
| NoneT : optionT A.
Implicit Arguments NoneT [A].
Definition is_transitive (A : Type) (r : A -> A -> Prop) :=
forall x y z : A, r x y -> r y z -> r x z.
Definition is_injective (A B : Type) (f : A -> B) :=
forall x y, f x = f y -> x = y.
Well-foundation |
Section well_foundation.
Variable A : Type.
Variable R : A -> A -> Prop.
Inductive accessible : A -> Prop :=
accessible_intro :
forall x, (forall y, R x y -> accessible y) -> accessible x.
Lemma accessible_inversion :
forall x, accessible x -> forall y, R x y -> accessible y.
Definition is_well_founded := forall x, accessible x.
Lemma well_founded_induction :
is_well_founded ->
forall P : A -> Prop,
(forall x, (forall y, R x y -> P y) -> P x) -> forall x, P x.
End well_foundation.
Core definitions and properties |
Worlds and values |
Module Type WORLDS.
Parameter world : Type.
Parameter world_sub : world -> world -> Prop.
Axiom world_sub_trans : is_transitive world_sub.
Axiom world_sub_well_founded : is_well_founded world_sub.
Parameter value : Type.
Parameter element : Type.
Parameter elem_to_val : element -> value -> Prop.
Axiom elem_to_val_surjective : forall e, exists v, elem_to_val e v.
Axiom elem_to_val_function :
forall e e' v, elem_to_val e v -> elem_to_val e' v -> e = e'.
End WORLDS.
Module Core (W : WORLDS).
Export W.
Configurations |
Record config : Type := { c_w : world; c_v : value }.
Definition config_sub c c' := world_sub (c_w c) (c_w c') /\ c_v c' = c_v c.
Lemma config_sub_trans : is_transitive config_sub.
Semantics of the logic |
Definition type := config -> Prop.
Definition Implies (s t : type) : type := fun c => s c -> t c.
Definition Conj (s t : type) : type := fun c => s c /\ t c.
Definition Disj (s t : type) : type := fun c => s c \/ t c.
Definition Later (t : type) : type :=
fun c => forall c', config_sub c c' -> t c'.
Definition T : type := fun _ => True.
Definition F : type := fun _ => False.
Definition Forall (A : Type) (f : A -> type) : type :=
fun c => forall x, f x c.
Definition Exists (A : Type) (f : A -> type) : type :=
fun c => exists x, f x c.
Definition EW (t : type) : type :=
fun c => forall v, t (Build_config (c_w c) v).
Definition SW (t : type) : type :=
fun c => exists v, t (Build_config (c_w c) v).
Notation "s ⇒ t" := (Implies s t) (at level 85, right associativity).
Notation "s ∧ t" := (Conj s t) (at level 81, left associativity).
Notation "s ∨ t" := (Disj s t) (at level 81, left associativity).
Notation "∆ t" := (Later t) (at level 75, right associativity).
Notation "∃ x , t" := (Exists (fun x => t)) (at level 200, x ident).
Notation "∀ x , t" :=
(Forall (fun x => t)) (at level 200, x ident, right associativity).
Definition Sequent (s t : type) := forall c, (s ⇒ t) c.
Notation "s ⊢ t" := (Sequent s t) (at level 86, right associativity).
Logic rules |
Lemma id : forall t, t ⊢ t.
Lemma cut : forall t1 t2 t3, t1 ⊢ t2 -> t2 ⊢ t3 -> t1 ⊢ t3.
Lemma conj_r : forall s t1 t2, s ⊢ t1 -> s ⊢ t2 -> s ⊢ t1 ∧ t2.
Lemma conj_l_1 : forall t1 t2, t1 ∧ t2 ⊢ t1.
Lemma conj_l_2 : forall t1 t2, t1 ∧ t2 ⊢ t2.
Lemma disj_l : forall s t1 t2, t1 ⊢ s -> t2 ⊢ s -> t1 ∨ t2 ⊢ s.
Lemma disj_r_1 : forall t1 t2, t1 ⊢ t1 ∨ t2.
Lemma disj_r_2 : forall t1 t2, t2 ⊢ t1 ∨ t2.
Lemma false_l : forall t, F ⊢ t.
Lemma true_r : forall t, t ⊢ T.
Lemma implies_i : forall s t1 t2, s ∧ t1 ⊢ t2 -> s ⊢ t1 ⇒ t2.
Lemma implies_e : forall s t1 t2, s ⊢ t1 ⇒ t2 -> s ∧ t1 ⊢ t2.
Lemma forall_r :
forall A (f : A -> type) t, (forall x, t ⊢ f x) -> t ⊢ Forall f.
Lemma forall_l : forall A a (f : A -> type), Forall f ⊢ f a.
Lemma exists_l :
forall A (f : A -> type) t, (forall x, f x ⊢ t) -> Exists f ⊢ t.
Lemma exists_r : forall A a (f : A -> type), f a ⊢ Exists f.
Lemma later_lift : forall s t, s ⊢ t -> ∆s ⊢ ∆t.
Lemma later_double : forall s, ∆s ⊢ ∆∆s.
Lemma later_fix : forall p, ∆p ⊢ p -> T ⊢ p.
Lemma later_conj : forall s t, ∆s ∧ ∆t ⊢ ∆(s ∧ t).
Lemma later_true : T ⊢ ∆T.
Lemma later_forall : forall A (f : A -> type), (∀x, ∆(f x)) ⊢ ∆ (Forall f).
Lemma everywhere_lift : forall s t, s ⊢ t -> EW s ⊢ EW t.
Lemma everywhere_double : forall t, EW t ⊢ EW (EW t).
Lemma everywhere_d : forall t, EW t ⊢ t.
Lemma everywhere_conj : forall s t, EW s ∧ EW t ⊢ EW (s ∧ t).
Lemma everywhere_true : T ⊢ EW T.
Lemma later_everywhere : forall t, EW (∆t) ⊢ ∆(EW t).
Lemma everywhere_later : forall t, ∆(EW t) ⊢ EW (∆t).
Lemma everywhere_implies : forall s t, EW (s ⇒ t) ⊢ SW s ⇒ SW t.
Lemma somewhere_l : forall s t, s ⊢ EW t -> SW s ⊢ EW t.
Derived rules |
Lemma implies_l : forall s t, (s ⇒ t) ∧ s ⊢ t.
Lemma implies_to_sequent : forall s t, T ⊢ s ⇒ t -> s ⊢ t.
Lemma conj_sym : forall s t, s ∧ t ⊢ t ∧ s.
Lemma conj_assoc_1 : forall t1 t2 t3, t1 ∧ (t2 ∧ t3) ⊢ (t1 ∧ t2) ∧ t3.
Lemma conj_assoc_2 : forall t1 t2 t3, (t1 ∧ t2) ∧ t3 ⊢ t1 ∧ (t2 ∧ t3).
Lemma conj_contract : forall t, t ⊢ t ∧ t.
Lemma disj_sym : forall s t, s ∨ t ⊢ t ∨ s.
Lemma disj_assoc_1 : forall t1 t2 t3, t1 ∨ (t2 ∨ t3) ⊢ (t1 ∨ t2) ∨ t3.
Lemma disj_assoc_2 : forall t1 t2 t3, (t1 ∨ t2) ∨ t3 ⊢ t1 ∨ (t2 ∨ t3).
Lemma later_r : forall s t, ∆s ⊢ t -> ∆s ⊢ ∆t.
Tactics useful for reasoning with the embedded logic |
Lemma peek_1 :
forall t1 t2 t1' t2' s, t1 ∧ t2 ⊢ t1' ∧ t2' -> t1 ∧ t2 ∧ s ⊢ t1' ∧ s ∧ t2'.
Ltac peek_rec n s0 t0 rem :=
match eval compute in n with
0 => apply (rem _ _ _ _ (@id (s0 ∧ t0)))
| S ?n =>
match s0 with
?t1 ∧ ?t2 =>
peek_rec n t1 t2
(fun s t s' t' (H : s ∧ t ⊢ s' ∧ t') =>
rem _ _ _ _ (peek_1 (s:= t0) H))
| _ =>
apply (rem _ _ _ _ (@conj_sym s0 t0))
end
end.
Ltac peek_hyp n :=
match goal with
|- ?s ∧ ?t ⊢ ?concl =>
peek_rec n s t
(fun s t s' t' (H : s ∧ t ⊢ s' ∧ t') => (@cut _ _ concl H))
| |- _ ⊢ _ =>
idtac
end.
Lemma conj_add :
forall s t1 t2, t1 ⊢ t2 -> s ∧ t1 ⊢ s ∧ t2.
Ltac leftapp t :=
first
[ refine (cut t _)
| refine (cut (conj_add t) _)
| refine (cut (@t _) _)
| refine (cut (conj_add (@t _)) _)
| refine (cut (@t _ _) _)
| refine (cut (conj_add (@t _ _)) _)
| refine (cut (@t _ _ _) _)
| refine (cut (conj_add (@t _ _ _)) _)
| refine (cut (@t _ _ _ _) _)
| refine (cut (@t _ _ _ _ _) _)
| refine (cut (@t _ _ _ _ _ _) _) ].
Ltac rightapp t :=
first
[ refine (cut _ t)
| refine (cut _ (conj_add t))
| refine (cut _ (@t _))
| refine (cut _ (conj_add (@t _)))
| refine (cut _ (@t _ _))
| refine (cut _ (conj_add (@t _ _)))
| refine (cut _ (@t _ _ _))
| refine (cut _ (conj_add (@t _ _ _)))
| refine (cut _ (@t _ _ _ _))
| refine (cut _ (@t _ _ _ _ _))
| refine (cut _ (@t _ _ _ _ _ _)) ].
Lemma exists_extrusion :
forall A (f : A -> type) s t,
(forall x, s ∧ f x ⊢ t) -> s ∧ (Exists f) ⊢ t.
Ltac normalize2 :=
match goal with
| |- _ ∧ T ⊢ _ =>
leftapp conj_l_1; normalize2
| |- _ ∧ (_ ∧ _) ⊢ _ =>
leftapp conj_assoc_1; apply implies_e; normalize2
| |- _ ∧ Exists _ ⊢ _ =>
apply exists_extrusion;
let x := fresh "x" in
(intro x; normalize2; generalize x; clear x)
| |- T ∧ _ ⊢ _ =>
leftapp conj_l_2; normalize2
| |- _ ⊢ _ ⇒ _ =>
apply implies_i; normalize2
| |- _ =>
idtac
end.
Ltac normalize :=
match goal with
| |- _ ∧ _ ⊢ _ =>
apply implies_e; normalize
| |- Exists _ ⊢ _ =>
apply exists_l;
let x := fresh "x" in
(intro x; normalize; generalize x; clear x)
| |- _ =>
normalize2
end.
Generalized Löb rule |
Lemma later_fix_2 :
forall s t, s ⊢ ∆s -> s ∧ ∆t ⊢ t -> s ⊢ t.
Equivalence (derived construction) |
Definition Equiv s t : type := (s ⇒ t) ∧ (t ⇒ s).
Notation "s ⇔ t" := (Equiv s t) (at level 85, right associativity).
Lemma equiv_refl : forall t, T ⊢ t ⇔ t.
Lemma equiv_trans : forall t1 t2 t3, (t1 ⇔ t2) ∧ (t2 ⇔ t3) ⊢ t1 ⇔ t3.
Lemma equiv_sym : forall s t, s ⇔ t ⊢ t ⇔ s.
Type equality |
Definition teq s t := EW (s ⇔ t).
Lemma teq_sym : forall s t, teq s t ⊢ teq t s.
Lemma teq_trans : forall t1 t2 t3, teq t1 t2 ∧ teq t2 t3 ⊢ teq t1 t3.
Singleton types |
Definition tjust (e : element) : type := fun c => elem_to_val e (c_v c).
Lemma later_tjust : forall e, tjust e ⊢ ∆tjust e.
Lemma later_tjust_2 : forall e t, tjust e ⇒ ∆t ⊢ ∆(tjust e ⇒ t).
Lemma somewhere_tjust : forall e, T ⊢ SW (tjust e).
Lemma tjust_subst :
forall A (f : A -> element) (g : A -> type) x x',
is_injective f -> tjust (f x) ∧ tjust (f x') ⊢ g x ⇒ g x'.
Definition thas e t := EW (tjust e ⇒ t).
Lemma later_thas : forall e t, thas e (∆t) ⊢ ∆(thas e t).
Lemma thas_lift : forall e s t, s ⊢ t -> thas e s ⊢ thas e t.
Lemma thas_e :
forall e t, thas e t ⊢ SW (tjust e ∧ t).
Lemma change_type :
forall e t t', ∆teq t t' ∧ ∆thas e t ⊢ ∆thas e t'.
Definition scalar_type (t : type) :=
forall w e v v',
elem_to_val e v -> elem_to_val e v' ->
t (Build_config w v) -> t (Build_config w v').
Lemma thas_exists_1 :
forall A e (f : A -> type), (∃x, thas e (f x)) ⊢ thas e (Exists f).
Lemma thas_exists_2 :
forall A e (f : A -> type),
(forall x, scalar_type (f x)) ->
thas e (Exists f) ⊢ ∃x, thas e (f x).
Definition necessary t := t ⊢ ∆t.
Lemma necessary_fold : forall t, necessary t -> t ⊢ ∆t.
Lemma conj_necessary :
forall s t, necessary s -> necessary t -> necessary (s ∧ t).
Lemma true_necessary : necessary T.
Lemma exists_necessary :
forall (A : Type) (f : A -> type),
(forall x, necessary (f x)) -> necessary (Exists f).
Lemma later_necessary : forall t, necessary (∆ t).
Lemma everywhere_necessary : forall t, necessary t -> necessary (EW t).
Lemma tjust_necessary : forall e, necessary (tjust e).
Lemma thas_necessary : forall e t, necessary t -> necessary (thas e t).
Hint Resolve necessary_fold conj_necessary true_necessary exists_necessary
later_necessary everywhere_necessary tjust_necessary
thas_necessary.
Necessity |
Definition nec t := t ∧ ∆t.
Lemma nec_true : T ⊢ nec T.
Lemma nec_lift : forall s t, s ⊢ t -> nec s ⊢ nec t.
Lemma nec_d : forall t, nec t ⊢ t.
Lemma nec_necessary : forall t, necessary (nec t).
Hint Resolve nec_necessary.
Lemma nec_and_necessity : forall t, necessary t -> t ⊢ nec t.
Lemma Grzegorczyk_axiom :
forall t, nec (nec (t ⇒ nec t) ⇒ t) ⊢ t.
Recursive types |
Definition contractive (f : type -> type) :=
forall s t, ∆ teq s t ⊢ teq (f s) (f t).
Definition contractive' (f : type -> type) :=
forall t t', ∆teq t t' ⊢ f t ⇒ f t'.
Lemma contractive'_to_contractive : forall f, contractive' f -> contractive f.
Lemma unique_fixpoint :
forall f, contractive f ->
forall s t, T ⊢ teq s (f s) -> T ⊢ teq t (f t) -> T ⊢ teq s t.
Section fixpoint.
Variable f : type -> type.
Fixpoint rec_def
(c : config) (r : accessible world_sub (c_w c)) {struct r} : Prop :=
f (fun c' => forall (H : world_sub (c_w c) (c_w c')),
@rec_def c' (accessible_inversion r H))
c.
Lemma rec_def_unfolding :
forall c (r : accessible world_sub (c_w c)),
@rec_def c r <->
f (fun c' => forall (H : world_sub (c_w c) (c_w c')),
@rec_def c' (accessible_inversion r H)) c.
Lemma rec_def_invariance :
contractive f ->
forall c (r r' : accessible world_sub (c_w c)),
@rec_def c r <-> @rec_def c r'.
End fixpoint.
Definition Rec (f : type -> type) : type :=
fun c => @rec_def f c (world_sub_well_founded (c_w c)).
Lemma fixpoint_property :
forall f : type -> type, contractive f -> T ⊢ teq (Rec f) (f (Rec f)).
Lemma unfolding : forall f : type -> type, contractive f -> Rec f ⊢ f (Rec f).
Lemma folding : forall f : type -> type, contractive f -> f (Rec f) ⊢ Rec f.
End of core definitions and properties |
End Core.
Dealing with the store |
Assumption for dealing with the store |
Module Type STORE_HYPS.
Parameter value : Type.
Parameter element : Type.
Parameter elem_to_val : element -> value -> Prop.
Parameter location : Type.
Parameter loc_to_elem : location -> element.
Axiom elem_to_val_surjective : forall e, exists v, elem_to_val e v.
Axiom elem_to_val_function :
forall e e' v, elem_to_val e v -> elem_to_val e' v -> e = e'.
Axiom loc_to_elem_injective : is_injective loc_to_elem.
Axiom eq_loc_dec : forall l l' : location, {l = l'} + {l <> l'}.
End STORE_HYPS.
Store typing |
Module Store (H : STORE_HYPS).
Export H.
Module Store_world.
Definition value := value.
Definition element := element.
Definition elem_to_val := elem_to_val.
Definition elem_to_val_surjective := elem_to_val_surjective.
Definition elem_to_val_function := elem_to_val_function.
Stratified types and store typings |
Fixpoint stype (n : nat) : Type :=
match n with
0 => unit
| S n => prodT (stype n)
(prodT value (location -> optionT (stype n)) -> Prop)
end.
Definition store_typing n := location -> optionT (stype n).
Inductive stype_sub : forall n n', stype n -> stype n' -> Prop :=
ps_refl :
forall n (t : stype n), stype_sub t t
| ps_incl :
forall n n' (t : stype n) (t' : stype n')
(s : prodT value (store_typing n') -> Prop),
stype_sub t t' -> stype_sub (n':= S n') t (pairT t' s).
Lemma stype_sub_trans :
forall n n' n'' (t : stype n) (t' : stype n') (t'' : stype n''),
stype_sub t t' -> stype_sub t' t'' -> stype_sub t t''.
Lemma stype_sub_rank :
forall n n' (t : stype n) (t' : stype n'),
stype_sub t t' -> n <= n'.
Definition st_sub n n' (ψ : store_typing n) (ψ' : store_typing n') :=
forall l,
match ψ l with
NoneT =>
True
| SomeT t =>
match ψ' l with
NoneT => False
| SomeT t' => stype_sub t' t
end
end.
Lemma st_sub_trans :
forall n n' n'' (ψ : store_typing n) (ψ' : store_typing n')
(ψ'' : store_typing n''),
st_sub ψ ψ' -> st_sub ψ' ψ'' -> st_sub ψ ψ''.
Definition st_weaken n (ψ : store_typing (S n)) : store_typing n :=
fun l =>
match ψ l with
NoneT => NoneT
| SomeT t => SomeT (fstT t)
end.
Lemma st_weaken_and_sub :
forall n (ψ : store_typing (S n)), st_sub ψ (st_weaken ψ).
Definition st_extend n (ψ : store_typing n) l t : store_typing n :=
fun l' => if eq_loc_dec l' l then t else ψ l'.
Lemma st_extend_and_sub :
forall n (ψ : store_typing n) l t,
ψ l = NoneT -> st_sub ψ (st_extend ψ l t).
Worlds |
Record world' : Type :=
{ w_t : nat; w_st : store_typing w_t }.
Definition world := world'.
Definition Build_world := Build_world'.
Definition world_sub w w' := w_t w > w_t w' /\ st_sub (w_st w) (w_st w').
Lemma world_sub_trans : is_transitive world_sub.
Lemma world_sub_well_founded : is_well_founded world_sub.
End Store_world.
Module C := Core (Store_world).
Export C.
Projection / embedding between types to stypes |
Fixpoint approx n (t : type) {struct n} : stype n :=
match n return stype n with
0 =>
tt
| (S n) =>
pairT (approx n t)
(fun c : prodT value (store_typing n) =>
let (v, ψ) := c in t (Build_config (Build_world ψ) v))
end.
Definition to_type n (t : stype n) : type.
Lemma approx_prop :
forall n t c, (w_t (c_w c)) < n -> (t ⇔ to_type (approx n t)) c.
Lemma approx_and_equality :
forall t c, (∆ teq t (to_type (approx (w_t (c_w c)) t))) c.
Store typing predicate |
Definition Get (l : location) (t : type) : type :=
fun c => match w_st (c_w c) l with
SomeT t' => t = to_type t'
| _ => False
end.
Notation "l ↦ t" := (Get l t) (at level 75, right associativity).
Lemma stype_sub_and_tequiv :
forall n n' (t : stype n) (t' : stype n') c,
stype_sub (n:=n') (n':=n) t' t ->
n' > (w_t (c_w c)) ->
(to_type t ⇔ to_type t') c.
Lemma get_and_later_1 :
forall l t1, l ↦ t1 ⊢ ∆(∃t2, l ↦ t2).
Lemma get_and_later_2 :
forall l t1, l ↦ t1 ⊢ ∆(∀t2, l ↦ t2 ⇒ ∆teq t1 t2).
Lemma everywhere_get : forall l t, l ↦ t ⊢ EW (l ↦ t).
Pure types |
Definition pure p := p ⊢ EW p.
Lemma pure_fold : forall p, pure p -> p ⊢ EW p.
Hint Resolve pure_fold.
Lemma conj_pure : forall p q, pure p -> pure q -> pure (p ∧ q).
Lemma everywhere_pure : forall p, pure (EW p).
Lemma true_pure : pure T.
Lemma exists_pure :
forall A (f : A -> type), (forall x, pure (f x)) -> pure (Exists f).
Lemma later_pure : forall p, pure p -> pure (∆p).
Lemma get_pure : forall l t, pure (l ↦ t).
Hint Resolve conj_pure everywhere_pure true_pure exists_pure
later_pure get_pure.
Lemma thas_pure : forall v p, pure (thas v p).
Lemma teq_pure : forall t t', pure (teq t t').
Hint Resolve thas_pure teq_pure.
XXXXX Extra property of thas |
Lemma thas_tjust :
forall l f, (forall l, pure (f l)) ->
thas (loc_to_elem l) (∃l, tjust (loc_to_elem l) ∧ f l) ⊢ f l.
Reference type |
Definition tref (t : type) : type :=
∃l, tjust (loc_to_elem l) ∧ ∃t', l ↦ t' ∧ ∆teq t t'.
Lemma tref_necessary : forall t, necessary (tref t).
Hint Resolve tref_necessary.
Lemma tref_contractive : contractive tref.
Lemma thas_tref :
forall l t,
thas (loc_to_elem l) (tref t) ⊢ ∃t', l ↦ t' ∧ ∆teq t t'.
The memory |
Definition memory := location -> element.
Definition mem_set (mem : memory) (l : location) (e : element) : memory :=
fun l' => if (eq_loc_dec l' l) then e else mem l'.
Lemma mem_set_eq : forall m l e, mem_set m l e l = e.
Lemma mem_set_not_eq : forall m l l' e, l' <> l -> mem_set m l e l' = m l'.
Definition validmem (m : memory) := ∀l, ∀t, l ↦ t ⇒ ∆thas (m l) t.
Type preservation |
Lemma memory_type_preservation :
forall l t e, l ↦ t ∧ ∆thas e t ⊢ ∆ ∀t', l ↦ t' ⇒ ∆thas e t'.
Lemma unchanged_memory :
forall m n (ψ : store_typing (1 + n)) v,
(validmem m) (Build_config (Build_world ψ) v) ->
exists ψ' : store_typing n,
world_sub (Build_world ψ) (Build_world ψ') /\
(validmem m) (Build_config (Build_world ψ') v).
Lemma memory_update :
forall m l e t n (ψ : store_typing (1 + n)) v,
necessary t ->
(validmem m) (Build_config (Build_world ψ) v) ->
(thas (loc_to_elem l) (tref t)) (Build_config (Build_world ψ) v) ->
(thas e t) (Build_config (Build_world ψ) v) ->
exists ψ' : store_typing n,
world_sub (Build_world ψ) (Build_world ψ') /\
(validmem (mem_set m l e)) (Build_config (Build_world ψ') v).
Lemma memory_allocation :
forall m l e t n (ψ : store_typing (1 + n)) v,
necessary t ->
(validmem m) (Build_config (Build_world ψ) v) ->
ψ l = NoneT ->
(thas e t) (Build_config (Build_world ψ) v) ->
exists ψ' : store_typing n,
world_sub (Build_world ψ) (Build_world ψ') /\
(validmem (mem_set m l e)) (Build_config (Build_world ψ') v) /\
(thas (loc_to_elem l) (tref t)) (Build_config (Build_world ψ') v).
Lemma memory_access :
forall w w' v l t m,
(thas (loc_to_elem l) (tref t)) (Build_config w v) ->
(validmem m) (Build_config w v) ->
world_sub w w' ->
(thas (m l) t) (Build_config w' v).
End of store definitions and properties |
End Store.
Van Neuman machines |
Module Store_hyps.
Parameter register : Type.
Definition element := nat.
Definition location := element.
Definition value := register -> element.
Axiom eq_reg_dec : forall r r' : register, {r = r'} + {r <> r'}.
Definition reg_set (v : value) r e :=
fun r' => if (eq_reg_dec r' r) then e else v r'.
Lemma reg_set_eq : forall v r e, reg_set v r e r = e.
Lemma reg_set_not_eq :
forall v r1 r2 e, r2 <> r1 -> reg_set v r1 e r2 = v r2.
Definition loc_to_elem (n : location) := n.
Lemma loc_to_elem_injective :
forall l l', loc_to_elem l = loc_to_elem l' -> l = l'.
Lemma eq_loc_dec : forall l l' : location, {l = l'} + {l <> l'}.
Module Vect.
Parameter r0 : register.
Definition vect e : value := fun r => e.
Definition elem_to_val e v := v = vect e.
Lemma elem_to_val_surjective : forall e, exists v, elem_to_val e v.
Lemma elem_to_val_function :
forall e e' v, elem_to_val e v -> elem_to_val e' v -> e = e'.
Lemma elem_to_val_rev_fun :
forall e v v', elem_to_val e v -> elem_to_val e v' -> v = v'.
End Vect.
Module Proj.
Parameter r0 : register.
Definition vect e : value := fun r => e.
Definition elem_to_val e (v : value) := v r0 = e.
Lemma elem_to_val_surjective : forall e, exists v, elem_to_val e v.
Lemma elem_to_val_function :
forall e e' v, elem_to_val e v -> elem_to_val e' v -> e = e'.
End Proj.
Definition elem_to_val := Vect.elem_to_val.
Definition elem_to_val_surjective := Vect.elem_to_val_surjective.
Definition elem_to_val_function := Vect.elem_to_val_function.
End Store_hyps.
Module S := Store (Store_hyps).
Export S.
Safety |
Parameter step : value -> memory -> value -> memory -> Prop.
Fixpoint safen (n : nat) (v : value) (m : memory) {struct n} : Prop :=
match n with
0 => True
| S n => (exists v', exists m', step v m v' m') /\
forall v' m', step v m v' m' -> safen n v' m'
end.
Definition safemem m : type := fun c => safen (w_t (c_w c)) (c_v c) m.
Definition safe : type := ∀m, validmem m ⇒ safemem m.
Definition tslot r t : type := fun c => (thas (c_v c r) t) c.
Lemma later_tslot : forall r t, tslot r (∆t) ⊢ ∆tslot r t.
Lemma tslot_lift : forall r s t, s ⊢ t -> tslot r s ⊢ tslot r t.
Lemma tslot_necessary : forall r t, necessary t -> necessary (tslot r t).
Hint Resolve tslot_necessary.
Lemma tslot_exists_1 :
forall A r (f : A -> type), (∃x, tslot r (f x)) ⊢ tslot r (Exists f).
Lemma tslot_exists_2 :
forall A r (f : A -> type),
(forall x, scalar_type (f x)) ->
tslot r (Exists f) ⊢ ∃x, tslot r (f x).
Lemma tslot_thas :
forall r t w v,
(tslot r t) (Build_config w v) -> (thas (v r) t) (Build_config w v).
Code pointer |
Parameter pc : register.
Definition tcodeptr (t : type) : type :=
∃l, tjust l ∧ ∆EW(tslot pc (tjust l) ⇒ t ⇒ safe).
Lemma tcodeptr_necessary : forall p, necessary (tcodeptr p).
Lemma tcodeptr_contravariant :
forall s t, ∆EW(s ⇒ t) ⊢ tcodeptr t ⇒ tcodeptr s.
Lemma tcodeptr_contractive : contractive tcodeptr.
Machine Instructions |
Definition machine_instruction := value -> memory -> value -> memory -> Prop.
Definition encodes n (i : machine_instruction) :=
forall v1 m1, m1 (v1 pc) = n ->
forall v2 m2, (step v1 m1 v2 m2 <-> i v1 m1 v2 m2).
Definition load r1 r2 (n : nat) : machine_instruction :=
fun v1 m1 v2 m2 =>
v2 = reg_set (reg_set v1 pc (1 + v1 pc)) r1 (m1 (n + v1 r2)) /\
m2 = m1.
Definition store r1 (n : nat) r2 : machine_instruction :=
fun v1 m1 v2 m2 =>
v2 = reg_set v1 pc (1 + v1 pc) /\
m2 = mem_set m1 (n + v1 r1) (v1 r2).
Definition addimm r1 r2 (n : nat) : machine_instruction :=
fun v1 m1 v2 m2 =>
v2 = reg_set (reg_set v1 pc (1 + v1 pc)) r1 (n + v1 r2) /\
m2 = m1.
Definition jump r : machine_instruction :=
fun v1 m1 v2 m2 =>
v2 = reg_set v1 pc (v1 r) /\
m2 = m1.
Typing Rules |
Definition tplus (l : location) k (l' : location) : type :=
fun w => k + l = l'.
Definition toffset k t :=
∃l, tjust (loc_to_elem l) ∧ ∃l', tplus l k l' ∧ thas l' t.
Lemma tjust_subst_2 :
forall A (f : A -> element) (g : A -> type) x x',
is_injective f -> T ⊢ g x -> tjust (f x) ∧ tjust (f x') ⊢ g x'.
Lemma tplus_subst :
forall (f : location -> type) l l' n,
tplus l n l' ⊢ f (n + l) ⇒ f l'.
Lemma tplus_subst_2 :
forall (f : location -> type) l l' n,
T ⊢ f (n + l) -> tplus l n l' ⊢ f l'.
Lemma simplify_typing_rule :
forall i s t,
(forall l s',
l ↦ s' ∧ ∆teq (tjust i) s' ∧
tslot pc (tjust (loc_to_elem l)) ∧ t ⊢
∆EW (tslot pc (tjust (1 + l)) ⇒ s ⇒ safe) ⇒ safe) ->
tref (tjust i) ∧ ∆toffset 1 (tcodeptr s) ⊢ tcodeptr t.
Lemma memory_contents :
forall l s t m,
l ↦ t ∧ ∆teq s t ∧ validmem m ⊢ ∆SW (tjust (m l) ∧ s).
Lemma simplify_typing_rule_2 :
forall i (s t : type),
(forall (l : element) (v : value) n (ψ : store_typing (1 + n))
(m : memory),
v pc = l -> m l = i ->
t (Build_config (Build_world ψ) v) ->
(validmem m) (Build_config (Build_world ψ) v) ->
(exists v' : value, (exists m' : memory, step v m v' m')) /\
forall v' m', step v m v' m' ->
exists ψ' : store_typing n,
st_sub ψ ψ' /\ v' pc = 1 + l /\
s (Build_config (Build_world ψ') v') /\
validmem m' (Build_config (Build_world ψ') v')) ->
tref (tjust i) ∧ ∆toffset 1 (tcodeptr s) ⊢ tcodeptr t.
Lemma tplus_pure : forall l l' k, pure (tplus l k l').
Hint Resolve tplus_pure.
Lemma thas_toffset :
forall l k t, thas l (toffset k t) ⊢ thas (k + l) t.
Lemma everywhere_forall :
forall A (f : A -> type), (∀x, EW(f x)) ⊢ EW (Forall f).
Lemma forall_pure :
forall A (f : A -> type), (forall x, pure (f x)) -> pure (Forall f).
Hint Resolve forall_pure.
Lemma implies_pure :
forall s t, pure s -> pure t -> pure (s ⇒ t).
Hint Resolve implies_pure.
Lemma validmem_pure : forall m, pure (validmem m).
Lemma simple_load_rule :
forall i r1 r2 k t,
encodes i (load r1 r2 k) -> r1 <> pc -> necessary t ->
tref (tjust i) ∧ ∆toffset 1 (tcodeptr (tslot r1 t)) ⊢
tcodeptr (tslot r2 (toffset k (tref t))).
Definition notindom r (φ : type) :=
forall w v l, φ (Build_config w v) -> φ (Build_config w (reg_set v r l)).
Lemma load_rule :
forall i r1 r2 k t φ,
encodes i (load r1 r2 k) -> r1 <> pc -> necessary t -> necessary φ ->
notindom r1 φ -> notindom pc φ ->
tref (tjust i) ∧ ∆toffset 1 (tcodeptr (φ ∧ tslot r1 t)) ⊢
tcodeptr (φ ∧ tslot r2 (toffset k (tref t))).
Lemma store_rule :
forall i r1 r2 k t φ,
encodes i (store r1 k r2) -> necessary t -> necessary φ ->
notindom pc φ ->
tref (tjust i) ∧ ∆toffset 1 (tcodeptr φ) ⊢
tcodeptr (φ ∧ tslot r1 (toffset k (tref t)) ∧ tslot r2 t).
Definition int := T.
Lemma addimm_rule :
forall i r1 r2 k t φ,
encodes i (addimm r1 r2 k) -> r1 <> pc -> necessary t -> necessary φ ->
notindom r1 φ -> notindom pc φ ->
tref (tjust i) ∧ ∆toffset 1 (tcodeptr (φ ∧ tslot r1 int)) ⊢
tcodeptr (φ ∧ tslot r2 int).
Lemma jump_rule :
forall i r φ,
encodes i (jump r) -> r <> pc -> necessary φ ->
notindom pc φ -> tref (tjust i) ∧ ∆toffset 1 (tcodeptr F) ⊢
tcodeptr (φ ∧ tslot r (tcodeptr φ)).
Soundness |
Require Import List.
Definition program := list nat.
Fixpoint nth (n : nat) (p : program) {struct p} : option nat :=
match n, p with
| O, i :: _ => Some i
| O, _ => None
| S m, nil => None
| S m, _ :: r => nth m r
end.
Definition loaded (p : program) (l : location) (v : value) (m : memory) :=
forall k,
match nth k p with
None => True
| Some i => m (k + l) = i
end.
Fixpoint program_type_rec (p : program) (k : nat) {struct p} : type :=
match p with
nil => T
| cons i r => toffset k (tref (tjust i)) ∧ program_type_rec r (1 + k)
end.
Definition program_type p := program_type_rec p 0.
Definition prog_st n (p : program) (l : location) : store_typing n :=
fun l' =>
if le_lt_dec l l' then
match nth (l' - l) p with
Some i => SomeT (approx n (tjust i))
| None => NoneT
end
else
NoneT.
Lemma thas_conj : forall l s t, thas l s ∧ thas l t ⊢ thas l (s ∧ t).
Lemma everywhere_somewhere : forall p, SW p ⊢ EW (SW p).
Lemma somewhere_pure : forall p, pure (SW p).
Hint Resolve somewhere_pure.
Lemma tplus_r : forall t l k, t ⊢ tplus l k (k + l).
Lemma thas_toffset_2 :
forall l k t, thas (k + l) t ⊢ thas l (toffset k t).
Lemma program_well_typed :
forall p l v m n,
loaded p l v m -> v pc = l ->
exists ψ : store_typing n,
(validmem m) (Build_config (Build_world ψ) v) /\
(tslot pc (program_type p)) (Build_config (Build_world ψ) v).
Theorem soundness :
forall p l v m n,
loaded p l v m -> v pc = l -> program_type p ⊢ tcodeptr T ->
safen n v m.
Isomorphisms regarding code pointers |
Lemma forall_exists :
forall A B (f : A -> B -> type),
(∃x, ∀y, f x y) ⊢ ∀y, ∃x, f x y.
Lemma toto :
forall A (f : A -> type), tcodeptr (Exists f) ⊢ ∀x, tcodeptr (f x).
Require Import Classical.
Lemma excluded_middle : forall t, T ⊢ t ∨ (t ⇒ F).
Lemma forall_and_exists_tjust :
forall A (x0 : A) (f : location -> A -> type),
(∀x, ∃l, tjust l ∧ f l x) ⊢ ∃l, tjust l ∧ ∀x, f l x.
Lemma titi :
forall A (x0 : A) (f : A -> type),
(∀x, tcodeptr (f x)) ⊢ tcodeptr (Exists f).