- Timestamp:
- Nov 25, 2011, 6:17:13 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/CostsProof.ma
r1564 r1567 222 222 include alias "arithmetics/nat.ma". 223 223 224 (* Useless now?224 (* 225 225 lemma minus_m_n_minus_minus_plus_1: 226 226 ∀m, n: nat. … … 229 229 /3 by lt_plus_to_minus_r, plus_minus/ 230 230 qed. 231 *) 231 232 232 233 lemma plus_minus_rearrangement_1: … … 245 246 (m - n) + (n - o) = m - o. 246 247 /2 by plus_minus_rearrangement_1/ 247 qed.*) 248 249 (* 248 qed. 249 250 axiom current_instruction_cost_non_zero: 251 ∀s: Status. 252 current_instruction_cost s > 0. 253 254 axiom minus_m_n_gt_o_0_le_n_m: 255 ∀m, n, o. 256 m - n = o → o > 0 → n ≤ m. 257 250 258 let rec compute_max_trace_label_label_cost_is_ok 251 (cost_labels: BitVectorTrie Byte16)259 (cost_labels: BitVectorTrie costlabel 16) 252 260 (trace_ends_flag: trace_ends_with_ret) 253 261 (start_status: Status) (final_status: Status) 254 262 (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag 255 263 start_status final_status) on the_trace: 256 compute_max_trace_label_label_cost cost_labels trace_ends_flag start_status final_status the_trace =257 (clock … final_status) - (clock … start_status) ≝ ?264 And (compute_max_trace_label_label_cost cost_labels trace_ends_flag start_status final_status the_trace = 265 (clock … final_status) - (clock … start_status)) (clock … start_status ≤ clock … final_status) ≝ ? 258 266 and compute_max_trace_any_label_cost_is_ok 259 (cost_labels: BitVectorTrie Byte16)267 (cost_labels: BitVectorTrie costlabel 16) 260 268 (trace_ends_flag: trace_ends_with_ret) 261 269 (start_status: Status) (final_status: Status) 262 270 (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status) 263 271 on the_trace: 264 compute_max_trace_any_label_cost cost_labels trace_ends_flag start_status final_status the_trace =265 (clock … final_status) - (clock … start_status) ≝ ?272 (compute_max_trace_any_label_cost cost_labels trace_ends_flag start_status final_status the_trace = 273 (clock … final_status) - (clock … start_status)) ∧ (clock … start_status ≤ clock … final_status) ≝ ? 266 274 and compute_max_trace_label_return_cost_is_ok 267 (cost_labels: BitVectorTrie Byte16)275 (cost_labels: BitVectorTrie costlabel 16) 268 276 (start_status: Status) (final_status: Status) 269 277 (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status) 270 278 on the_trace: 271 compute_max_trace_label_return_cost cost_labels start_status final_status the_trace =272 (clock … final_status) - (clock … start_status) ≝ ?.279 (compute_max_trace_label_return_cost cost_labels start_status final_status the_trace = 280 (clock … final_status) - (clock … start_status)) ∧ (clock … start_status ≤ clock … final_status) ≝ ?. 273 281 [1: 274 282 cases the_trace … … 276 284 normalize @compute_max_trace_any_label_cost_is_ok 277 285 |2: 286 cases the_trace 287 [1: 288 #start_status #final_status #is_next #is_not_return #is_costed 289 change with (current_instruction_cost start_status) in ⊢ (?(??%?)?); 290 cases(is_next) 291 @conj 292 [1: 293 cases(execute_1 start_status) 294 #the_status #assm 295 whd in match eject; normalize nodelta 296 >assm % 297 |2: 298 cases(execute_1 start_status) 299 #the_status #assm 300 whd in match eject; normalize nodelta 301 @(minus_m_n_gt_o_0_le_n_m ? ? (current_instruction_cost start_status)) 302 [1: assumption 303 |2: @current_instruction_cost_non_zero 304 ] 305 ] 306 |2: 307 #start_status #final_status #is_next #is_return 308 change with (current_instruction_cost start_status) in ⊢ (?(??%?)?); 309 cases(is_next) 310 @conj 311 [1: 312 cases(execute_1 start_status) 313 #the_status #assm 314 whd in match eject; normalize nodelta 315 >assm % 316 |2: 317 cases(execute_1 start_status) 318 #the_status #assm 319 whd in match eject; normalize nodelta 320 @(minus_m_n_gt_o_0_le_n_m ? ? (current_instruction_cost start_status)) 321 [1: assumption 322 |2: @current_instruction_cost_non_zero 323 ] 324 ] 325 |3: 326 #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call 327 #status_final #is_next #is_call #is_after_return #call_trace #final_trace 328 change with ( 329 let current_instruction_cost ≝ current_instruction_cost status_pre_fun_call in 330 let call_trace_cost ≝ compute_max_trace_label_return_cost … call_trace in 331 let final_trace_cost ≝ compute_max_trace_any_label_cost cost_labels end_flag … final_trace in 332 call_trace_cost + current_instruction_cost + final_trace_cost) in ⊢ (?(??%?)?); 333 normalize nodelta; 334 @conj 335 [1: 336 cases(compute_max_trace_label_return_cost_is_ok cost_labels status_start_fun_call 337 status_after_fun_call call_trace) 338 #trace_label_return_eq #trace_label_return_le 339 cases(compute_max_trace_any_label_cost_is_ok cost_labels end_flag status_after_fun_call 340 status_final final_trace) 341 #trace_any_label_eq #trace_any_label_le 342 >trace_label_return_eq >trace_any_label_eq 343 cases daemon (* XXX: complete me *) 344 |2: 345 cases daemon (* XXX: complete me *) 346 ] 347 |4: 348 #end_flag #status_pre #status_init #status_end #is_next 349 #trace_any_label #is_other #is_not_costed 350 cases daemon (* XXX: complete me *) 351 ] 278 352 |3: 279 353 cases the_trace … … 283 357 |2: 284 358 #status_initial #status_labelled #status_final #labelled_trace #ret_trace 285 normalize >compute_max_trace_label_label_cost_is_ok 286 >compute_max_trace_label_return_cost_is_ok 359 normalize 360 cases(compute_max_trace_label_label_cost_is_ok cost_labels doesnt_end_with_ret status_initial status_labelled labelled_trace); 361 #label_label_trace_equality #label_label_trace_leq 362 cases(compute_max_trace_label_return_cost_is_ok cost_labels status_labelled status_final ret_trace); 363 #label_return_trace_equality #label_return_trace_leq 364 >label_label_trace_equality >label_return_trace_equality 365 @conj 366 [2: @(transitive_le (clock (BitVectorTrie (Vector bool 8) 16) status_initial) 367 (clock (BitVectorTrie Byte 16) status_labelled) 368 (clock (BitVectorTrie (Vector bool 8) 16) status_final)) 369 |1: @plus_minus_rearrangement_1 370 ] 371 assumption 287 372 ] 288 ] .289 *) 373 ] 374 qed. 290 375 291 376 (* XXX: work below here: *)
Note: See TracChangeset
for help on using the changeset viewer.