1 | include "RTLabs/RTLabs_semantics.ma". |
---|
2 | |
---|
3 | (* Avoid aliasing in interstage proofs *) |
---|
4 | |
---|
5 | definition RTLabs_state ≝ state. |
---|
6 | definition RTLabs_genv ≝ genv. |
---|
7 | |
---|
8 | (* Build a full abstract status record that can be used with structured traces. *) |
---|
9 | |
---|
10 | include "common/StructuredTraces.ma". |
---|
11 | include "RTLabs/CostSpec.ma". (* TODO: relocate definitions? *) |
---|
12 | include "utilities/deqsets.ma". |
---|
13 | discriminator status_class. |
---|
14 | |
---|
15 | (* We augment states with a stack of function blocks (i.e. pointers) so that we |
---|
16 | can make sensible "program counters" for the abstract state definition, along |
---|
17 | with a proof that we will get the correct code when we do the lookup (which |
---|
18 | is done to find cost labels given a pc). |
---|
19 | |
---|
20 | Adding them to the semantics is an alternative, more direct approach. |
---|
21 | However, it makes animating the semantics extremely difficult, because it |
---|
22 | is hard to avoid normalising and displaying irrelevant parts of the global |
---|
23 | environment and proofs. |
---|
24 | |
---|
25 | We use blocks rather than identifiers because the global environments go |
---|
26 | |
---|
27 | identifier → block → definition |
---|
28 | |
---|
29 | and we'd have to introduce backwards lookups to find identifiers for |
---|
30 | function pointers. |
---|
31 | *) |
---|
32 | |
---|
33 | definition Ras_Fn_Match ≝ |
---|
34 | λge,state,fn_stack. |
---|
35 | match state with |
---|
36 | [ State f fs m ⇒ All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) (f::fs) fn_stack |
---|
37 | | Callstate _ fd _ _ fs _ ⇒ |
---|
38 | match fn_stack with |
---|
39 | [ nil ⇒ False |
---|
40 | | cons h t ⇒ find_funct_ptr ? ge h = Some ? fd ∧ |
---|
41 | All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) fs t |
---|
42 | ] |
---|
43 | | Returnstate _ _ fs _ ⇒ |
---|
44 | All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) fs fn_stack |
---|
45 | | Finalstate _ ⇒ fn_stack = [ ] |
---|
46 | ]. |
---|
47 | |
---|
48 | record RTLabs_ext_state (ge:genv) : Type[0] ≝ { |
---|
49 | Ras_state :> state; |
---|
50 | Ras_fn_stack : list block; |
---|
51 | Ras_fn_match : Ras_Fn_Match ge Ras_state Ras_fn_stack |
---|
52 | }. |
---|
53 | |
---|
54 | (* Given a plain step of the RTLabs semantics, give the next state along with |
---|
55 | the shadow stack of function block numbers. Carefully defined so that the |
---|
56 | coercion back to the plain state always reduces. *) |
---|
57 | definition next_state : ∀ge. ∀s:RTLabs_ext_state ge. ∀s':state. ∀t. |
---|
58 | eval_statement ge s = Value ??? 〈t,s'〉 → RTLabs_ext_state ge ≝ |
---|
59 | λge,s,s',t,EX. mk_RTLabs_ext_state ge s' |
---|
60 | (match s' return λs'. eval_statement ge s = Value ??? 〈t,s'〉 → ? with [ State _ _ _ ⇒ λ_. Ras_fn_stack … s | Callstate _ _ _ _ _ _ ⇒ λEX. func_block_of_exec … EX::Ras_fn_stack … s | Returnstate _ _ _ _ ⇒ λ_. tail … (Ras_fn_stack … s) | Finalstate _ ⇒ λ_. [ ] ] EX) |
---|
61 | ?. |
---|
62 | cases s' in EX ⊢ %; |
---|
63 | [ -s' #f #fs #m cases s -s #s #stk #mtc #EX whd in ⊢ (???%); inversion (eval_preserves … EX) |
---|
64 | [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct |
---|
65 | whd cases stk in mtc ⊢ %; [ * ] |
---|
66 | #hd #tl * #M1 #M2 % [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct // |
---|
67 | | @M2 ] |
---|
68 | | #ge' #f1 #fs1 #m1 #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #E4 destruct |
---|
69 | | #ge' #vf #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct |
---|
70 | whd cases stk in mtc ⊢ %; [ * ] |
---|
71 | #hd #tl #H @H |
---|
72 | | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 destruct |
---|
73 | | #ge' #f0 #fs0 #rtv #dst #f' #m0 #N #F #E1 #E2 #E3 #E4 destruct |
---|
74 | cases stk in mtc ⊢ %; [ * ] #hd #tl * #M1 #M2 % |
---|
75 | [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct // | @M2 ] |
---|
76 | | #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct |
---|
77 | ] |
---|
78 | | -s' #vf #fd #args #dst #fs #m #EX whd in ⊢ (???%); cases (func_block_of_exec … EX) #func_block #FFP |
---|
79 | whd % // -func_block cases s in EX ⊢ %; -s #s #stk #mtc #EX inversion (eval_preserves … EX) |
---|
80 | [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct |
---|
81 | | #ge' #vf1 #f1 #fs1 #m1 #fd' #args' #f' #dst' #F #b #FFP #E1 #E2 #E3 #E4 destruct |
---|
82 | cases stk in mtc; [ * ] #b1 #bs * #M1 #M2 % |
---|
83 | [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct // | @M2 ] |
---|
84 | | #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct |
---|
85 | | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 destruct |
---|
86 | | #ge' #f0 #fs0 #rtv #dst #f' #m0 #F #E1 #E2 #E3 #E4 destruct |
---|
87 | | #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct |
---|
88 | ] |
---|
89 | | -s' #rtv #dst #fs #m #EX whd in ⊢ (???%); cases s in EX ⊢ %; -s #s #stk #mtc #EX inversion (eval_preserves … EX) |
---|
90 | [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct |
---|
91 | | #ge' #f1 #fs1 #m1 #fd' #args' #f' #dst' #F #b #FFP #E1 #E2 #E3 #E4 destruct |
---|
92 | | #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct |
---|
93 | | #ge' #f #fs' #m' #rtv' #dst' #m' #E1 #E2 #E3 #E4 destruct |
---|
94 | cases stk in mtc ⊢ %; [ * ] #b #bs * #_ #H @H |
---|
95 | | #ge' #f0 #fs0 #rtv #dst #f' #m0 #F #E1 #E2 #E3 #E4 destruct |
---|
96 | | #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct |
---|
97 | ] |
---|
98 | | #r #EX whd @refl |
---|
99 | ] qed. |
---|
100 | |
---|
101 | |
---|
102 | (* NB: For RTLabs we only classify branching behaviour as jumps. Other jumps |
---|
103 | will be added later (LTL → LIN). *) |
---|
104 | |
---|
105 | definition RTLabs_classify : state → status_class ≝ |
---|
106 | λs. match s with |
---|
107 | [ State f _ _ ⇒ |
---|
108 | match next_instruction f with |
---|
109 | [ St_cond _ _ _ ⇒ cl_jump |
---|
110 | (* | St_jumptable _ _ ⇒ cl_jump*) |
---|
111 | | _ ⇒ cl_other |
---|
112 | ] |
---|
113 | | Callstate _ _ _ _ _ _ ⇒ cl_call |
---|
114 | | Returnstate _ _ _ _ ⇒ cl_return |
---|
115 | | Finalstate _ ⇒ cl_other |
---|
116 | ]. |
---|
117 | |
---|
118 | (* As with is_cost_label/cost_label_of we define a boolean function as well |
---|
119 | as one which extracts the cost label so that we can use it in hypotheses |
---|
120 | without naming the cost label. *) |
---|
121 | |
---|
122 | definition RTLabs_cost : state → bool ≝ |
---|
123 | λs. match s with |
---|
124 | [ State f fs m ⇒ |
---|
125 | is_cost_label (next_instruction f) |
---|
126 | | _ ⇒ false |
---|
127 | ]. |
---|
128 | |
---|
129 | definition RTLabs_cost_label : state → option costlabel ≝ |
---|
130 | λs. match s with |
---|
131 | [ State f fs m ⇒ |
---|
132 | cost_label_of (next_instruction f) |
---|
133 | | _ ⇒ None ? |
---|
134 | ]. |
---|
135 | |
---|
136 | (* "Program counters" need to identify the current state, either as a pair of |
---|
137 | the function and current instruction, or the function being entered or |
---|
138 | left. Functions are identified by their function pointer block because |
---|
139 | this avoids introducing functions to map back pointers to function ids using |
---|
140 | the global environment. (See the comment at the start of this file, too.) |
---|
141 | |
---|
142 | Calls also get the caller's instruction label (or None for the initial call) |
---|
143 | so that we can distinguish different calls. This is used only for the |
---|
144 | t.*_unrepeating property, which includes the pc for call states. |
---|
145 | *) |
---|
146 | |
---|
147 | inductive RTLabs_pc : Type[0] ≝ |
---|
148 | | rapc_state : block → label → RTLabs_pc |
---|
149 | | rapc_call : option label → block → RTLabs_pc |
---|
150 | | rapc_ret : option block → RTLabs_pc |
---|
151 | | rapc_fin : RTLabs_pc |
---|
152 | . |
---|
153 | |
---|
154 | definition RTLabs_pc_eq : RTLabs_pc → RTLabs_pc → bool ≝ |
---|
155 | λx,y. match x with |
---|
156 | [ rapc_state b1 l1 ⇒ match y with [ rapc_state b2 l2 ⇒ eq_block b1 b2 ∧ eq_identifier … l1 l2 | _ ⇒ false ] |
---|
157 | | rapc_call o1 b1 ⇒ match y with [ rapc_call o2 b2 ⇒ |
---|
158 | eqb ? o1 o2 |
---|
159 | ∧ eq_block b1 b2 |
---|
160 | | _ ⇒ false ] |
---|
161 | | rapc_ret b1 ⇒ match y with [ rapc_ret b2 ⇒ eqb ? b1 b2 | _ ⇒ false ] |
---|
162 | | rapc_fin ⇒ match y with [ rapc_fin ⇒ true | _ ⇒ false ] |
---|
163 | ]. |
---|
164 | |
---|
165 | definition RTLabs_deqset : DeqSet ≝ mk_DeqSet RTLabs_pc RTLabs_pc_eq ?. |
---|
166 | whd in match RTLabs_pc_eq; |
---|
167 | * [ #b1 #l1 | #bl1 #b1 | #ob1 | ] |
---|
168 | * [ 1,5,9,13: #b2 #l2 | 2,6,10,14: #bl2 #b2 | 3,7,11,15: #ob2 | *: ] |
---|
169 | normalize nodelta |
---|
170 | [ @eq_block_elim [ #E destruct | * #NE ] ] |
---|
171 | [ @eq_identifier_elim [ #E destruct | *: * #NE ] ] |
---|
172 | [ 8,13: @eqb_elim [ 1,3: #E destruct | *: * #NE ] ] |
---|
173 | [ @eq_block_elim [ #E destruct | * #NE ] ] |
---|
174 | normalize % #E destruct try (cases (NE (refl ??))) @refl |
---|
175 | qed. |
---|
176 | |
---|
177 | definition RTLabs_ext_state_to_pc : ∀ge. RTLabs_ext_state ge → RTLabs_deqset ≝ |
---|
178 | λge,s. match s with [ mk_RTLabs_ext_state s' stk mtc0 ⇒ |
---|
179 | match s' return λs'. Ras_Fn_Match ? s' ? → ? with |
---|
180 | [ State f fs m ⇒ match stk return λstk. Ras_Fn_Match ?? stk → ? with [ nil ⇒ λmtc. ⊥ | cons b _ ⇒ λ_. rapc_state b (next … f) ] |
---|
181 | | Callstate _ _ _ _ fs _ ⇒ match stk return λstk. Ras_Fn_Match ?? stk → ? with [ nil ⇒ λmtc. ⊥ | cons b _ ⇒ λ_. rapc_call (match fs with [ nil ⇒ None ? | cons f _ ⇒ Some ? (next f) ]) b ] |
---|
182 | | Returnstate _ _ _ _ ⇒ match stk with [ nil ⇒ λ_. rapc_ret (None ?) | cons b _ ⇒ λ_. rapc_ret (Some ? b) ] |
---|
183 | | Finalstate _ ⇒ λmtc. rapc_fin |
---|
184 | ] mtc0 ]. |
---|
185 | whd in mtc; cases mtc |
---|
186 | qed. |
---|
187 | |
---|
188 | definition RTLabs_pc_to_cost_label : ∀ge. RTLabs_pc → option costlabel ≝ |
---|
189 | λge,pc. |
---|
190 | match pc with |
---|
191 | [ rapc_state b l ⇒ |
---|
192 | match find_funct_ptr … ge b with [ None ⇒ None ? | Some fd ⇒ |
---|
193 | match fd with [ Internal f ⇒ match lookup ?? (f_graph f) l with [ Some s ⇒ cost_label_of s | _ ⇒ None ? ] | _ ⇒ None ? ] ] |
---|
194 | | _ ⇒ None ? |
---|
195 | ]. |
---|
196 | |
---|
197 | (* After returning from a function, we should be ready to execute the next |
---|
198 | instruction of the caller and the shadow stack should be preserved (we have |
---|
199 | to take the top element off because the Callstate includes the callee); *or* |
---|
200 | we're in the final state. |
---|
201 | *) |
---|
202 | |
---|
203 | definition RTLabs_after_return : ∀ge. (Σs:RTLabs_ext_state ge. Some ? (RTLabs_classify s) = Some ? cl_call) → RTLabs_ext_state ge → Prop ≝ |
---|
204 | λge,s,s'. |
---|
205 | match s with |
---|
206 | [ mk_Sig s p ⇒ |
---|
207 | match s return λs. Some ? (RTLabs_classify s) = Some ? cl_call → ? with |
---|
208 | [ Callstate _ fd args dst stk m ⇒ |
---|
209 | λ_. match s' with |
---|
210 | [ State f fs m ⇒ match stk with [ nil ⇒ False | cons h t ⇒ |
---|
211 | next h = next f ∧ |
---|
212 | f_graph (func h) = f_graph (func f) ∧ |
---|
213 | match Ras_fn_stack … s with [ nil ⇒ False | cons _ stk' ⇒ stk' = Ras_fn_stack … s' ] ] |
---|
214 | | Finalstate r ⇒ stk = [ ] |
---|
215 | | _ ⇒ False |
---|
216 | ] |
---|
217 | | State f fs m ⇒ λH.⊥ |
---|
218 | | _ ⇒ λH.⊥ |
---|
219 | ] p |
---|
220 | ]. |
---|
221 | [ whd in H:(??(??%)?); |
---|
222 | cases (next_instruction f) in H; |
---|
223 | normalize try #a try #b try #c try #d try #e try #g try #h try #i try #j destruct |
---|
224 | | normalize in H; destruct |
---|
225 | | normalize in H; destruct |
---|
226 | ] qed. |
---|
227 | |
---|
228 | definition RTLabs_call_ident : ∀ge. (Σs:RTLabs_ext_state ge. Some ? (RTLabs_classify s) = Some ? cl_call) → ident ≝ |
---|
229 | λge,s. |
---|
230 | match s with |
---|
231 | [ mk_Sig s p ⇒ |
---|
232 | match s return λs':RTLabs_ext_state ge. Some ? (RTLabs_classify s') = Some ? cl_call → ident with |
---|
233 | [ mk_RTLabs_ext_state s' stk mtc0 ⇒ |
---|
234 | match s' return λs'. Ras_Fn_Match ? s' ? → Some ? (RTLabs_classify s') = Some ? cl_call → ident with |
---|
235 | [ Callstate _ fd _ _ _ _ ⇒ |
---|
236 | match stk return λstk. Ras_Fn_Match ?? stk → ? → ident with |
---|
237 | [ nil ⇒ λmtc. ⊥ |
---|
238 | | cons b _ ⇒ λmtc. λX. symbol_of_function_block … ge b ? |
---|
239 | ] |
---|
240 | | State f _ _ ⇒ λ_. λH.⊥ |
---|
241 | | _ ⇒ λ_. λH.⊥ |
---|
242 | ] mtc0 |
---|
243 | ] p |
---|
244 | ]. |
---|
245 | [ whd in H:(??(??%)?); |
---|
246 | cases (next_instruction f) in H; |
---|
247 | normalize try #a try #b try #c try #d try #e try #g try #h try #i try #j destruct |
---|
248 | | 4,5: normalize in H; destruct (H) |
---|
249 | | cases mtc |
---|
250 | | cases mtc #FFP #_ >FFP % #E destruct (E) |
---|
251 | ] qed. |
---|
252 | |
---|
253 | lemma RTLabs_notail : ∀s. |
---|
254 | RTLabs_classify s = cl_tailcall → |
---|
255 | False. |
---|
256 | * [ #f #fs #m whd in ⊢ (??%? → ?); cases (next_instruction f) ] |
---|
257 | normalize |
---|
258 | #a try #b try #c try #d try #e try #g try #h try #i try #j destruct |
---|
259 | qed. |
---|
260 | |
---|
261 | (* Roughly corresponding to as_classifier *) |
---|
262 | lemma RTLabs_notail' : ∀s. |
---|
263 | Some ? (RTLabs_classify s) = Some ? cl_tailcall → |
---|
264 | False. |
---|
265 | #s #E @(RTLabs_notail … s) |
---|
266 | generalize in match (RTLabs_classify s) in E ⊢ %; |
---|
267 | #c #E' destruct % |
---|
268 | qed. |
---|
269 | |
---|
270 | definition RTLabs_status : genv → abstract_status ≝ |
---|
271 | λge. |
---|
272 | mk_abstract_status |
---|
273 | (RTLabs_ext_state ge) |
---|
274 | (λs,s'. ∃t,EX. next_state ge s s' t EX = s') |
---|
275 | RTLabs_deqset |
---|
276 | (RTLabs_ext_state_to_pc ge) |
---|
277 | (λs. Some ? (RTLabs_classify s)) |
---|
278 | (RTLabs_pc_to_cost_label ge) |
---|
279 | (RTLabs_after_return ge) |
---|
280 | (λs. RTLabs_is_final s ≠ None ?) |
---|
281 | (RTLabs_call_ident ge) |
---|
282 | (λs. ⊥). |
---|
283 | (* No tailcalls here for now. *) |
---|
284 | cases s @RTLabs_notail' |
---|
285 | qed. |
---|
286 | |
---|
287 | (* Allow us to move between the different notions of when a state is cost |
---|
288 | labelled. *) |
---|
289 | |
---|
290 | lemma RTLabs_costed : ∀ge. ∀s:RTLabs_ext_state ge. |
---|
291 | RTLabs_cost s = true ↔ |
---|
292 | as_costed (RTLabs_status ge) s. |
---|
293 | cut (None (identifier CostTag) ≠ None ? → False) [ * /2/ ] #NONE |
---|
294 | #ge * * |
---|
295 | [ * #func #locals #next #nok #sp #r #fs #m #stk #mtc |
---|
296 | whd in ⊢ (??%); whd in ⊢ (??(?(??%?))); |
---|
297 | whd in match (as_pc_of ??); |
---|
298 | cases stk in mtc ⊢ %; [ * ] #func_block #stk' * #M1 #M2 |
---|
299 | whd in ⊢ (??(?(??%?))); >M1 whd in ⊢ (??(?(??%?))); |
---|
300 | whd in ⊢ (?(??%?)?); change with (lookup_present ?????) in match (next_instruction ?); |
---|
301 | >(lookup_lookup_present … nok) whd in ⊢ (?(??%?)(?(??%?))); |
---|
302 | % cases (lookup_present ?? (f_graph func) ??) normalize |
---|
303 | #A try #B try #C try #D try #E try #F try #G try #H try #G destruct |
---|
304 | try (% #E' destruct) |
---|
305 | cases (NONE ?) assumption |
---|
306 | | #vf #fd #args #dst #fs #m #stk #mtc % |
---|
307 | [ #E normalize in E; destruct |
---|
308 | | whd in ⊢ (% → ?); whd in ⊢ (?(??%?) → ?); whd in match (as_pc_of ??); |
---|
309 | cases stk in mtc ⊢ %; [*] #fblk #fblks #mtc whd in ⊢ (?(??%?) → ?); |
---|
310 | #H cases (NONE H) |
---|
311 | ] |
---|
312 | | #v #dst #fs #m #stk #mtc % |
---|
313 | [ #E normalize in E; destruct |
---|
314 | | whd in ⊢ (% → ?); whd in ⊢ (?(??%?) → ?); whd in match (as_pc_of ??); |
---|
315 | cases stk in mtc ⊢ %; [2: #fblk #fblks ] #mtc whd in ⊢ (?(??%?) → ?); |
---|
316 | #H cases (NONE H) |
---|
317 | ] |
---|
318 | | #r #stk #mtc % |
---|
319 | [ #E normalize in E; destruct |
---|
320 | | #E normalize in E; cases (NONE E) |
---|
321 | ] |
---|
322 | ] qed. |
---|
323 | |
---|
324 | lemma RTLabs_not_cost : ∀ge. ∀s:RTLabs_ext_state ge. |
---|
325 | RTLabs_cost s = false → |
---|
326 | ¬ as_costed (RTLabs_status ge) s. |
---|
327 | #ge #s #E % #C >(proj2 … (RTLabs_costed ??)) in E; // #E destruct |
---|
328 | qed. |
---|