Changeset 1902


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

Reverted needless changes to StructuredTraces?

Location:
src
Files:
2 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
  • src/common/StructuredTraces.ma

    r1901 r1902  
    1515  as_classifier : as_status → status_class → Prop;
    1616  as_costed : as_status → Prop;
    17   as_after_return : (Σs:as_status. as_classifier s cl_call) → as_status → Prop;
    18   as_program_counters_properly_related: as_status → as_status → Prop
     17  as_after_return : (Σs:as_status. as_classifier s cl_call) → as_status → Prop
    1918}.
    2019
     
    7170          trace_label_return S status_start_fun_call status_final →
    7271          as_costed S status_final →
    73           as_program_counters_properly_related S status_pre_fun_call status_final →
    7472            trace_any_label S doesnt_end_with_ret status_pre_fun_call status_final
    7573  (* A call followed by a non-empty trace. *)
     
    8583          trace_label_return S status_start_fun_call status_after_fun_call →
    8684          ¬ as_costed S status_after_fun_call →
    87           as_program_counters_properly_related S status_pre_fun_call status_after_fun_call →
    8885          trace_any_label S end_flag status_after_fun_call status_final →
    8986            trace_any_label S end_flag status_pre_fun_call status_final
     
    219216[ tal_base_not_return start final _ _ C ⇒ C
    220217| tal_base_return _ _  _ _ ⇒ I
    221 | tal_base_call _ _ _ _ _ _ _ C _ ⇒ C
    222 | tal_step_call f pre start after final X C RET PROPER LR C' tr' ⇒ trace_any_label_label … tr'
     218| tal_base_call _ _ _ _ _ _ _ C ⇒ C
     219| tal_step_call f pre start after final X C RET LR C' tr' ⇒ trace_any_label_label … tr'
    223220| tal_step_default f pre init end X tr' C C' ⇒ trace_any_label_label … tr'
    224221].
Note: See TracChangeset for help on using the changeset viewer.