Changeset 3145 for src/ASM/ASMCosts.ma


Ignore:
Timestamp:
Apr 15, 2013, 4:31:50 PM (7 years ago)
Author:
tranquil
Message:
  • removed sigma types from traces of intensional events
  • completed correctness.ma using axiom files, a single daemon remains
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r3112 r3145  
    2929
    3030 λprog,cm,s0.
     31 let dummy : ident ≝ an_identifier … one in
    3132  let pc ≝ program_counter ?? (execute_1' cm s0) in
    3233  match lookup_opt ?? pc (symboltable prog) with
    33   [ None ⇒ ⊥ | Some id ⇒ id ].
    34 cases daemon (*CSC: we need a specification of the symboltable for this *)
     34  [ None ⇒ dummy (* in order to avoid this case we need a specification of the symboltable for this *)
     35  | Some id ⇒ id ].
     36
     37definition OC_result : ∀loc.Status (cm loc) → option int ≝
     38λprog,st. as_result_of_finaladdr … st (final_pc prog).
     39
     40lemma OC_exclude_tailcall :
     41∀p : labelled_object_code.
     42∀st : Status (cm p).
     43OC_classify … st ≠ cl_tailcall.
     44#p #st whd in ⊢ (?(??%?));
     45cases current_instruction [7: * ] normalize
     46try #x try #y % #ABS destruct
    3547qed.
    3648
     
    3951    mk_abstract_status
    4052      (Status (cm prog))
    41       (λs1,s2. execute_1 … s1 = s2)
     53      (λs1,s2.OC_result … s1 = None ? ∧ execute_1 … s1 = s2)
    4254      word_deqset
    4355      (program_counter …)
     
    4557      (λpc.lookup_opt … pc (costlabels prog))
    4658      (next_instruction_properly_relates_program_counters …)
    47       (λst. as_result_of_finaladdr … st (final_pc prog))
     59      (OC_result ?)
    4860      (OC_as_call_ident prog …)
    49       ?.
    50  * #st whd in ⊢ (??%? → ?); cases current_instruction [7: *] normalize
    51  try (#x #y #abs) try (#x #abs) try #abs destruct
    52 qed.
     61      (λst.⊥).
     62@hide_prf cases st -st #st #ABS @(absurd … ABS) @OC_exclude_tailcall qed.
    5363
    5464lemma OC_costed_is_nop : ∀loc.
     
    312322  @(trace_any_label_inv_ind … the_trace)
    313323    [2:
    314       #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
     324      #start_status' #final_status' * #no_result #execute_assm #classifier_assm #trace_ends_assm
    315325      #start_status_refl #final_status_refl #the_trace_assm destruct @⊥
    316326    |3:
    317       #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
     327      #status_pre_fun_call #status_start_fun_call #status_final * #no_result #execute_assm
    318328      #classifier_assm #after_return_assm #trace_label_return #costed_assm
    319329      #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    320330      destruct @⊥
    321331    |4:
    322       #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
     332      #status_pre_fun_call #status_start_fun_call #status_final * #no_result #execute_assm
    323333      #classifier_assm #trace_label_return
    324334      #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
     
    326336    |5:
    327337      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
    328       #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
     338      #status_final * #no_result #execute_assm #classifier_assm #after_return_assm #trace_label_return
    329339      #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
    330340      #final_status_refl #the_trace_refl destruct @⊥
    331341    |6:
    332       #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
     342      #end_flag #status_pre #status_init #status_end * #no_result #execute_assm #trace_any_label
    333343      #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
    334344      #the_trace_refl
     
    371381      ]
    372382    |1:
    373       #status_start #status_final #execute_assm #classifier_assm #costed_assm
     383      #status_start #status_final * #no_result #execute_assm #classifier_assm #costed_assm
    374384      #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    375385      destruct
     
    450460  @(trace_any_label_inv_ind … the_trace)
    451461  [6:
    452     #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
     462    #end_flag #status_pre #status_init #status_end * #no_result #execute_assm #trace_any_label
    453463    #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
    454464    #the_trace_refl destruct @⊥
    455465  |1:
    456     #status_start #status_final #execute_assm #classifier_assm #costed_assm
     466    #status_start #status_final * #no_result #execute_assm #classifier_assm #costed_assm
    457467    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    458468    destruct
     
    461471    <FETCH %
    462472  |2:
    463     #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
     473    #start_status' #final_status' * #no_result #execute_assm #classifier_assm #trace_ends_assm
    464474    #start_status_refl #final_status_refl #the_trace_assm destruct @⊥
    465475  |3:
    466     #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
     476    #status_pre_fun_call #status_start_fun_call #status_final * #no_result #execute_assm
    467477    #classifier_assm #after_return_assm #trace_label_return #costed_assm
    468478    #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    469479    destruct @⊥
    470480  |4:
    471     #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
     481    #status_pre_fun_call #status_start_fun_call #status_final * #no_result #execute_assm
    472482    #classifier_assm #trace_label_return
    473483    #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
     
    475485  |5:
    476486    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
    477     #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
     487    #status_final * #no_result #execute_assm #classifier_assm #after_return_assm #trace_label_return
    478488    #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
    479489    #final_status_refl #the_trace_refl destruct @⊥
     
    524534  @(trace_any_label_inv_ind … the_trace)
    525535  [6:
    526     #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
     536    #end_flag #status_pre #status_init #status_end * #no_result #execute_assm #trace_any_label
    527537    #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
    528538    #the_trace_refl destruct @⊥
    529539  |1:
    530     #status_start #status_final #execute_assm #classifier_assm #costed_assm
     540    #status_start #status_final * #no_result #execute_assm #classifier_assm #costed_assm
    531541    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    532542    destruct @⊥
    533543  |2:
    534     #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
     544    #start_status' #final_status' * #no_result #execute_assm #classifier_assm #trace_ends_assm
    535545    #start_status_refl #final_status_refl #the_trace_assm destruct @⊥
    536546  |3:
    537     #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
     547    #status_pre_fun_call #status_start_fun_call #status_final * #no_result #execute_assm
    538548    #classifier_assm #after_return_assm #trace_label_return #costed_assm
    539549    #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
     
    571581    ]
    572582  |4:
    573     #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
     583    #status_pre_fun_call #status_start_fun_call #status_final * #no_result #execute_assm
    574584    #classifier_assm #trace_label_return
    575585    #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
     
    577587  |5:
    578588    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
    579     #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
     589    #status_final * #no_result #execute_assm #classifier_assm #after_return_assm #trace_label_return
    580590    #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
    581591    #final_status_refl #the_trace_refl
     
    643653  @(trace_any_label_inv_ind … the_trace)
    644654  [1:
    645     #start_status' #final_status' #execute_assm #classifier_assm #costed_assm
     655    #start_status' #final_status' * #no_result #execute_assm #classifier_assm #costed_assm
    646656    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    647657    destruct @⊥
    648658  |2:
    649     #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_flag_refl
     659    #start_status' #final_status' * #no_result #execute_assm #classifier_assm #trace_ends_flag_refl
    650660    #start_status_refl #final_status_refl #the_trace_refl destruct
    651661    whd in match (trace_any_label_length … (tal_base_return …));
     
    653663    <FETCH %
    654664  |3:
    655     #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
     665    #status_pre_fun_call #status_start_fun_call #status_final * #no_result #execute_assm
    656666    #classifier_assm #after_return_assm #trace_label_return #costed_assm
    657667    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    658668    destruct @⊥
    659669  |4:
    660     #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
     670    #status_pre_fun_call #status_start_fun_call #status_final * #no_result #execute_assm
    661671    #classifier_assm
    662672    destruct @⊥
     
    669679  |5:
    670680    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
    671     #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
     681    #status_final * #no_result #execute_assm #classifier_assm #after_return_assm #trace_label_return
    672682    #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
    673683    #final_status_refl #the_trace_refl
    674684    destruct @⊥
    675685  |6:
    676     #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
     686    #end_flag #status_pre #status_init #status_end * #no_result #execute_assm #trace_any_label
    677687    #classifier_assm #costed_assm #trace_ends_flag_refl #start_status_refl
    678688    #final_status_refl #the_trace_refl destruct @⊥
Note: See TracChangeset for help on using the changeset viewer.