source: src/RTLabs/MeasurableToStructured.ma @ 2839

Last change on this file since 2839 was 2839, checked in by campbell, 7 years ago

Basic structure of RTLabs measurable to structured traces results.

File size: 10.0 KB
Line 
1
2include "RTLabs/RTLabs_partial_traces.ma".
3include "common/Measurable.ma".
4include "common/stacksize.ma".
5
6definition RTLabs_stack_ident :
7  genv →
8  ∀s:state.
9  match RTLabs_classify s with [ cl_call ⇒ True | _ ⇒ False ] →
10  ident ≝
11λge,s.
12match 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].
17try @H
18whd in match (RTLabs_classify ?) in H;
19cases (next_instruction f) in H;
20normalize //
21qed.
22
23definition RTLabs_pcsys ≝ mk_preclassified_system
24  RTLabs_fullexec
25  (λ_.RTLabs_cost)
26  (λ_.RTLabs_classify)
27  RTLabs_stack_ident.
28
29definition 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
39definition eval_ext_statement : ∀ge. RTLabs_ext_state ge → IO io_out io_in (trace × (RTLabs_ext_state ge)) ≝
40λge,s.
41match 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//
47qed.
48
49definition 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
52definition 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 | % ]
62qed.
63
64lemma 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
68cases (bind_inversion ????? E) -E #m * #E1 #E
69cases (bind_inversion ????? E) -E #b * #E2 #E
70cases (bind_as_inversion ????? E) -E #f * #Ef #E
71whd in ⊢ (??%?); >E1
72whd in ⊢ (??%?); >E2
73whd in ⊢ (??%?); >Ef
74whd in E:(??%%) ⊢ (??%?); destruct
75%
76qed.
77
78lemma 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
82cases (bind_inversion ????? E) -E #m * #E1 #E
83cases (bind_inversion ????? E) -E #b * #E2 #E
84cases (bind_inversion ????? E) -E #f * #Ef #E
85whd in E:(??%%); destruct
86%{[b]} % [ % [ @Ef | % ] ]
87whd in ⊢ (??%?); >E1
88whd in ⊢ (??%?); >E2
89whd in ⊢ (??%?); generalize in match (refl ??);
90>Ef in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)?); #Ef' %
91qed.
92
93
94definition RTLabs_ext_fullexec : fullexec io_out io_in ≝
95  mk_fullexec … RTLabs_ext_exec make_global make_ext_initial_state.
96
97definition 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
103definition lift_some : ∀A,B:Type[0]. (A → B) → A → option B ≝
104λA,B,f,a. Some B (f a).
105
106definition 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. *)
113record 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
121lemma 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
125lapply (refl ? (eval_statement ge s))
126cases (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
140lemma 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
192lemma 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
229theorem 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
238change with (make_global … RTLabs_fullexec p) in match (make_global p);
239* #s0 * #prefix' * #s1 * #interesting' * #s2
240letin ge ≝ (make_global … RTLabs_fullexec p)
241* * * * * #INIT #EXEC1 #EXEC2 #LABEL_TO_RETURN #RETURNS #STACK
242whd in ⊢ (??%? → ?); >INIT
243whd in ⊢ (??%? → ?); >EXEC1
244whd in ⊢ (??%? → ?); >EXEC2
245whd in ⊢ (??%? → ?); @breakup_pair #E whd in E:(??%%); destruct
246cases (initial_states_OK' … INIT) #S * #M #INIT'
247cases (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'
249lapply (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
Note: See TracBrowser for help on using the repository browser.