Changeset 1581 for src/ASM/CostsProof.ma


Ignore:
Timestamp:
Dec 1, 2011, 3:15:15 PM (9 years ago)
Author:
mulligan
Message:

Dangling de Bruijn pointer when trying to propagate russell to set_arg_1

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1579 r1581  
    374374  ].
    375375qed.
    376    
    377 let rec compute_max_trace_label_label_cost_is_ok
    378   (cost_labels: BitVectorTrie costlabel 16)
    379    (trace_ends_flag: trace_ends_with_ret)
    380     (start_status: Status) (final_status: Status)
    381       (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
    382         start_status final_status) on the_trace:
    383           And (compute_max_trace_label_label_cost cost_labels trace_ends_flag start_status final_status the_trace =
    384             (clock … final_status) - (clock … start_status)) (clock … start_status ≤ clock … final_status) ≝ ?
    385 and compute_max_trace_any_label_cost_is_ok
    386   (cost_labels: BitVectorTrie costlabel 16)
    387   (trace_ends_flag: trace_ends_with_ret)
    388    (start_status: Status) (final_status: Status)
    389      (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
    390        on the_trace:
    391          (compute_max_trace_any_label_cost cost_labels trace_ends_flag start_status final_status the_trace =
    392            (clock … final_status) - (clock … start_status)) ∧ (clock … start_status ≤ clock … final_status) ≝ ?
    393 and compute_max_trace_label_return_cost_is_ok
    394   (cost_labels: BitVectorTrie costlabel 16)
    395   (start_status: Status) (final_status: Status)
    396     (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
    397       on the_trace:
    398         (compute_max_trace_label_return_cost cost_labels start_status final_status the_trace =
    399           (clock … final_status) - (clock … start_status)) ∧ (clock … start_status ≤ clock … final_status) ≝ ?.
    400   [1:
    401     cases the_trace
    402     #ends_flag #start_status #end_status #any_label_trace #is_costed
    403     normalize @compute_max_trace_any_label_cost_is_ok
    404   |2:
    405     cases the_trace
    406     [1:
    407       #start_status #final_status #is_next #is_not_return #is_costed
    408       change with (current_instruction_cost start_status) in ⊢ (?(??%?)?);
    409       cases(is_next)
    410       @conj
    411       cases(execute_1 start_status)
    412       #the_status #assm
    413       whd in match eject; normalize nodelta
    414       >assm
    415       [1:
    416         @minus_plus_m_m
    417       |2:
    418         @m_le_plus_n_m
    419       ]
    420     |2:
    421       #start_status #final_status #is_next #is_return
    422       change with (current_instruction_cost start_status) in ⊢ (?(??%?)?);
    423       cases(is_next)
    424       @conj
    425       cases(execute_1 start_status)
    426       #the_status #assm
    427       whd in match eject; normalize nodelta
    428       >assm
    429       [1:
    430         @minus_plus_m_m
    431       |2:
    432         @m_le_plus_n_m
    433       ]
    434     |3:
    435       #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
    436       #status_final #is_next #is_call #is_after_return #call_trace #final_trace
    437       change with (
    438       let current_instruction_cost ≝ current_instruction_cost status_pre_fun_call in
    439       let call_trace_cost ≝ compute_max_trace_label_return_cost … call_trace in
    440       let final_trace_cost ≝ compute_max_trace_any_label_cost cost_labels end_flag … final_trace in
    441         call_trace_cost + current_instruction_cost + final_trace_cost) in ⊢ (?(??%?)?);
    442       normalize nodelta;
    443       @conj
    444       [1:
    445         cases(compute_max_trace_label_return_cost_is_ok cost_labels status_start_fun_call
    446           status_after_fun_call call_trace)
    447         #trace_label_return_eq #trace_label_return_le
    448         cases(compute_max_trace_any_label_cost_is_ok cost_labels end_flag status_after_fun_call
    449           status_final final_trace)
    450         #trace_any_label_eq #trace_any_label_le
    451         >trace_any_label_eq >trace_label_return_eq
    452         cases(is_next)
    453         cases(execute_1 status_pre_fun_call)
    454         #the_status #assm
    455         whd in match eject; normalize nodelta;
    456         >assm >commutative_plus in match
    457           (current_instruction_cost status_pre_fun_call
    458             + clock (BitVectorTrie Byte 16) status_pre_fun_call);
    459         >m_minus_n_plus_o_m_minus_n_minus_o
    460         <(plus_minus_m_m
    461           (clock (BitVectorTrie Byte 16) status_after_fun_call
    462             - clock (BitVectorTrie Byte 16) status_pre_fun_call)
    463           (current_instruction_cost status_pre_fun_call))
    464         [1:
    465           @plus_minus_rearrangement_1
    466           lapply(transitive_le
    467             (clock … status_pre_fun_call)
    468             (clock … status_start_fun_call)
    469             (clock … status_after_fun_call) ? trace_label_return_le)
    470           [1,3:
    471             cases(is_next)
    472             cases(execute_1 status_pre_fun_call)
    473             whd in match eject; normalize nodelta;
    474             #the_new_status #assm >assm @m_le_plus_n_m
    475           |2,4:
    476             #assm assumption
    477           ]
    478         |2:
    479           cases(is_next)
    480           assumption
    481       |2:
    482         cases(compute_max_trace_label_return_cost_is_ok cost_labels status_start_fun_call
    483           status_after_fun_call call_trace)
    484         #trace_label_return_eq
    485         cases(compute_max_trace_any_label_cost_is_ok cost_labels end_flag status_after_fun_call
    486           status_final final_trace)
    487         #trace_any_label_eq cases(is_next)
    488         cases(execute_1 status_pre_fun_call)
    489         #the_status #assm
    490         whd in match eject; normalize nodelta;
    491         >assm #after_final_le #pre_after_le
    492         lapply(n_plus_m_le_o_to_m_le_o
    493           (clock … status_pre_fun_call)
    494           (current_instruction_cost status_pre_fun_call)
    495           (clock … status_after_fun_call) pre_after_le);
    496         #pre_after_le'
    497         @(transitive_le
    498           (clock … status_pre_fun_call)
    499           (clock … status_after_fun_call)
    500           (clock … status_final))
    501         assumption
    502       ]
    503     |*: cases daemon (* XXX: for now
    504       #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
    505       #status_final #is_next #is_call #is_after_return #call_trace #final_trace
    506       change with (
    507       let current_instruction_cost ≝ current_instruction_cost status_pre_fun_call in
    508       let call_trace_cost ≝ compute_max_trace_label_return_cost … call_trace in
    509       let final_trace_cost ≝ compute_max_trace_any_label_cost cost_labels end_flag … final_trace in
    510         call_trace_cost + current_instruction_cost + final_trace_cost) in ⊢ (?(??%?)?);
    511       normalize nodelta;
    512       @conj
    513       [1:
    514         cases(compute_max_trace_label_return_cost_is_ok cost_labels status_start_fun_call
    515           status_after_fun_call call_trace)
    516         #trace_label_return_eq #trace_label_return_le
    517         cases(compute_max_trace_any_label_cost_is_ok cost_labels end_flag status_after_fun_call
    518           status_final final_trace)
    519         #trace_any_label_eq #trace_any_label_le
    520         >trace_label_return_eq >trace_any_label_eq
    521         cases(is_next)
    522         >(clock_execute_1 status_pre_fun_call) in match (clock … (execute_1 status_pre_fun_call));
    523         >commutative_plus in match (
    524           (current_instruction_cost status_pre_fun_call
    525             + clock (BitVectorTrie Byte 16) status_pre_fun_call));
    526         <minus_plus
    527         <(plus_minus_m_m (clock (BitVectorTrie Byte 16) status_after_fun_call
    528   -clock (BitVectorTrie Byte 16) status_pre_fun_call) (current_instruction_cost status_pre_fun_call))
    529         [1:
    530           >plus_minus_rearrangement_1
    531           [1:
    532             %
    533           |2:
    534             assumption
    535           |3:
    536             generalize in match trace_label_return_le;
    537             cases(is_next)
    538             >(clock_execute_1 status_pre_fun_call)
    539             @plus_le_le
    540           ]
    541         |2:
    542           cases daemon (* XXX: todo *)
    543         ]
    544       |2:
    545         cases(compute_max_trace_label_return_cost_is_ok cost_labels status_start_fun_call
    546           status_after_fun_call call_trace)
    547         #trace_label_return_eq cases(is_next)
    548         >clock_execute_1
    549         #trace_label_return_le
    550         lapply (plus_le_le … trace_label_return_le)
    551         #trace_label_return_le'
    552         cases(compute_max_trace_any_label_cost_is_ok cost_labels end_flag status_after_fun_call
    553           status_final final_trace)
    554         #trace_any_label_eq #trace_any_label_le
    555         @(transitive_le (clock … status_pre_fun_call) (clock … status_after_fun_call) (clock … status_final))
    556         assumption
    557       ]
    558     |4:
    559       #end_flag #status_pre #status_init #status_end #is_next
    560       #trace_any_label #is_other #is_not_costed
    561       change with (
    562       let current_instruction_cost ≝ current_instruction_cost status_pre in
    563       let tail_trace_cost ≝
    564        compute_max_trace_any_label_cost cost_labels end_flag
    565         status_init status_end trace_any_label
    566       in
    567         current_instruction_cost + tail_trace_cost) in ⊢ (?(??%?)?);
    568       normalize nodelta;
    569       @conj
    570       [1:
    571         cases(compute_max_trace_any_label_cost_is_ok cost_labels end_flag
    572         status_init status_end trace_any_label)
    573         #trace_any_label_eq #trace_any_label_le
    574         >trace_any_label_eq
    575         cases(is_next)
    576         >commutative_plus
    577         >clock_execute_1
    578         >commutative_plus in match ((current_instruction_cost status_pre+clock (BitVectorTrie Byte 16) status_pre));
    579         <minus_plus
    580         <plus_minus_m_m
    581         [1: %
    582         |2: cases daemon (* XXX: todo *)
    583         ]
    584       |2:
    585         cases(compute_max_trace_any_label_cost_is_ok cost_labels end_flag
    586         status_init status_end trace_any_label)
    587         #trace_any_label_eq
    588         cases(is_next)
    589         >clock_execute_1
    590         @plus_le_le
    591       ]*)
    592     ]
    593   |3:
    594     cases the_trace
    595     [1:
    596       #status_before #status_after #trace_to_lift
    597       normalize @compute_max_trace_label_label_cost_is_ok
    598     |2:
    599       #status_initial #status_labelled #status_final #labelled_trace #ret_trace
    600       normalize
    601       cases(compute_max_trace_label_label_cost_is_ok cost_labels doesnt_end_with_ret status_initial status_labelled labelled_trace);
    602       #label_label_trace_equality #label_label_trace_leq
    603       cases(compute_max_trace_label_return_cost_is_ok cost_labels status_labelled status_final ret_trace);
    604       #label_return_trace_equality #label_return_trace_leq
    605       >label_label_trace_equality >label_return_trace_equality
    606       @conj
    607       [2: @(transitive_le (clock (BitVectorTrie (Vector bool 8) 16) status_initial)
    608             (clock (BitVectorTrie Byte 16) status_labelled)
    609             (clock (BitVectorTrie (Vector bool 8) 16) status_final))
    610       |1: @plus_minus_rearrangement_1
    611       ]
    612       assumption
    613     ]
    614   ]
    615 qed.
    616376
    617377(* XXX: work below here: *)
Note: See TracChangeset for help on using the changeset viewer.