Changeset 1902 for src/ASM/ASMCosts.ma


Ignore:
Timestamp:
Apr 26, 2012, 4:20:32 PM (8 years ago)
Author:
mulligan
Message:

Reverted needless changes to StructuredTraces?

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1901 r1902  
    347347  #T #n #o #Q #fixed_v #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10
    348348  #P11 #P12 #P13 #P14 #P15 #P16 #P17 #P18 #P19 #v1 #v2 #fixed_v_proof
     349  generalize in match fixed_v_proof; -fixed_v_proof
    349350  cases daemon
    350351qed.
     
    377378  λbefore: Status code_memory.
    378379  λafter : Status code_memory.
     380    let program_counter_before ≝ program_counter ? code_memory before in
     381    let 〈instruction, program_counter_after, ticks〉 ≝ fetch code_memory program_counter_before in
     382      program_counter ? code_memory after = program_counter_after.
     383(* XXX: why defined like this?
    379384  let size ≝ current_instruction_cost code_memory before in
    380385  let pc_before ≝ program_counter … code_memory before in
     
    382387  let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in
    383388    sum = pc_after.
    384 
    385 definition program_counters_properly_related:
    386     ∀code_memory: BitVectorTrie Byte 16. Status code_memory → Status code_memory → Prop ≝
    387   λcode_memory: BitVectorTrie Byte 16.
    388   λbefore: Status code_memory.
    389   λafter: Status code_memory.
    390     let program_counter_before ≝ program_counter ? code_memory before in
    391     let 〈instruction, program_counter_after, ticks〉 ≝ fetch code_memory program_counter_before in
    392       program_counter ? code_memory after = program_counter_after.
     389*)
    393390
    394391definition ASM_abstract_status: ∀code_memory. BitVectorTrie costlabel 16 → abstract_status ≝
     
    400397      (λs,class. ASM_classify … s = class)
    401398      (current_instruction_is_labelled … cost_labels)
    402       (next_instruction_properly_relates_program_counters code_memory)
    403       (program_counters_properly_related code_memory).
     399      (next_instruction_properly_relates_program_counters code_memory).
    404400
    405401let rec trace_any_label_length
     
    411407  match the_trace with
    412408  [ tal_base_not_return the_status _ _ _ _ ⇒ 0
    413   | tal_base_call pre_fun_call start_fun_call final _ _ _ _ call_trace _ ⇒ 0
     409  | tal_base_call pre_fun_call start_fun_call final _ _ _ _ call_trace ⇒ 0
    414410  | tal_base_return the_status _ _ _ ⇒ 0
    415   | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final _ _ _ _ call_trace _ final_trace ⇒
     411  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final _ _ _ call_trace _ final_trace ⇒
    416412      let tail_length ≝ trace_any_label_length … final_trace in
    417413      let pc_difference ≝ nat_of_bitvector … (program_counter … after_fun_call) - nat_of_bitvector … (program_counter … pre_fun_call) in       
     
    432428  [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost … the_status
    433429  | tal_base_return the_status _ _ _ ⇒ current_instruction_cost … the_status
    434   | tal_base_call pre_fun_call start_fun_call final _ _ _ _ call_trace _ ⇒ current_instruction_cost … pre_fun_call
     430  | tal_base_call pre_fun_call start_fun_call final _ _ _ _ call_trace ⇒ current_instruction_cost … pre_fun_call
    435431  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
    436      _ _ _ _ call_trace _ final_trace ⇒
     432     _ _ _ call_trace _ final_trace ⇒
    437433      let current_instruction_cost ≝ current_instruction_cost … pre_fun_call in
    438434      let final_trace_cost ≝ compute_paid_trace_any_label … cost_labels end_flag … final_trace in
     
    840836    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
    841837    #classifier_assm #after_return_assm #trace_label_return #costed_assm
    842     #program_counters_properly_related_assm #ends_flag_refl #start_status_refl
    843     #final_status_refl #the_trace_refl
     838    #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    844839    destruct
    845840    whd in match (trace_any_label_length … (tal_base_call …));
     
    858853      cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' status_final))
    859854      [1:
    860         generalize in match program_counters_properly_related_assm;
     855        generalize in match after_return_assm;
    861856        whd in ⊢ (% → ?); <FETCH normalize nodelta #relevant <relevant %
    862857      |2:
     
    881876    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
    882877    #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
    883     #costed_assm #program_counters_properly_related_assm #trace_any_label
    884     #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
     878    #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
     879    #final_status_refl #the_trace_refl
    885880    generalize in match execute_assm; destruct #execute_assm
    886881    whd in match (trace_any_label_length … (tal_step_call …));
     
    897892      cut(program_counter'' = program_counter … status_after_fun_call)
    898893      [1:
    899         generalize in match program_counters_properly_related_assm;
     894        generalize in match after_return_assm;
    900895        whd in ⊢ (% → ?); <FETCH normalize nodelta #relevant >relevant %
    901896      |2:
     
    16421637  [ O ⇒ ?
    16431638  | S n' ⇒ ?
    1644   ].trace_any_label_length
     1639  ].
    16451640  [1,3:
    16461641    normalize #assm assumption
Note: See TracChangeset for help on using the changeset viewer.