source: src/Clight/labelSimulation.ma @ 1893

Last change on this file since 1893 was 1893, checked in by campbell, 8 years ago

Show stronger result about labelling of expressions.

File size: 10.7 KB
Line 
1
2include "Clight/label.ma".
3include "Clight/Cexec.ma".
4
5(* for the induction principle *)
6include "Clight/CexecSound.ma".
7
8lemma commute_fst_pair : ∀A,B,C,D:Type[0].∀e:A×B.∀F:A → B → C×D.
9  \fst (let 〈x,y〉 ≝ e in F x y) =  let 〈x,y〉 ≝ e in \fst (F x y).
10#A #B #C #D * //
11qed.
12
13lemma shift_fst : ∀A,B,C,D:Type[0].∀e:A×B.∀F:A → C.∀G:B → D.
14  \fst (let 〈x,y〉 ≝ e in 〈F x, G y〉) =  F (\fst e).
15#A #B #C #D * //
16qed.
17
18lemma label_expr_elim : ∀e,u.∀T:Type[0].∀F:expr → universe CostTag → T. ∀P:T → Type[0].
19  (∀u'. P (F (\fst (label_expr e u)) u')) →
20  P (let 〈e',u'〉 ≝ label_expr e u in F e' u').
21#e #u #T #F #P
22cases (label_expr e u)
23#e' #u' #H @H
24qed.
25
26lemma add_cost_expr_elim : ∀e,u.∀T:Type[0].∀F:expr → universe CostTag → T. ∀P:T → Type[0].
27  (∀u',l. P (F (Expr (Ecost l e) (typeof e)) u')) →
28  P (let 〈e',u'〉 ≝ add_cost_expr e u in F e' u').
29#e #u #T #F #P #H whd in match (add_cost_expr ??);
30cases (fresh ??) #l #u' @H
31qed.
32
33
34
35lemma label_expr_type : ∀e,u.
36  typeof (\fst (label_expr e u)) = typeof e.
37* #e #ty #u >shift_fst //
38qed.
39
40inductive trace_with_extra_labels : trace → trace → Prop ≝
41| twel_0 : trace_with_extra_labels E0 E0
42| twel_both : ∀h,t1,t2. trace_with_extra_labels t1 t2 → trace_with_extra_labels (h::t1) (h::t2)
43| twel_new : ∀c,t1,t2. trace_with_extra_labels t1 t2 → trace_with_extra_labels t1 (EVcost c::t2).
44
45lemma twel_refl : ∀tr. trace_with_extra_labels tr tr.
46#tr elim tr /2/
47qed.
48
49lemma twel_app : ∀tr1,tr2,tr1',tr2'.
50  trace_with_extra_labels tr1 tr1' →
51  trace_with_extra_labels tr2 tr2' →
52  trace_with_extra_labels (tr1⧺tr2) (tr1'⧺tr2').
53#tr1 #tr2 #tr1' #tr2' #twel1 elim twel1 /3/
54qed. 
55
56lemma label_expr_ok : ∀ge,en,m,e,v,tr.
57  exec_expr ge en m e = OK … 〈v,tr〉 →
58  ∀u. ∃tr'. exec_expr ge en m (\fst (label_expr e u)) = OK … 〈v,tr'〉 ∧
59            trace_with_extra_labels tr tr'.
60#ge #en #m #e
61@(expr_lvalue_ind ?
62  (λe,ty. ∀b,o,tr. exec_lvalue' ge en m e ty = OK … 〈〈b,o〉,tr〉 →
63          ∀u. ∃tr'. exec_lvalue' ge en m (\fst (label_expr_descr e u ty)) ty = OK … 〈〈b,o〉,tr'〉 ∧
64                    trace_with_extra_labels tr tr') … e)
65[ 1,2: normalize /3 by ex_intro, conj/
66| * //
67 [ normalize /3 by ex_intro, conj/
68 | #e1 #ty #IH #v #tr #EX #u
69   cases (bind_inversion ????? EX) * * #b #o #tr1 * #EX1 #EX1r
70   cases (bind_inversion ????? EX1r) #v * #EXl #EXrem
71   normalize in EXrem; destruct
72   cases (IH … EX1 u) #tr1' * #EX1' #twel1
73   %{tr1'} >shift_fst in EX1'; >shift_fst >shift_fst #EX1' whd in ⊢ (?(??%?)?); >EX1'
74   whd in ⊢ (?(??%?)?); >EXl /2/
75 | #e1 #id #ty #IH #v #tr #EX #u
76   cases (bind_inversion ????? EX) * * #b #o #tr1 * #EX1 #EX1r
77   cases (bind_inversion ????? EX1r) #v * #EXl #EXrem
78   normalize in EXrem; destruct
79   cases (IH … EX1 u) #tr1' * #EX1' #twel1
80   %{tr1'} >shift_fst in EX1'; >shift_fst >shift_fst #EX1' % // whd in ⊢ (??%?); >EX1'
81   whd in ⊢ (??%?); >EXl @refl
82 ]
83| #v #ty #b #o #tr #EX #u %{tr} % /2/
84| #e1 #ty #IH #b #o #tr #EX #u
85  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
86  cases (IH … EX1 u) #tr1' * #EX1' #twel1
87  %{tr1'} >shift_fst whd in ⊢ (?(??%?)?); >EX1'
88  whd in ⊢ (?(??%?)?);
89  cases v1 in EX1rem ⊢ %; normalize #A try #B try #C destruct /2/
90| #ty' #e1 #ty #IH #v #tr #EX #u
91  cases (bind_inversion ????? EX) * * #b1 #o1 #tr1 * #EX1 #EX1rem
92  cases (IH … EX1 u) #tr1' * #EX1' #twel1
93  %{tr1'} >shift_fst >shift_fst >shift_fst whd in ⊢ (?(??%?)?);
94  whd in ⊢ (?(??(match % with [_⇒?|_⇒?])?)?); >EX1'
95  whd in ⊢ (?(??%?)?);
96  cases ty' in EX1rem ⊢ %;
97  [ 4: #r #ty' whd in ⊢ (??%? → ?(??%?)?); cases (pointer_compat_dec b1 r)
98       #pc normalize #E destruct /2/
99  | *: normalize #A try #B try #C try #D destruct
100  ]
101| #ty #op #e1 #IH #v #tr #EX #u
102  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
103  cases (bind_inversion ????? EX1rem) #v2 * #EX2 #EXrem
104  normalize in EXrem; destruct
105  cases (IH … EX1 u) #tr1' * #EX1' #twel1
106  %{tr1'} % // >shift_fst
107  whd in ⊢ (??(????(?(???%)?))?);
108  @label_expr_elim #u2
109  whd in ⊢ (??%?); >EX1'
110  whd in ⊢ (??%?); >label_expr_type >EX2 @refl
111| #ty #op #e1 #e2 #IH1 #IH2 #v #tr #EX
112  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
113  cases (bind_inversion ????? EX1rem) * #v2 #tr2 * #EX2 #EX2rem
114  cases (bind_inversion ????? EX2rem) #v' * #EXop #EXop'
115  #u
116  cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
117  >shift_fst
118  whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?));
119  @label_expr_elim #u2
120  cases (IH2 … EX2 u2) #tr2' * #EX2' #twel2
121  @label_expr_elim #u3 %{(tr1'⧺tr2')}
122  whd in ⊢ (?(??%?)?); >EX1'
123  whd in ⊢ (?(??%?)?); >EX2'
124  whd in ⊢ (?(??%?)?); >label_expr_type >label_expr_type >EXop
125  normalize in EXop'; destruct % /2/
126| #ty #ty' #e1 #IH #v #tr #EX #u
127  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
128  cases (bind_inversion ????? EX1rem) #v2 * #EX2 #EX2rem
129  normalize in EX2rem; destruct
130  cases (IH … EX1 u) #tr1' * #EX1' #twel1
131  %{tr1'} % // >shift_fst >shift_fst
132  whd in ⊢ (??%?); >EX1'
133  whd in ⊢ (??%?); >label_expr_type >EX2 @refl
134| #ty #e1 #e2 #e3 #IH1 #IH2 #IH3 #v #tr #EX #u
135  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
136  cases (bind_inversion ????? EX1rem) * * #EXguard #EXguardrem
137  cases (bind_inversion ????? EXguardrem) * #v2 #tr2 * #EX2 #EX2rem
138  normalize in EX2rem; destruct
139  cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
140  >shift_fst whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?));
141  @label_expr_elim #u2
142  @label_expr_elim #u3
143  @add_cost_expr_elim #u4 #l4
144  @label_expr_elim #u5
145  @add_cost_expr_elim #u6 #l6
146  [ cases (IH2 … EX2 u2) | cases (IH3 … EX2 u4) ] #trx' * #EXx' #twelx
147  [ %{(tr1'⧺trx'⧺(Echarge l4))} | %{(tr1'⧺trx'⧺(Echarge l6))} ]
148  whd in ⊢ (?(??%?)?); >EX1'
149  whd in ⊢ (?(??%?)?); >label_expr_type >EXguard
150  whd in ⊢ (?(??%?)?); whd in ⊢ (?(??(match % with [_⇒?|_⇒?])?)?); >EXx'
151  normalize % // @twel_app // <(E0_right tr2) @twel_app /2/
152| #ty #e1 #e2 #IH1 #IH2 #v #tr #EX #u
153  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
154  cases (bind_inversion ????? EX1rem) * * #EXguard #EXguardrem
155  >shift_fst whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?));
156  @label_expr_elim #u2
157  @label_expr_elim #u3
158  @add_cost_expr_elim #u4 #l4
159  @add_cost_expr_elim #u5 #l5
160  [ cases (bind_inversion ????? EXguardrem) * #v2 #tr2 * #EX2 #EX2rem
161    cases (bind_inversion ????? EX2rem) * * #EX3 #EX3rem
162    -EX1rem -EXguardrem -EX2rem
163    cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
164    cases (IH2 … EX2 u2) #tr2' * #EX2' #twel2
165    %{(tr1'⧺(tr2'⧺E0)⧺Echarge l4)}
166    whd in ⊢ (?(??%?)?); >EX1'
167    whd in ⊢ (?(??%?)?); >label_expr_type >EX2' >EXguard
168    whd in ⊢ (?(??%?)?); whd in ⊢ (?(??(match % with [_⇒?|_⇒?])?)?);
169    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >EX2'
170    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >label_expr_type >EX3
171    normalize in EX3rem ⊢ %; destruct % [ 1,3: @refl | *: @twel_app // <(E0_right tr2) @twel_app /2/ ]
172  | cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
173    %{(tr1'⧺E0⧺Echarge l5)}
174    whd in ⊢ (?(??%?)?); >EX1'
175    whd in ⊢ (?(??%?)?); >label_expr_type >EXguard
176    normalize in EXguardrem; destruct % // <(E0_right tr) @twel_app /2/
177  ]
178| #ty #e1 #e2 #IH1 #IH2 #v #tr #EX #u
179  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
180  cases (bind_inversion ????? EX1rem) * * #EXguard #EXguardrem
181  >shift_fst whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?));
182  @label_expr_elim #u2
183  @add_cost_expr_elim #u4 #l4
184  @label_expr_elim #u3
185  @add_cost_expr_elim #u5 #l5
186  [ cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
187    %{(tr1'⧺Echarge l4)}
188    whd in ⊢ (?(??%?)?); >EX1'
189    whd in ⊢ (?(??%?)?); >label_expr_type >EXguard
190    normalize in EXguardrem ⊢ %; destruct % // <(E0_right tr) /3/
191  | cases (bind_inversion ????? EXguardrem) * #v2 #tr2 * #EX2 #EX2rem
192    cases (bind_inversion ????? EX2rem) * * #EX3 #EX3rem
193    cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
194    cases (IH2 … EX2 u4) #tr2' * #EX2' #twel2
195    %{(tr1'⧺(tr2'⧺E0)⧺Echarge l5)}
196    whd in ⊢ (?(??%?)?); >EX1'
197    whd in ⊢ (?(??%?)?); >label_expr_type >EX2' >EXguard
198    whd in ⊢ (?(??%?)?); whd in ⊢ (?(??(match % with [_⇒?|_⇒?])?)?);
199    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >EX2'
200    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >label_expr_type >EX3
201    normalize in EX3rem ⊢ %; destruct % // @twel_app // <(E0_right tr2) @twel_app /2/
202  ]
203| #ty #ty' #v #tr normalize /3/
204| #ty #e1 #ty' #id #IH #b #o #tr #EX #u cases ty' in IH EX ⊢ %;
205  [ 7: #id #fl #IH #EX
206    cases (bind_inversion ????? EX) * * #b1 #o1 #tr1 * #EX1 #EX1rem
207    cases (bind_inversion ????? EX1rem) #n * #EXoff #EXoffrem
208    whd in EXoffrem:(???%); destruct >shift_fst >shift_fst
209    cases (IH … EX1 u) #tr1' * #EX1' #twel1
210    %{tr1'} % //
211    whd in ⊢ (??%?); whd in ⊢ (??(match % with [_⇒?|_⇒?])?); >EX1'
212    whd in ⊢ (??%?); >EXoff whd in ⊢ (??%?); @refl
213  | 8: #id #fl #IH #EX
214    cases (bind_inversion ????? EX) * * #b1 #o1 #tr1 * #EX1 #EX1rem
215    whd in EX1rem:(???%); destruct >shift_fst >shift_fst
216    cases (IH … EX1 u) #tr1' * #EX1' #twel1
217    %{tr1'} % //
218    whd in ⊢ (??%?); whd in ⊢ (??(match % with [_⇒?|_⇒?])?); >EX1'
219    whd in ⊢ (??%?); @refl
220  | *: normalize #A #B try #C try #D try #F destruct
221  ]
222| #ty #l #e1 #IH #v #tr #EX #u
223  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
224  whd in EX1rem:(???%); destruct
225  cases (IH … EX1 u) #tr1' * #EX1' #twel1 %{(tr1'@Echarge l)}
226  >shift_fst >shift_fst whd in ⊢ (?(??%?)?); >EX1'
227  whd in ⊢ (?(??%?)?); /3/
228| #e1 #ty #NLV #b #o #tr #EX @⊥
229  cases e1 in NLV EX; normalize //
230  #A #B #C try #D try #F destruct
231] qed.
232
233(* Plan:
234     - extend labelling functions to continuations and hence states
235       NO - this doesn't work because we don't know *which* cost labels to add
236       realistically we'll have to define erasure functions
237     - build a simulation relation linking states to their labelled counterparts
238     - write a predicate stating that two traces are the same except for some
239       extra costs
240     - show some labelling relationship for global environments
241     - prove that
242         exec_step ge s1 = = Value … 〈tr,s2〉 →
243         cost_related s1 s1' →
244         ∃tr'. equal_up_to_costs tr tr' ∧
245               plus ge' s1' tr' s2' ∧
246               cost_related s2 s2'
247       using some relationship between ge and ge'.
248
249WAIT - do I really want functions to erase the labels?  Or a predicate?
250
251let rec erase_label_expr (e:expr) : expr ≝
252match e with
253[ Expr ed ty ⇒ Expr (erase_label_expr_descr ed) ty
254]
255and erase_label_expr_descr (e:expr_descr) : expr_descr ≝
256match e with
257[ Ederef e' ⇒ Ederef (erase_label_expr_descr e')
258| Eaddrof e' ⇒ Eaddrof (erase_label_expr_descr e')
259| Eunop op e'
260*)
Note: See TracBrowser for help on using the repository browser.