1 | |
---|
2 | include "RTLabs/RTLabs_partial_traces.ma". |
---|
3 | include "common/Measurable.ma". |
---|
4 | include "common/stacksize.ma". |
---|
5 | |
---|
6 | definition RTLabs_stack_ident : |
---|
7 | genv → |
---|
8 | ∀s:state. |
---|
9 | match RTLabs_classify s with [ cl_call ⇒ True | _ ⇒ False ] → |
---|
10 | ident ≝ |
---|
11 | λge,s. |
---|
12 | match s return λs. match RTLabs_classify s with [ cl_call ⇒ True | _ ⇒ False ] → ident with |
---|
13 | [ Callstate id _ _ _ _ _ ⇒ λ_. id |
---|
14 | | State f fs m ⇒ λH.⊥ |
---|
15 | | _ ⇒ λH.⊥ |
---|
16 | ]. |
---|
17 | try @H |
---|
18 | whd in match (RTLabs_classify ?) in H; |
---|
19 | cases (next_instruction f) in H; |
---|
20 | normalize // |
---|
21 | qed. |
---|
22 | |
---|
23 | definition RTLabs_pcsys ≝ mk_preclassified_system |
---|
24 | RTLabs_fullexec |
---|
25 | (λ_.RTLabs_cost) |
---|
26 | (λ_.RTLabs_classify) |
---|
27 | RTLabs_stack_ident. |
---|
28 | |
---|
29 | definition state_at : ∀C:preclassified_system. |
---|
30 | ∀p:program ?? C. nat → |
---|
31 | res (state … C (make_global … C p)) ≝ |
---|
32 | λC,p,n. |
---|
33 | let g ≝ make_global … (pcs_exec … C) p in |
---|
34 | let C' ≝ pcs_to_cs C g in |
---|
35 | ! s0 ← make_initial_state … p; |
---|
36 | ! 〈prefix,s1〉 ← exec_steps n ?? (cs_exec … C') g s0; |
---|
37 | return s1. |
---|
38 | |
---|
39 | definition eval_ext_statement : ∀ge. RTLabs_ext_state ge → IO io_out io_in (trace × (RTLabs_ext_state ge)) ≝ |
---|
40 | λge,s. |
---|
41 | match eval_statement ge s return λx. (∀s',t. x = Value ??? 〈t,s'〉 → RTLabs_ext_state ge) → ? with |
---|
42 | [ Value ts ⇒ λnext. Value ??? 〈\fst ts, next (\snd ts) (\fst ts) ?〉 |
---|
43 | | Wrong m ⇒ λ_. Wrong ??? m |
---|
44 | | Interact o k ⇒ λ_. Wrong … (msg UnexpectedIO) |
---|
45 | ] (next_state ge s). |
---|
46 | // |
---|
47 | qed. |
---|
48 | |
---|
49 | definition RTLabs_ext_exec : trans_system io_out io_in ≝ |
---|
50 | mk_trans_system io_out io_in ? RTLabs_ext_state (λ_.RTLabs_is_final) eval_ext_statement. |
---|
51 | |
---|
52 | definition make_ext_initial_state : ∀p:RTLabs_program. res (RTLabs_ext_state (make_global p)) ≝ |
---|
53 | λp. |
---|
54 | let ge ≝ make_global p in |
---|
55 | do m ← init_mem … (λx.[Init_space x]) p; |
---|
56 | let main ≝ prog_main ?? p in |
---|
57 | do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol … ge main); |
---|
58 | do f as Ef ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr … ge b); |
---|
59 | let s ≝ Callstate main f (nil ?) (None ?) (nil ?) m in |
---|
60 | return (mk_RTLabs_ext_state (make_global p) s [b] ?). |
---|
61 | % [ @Ef | % ] |
---|
62 | qed. |
---|
63 | |
---|
64 | lemma initial_states_OK : ∀p,s. |
---|
65 | make_ext_initial_state p = return s → |
---|
66 | make_initial_state p = return (Ras_state … s). |
---|
67 | #p #s #E |
---|
68 | cases (bind_inversion ????? E) -E #m * #E1 #E |
---|
69 | cases (bind_inversion ????? E) -E #b * #E2 #E |
---|
70 | cases (bind_as_inversion ????? E) -E #f * #Ef #E |
---|
71 | whd in ⊢ (??%?); >E1 |
---|
72 | whd in ⊢ (??%?); >E2 |
---|
73 | whd in ⊢ (??%?); >Ef |
---|
74 | whd in E:(??%%) ⊢ (??%?); destruct |
---|
75 | % |
---|
76 | qed. |
---|
77 | |
---|
78 | lemma initial_states_OK' : ∀p,s. |
---|
79 | make_initial_state p = return s → |
---|
80 | ∃S,M. make_ext_initial_state p = return (mk_RTLabs_ext_state (make_global p) s S M). |
---|
81 | #p #s #E |
---|
82 | cases (bind_inversion ????? E) -E #m * #E1 #E |
---|
83 | cases (bind_inversion ????? E) -E #b * #E2 #E |
---|
84 | cases (bind_inversion ????? E) -E #f * #Ef #E |
---|
85 | whd in E:(??%%); destruct |
---|
86 | %{[b]} % [ % [ @Ef | % ] ] |
---|
87 | whd in ⊢ (??%?); >E1 |
---|
88 | whd in ⊢ (??%?); >E2 |
---|
89 | whd in ⊢ (??%?); generalize in match (refl ??); |
---|
90 | >Ef in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)?); #Ef' % |
---|
91 | qed. |
---|
92 | |
---|
93 | |
---|
94 | definition RTLabs_ext_fullexec : fullexec io_out io_in ≝ |
---|
95 | mk_fullexec … RTLabs_ext_exec make_global make_ext_initial_state. |
---|
96 | |
---|
97 | definition RTLabs_ext_pcsys ≝ mk_preclassified_system |
---|
98 | RTLabs_ext_fullexec |
---|
99 | (λg,s. RTLabs_cost (Ras_state … s)) |
---|
100 | (λg,s. RTLabs_classify (Ras_state … s)) |
---|
101 | (λg,s,H. RTLabs_stack_ident g (Ras_state … s) H). |
---|
102 | |
---|
103 | definition lift_some : ∀A,B:Type[0]. (A → B) → A → option B ≝ |
---|
104 | λA,B,f,a. Some B (f a). |
---|
105 | |
---|
106 | definition max_stack_of_tlr : ∀S,s1,s2. trace_label_return S s1 s2 → (ident → option nat) → ident → nat → nat ≝ |
---|
107 | λS,s1,s2,tlr,stack_cost,currentfn,initial. |
---|
108 | maximum (update_stacksize_info stack_cost (mk_stacksize_info initial 0) (extract_call_ud_from_tlr S s1 s2 tlr currentfn)). |
---|
109 | |
---|
110 | (* A bit of mucking around because we're going to build a will_return in Type[0]. |
---|
111 | In principle we could drop the alternative form of will_return entirely, but |
---|
112 | time pressures don't really allow for that. *) |
---|
113 | record cft (ge:genv) (n:nat) (s:state) (hd:state×trace) (rem:list (state × trace)) (s':state) (EX:?) : Type[0] ≝ { |
---|
114 | cft_tr : trace; |
---|
115 | cft_s : state; |
---|
116 | cft_EV : eval_statement ge s = Value ??? 〈cft_tr,cft_s〉; |
---|
117 | cft_EX : exec_steps n … RTLabs_fullexec ge cft_s = OK ? 〈rem,s'〉; |
---|
118 | cft_E : make_flat_trace ge (S n) s (hd::rem) s' EX = ft_step ??? s cft_tr cft_s cft_EV (make_flat_trace ge n cft_s rem s' cft_EX) |
---|
119 | }. |
---|
120 | |
---|
121 | lemma cons_flat_trace : ∀ge,n,s,hd,trace,s'. |
---|
122 | ∀EX:exec_steps (S n) … RTLabs_fullexec ge s = return 〈hd::trace,s'〉. |
---|
123 | cft ge n s hd trace s' EX. |
---|
124 | #ge #n #s #hd #trace #s' #EX |
---|
125 | lapply (refl ? (eval_statement ge s)) |
---|
126 | cases (eval_statement ge s) in ⊢ (???% → ?); |
---|
127 | [ #o #k | 3: #m ] |
---|
128 | [ 1,2: #EV @⊥ cases (exec_steps_S … EX) #NF * #tr * #s2 * #tl * * #E1 destruct |
---|
129 | change with (eval_statement ??) in ⊢ (??%? → ?); >EV #E destruct |
---|
130 | ] * #tr #s1 #EV |
---|
131 | @(mk_cft … tr s1 EV) |
---|
132 | [ cases (exec_steps_S … EX) #NF * #tr2 * #s2 * #tl * * #E1 destruct |
---|
133 | change with (eval_statement ??) in ⊢ (??%? → ?); |
---|
134 | >EV in ⊢ (% → ?); #E destruct #EX' @EX' |
---|
135 | | whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); |
---|
136 | >EV in ⊢ (???% → ??(match % with [_⇒?|_⇒?|_⇒?]?)?); |
---|
137 | #ST' whd in ⊢ (??%?); % |
---|
138 | ] qed. |
---|
139 | |
---|
140 | lemma will_return_equiv : ∀ge,trace,depth,n,s,s',EX. |
---|
141 | will_return_aux (pcs_to_cs … RTLabs_pcsys ge) depth trace → |
---|
142 | will_return ge depth s (make_flat_trace ge n s trace s' EX). |
---|
143 | #ge #trace0 elim trace0 |
---|
144 | [ #depth #n #s #s' #EX * |
---|
145 | | * #s1 #tr1 #tl #IH #depth #n #s #s' #EX |
---|
146 | lapply (exec_steps_length … EX) #E1 |
---|
147 | lapply (exec_steps_first … EX) #E2 |
---|
148 | lapply (refl ? (eval_statement ge s)) |
---|
149 | cases (eval_statement ge s) in ⊢ (???% → ?); |
---|
150 | [ #o #k destruct #EV @⊥ |
---|
151 | whd in EX:(??%?); cases (is_final io_out io_in RTLabs_fullexec ge s1) in EX; |
---|
152 | [ whd in ⊢ (??%? → ?); change with (eval_statement ??) in match (step ?????); |
---|
153 | >EV #EX whd in EX:(??%%); destruct |
---|
154 | | #r #EX whd in EX:(??%%); destruct |
---|
155 | ] |
---|
156 | | 3: #m #EV @⊥ destruct |
---|
157 | whd in EX:(??%?); cases (is_final io_out io_in RTLabs_fullexec ge s1) in EX; |
---|
158 | [ whd in ⊢ (??%? → ?); change with (eval_statement ??) in match (step ?????); |
---|
159 | >EV #EX whd in EX:(??%%); destruct |
---|
160 | | #r #EX whd in EX:(??%%); destruct |
---|
161 | ] |
---|
162 | ] * #tr2 #s2 #EV >E1 in EX; #EX |
---|
163 | whd in ⊢ (?% → ?); |
---|
164 | lapply (refl ? (cs_classify ? s1)) |
---|
165 | cases (cs_classify ??) in ⊢ (???% → %); |
---|
166 | #CL whd in ⊢ (?% → ?); |
---|
167 | [ cases depth |
---|
168 | [ whd in ⊢ (?% → ?); cases tl in EX ⊢ %; |
---|
169 | [ #EX #_ |
---|
170 | lapply (cons_flat_trace … EX) #CFT >(cft_E … CFT) |
---|
171 | @wr_base |
---|
172 | destruct @CL |
---|
173 | | * #s3 #tr3 #tl3 #EX * |
---|
174 | ] |
---|
175 | | #depth' whd in ⊢ (?% → ?); #H |
---|
176 | lapply (cons_flat_trace … EX) #CFT >(cft_E … CFT) |
---|
177 | @wr_ret |
---|
178 | [ destruct @CL |
---|
179 | | @IH @H |
---|
180 | ] |
---|
181 | ] |
---|
182 | | #H lapply (cons_flat_trace … EX) #CFT >(cft_E … CFT) |
---|
183 | @wr_step [ %2 destruct @CL | @IH @H ] |
---|
184 | | #H lapply (cons_flat_trace … EX) #CFT >(cft_E … CFT) |
---|
185 | @wr_call [ destruct @CL | @IH @H ] |
---|
186 | | cases (RTLabs_notail … CL) |
---|
187 | | #H lapply (cons_flat_trace … EX) #CFT >(cft_E … CFT) |
---|
188 | @wr_step [ %1 destruct @CL | @IH @H ] |
---|
189 | ] |
---|
190 | ] qed. |
---|
191 | |
---|
192 | lemma extend_RTLabs_exec_steps : ∀ge,n. ∀s:RTLabs_ext_state ge. ∀trace,s'. |
---|
193 | exec_steps n … RTLabs_fullexec ge (Ras_state … s) = return 〈trace,s'〉 → |
---|
194 | ∃trace',S,M. exec_steps n … RTLabs_ext_fullexec ge s = return 〈trace',mk_RTLabs_ext_state … s' S M〉. |
---|
195 | #ge #n0 elim n0 |
---|
196 | [ #s #trace #s' #E whd in E:(??%%); destruct %{[ ]} cases s #s' #S #M |
---|
197 | %{S} %{M} % |
---|
198 | | #n #IH #s #trace #s' #EX |
---|
199 | cases (exec_steps_S … EX) #NF * #tr * #s1 * #tl * * #E #STEP #EX' |
---|
200 | lapply (refl ? (eval_ext_statement ge s)) |
---|
201 | whd in ⊢ (???% → ?); |
---|
202 | change with (eval_statement ge s) in STEP:(??%?); |
---|
203 | letin f ≝ (next_state ge s) (* Is there a more natural way to generalize partial applications? *) |
---|
204 | cut (∀s',t,EV. Ras_state … (f s' t EV) = s') |
---|
205 | [ // ] |
---|
206 | generalize in match f; -f |
---|
207 | >STEP #next #NEXT whd in ⊢ (???% → ?); letin s1' ≝ (next s1 tr ?) #STEP' |
---|
208 | <(NEXT … (refl ??)) in EX'; #EX' |
---|
209 | cases (IH s1' … EX') |
---|
210 | #tl' * #S'' * #M'' #STEPS'' |
---|
211 | %{(〈s,tr〉::tl')} %{S''} %{M''} |
---|
212 | whd in ⊢ (??%?); |
---|
213 | change with (RTLabs_is_final s) in match (is_final ?????); |
---|
214 | change with (RTLabs_is_final s) in match (is_final ?????) in NF; |
---|
215 | >NF whd in ⊢ (??%?); |
---|
216 | change with (eval_ext_statement ??) in match (step ?????); |
---|
217 | >STEP' whd in ⊢ (??%?); |
---|
218 | >STEPS'' % |
---|
219 | ] qed. |
---|
220 | |
---|
221 | |
---|
222 | |
---|
223 | (* I'm not entirely certain that existentially quantifying fn is the right thing |
---|
224 | to do. In principle we must provide the right one to satisfy the condition |
---|
225 | about observables, but perhaps we ought to show how to produce it explicitly. |
---|
226 | *) |
---|
227 | |
---|
228 | |
---|
229 | theorem measurable_subtraces_are_structured : ∀p,m,n,stack_cost,max,prefix,interesting. |
---|
230 | measurable RTLabs_pcsys p m n stack_cost max → |
---|
231 | observables RTLabs_pcsys p m n = return 〈prefix,interesting〉 → |
---|
232 | let midstack ≝ \fst (measure_stack stack_cost 0 prefix) in |
---|
233 | ∃sm,sn,fn.∃tlr:trace_label_return (RTLabs_status (make_global p)) sm sn. |
---|
234 | state_at RTLabs_ext_pcsys p m = return sm ∧ |
---|
235 | le (max_stack_of_tlr ??? tlr (lift_some … stack_cost) fn midstack) max ∧ |
---|
236 | pi1 … (observables_trace_label_return (RTLabs_status (make_global p)) sm sn tlr fn) = interesting. |
---|
237 | #p #m #n #stack_cost #max #prefix #interesting |
---|
238 | change with (make_global … RTLabs_fullexec p) in match (make_global p); |
---|
239 | * #s0 * #prefix' * #s1 * #interesting' * #s2 |
---|
240 | letin ge ≝ (make_global … RTLabs_fullexec p) |
---|
241 | * * * * * #INIT #EXEC1 #EXEC2 #LABEL_TO_RETURN #RETURNS #STACK |
---|
242 | whd in ⊢ (??%? → ?); >INIT |
---|
243 | whd in ⊢ (??%? → ?); >EXEC1 |
---|
244 | whd in ⊢ (??%? → ?); >EXEC2 |
---|
245 | whd in ⊢ (??%? → ?); @breakup_pair #E whd in E:(??%%); destruct |
---|
246 | cases (initial_states_OK' … INIT) #S * #M #INIT' |
---|
247 | cases (extend_RTLabs_exec_steps ?? (mk_RTLabs_ext_state (make_global p) s0 S M) … EXEC1) |
---|
248 | #prefix'' * #S1 * #M1 letin s1' ≝ (mk_RTLabs_ext_state ? s1 S1 M1) #EXEC1' |
---|
249 | lapply (make_label_return' ge 0 s1' (make_flat_trace ????? EXEC2) ????) |
---|
250 | [ @will_return_equiv assumption |
---|
251 | | |
---|
252 | | |
---|
253 | | |
---|
254 | | * #s2' #rem #_ #tlr #STACK #_ |
---|
255 | %{s1'} %{s2'} % [2: %{tlr} |
---|
256 | % [ % |
---|
257 | [ whd in ⊢ (??%?); |
---|
258 | change with (make_ext_initial_state p) in match (make_initial_state ????); |
---|
259 | >INIT' whd in ⊢ (??%?); |
---|
260 | >EXEC1' % |
---|
261 | | |
---|
262 | ]| |
---|
263 | ] |
---|
264 | ]] |
---|
265 | |
---|
266 | |
---|