Changeset 1663


Ignore:
Timestamp:
Jan 26, 2012, 5:40:53 PM (6 years ago)
Author:
mulligan
Message:

old cases working again, work on new ones

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1658 r1663  
    481481include alias "basics/logic.ma".
    482482
    483 (* Bug to be fixed in the refiner! Compare the two checks
    484 axiom T:Type[0].
    485 axiom S:Type[0].
    486 axiom k: S → T.
    487 coercion k.
    488 check (λf: T → nat. (f: S → nat))
    489 check ((λx:T.0) : S → nat) *)
    490 definition foo ≝ (match match 1 with [O ⇒ 0 | S n ⇒ S ?] : Σn:nat. n=n).
     483lemma plus_right_monotone:
     484  ∀m, n, o: nat.
     485    m = n → m + o = n + o.
     486  #m #n #o #refl >refl %
     487qed.
    491488
    492489let rec block_cost'
     
    509506  [ O ⇒ λbase_case. ⊥
    510507  | S program_size' ⇒ λrecursive_case.
    511     let 〈instruction, program_counter'', ticks〉 ≝ fetch code_memory' program_counter' in
     508    let 〈instruction, program_counter'', ticks〉 as FETCH ≝ fetch code_memory' program_counter' in
    512509    let to_continue ≝
    513510      match lookup_opt … program_counter'' cost_labels with
     
    517514    in
    518515      if to_continue then
    519         match instruction with
    520         [ RealInstruction real_instruction ⇒
    521           match real_instruction with
    522           [ RET                    ⇒ ticks
    523           | JC   relative          ⇒ ticks
    524           | JNC  relative          ⇒ ticks
    525           | JB   bit_addr relative ⇒ ticks
    526           | JNB  bit_addr relative ⇒ ticks
    527           | JBC  bit_addr relative ⇒ ticks
    528           | JZ   relative          ⇒ ticks
    529           | JNZ  relative          ⇒ ticks
    530           | CJNE src_trgt relative ⇒ ticks
    531           | DJNZ src_trgt relative ⇒ ticks
    532           | _                      ⇒
     516        match instruction return λx. x = instruction → ? with
     517        [ RealInstruction real_instruction ⇒ λreal_instruction_refl.
     518          match real_instruction return λx. x = real_instruction →
     519          Σcost_of_block: nat.
     520            ∀start_status: Status.
     521            ∀final_status: Status.
     522            ∀trace_ends_flag.
     523            ∀the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status.
     524              code_memory' = code_memory … start_status →
     525                program_counter' = program_counter … start_status →
     526                    (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧
     527                      cost_of_block = compute_paid_trace_any_label cost_labels trace_ends_flag start_status final_status the_trace with
     528          [ RET                    ⇒ λinstr. ticks
     529          | JC   relative          ⇒ λinstr. ticks
     530          | JNC  relative          ⇒ λinstr. ticks
     531          | JB   bit_addr relative ⇒ λinstr. ticks
     532          | JNB  bit_addr relative ⇒ λinstr. ticks
     533          | JBC  bit_addr relative ⇒ λinstr. ticks
     534          | JZ   relative          ⇒ λinstr. ticks
     535          | JNZ  relative          ⇒ λinstr. ticks
     536          | CJNE src_trgt relative ⇒ λinstr. ticks
     537          | DJNZ src_trgt relative ⇒ λinstr. ticks
     538          | _                      ⇒ λinstr.
    533539              ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
    534           ]
    535         | ACALL addr     ⇒
     540          ] (refl …)
     541        | ACALL addr     ⇒ λinstr.
    536542            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
    537         | AJMP  addr     ⇒ ticks
    538         | LCALL addr     ⇒
     543        | AJMP  addr     ⇒ λinstr. ticks
     544        | LCALL addr     ⇒ λinstr.
    539545            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
    540         | LJMP  addr     ⇒ ticks
    541         | SJMP  addr     ⇒ ticks
    542         | JMP   addr     ⇒ (* XXX: actually a call due to use with fptrs *)
     546        | LJMP  addr     ⇒ λinstr. ticks
     547        | SJMP  addr     ⇒ λinstr. ticks
     548        | JMP   addr     ⇒ λinstr. (* XXX: actually a call due to use with fptrs *)
    543549            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
    544         | MOVC  src trgt ⇒
     550        | MOVC  src trgt ⇒ λinstr.
    545551            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
    546         ]
     552        ] (refl …)
    547553      else
    548         0
     554        (0 : (Σn: nat. ?))
    549555  ].
    550   [57:
    551556  [1:
    552557    cases reachable_program_counter_witness #_ #hyp
    553558    @(absurd (total_program_size < total_program_size) … (not_le_Sn_n …))
    554559    @(le_to_lt_to_lt … base_case hyp)
     560  |4:
     561    #start_status #final_status #trace_ends_flag #the_trace #code_memory_refl #program_counter_refl
     562    cases(block_cost' ?????????) -block_cost'
     563    #recursive_block_cost #recursive_assm
     564    @(trace_any_label_inv_ind … the_trace)
     565    [1:
     566      #start_status' #final_status' #execute_assm #classifier_assm #costed_assm
     567      #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl destruct
     568      cases classifier_assm
     569      whd in match (as_classifier ???);
     570      whd in ⊢ (??%? → ?);
     571      whd in match current_instruction; normalize nodelta
     572      whd in match current_instruction0; normalize nodelta
     573      #absurd @⊥ <FETCH in absurd; normalize nodelta
     574      #absurd destruct(absurd)
     575    |2:
     576      #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
     577      #start_status_refl #final_status_refl #the_trace_assm destruct
     578      whd in classifier_assm;
     579      whd in classifier_assm:(??%?);
     580      whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
     581      whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
     582      @⊥ <FETCH in classifier_assm; normalize nodelta
     583      #absurd destruct(absurd)
     584    |3:
     585      #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
     586      #classifier_assm #after_return_assm #trace_label_return #costed_assm
     587      #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
     588      destruct
     589      cases(recursive_assm status_pre_fun_call status_final doesnt_end_with_ret
     590        (tal_base_call (ASM_abstract_status cost_labels) status_pre_fun_call
     591          (execute_1 status_pre_fun_call) status_final
     592          (refl Status (execute_1 status_pre_fun_call)) classifier_assm
     593          after_return_assm trace_label_return costed_assm) ? ?)
     594      [2: %
     595      |3:
     596      |1:
     597      ]
     598    |4:
     599      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
     600      #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
     601      #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
     602      #final_status_refl #the_trace_refl destruct
     603      whd in match (compute_paid_trace_any_label … (tal_step_call …));
     604      whd in match (trace_any_label_length … (tal_step_call …));
     605      cases(recursive_assm status_after_fun_call status_final end_flag trace_any_label ? ?)
     606      [1:
     607        * #recursive_n #recursive_trace_total #recursive_block_cost_assm
     608        >recursive_block_cost_assm <recursive_trace_total %
     609        [1:
     610          %
     611          [1:
     612          |2:
     613            >commutative_plus in ⊢ (??%?);
     614            >commutative_plus in ⊢ (???%);
     615          ]
     616        |2:
     617          @plus_right_monotone
     618          whd in match (current_instruction_cost status_pre_fun_call);
     619          <FETCH %
     620        ]
     621      |2:
     622      |3:
     623      ]
     624    |5:
     625      #end_flag #status_pre #status_init #status_end #execute_assm #the_trace'
     626      #classifier_assm #costed_assm #trace_ends_flag_refl #start_status_refl
     627      #final_status_refl #trace_refl
     628      generalize in match the_trace; destruct #the_trace
     629      whd in classifier_assm;
     630      whd in classifier_assm:(??%?);
     631      whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
     632      whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
     633      @⊥ <FETCH in classifier_assm; normalize nodelta
     634      #absurd destruct(absurd)
     635    ]
     636  |7,8,9,10,13,16,19,22,25,28,31,34,37,40,41,42,43,44,45,46,47,48,49,52,55,58,61,
     637    64,67,70,73,76,79,82,85,88,91,94,97,100,101,104,108,107:
     638    cases daemon (* XXX: massive terms *)
    555639  |2:
    556640    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    557641    lapply(good_program_witness program_counter' reachable_program_counter_witness)
    558     <FETCH normalize nodelta >instr normalize nodelta
     642    <FETCH normalize nodelta <instr normalize nodelta
    559643    @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
    560644    cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta
     
    576660    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    577661    lapply(good_program_witness program_counter' reachable_program_counter_witness)
    578     <FETCH normalize nodelta >instr normalize nodelta
     662    <FETCH normalize nodelta <instr normalize nodelta
    579663    @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
    580664    cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta
     
    590674      assumption
    591675    ]
    592   |4:
    593676  |5:
    594677    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    595678    lapply(good_program_witness program_counter' reachable_program_counter_witness)
    596       <FETCH normalize nodelta >instr normalize nodelta
     679      <FETCH normalize nodelta <instr normalize nodelta
    597680    @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
    598681    * * * * #n'
     
    609692        nat_of_bitvector … program_counter'')
    610693    assumption
    611  
     694  |6:
     695    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
     696    lapply(good_program_witness program_counter' reachable_program_counter_witness)
     697      <FETCH normalize nodelta <instr normalize nodelta
     698    @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
     699    * * * * #n'
     700    #_ #_ #program_counter_lt' #program_counter_lt_tps'
     701    %
     702    [1:
     703      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
     704      <FETCH normalize nodelta whd in match ltb; normalize nodelta
     705      >(le_to_leb_true … program_counter_lt') %
     706    |2:
     707      assumption
     708    ]
     709  |11,14: (* JMP and MOVC *)
     710    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
     711    lapply(good_program_witness program_counter' reachable_program_counter_witness)
     712    <FETCH normalize nodelta <instr normalize nodelta
     713    try(<real_instruction_refl <instr normalize nodelta) *
     714    #pc_pc_lt_hyp' #pc_tps_lt_hyp'
     715    @(transitive_le
     716      total_program_size
     717      ((S program_size') + nat_of_bitvector … program_counter')
     718      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
     719    normalize in match (S program_size' + nat_of_bitvector … program_counter');
     720    >plus_n_Sm
     721    @monotonic_le_plus_r
     722    change with (
     723      nat_of_bitvector … program_counter' <
     724        nat_of_bitvector … program_counter'')
     725    assumption
     726  |12,15:
     727    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
     728    lapply(good_program_witness program_counter' reachable_program_counter_witness)
     729    <FETCH normalize nodelta <instr normalize nodelta *
     730    #program_counter_lt' #program_counter_lt_tps' %
     731    [1,3:
     732      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
     733      <FETCH normalize nodelta whd in match ltb; normalize nodelta
     734      >(le_to_leb_true … program_counter_lt') %
     735    |2,4:
     736      assumption
     737    ]
     738  |17,20,23,26,29,32,35,38,50,53,56,59,62,65,68,71,74,77,80,83,86,89,92,95,98,
     739   102,105:
     740    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
     741    lapply(good_program_witness program_counter' reachable_program_counter_witness)
     742    <FETCH normalize nodelta
     743    <real_instruction_refl <instr normalize nodelta *
     744    #pc_pc_lt_hyp' #pc_tps_lt_hyp'
     745    @(transitive_le
     746      total_program_size
     747      ((S program_size') + nat_of_bitvector … program_counter')
     748      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
     749    normalize in match (S program_size' + nat_of_bitvector … program_counter');
     750    >plus_n_Sm
     751    @monotonic_le_plus_r
     752    change with (
     753      nat_of_bitvector … program_counter' <
     754        nat_of_bitvector … program_counter'')
     755    assumption
     756  |18,21,24,27,30,33,36,39,51,54,57,60,63,66,69,72,75,78,
     757    81,84,87,90,93,96,99,103,106:
     758    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
     759    lapply(good_program_witness program_counter' reachable_program_counter_witness)
     760    <FETCH normalize nodelta <real_instruction_refl <instr normalize nodelta *
     761    #program_counter_lt' #program_counter_lt_tps' %
     762    try assumption
     763    [*:
     764      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
     765      <FETCH normalize nodelta whd in match ltb; normalize nodelta
     766      >(le_to_leb_true … program_counter_lt') %
     767    ]
    612768  [1:
    613769    #start_status #final_status #trace_ends_flag #the_trace #code_memory_refl #program_counter_refl
Note: See TracChangeset for help on using the changeset viewer.