1 | |
---|
2 | include "RTLabs/semantics.ma". |
---|
3 | include "common/StructuredTraces.ma". |
---|
4 | |
---|
5 | discriminator status_class. |
---|
6 | |
---|
7 | (* NB: we do not consider jumps in the traces of RTLabs programs. *) |
---|
8 | |
---|
9 | inductive RTLabs_classify : state → status_class → Prop ≝ |
---|
10 | | rtla_other : ∀f,fs,m. RTLabs_classify (State f fs m) cl_other |
---|
11 | | rtla_call : ∀a,b,c,d,e. RTLabs_classify (Callstate a b c d e) cl_call |
---|
12 | | rtla_ret : ∀a,b,c,d. RTLabs_classify (Returnstate a b c d) cl_return |
---|
13 | . |
---|
14 | |
---|
15 | inductive RTLabs_stmt_cost : statement → Prop ≝ |
---|
16 | | stmt_cost : ∀c,l. RTLabs_stmt_cost (St_cost c l). |
---|
17 | |
---|
18 | inductive RTLabs_cost : state → Prop ≝ |
---|
19 | | cost_instr : ∀f,fs,m. |
---|
20 | RTLabs_stmt_cost (lookup_present ?? (f_graph (func f)) (next f) (next_ok f)) → |
---|
21 | RTLabs_cost (State f fs m). |
---|
22 | |
---|
23 | definition RTLabs_status : genv → abstract_status ≝ |
---|
24 | λge. |
---|
25 | mk_abstract_status |
---|
26 | state |
---|
27 | (λs,s'. ∃t. eval_statement ge s = Value ??? 〈t,s'〉) |
---|
28 | RTLabs_classify |
---|
29 | RTLabs_cost |
---|
30 | (λs,s'. match s with |
---|
31 | [ dp s p ⇒ |
---|
32 | match s return λs. RTLabs_classify s cl_call → ? with |
---|
33 | [ Callstate fd args dst stk m ⇒ |
---|
34 | λ_. match s' with |
---|
35 | [ State f fs m ⇒ match stk with [ nil ⇒ False | cons h t ⇒ next h = next f ] |
---|
36 | | _ ⇒ False |
---|
37 | ] |
---|
38 | | State f fs m ⇒ λH.⊥ |
---|
39 | | _ ⇒ λH.⊥ |
---|
40 | ] p |
---|
41 | ]). |
---|
42 | inversion H try #a try #b try #c try #d try #e try #f destruct |
---|
43 | qed. |
---|
44 | |
---|
45 | (* Before attempting to construct a structured trace, let's show that we can |
---|
46 | form flat traces with evidence that they were constructed from an execution. |
---|
47 | |
---|
48 | For now we don't consider I/O. *) |
---|
49 | |
---|
50 | |
---|
51 | coinductive exec_no_io (o:Type[0]) (i:o → Type[0]) : execution state o i → Prop ≝ |
---|
52 | | noio_stop : ∀a,b,c. exec_no_io o i (e_stop … a b c) |
---|
53 | | noio_step : ∀a,b,e. exec_no_io o i e → exec_no_io o i (e_step … a b e) |
---|
54 | | noio_wrong : ∀m. exec_no_io o i (e_wrong … m). |
---|
55 | |
---|
56 | (* add I/O? *) |
---|
57 | coinductive flat_trace (o:Type[0]) (i:o → Type[0]) (ge:genv) : state → Type[0] ≝ |
---|
58 | | ft_stop : ∀s. RTLabs_is_final s ≠ None ? → flat_trace o i ge s |
---|
59 | | ft_step : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → flat_trace o i ge s' → flat_trace o i ge s |
---|
60 | | ft_wrong : ∀s,m. eval_statement ge s = Wrong ??? m → flat_trace o i ge s. |
---|
61 | |
---|
62 | let corec make_flat_trace ge s |
---|
63 | (H:exec_no_io … (exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s))) : |
---|
64 | flat_trace io_out io_in ge s ≝ |
---|
65 | let e ≝ exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s) in |
---|
66 | match e return λx. e = x → ? with |
---|
67 | [ e_stop tr i s' ⇒ λE. ft_step … s tr s' ? (ft_stop … s' ?) |
---|
68 | | e_step tr s' e' ⇒ λE. ft_step … s tr s' ? (make_flat_trace ge s' ?) |
---|
69 | | e_wrong m ⇒ λE. ft_wrong … s m ? |
---|
70 | | e_interact o f ⇒ λE. ⊥ |
---|
71 | ] (refl ? e). |
---|
72 | [ 1,2: whd in E:(??%?); >exec_inf_aux_unfold in E; |
---|
73 | cases (eval_statement ge s) |
---|
74 | [ 1,4: #O #K whd in ⊢ (??%? → ?); #E destruct |
---|
75 | | 2,5: * #tr #s1 whd in ⊢ (??%? → ?); |
---|
76 | >(?:is_final ????? = RTLabs_is_final s1) // |
---|
77 | lapply (refl ? (RTLabs_is_final s1)) |
---|
78 | cases (RTLabs_is_final s1) in ⊢ (???% → %); |
---|
79 | [ 1,3: #_ whd in ⊢ (??%? → ?); #E destruct |
---|
80 | | #i #_ whd in ⊢ (??%? → ?); #E destruct /2/ @refl |
---|
81 | | #i #E whd in ⊢ (??%? → ?); #E2 destruct >E % #E' destruct |
---|
82 | ] |
---|
83 | | *: #m whd in ⊢ (??%? → ?); #E destruct |
---|
84 | ] |
---|
85 | | whd in E:(??%?); >exec_inf_aux_unfold in E; |
---|
86 | cases (eval_statement ge s) |
---|
87 | [ #O #K whd in ⊢ (??%? → ?); #E destruct |
---|
88 | | * #tr #s1 whd in ⊢ (??%? → ?); |
---|
89 | cases (is_final ?????) |
---|
90 | [ whd in ⊢ (??%? → ?); #E destruct @refl |
---|
91 | | #i whd in ⊢ (??%? → ?); #E destruct |
---|
92 | ] |
---|
93 | | #m whd in ⊢ (??%? → ?); #E destruct |
---|
94 | ] |
---|
95 | | whd in E:(??%?); >E in H; #H >exec_inf_aux_unfold in E; |
---|
96 | cases (eval_statement ge s) |
---|
97 | [ #O #K whd in ⊢ (??%? → ?); #E destruct |
---|
98 | | * #tr #s1 whd in ⊢ (??%? → ?); |
---|
99 | cases (is_final ?????) |
---|
100 | [ whd in ⊢ (??%? → ?); #E |
---|
101 | change with (eval_statement ge s1) in E:(??(??????(?????%))?); |
---|
102 | destruct |
---|
103 | inversion H |
---|
104 | [ #a #b #c #E1 destruct |
---|
105 | | #trx #sx #ex #H1 #E2 #E3 destruct @H1 |
---|
106 | | #m #E1 destruct |
---|
107 | ] |
---|
108 | | #i whd in ⊢ (??%? → ?); #E destruct |
---|
109 | ] |
---|
110 | | #m whd in ⊢ (??%? → ?); #E destruct |
---|
111 | ] |
---|
112 | | whd in E:(??%?); >exec_inf_aux_unfold in E; |
---|
113 | cases (eval_statement ge s) |
---|
114 | [ #O #K whd in ⊢ (??%? → ?); #E destruct |
---|
115 | | * #tr1 #s1 whd in ⊢ (??%? → ?); |
---|
116 | cases (is_final ?????) |
---|
117 | [ whd in ⊢ (??%? → ?); #E destruct |
---|
118 | | #i whd in ⊢ (??%? → ?); #E destruct |
---|
119 | ] |
---|
120 | | #m whd in ⊢ (??%? → ?); #E destruct @refl |
---|
121 | ] |
---|
122 | | whd in E:(??%?); >E in H; #H |
---|
123 | inversion H |
---|
124 | [ #a #b #c #E destruct |
---|
125 | | #a #b #c #d #E1 destruct |
---|
126 | | #m #E1 destruct |
---|
127 | ] |
---|
128 | ] qed. |
---|
129 | |
---|
130 | let corec make_whole_flat_trace p s |
---|
131 | (H:exec_no_io … (exec_inf … RTLabs_fullexec p)) |
---|
132 | (I:make_initial_state ??? p = OK ? s) : |
---|
133 | flat_trace io_out io_in (make_global … RTLabs_fullexec p) s ≝ |
---|
134 | let ge ≝ make_global … p in |
---|
135 | let e ≝ exec_inf_aux ?? RTLabs_fullexec ge (Value … 〈E0, s〉) in |
---|
136 | match e return λx. e = x → ? with |
---|
137 | [ e_stop tr i s' ⇒ λE. ft_stop ?? ge s ? |
---|
138 | | e_step _ _ e' ⇒ λE. make_flat_trace ge s ? |
---|
139 | | e_wrong m ⇒ λE. ⊥ |
---|
140 | | e_interact o f ⇒ λE. ⊥ |
---|
141 | ] (refl ? e). |
---|
142 | [ whd in E:(??%?); >exec_inf_aux_unfold in E; |
---|
143 | whd in ⊢ (??%? → ?); |
---|
144 | >(?:is_final ????? = RTLabs_is_final s) // |
---|
145 | lapply (refl ? (RTLabs_is_final s)) |
---|
146 | cases (RTLabs_is_final s) in ⊢ (???% → %); |
---|
147 | [ #_ whd in ⊢ (??%? → ?); #E destruct |
---|
148 | | #i #E whd in ⊢ (??%? → ?); #E2 % #E3 destruct |
---|
149 | ] |
---|
150 | | whd in H:(???%); >I in H; whd in ⊢ (???% → ?); whd in E:(??%?); |
---|
151 | >exec_inf_aux_unfold in E ⊢ %; whd in ⊢ (??%? → ???% → ?); cases (is_final ?????) |
---|
152 | [ whd in ⊢ (??%? → ???% → ?); #E #H inversion H |
---|
153 | [ #a #b #c #E1 destruct |
---|
154 | | #tr1 #s1 #e1 #H1 #E1 #E2 -E2 -I destruct (E1) |
---|
155 | @H1 |
---|
156 | | #m #E1 destruct |
---|
157 | ] |
---|
158 | | #i whd in ⊢ (??%? → ???% → ?); #E destruct |
---|
159 | ] |
---|
160 | | whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?); |
---|
161 | cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct |
---|
162 | | whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?); |
---|
163 | cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct |
---|
164 | ] qed. |
---|
165 | |
---|