Changeset 1576
 Timestamp:
 Nov 29, 2011, 5:22:37 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CostsProof.ma
r1575 r1576 249 249 qed. 250 250 251 axiom c urrent_instruction_cost_non_zero:251 axiom clock_execute_1: 252 252 ∀s: Status. 253 c urrent_instruction_cost s > 0.254 255 lemma le_monotonic_plus:253 clock … (execute_1 s) = current_instruction_cost s + clock … s. 254 255 axiom plus_minus_minus: 256 256 ∀m, n, o: nat. 257 m ≤ n → m + o ≤ n + o. 258 #m #n #o #hyp /2/ 259 qed. 260 261 lemma le_plus_to_minus_l: 257 m  (n + o) = (m  n)  o. 258 259 axiom plus_le_le: 262 260 ∀m, n, o: nat. 263 n ≤ o → m ≤ o  n → m + n ≤ o. 264 #m #n #o #le_hyp #hyp 265 generalize in match (le_monotonic_plus m (o  n) n hyp); 266 generalize in match (plus_minus_m_m o n le_hyp); 267 #assm <assm in ⊢ (% → ?); #finished assumption 268 qed. 261 m + n ≤ o → n ≤ o. 269 262 270 axiom minus_m_n_gt_o_O_le_n_m:271 ∀m, n, o.272 m  n = o → o > 0 → n ≤ m.273 (* #m #n #o #eq_hyp <eq_hyp in ⊢ (% → ?);274 normalize in ⊢ (% → ?);275 >le_monot *)276 277 263 let rec compute_max_trace_label_label_cost_is_ok 278 264 (cost_labels: BitVectorTrie costlabel 16) … … 313 299 #the_status #assm 314 300 whd in match eject; normalize nodelta 315 >assm % 301 cases(assm) 302 #eq_hyp #le_hyp 303 >eq_hyp % 316 304 2: 317 305 cases(execute_1 start_status) 318 306 #the_status #assm 319 307 whd in match eject; normalize nodelta 320 @(minus_m_n_gt_o_O_le_n_m ? ? (current_instruction_cost start_status)) 321 [1: assumption 322 2: @(current_instruction_cost_non_zero start_status) 323 ] 308 cases(assm) 309 #eq_hyp #le_hyp 310 assumption 324 311 ] 325 312 2: … … 332 319 #the_status #assm 333 320 whd in match eject; normalize nodelta 334 >assm % 321 cases(assm) 322 #eq_hyp #le_hyp 323 >eq_hyp % 335 324 2: 336 325 cases(execute_1 start_status) 337 326 #the_status #assm 338 327 whd in match eject; normalize nodelta 339 @(minus_m_n_gt_o_O_le_n_m ? ? (current_instruction_cost start_status)) 340 [1: assumption 341 2: @current_instruction_cost_non_zero 342 ] 328 cases(assm) 329 #eq_hyp #le_hyp 330 assumption 343 331 ] 344 332 3: … … 360 348 #trace_any_label_eq #trace_any_label_le 361 349 >trace_label_return_eq >trace_any_label_eq 362 >commutative_plus 363 364 cut ((clock (BitVectorTrie Byte 16) status_after_fun_call 365 clock (BitVectorTrie Byte 16) status_start_fun_call 366 +current_instruction_cost status_pre_fun_call 367 +(clock (BitVectorTrie Byte 16) status_final 368 clock (BitVectorTrie Byte 16) status_after_fun_call) = 369 ((clock (BitVectorTrie Byte 16) status_after_fun_call 370  clock (BitVectorTrie Byte 16) status_start_fun_call) 371 + (clock (BitVectorTrie Byte 16) status_final 372  clock (BitVectorTrie Byte 16) status_after_fun_call)) 373 + current_instruction_cost status_pre_fun_call)) 374 [ 1: 375 cases daemon (* XXX: complete me *) 376  2: 377 #eq_hyp >eq_hyp 350 cases(is_next) 351 >(clock_execute_1 status_pre_fun_call) in match (clock … (execute_1 status_pre_fun_call)); 352 >commutative_plus in match ( 353 (current_instruction_cost status_pre_fun_call 354 + clock (BitVectorTrie Byte 16) status_pre_fun_call)); 355 >plus_minus_minus 356 <(plus_minus_m_m (clock (BitVectorTrie Byte 16) status_after_fun_call 357 clock (BitVectorTrie Byte 16) status_pre_fun_call) (current_instruction_cost status_pre_fun_call)) 358 [1: 378 359 >plus_minus_rearrangement_1 379 360 [1: 380 2, 3: 361 % 362 2: 381 363 assumption 364 3: 365 generalize in match trace_label_return_le; 366 cases(is_next) 367 >(clock_execute_1 status_pre_fun_call) 368 @plus_le_le 382 369 ] 370 2: 371 cases daemon (* XXX: todo *) 383 372 ] 384 373 2: 385 cases daemon (* XXX: complete me *) 374 cases(compute_max_trace_label_return_cost_is_ok cost_labels status_start_fun_call 375 status_after_fun_call call_trace) 376 #trace_label_return_eq cases(is_next) 377 >clock_execute_1 378 #trace_label_return_le 379 lapply (plus_le_le … trace_label_return_le) 380 #trace_label_return_le' 381 cases(compute_max_trace_any_label_cost_is_ok cost_labels end_flag status_after_fun_call 382 status_final final_trace) 383 #trace_any_label_eq #trace_any_label_le 384 @(transitive_le (clock … status_pre_fun_call) (clock … status_after_fun_call) (clock … status_final)) 385 assumption 386 386 ] 387 387 4: 388 388 #end_flag #status_pre #status_init #status_end #is_next 389 389 #trace_any_label #is_other #is_not_costed 390 cases daemon (* XXX: complete me *) 390 change with ( 391 let current_instruction_cost ≝ current_instruction_cost status_pre in 392 let tail_trace_cost ≝ 393 compute_max_trace_any_label_cost cost_labels end_flag 394 status_init status_end trace_any_label 395 in 396 current_instruction_cost + tail_trace_cost) in ⊢ (?(??%?)?); 397 normalize nodelta; 398 @conj 399 [1: 400 cases(compute_max_trace_any_label_cost_is_ok cost_labels end_flag 401 status_init status_end trace_any_label) 402 #trace_any_label_eq #trace_any_label_le 403 >trace_any_label_eq 404 cases(is_next) 405 >commutative_plus 406 >clock_execute_1 407 >commutative_plus in match ((current_instruction_cost status_pre+clock (BitVectorTrie Byte 16) status_pre)); 408 >plus_minus_minus 409 <plus_minus_m_m 410 [1: % 411 2: cases daemon (* XXX: todo *) 412 ] 413 2: 414 cases(compute_max_trace_any_label_cost_is_ok cost_labels end_flag 415 status_init status_end trace_any_label) 416 #trace_any_label_eq 417 cases(is_next) 418 >clock_execute_1 419 @plus_le_le 420 ] 391 421 ] 392 422 3:
Note: See TracChangeset
for help on using the changeset viewer.