-
Notifications
You must be signed in to change notification settings - Fork 2
/
Types.v
139 lines (92 loc) · 2.98 KB
/
Types.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
Require Import Bool Arith List CpdtTactics SfLib LibTactics.
Require Import Coq.Program.Equality.
Set Implicit Arguments.
Require Import Identifier Environment.
Require Import Imperative.
(* Type system *)
Inductive level :=
| Low : level
| High : level.
Lemma eq_level_dec: forall l1 l2: level, {l1 = l2} + { l1<>l2 }.
Proof.
decide equality.
Qed.
Hint Resolve eq_level_dec.
Hint Resolve eq_exp_dec.
Hint Resolve eq_id_dec.
Tactic Notation "level_cases" tactic (first) ident (c):=
first;
[Case_aux c "Low" | Case_aux c "High" ].
Inductive flowsto: level -> level -> Prop :=
| flowsto_sym: forall ℓ, flowsto ℓ ℓ
| flowsto_ord: flowsto Low High.
Hint Constructors flowsto.
Notation "ℓ '⊑' ℓ'" := (flowsto ℓ ℓ') (at level 35).
Definition typenv := @Env level.
Reserved Notation "'{{' Γ '⊢' e ':' ℓ '}}'" (at level 0, Γ at level 50, e at level 99).
Inductive exp_has_level : typenv -> exp -> level -> Prop :=
| T_Const : forall Γ n ℓ,
{{ Γ ⊢ ENum n : ℓ }}
| T_Id : forall Γ x ℓ,
(Γ x) = Some ℓ ->
{{ Γ ⊢ EId x : ℓ }}
| T_Plus : forall Γ e1 e2 ℓ,
{{ Γ ⊢ e1 : ℓ }} ->
{{ Γ ⊢ e2 : ℓ }} ->
{{ Γ ⊢ (EPlus e1 e2) : ℓ }}
| T_Sub : forall Γ e ℓ ℓ',
{{ Γ ⊢ e : ℓ }} ->
ℓ ⊑ ℓ' ->
{{ Γ ⊢ e : ℓ' }}
where "'{{' Γ '⊢' e ':' ℓ '}}' " := (exp_has_level Γ e ℓ).
Tactic Notation "exp_has_level_cases" tactic (first) ident (c) :=
first;
[Case_aux c "T_Const" | Case_aux c "T_Id" | Case_aux c "T_Plus" | Case_aux c "T_Sub" ].
(* Volpano-Smith simple typing *)
Reserved Notation "'-{' Γ ',' pc '⊢' c '}-'" (at level 0, Γ at level 55, pc at level 35).
Inductive cmd_has_type : typenv -> level -> cmd -> Prop :=
| T_Skip : forall Γ pc,
-{ Γ, pc ⊢ SKIP }-
| T_Assign: forall Γ pc x e ℓ ℓ',
{{ Γ ⊢ e : ℓ }} ->
Γ x = Some ℓ' ->
ℓ ⊑ ℓ' ->
pc ⊑ ℓ' ->
-{ Γ , pc ⊢ (x::=e) }-
| T_Seq : forall Γ pc c1 c2,
-{ Γ, pc ⊢ c1 }- ->
-{ Γ, pc ⊢ c2 }- ->
-{ Γ, pc ⊢ c1;;c2 }-
| T_If : forall Γ pc e ℓ pc' c1 c2,
{{ Γ ⊢ e : ℓ }} ->
ℓ ⊑ pc' ->
pc ⊑ pc' ->
-{ Γ, pc' ⊢ c1 }- ->
-{ Γ, pc' ⊢ c2 }- ->
-{ Γ, pc ⊢ IFB e THEN c1 ELSE c2 FI }-
| T_While : forall Γ pc e ℓ pc' c,
{{ Γ ⊢ e : ℓ }} ->
ℓ ⊑ pc' ->
pc ⊑ pc' ->
-{ Γ, pc' ⊢ c }- ->
-{ Γ, pc ⊢ WHILE e DO c END }-
where "'-{' Γ ',' pc '⊢' c '}-'" := (cmd_has_type Γ pc c).
Tactic Notation "cmd_has_type_cases" tactic (first) ident (c) :=
first;
[
Case_aux c "T_Skip" | Case_aux c "T_Assign" | Case_aux c "T_Seq"
| Case_aux c "T_if" | Case_aux c "T_While" ].
Lemma high_does_not_flow_to_low: ~ High ⊑ Low.
Proof.
crush; inversion H.
Qed.
Lemma wt_programs_are_not_stop:
forall Γ pc c,
-{ Γ, pc ⊢ c }- ->
c <> STOP.
Proof.
intros.
induction H;
congruence.
Qed.
Hint Resolve wt_programs_are_not_stop.