-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathResourceExhaustionExample.v
180 lines (152 loc) · 5.16 KB
/
ResourceExhaustionExample.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
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
Require Import LanguageModel.
Require Import ChainModel.
Require Import TraceCriterion.
Require Import TypeRelationExample.
Require Import ResourceExhaustion.
Require Import TraceModel.
Require Import TraceCriterion.
(* Careful: we should make sure to not mix the definition between TypeRelationExample and this file *)
Set Bullet Behavior "Strict Subproofs".
Section Traces.
Definition event : TraceModel.Events.
exists HTrace (HTBool true) (HTNat 0).
congruence.
intros e1 e2. destruct e1, e2; try (left; congruence); try (right; congruence).
destruct b, b0; try (left; congruence); try (right; congruence).
pose proof Coq.Arith.Peano_dec.eq_nat_dec n n0.
destruct H. left; now subst.
right; congruence.
Defined.
Definition endstate : TraceModel.Endstates.
exists unit. exact tt.
Defined.
Definition trace := @TraceModel.trace event endstate.
End Traces.
Section Source.
Definition sprg := {e : HExp | exists τ, typing e τ }.
Definition spar := sprg.
Definition sctx := unit.
Definition splug (p : spar) (c : sctx) := p.
Definition source := {| prg := sprg; par := spar; ctx := sctx; plug := splug |}.
Definition traceS := trace.
Definition semS : sprg -> traceS -> Prop :=
fun p t =>
match t with
| TraceModel.tstop (t :: nil) tt => hsem (proj1_sig p) = t
| _ => False
end.
Lemma non_empty_semS : forall W, exists t, semS W t.
Proof.
destruct W as [e [[|] Hty]].
- destruct (type_correct_nat _ Hty) as [n Hn].
now (exists (TraceModel.tstop ((HTNat n : ev event) :: nil) (tt : es endstate) : traceS)).
- destruct (type_correct_bool _ Hty) as [b Hb].
now (exists (TraceModel.tstop ((HTBool b : ev event) :: nil) (tt : es endstate) : traceS)).
Qed.
Definition semanticsS : Semantics source traceS :=
{| sem := semS : prg source -> traceS -> Prop;
non_empty_sem := non_empty_semS |}.
End Source.
Section Target.
Definition tprg := {e : HExp | exists τ, typing e τ}.
Definition tpar := tprg.
Definition tctx := unit.
Definition tplug (p : tpar) (c : tctx) := p.
Definition target := {| prg := tprg; par := tpar; ctx := tctx; plug := tplug |}.
Definition endstateT := ResourceExhaustion.endstateT endstate.
Definition traceT := ResourceExhaustion.traceT event endstate.
Fixpoint size (e : HExp) :=
match e with
| HNat n => 1
| HBool _ => 1
| HPlus e1 e2 => 1 + size e1 + size e2
| HTimes e1 e2 => 1 + size e1 + size e2
| HIte e1 e2 e3 => 1 + size e1 + size e2 + size e3
| HLe e1 e2 => 1 + size e1 + size e2
end.
Definition semT' (n : nat) : tprg -> traceT :=
fun p => if Nat.leb (size (proj1_sig p)) n then (tstop ((hsem (proj1_sig p) : ev event):: nil) (inl tt : es endstateT))
else tstop nil (OOM endstate ).
Definition semT : tprg -> traceT -> Prop := fun p t => exists n, semT' n p = t.
Lemma non_empty_semT : forall W, exists t, semT W t.
Proof.
destruct W as [e ?].
exists (tstop nil (OOM endstate)).
exists 0.
unfold semT'.
simpl. assert (H: Nat.leb (size e) 0 = false) by now induction e.
now rewrite H.
Qed.
Definition semanticsT : Semantics target traceT :=
{| sem := semT : prg target -> traceT -> Prop;
non_empty_sem := non_empty_semT |}.
End Target.
Section CompilationChain.
Definition compile_w : prg source -> prg target :=
id.
Definition compiler : CompilationChain source target :=
{| compile_whole := compile_w;
compile_par := compile_w;
compile_ctx := id |}.
End CompilationChain.
Definition rel := ResourceExhaustion.rel event endstate.
Definition rel_TC := rel_TC compiler semanticsS semanticsT rel.
Lemma no_silent : forall e tt l,
semT e tt -> tt <> tsilent l.
Proof.
intros e tt l Hsem.
destruct tt.
- congruence.
- unfold semT in Hsem.
destruct Hsem as [n Hsem].
unfold semT' in Hsem.
destruct (Nat.leb (size (proj1_sig e)));
now inversion Hsem.
- congruence.
Qed.
Lemma no_stream : forall e tt s,
semT e tt -> tt <> tstream s.
Proof.
intros e tt s Hsem.
destruct tt.
- congruence.
- congruence.
- unfold semT in Hsem.
destruct Hsem as [n Hsem].
unfold semT' in Hsem.
destruct (Nat.leb (size (proj1_sig e)));
now inversion Hsem.
Qed.
Lemma correctness : rel_TC.
Proof.
unfold rel_TC.
unfold TraceCriterion.rel_TC.
intros [e Hty] tt Hsem.
inversion Hty as [τ Hty'].
destruct tt; simpl in Hsem.
- (* the interesting case *)
destruct Hsem as [n Hsem].
unfold semT' in Hsem.
destruct (Nat.leb
(size
(proj1_sig
(compile_w
(exist (fun e : HExp => exists τ : type, typing e τ)
e Hty)))) n) eqn:Heq.
+ simpl in *.
inversion Hsem; subst; clear Hsem.
exists (tstop ((hsem e : ev event) :: nil) (tt : es endstate)).
split.
* now repeat constructor.
* reflexivity.
+ simpl in *.
inversion Hsem; subst; clear Hsem.
exists (tstop ((hsem e : ev event) :: nil) (tt : es endstate)).
split.
right; eexists; split; constructor.
reflexivity.
- exfalso.
now eapply no_silent; eauto.
- exfalso.
now eapply no_stream; eauto.
Qed.