Changeset 1901 for src/ASM/ASMCosts.ma


Ignore:
Timestamp:
Apr 26, 2012, 3:35:01 PM (8 years ago)
Author:
mulligan
Message:

Slight changes to StructuredTraces?: should not change too much

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1895 r1901  
    383383    sum = pc_after.
    384384
     385definition 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.
     393
    385394definition ASM_abstract_status: ∀code_memory. BitVectorTrie costlabel 16 → abstract_status ≝
    386395  λcode_memory.
     
    391400      (λs,class. ASM_classify … s = class)
    392401      (current_instruction_is_labelled … cost_labels)
    393       (next_instruction_properly_relates_program_counters code_memory).
     402      (next_instruction_properly_relates_program_counters code_memory)
     403      (program_counters_properly_related code_memory).
    394404
    395405let rec trace_any_label_length
     
    401411  match the_trace with
    402412  [ tal_base_not_return the_status _ _ _ _ ⇒ 0
    403   | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒ 0
     413  | tal_base_call pre_fun_call start_fun_call final _ _ _ _ call_trace _ ⇒ 0
    404414  | tal_base_return the_status _ _ _ ⇒ 0
    405   | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final _ _ _ call_trace _ final_trace ⇒
     415  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final _ _ _ _ call_trace _ final_trace ⇒
    406416      let tail_length ≝ trace_any_label_length … final_trace in
    407417      let pc_difference ≝ nat_of_bitvector … (program_counter … after_fun_call) - nat_of_bitvector … (program_counter … pre_fun_call) in       
     
    422432  [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost … the_status
    423433  | tal_base_return the_status _ _ _ ⇒ current_instruction_cost … the_status
    424   | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒ current_instruction_cost … pre_fun_call
     434  | tal_base_call pre_fun_call start_fun_call final _ _ _ _ call_trace _ ⇒ current_instruction_cost … pre_fun_call
    425435  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
    426      _ _ _ call_trace _ final_trace ⇒
     436     _ _ _ _ call_trace _ final_trace ⇒
    427437      let current_instruction_cost ≝ current_instruction_cost … pre_fun_call in
    428438      let final_trace_cost ≝ compute_paid_trace_any_label … cost_labels end_flag … final_trace in
     
    456466    m = n → m + o = n + o.
    457467  #m #n #o #refl >refl %
     468qed.
     469
     470lemma plus_left_monotone:
     471  ∀m, n, o: nat.
     472    m = n → o + m = o + n.
     473  #m #n #o #refl destruct %
    458474qed.
    459475
     
    524540      ∀the_trace0:trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag0 start_status0 final_status0.
    525541        program_counter'' = program_counter (BitVectorTrie Byte 16) code_memory' start_status0 →
    526         (∃n:ℕ
    527                     .trace_any_label_length code_memory' cost_labels
    528                      trace_ends_flag0 start_status0 final_status0 the_trace0
    529                      +S n
    530                      =total_program_size)
    531                    ∧pi1
     542        (∃n:ℕ.
     543            trace_any_label_length code_memory' cost_labels
     544              trace_ends_flag0 start_status0 final_status0 the_trace0
     545                + S n
     546                  = total_program_size) ∧
     547                  pi1
    532548                    =compute_paid_trace_any_label code_memory' cost_labels
    533549                     trace_ends_flag0 start_status0 final_status0 the_trace0
    534550    else (pi1=O) )
    535    →(∃n:ℕ
    536      .trace_any_label_length code_memory' cost_labels trace_ends_flag
     551   →(∃n:ℕ.
     552     trace_any_label_length code_memory' cost_labels trace_ends_flag
    537553      start_status final_status the_trace
    538554      +S n
     
    576592          normalize nodelta #new_recursive_assm
    577593          cases(new_recursive_assm (execute_1 code_memory' status_pre) status_end
    578             end_flag trace_any_label ?) [2: % ]
     594            end_flag trace_any_label ?) try %
    579595          #exists_assm #recursive_block_cost_assm %
    580596          [1:
    581597            cases exists_assm #exists_n #total_program_size_refl
    582598            <total_program_size_refl
    583             %{(exists_n - current_instruction_cost … status_pre)}
    584             (* XXX: Christ knows what's going on with the rewrite tactic here? *)
     599            %{(exists_n - (nat_of_bitvector 16
     600                (program_counter (BitVectorTrie Byte 16) code_memory'
     601                  (execute_1 code_memory' status_pre))
     602                - nat_of_bitvector 16
     603                  (program_counter (BitVectorTrie Byte 16) code_memory' status_pre)))}
     604            <plus_n_Sm <plus_n_Sm @eq_f >commutative_plus
    585605            cases daemon
    586606          |2:
     
    820840    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
    821841    #classifier_assm #after_return_assm #trace_label_return #costed_assm
    822     #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
     842    #program_counters_properly_related_assm #ends_flag_refl #start_status_refl
     843    #final_status_refl #the_trace_refl
    823844    destruct
    824845    whd in match (trace_any_label_length … (tal_base_call …));
     
    837858      cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' status_final))
    838859      [1:
    839         whd in after_return_assm; <after_return_assm; (* XXX: here *)
    840         cases daemon
     860        generalize in match program_counters_properly_related_assm;
     861        whd in ⊢ (% → ?); <FETCH normalize nodelta #relevant <relevant %
    841862      |2:
    842863        #program_counter_assm >program_counter_assm <Some_lookup_opt
     
    860881    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
    861882    #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
    862     #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
    863     #final_status_refl #the_trace_refl destruct
     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
     885    generalize in match execute_assm; destruct #execute_assm
    864886    whd in match (trace_any_label_length … (tal_step_call …));
    865887    whd in match (compute_paid_trace_any_label … (tal_step_call …));
     
    875897      cut(program_counter'' = program_counter … status_after_fun_call)
    876898      [1:
    877         cases daemon
     899        generalize in match program_counters_properly_related_assm;
     900        whd in ⊢ (% → ?); <FETCH normalize nodelta #relevant >relevant %
    878901      |2:
    879902        #program_counter_refl >program_counter_refl <None_lookup_opt_assm
     
    887910            whd in ⊢ (???%); <FETCH %
    888911          |1:
    889             (*
    890             cases exists_assm #recursive_n #new_exists_assm
    891             <new_exists_assm
    892            
    893             %
    894             [1:
    895               @(recursive_n - current_instruction_cost … status_pre_fun_call)
    896             |2:
    897              
    898               cut(current_instruction_cost … status_pre_fun_call =
    899                 (nat_of_bitvector 16
    900   (program_counter (BitVectorTrie Byte 16) code_memory' status_after_fun_call)
    901   -nat_of_bitvector 16
    902    (program_counter (BitVectorTrie Byte 16) code_memory' status_pre_fun_call)))
    903               [1:
    904               |2:
    905                 #eq_assm <eq_assm -eq_assm -new_exists_assm -recursive_block_cost_assm
    906                 <plus_n_Sm <plus_n_Sm @eq_f
    907                 >associative_plus in ⊢ (??%?); >commutative_plus in ⊢ (??%?);
    908                 >associative_plus @eq_f
    909                 <plus_minus_m_m [1: % ]
    910               ]
    911             ] *)
    912             cases daemon
     912            cases exists_assm #exists_n #trace_total_program_size_assm
     913            generalize in match execute_assm; destruct #execute_assm
     914            %{(exists_n - ((nat_of_bitvector … (program_counter … status_after_fun_call)
     915                - nat_of_bitvector … (program_counter … status_pre_fun_call))))}
     916            >commutative_plus in ⊢ (??(?%?)?);
     917            <plus_n_Sm <plus_n_Sm @eq_f >associative_plus in ⊢ (??%?);
     918            @plus_left_monotone @sym_eq <commutative_plus in ⊢ (???%);
     919            @plus_minus_m_m
     920            cases daemon (* XXX: !!! *)
    913921          ]
    914922        |2,4:
     
    10031011  #absurd destruct(absurd)
    10041012qed.
    1005      
    10061013     
    10071014let rec block_cost'
     
    12101217    <FETCH normalize nodelta whd in match ltb; normalize nodelta
    12111218    >(le_to_leb_true … program_counter_lt') %
    1212     (* XXX: got to here *)
    12131219  |6,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,71,74,77,80,83,86,89,
    12141220   92:
     
    16361642  [ O ⇒ ?
    16371643  | S n' ⇒ ?
    1638   ].
     1644  ].trace_any_label_length
    16391645  [1,3:
    16401646    normalize #assm assumption
Note: See TracChangeset for help on using the changeset viewer.