Changeset 1910 for src/ASM/ASMCosts.ma


Ignore:
Timestamp:
Apr 27, 2012, 5:48:20 PM (8 years ago)
Author:
mulligan
Message:

Finished proof modulo termination argument

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/ASMCosts.ma

    r1909 r1910  
    224224qed.
    225225
    226 (*
    227226(* XXX: indexing bug *)
    228 lemma fetch_twice_fetch_execute_1:
     227lemma execute_1_and_program_counter_after_other_in_lockstep:
    229228  ∀code_memory: BitVectorTrie Byte 16.
    230229  ∀start_status: Status code_memory.
    231230    ASM_classify code_memory start_status = cl_other →
    232     \snd (\fst (fetch code_memory (program_counter … start_status))) =
    233       program_counter … (execute_1 … start_status).
     231      let 〈instruction, pc, ticks〉 ≝ fetch code_memory (program_counter … start_status) in
     232        program_counter ? ? (execute_1 … start_status) =
     233          program_counter_after_other pc instruction.
    234234  #code_memory #start_status #classify_assm
    235235  whd in match execute_1; normalize nodelta
    236236  cases (execute_1' code_memory start_status) #the_status
    237   * #_ #classify_assm' @classify_assm' assumption
     237  * #_ whd in classify_assm:(??%?); whd in match (current_instruction ??) in classify_assm;
     238  cases (fetch ? ?) in classify_assm; * #instruction #pc #ticks
     239  #classify_assm #classify_assm' @classify_assm' assumption
    238240qed-.
    239 *)
    240241
    241242lemma reachable_program_counter_to_0_lt_total_program_size:
    … …  
    268269  ∀program_counter'' : Word.
    269270  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter').
     271  let program_counter''' ≝ program_counter_after_other program_counter'' instruction in
    270272  ∀start_status : (Status code_memory').
    271273  ∀final_status : (Status code_memory').
    … …  
    275277  ∀classify_assm: ASM_classify0 instruction = cl_other.
    276278  ∀pi1 : ℕ.
    277    (if match lookup_opt costlabel 16 program_counter'' cost_labels with 
     279   (if match lookup_opt costlabel 16 program_counter''' cost_labels with 
    278280         [None ⇒ true
    279281         |Some _ ⇒ false
    … …  
    284286      ∀trace_ends_flag0:trace_ends_with_ret.
    285287      ∀the_trace0:trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag0 start_status0 final_status0.
    286         program_counter'' = program_counter (BitVectorTrie Byte 16) code_memory' start_status0 →
     288        program_counter''' = program_counter (BitVectorTrie Byte 16) code_memory' start_status0 →
    287289                  pi1
    288290                    =compute_paid_trace_any_label code_memory' cost_labels
    … …  
    313315      #lookup_assm cases lookup_assm
    314316      [1:
    315         #None_lookup_opt_assm normalize nodelta #ignore
     317        #None_lookup_opt_assm normalize nodelta #_
    316318        generalize in match recursive_assm;
    317         cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' (execute_1 code_memory' status_pre)))
    318         [1:
    319           <fetch_twice_fetch_execute_1
    320           [1:
    321             <FETCH %
    322           |2:
    323             >classifier_assm %
    324           ]
     319        lapply (execute_1_and_program_counter_after_other_in_lockstep code_memory' ? classifier_assm)
     320        <FETCH normalize nodelta #rewrite_assm >rewrite_assm in None_lookup_opt_assm;
     321        #None_lookup_opt_assm <None_lookup_opt_assm
     322        normalize nodelta #new_recursive_assm
     323        cases(new_recursive_assm (execute_1 code_memory' status_pre) status_end
     324          end_flag trace_any_label ?) try %
     325        whd in match (current_instruction_cost … status_pre);
     326        cut(ticks = \snd (fetch code_memory'
     327           (program_counter (BitVectorTrie Byte 16) code_memory' status_pre)))
     328        [1,3:
     329          <FETCH %
    325330        |2:
    326           #program_counter_assm >program_counter_assm <None_lookup_opt_assm
    327           normalize nodelta #new_recursive_assm
    328           cases(new_recursive_assm (execute_1 code_memory' status_pre) status_end
    329             end_flag trace_any_label ?) try %
    330           whd in match (current_instruction_cost … status_pre);
    331           cut(ticks = \snd (fetch code_memory'
    332              (program_counter (BitVectorTrie Byte 16) code_memory' status_pre)))
    333           [1:
    334             <FETCH %
    335           |2:
    336             #ticks_refl_assm >ticks_refl_assm %
    337           ]
     331          #ticks_refl_assm >ticks_refl_assm %
     332        |4:
     333          #ticks_refl_assm
     334          >rewrite_assm %
    338335        ]
    339336      |2:
    … …  
    359356        #costlabel #Some_lookup_opt_assm normalize nodelta #ignore
    360357        generalize in match recursive_assm;
    361         cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' (execute_1 … status_start)))
     358        cases classifier_assm
    362359        [1:
    363           <fetch_twice_fetch_execute_1
    364           [1:
    365             <FETCH %
    366           |2:
    367             cases classifier_assm
    368             [1:
    369               whd in ⊢ (% → ?);
    370               whd in ⊢ (??%? → ?);
    371               whd in match (current_instruction code_memory' status_start);
    372               <FETCH generalize in match classify_assm;
    373               cases instruction
    374               [8:
    375                 #preinstruction normalize nodelta
    376                 whd in match ASM_classify0; normalize nodelta
    377                 #contradiction >contradiction #absurd destruct(absurd)
    378               ]
    379               try(#addr1 #addr2 normalize nodelta #ignore #absurd destruct(absurd))
    380               try(#addr normalize nodelta #ignore #absurd destruct(absurd))
    381               normalize in ignore; destruct(ignore)
    382             |2:
    383               #classifier_assm' >classifier_assm' %
    384             ]
     360          whd in ⊢ (% → ?);
     361          whd in ⊢ (??%? → ?);
     362          whd in match (current_instruction code_memory' status_start);
     363          <FETCH generalize in match classify_assm;
     364          cases instruction
     365          [8:
     366            #preinstruction normalize nodelta
     367            whd in match ASM_classify0; normalize nodelta
     368            #contradiction >contradiction #absurd destruct(absurd)
    385369          ]
     370          try(#addr1 #addr2 normalize nodelta #ignore #absurd destruct(absurd))
     371          try(#addr normalize nodelta #ignore #absurd destruct(absurd))
     372          normalize in ignore; destruct(ignore)
    386373        |2:
    387           #program_counter_assm >program_counter_assm <Some_lookup_opt_assm
     374          -classifier_assm #classifier_assm
     375          lapply (execute_1_and_program_counter_after_other_in_lockstep code_memory' ? classifier_assm)
     376          <FETCH normalize nodelta #rewrite_assm >rewrite_assm in Some_lookup_opt_assm;
     377          #Some_lookup_opt_assm <Some_lookup_opt_assm
    388378          normalize nodelta #new_recursive_assm >new_recursive_assm
    389379          cut(ticks = \snd (fetch code_memory'
    … …  
    415405  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
    416406  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
    417 qed. *)
     407qed.
    418408
    419409lemma trace_compute_paid_trace_cl_jump:
    … …  
    674664     
    675665let rec block_cost'
    676   (code_memory': BitVectorTrie Byte 16) (program_counter': Word)
     666  (code_memory': BitVectorTrie Byte 16) (program_counter': Word) (visited: list Word)
    677667    (program_size: nat) (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16)
    678668      (reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter')
    … …  
    691681            (cost_of_block = 0) ≝
    692682  match program_size return λprogram_size: nat. total_program_size ≤ program_size + nat_of_bitvector … program_counter' → ? with
    693   [ O ⇒ λbase_case. ⊥
     683  [ O ⇒ λbase_case. ⊥ (* XXX: dummy to be inserted here *)
    694684  | S program_size' ⇒ λrecursive_case.
    695685    let 〈instruction, program_counter'', ticks〉 as FETCH ≝ fetch code_memory' program_counter' in
    … …  
    723713          | DJNZ src_trgt relative ⇒ λinstr. ticks
    724714          | _                      ⇒ λinstr.
    725          
    726               ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
     715              ticks + block_cost' code_memory' program_counter'' (program_counter'::visited) program_size' total_program_size cost_labels ? good_program_witness false ?
    727716          ] (refl …)
    728717        | ACALL addr     ⇒ λinstr.
    729             ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
     718            ticks + block_cost' code_memory' program_counter'' (program_counter'::visited) program_size' total_program_size cost_labels ? good_program_witness false ?
    730719        | AJMP  addr     ⇒ λinstr.
    731             ticks + block_cost' code_memory' ? program_size' total_program_size cost_labels ? good_program_witness false ?
     720          let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in
     721            ticks + block_cost' code_memory' jump_target (program_counter'::visited) program_size' total_program_size cost_labels ? good_program_witness false ?
    732722        | LCALL addr     ⇒ λinstr.
    733             ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
    734         | LJMP  addr     ⇒ λinstr. ticks
    735         | SJMP  addr     ⇒ λinstr. ticks
     723            ticks + block_cost' code_memory' program_counter'' (program_counter'::visited) program_size' total_program_size cost_labels ? good_program_witness false ?
     724        | LJMP  addr     ⇒ λinstr.
     725          let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in
     726            ticks + block_cost' code_memory' jump_target (program_counter'::visited) program_size' total_program_size cost_labels ? good_program_witness false ?
     727        | SJMP  addr     ⇒ λinstr.
     728          let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in
     729            ticks + block_cost' code_memory' jump_target (program_counter'::visited) program_size' total_program_size cost_labels ? good_program_witness false ?
    736730        | JMP   addr     ⇒ λinstr. (* XXX: actually a call due to use with fptrs *)
    737             ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
     731            ticks + block_cost' code_memory' program_counter'' (program_counter'::visited) program_size' total_program_size cost_labels ? good_program_witness false ?
    738732        | MOVC  src trgt ⇒ λinstr.
    739             ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
     733            ticks + block_cost' code_memory' program_counter'' (program_counter'::visited) program_size' total_program_size cost_labels ? good_program_witness false ?
    740734        ] (refl …))
    741735      else
    … …  
    754748          ])
    755749  ].
    756   [1:
     750  [2:
     751    change with (if to_continue then ? else (? = 0))
     752    >p in ⊢ (match % return ? with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta
     753    @pi2
     754  |1:
    757755    cases reachable_program_counter_witness #_ #hyp
    758756    @(absurd (total_program_size < total_program_size) … (not_le_Sn_n …))
    759757    @(le_to_lt_to_lt … base_case hyp)
    760   |2:
    761     change with (if to_continue then ? else (? = 0))
    762     >p in ⊢ (match % return ? with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta
    763     @pi2
    764758  |3:
    765759    change with (if to_continue then ? else (0 = 0))
    … …  
    769763    @(trace_compute_paid_trace_cl_return … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl)
    770764    destruct %
    771   |96,102,105:
     765  |96,108,111:
    772766    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
    773     cases(block_cost' ?????????) -block_cost'
     767    cases(block_cost' ??????????) -block_cost'
    774768    @(trace_compute_paid_trace_cl_call … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … program_counter_refl)
    775769    destruct %
    776770  |4,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,69,72,75,78,81,84,87,
    777    90,93:
     771   90,93,99,102,105:
    778772    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
    779     cases(block_cost' ?????????) -block_cost'
    780     @(trace_compute_paid_trace_cl_other … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl)
    781     destruct %
    782   |60,61,62,63,64,65,66,67,68,69,99,101,100,102:
     773    cases(block_cost' ??????????) -block_cost'
     774    lapply (trace_compute_paid_trace_cl_other ???? reachable_program_counter_witness good_program_witness ? recursive_case ??? FETCH ??? the_trace program_counter_refl)
     775    normalize nodelta destruct #assm @assm %
     776  |60,61,62,63,64,65,66,67,68:
    783777    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
    784778    @(trace_compute_paid_trace_cl_jump … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl)
    785779    destruct %
    786   |103:
     780  ]
     781  -block_cost'
     782  [63:
    787783    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    788784    lapply(good_program_witness program_counter' reachable_program_counter_witness)
    … …  
    799795      assumption
    800796    ]
    801   |104:
     797  |64:
    802798    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    803799    lapply(good_program_witness program_counter' reachable_program_counter_witness)
    … …  
    817813        nat_of_bitvector … program_counter'')
    818814    assumption
    819   |106:
     815  |65:
    820816    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    821817    lapply(good_program_witness program_counter' reachable_program_counter_witness)
    … …  
    834830      assumption
    835831    ]
    836   |107:
     832  |66:
    837833    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    838834    lapply(good_program_witness program_counter' reachable_program_counter_witness)
    … …  
    854850        nat_of_bitvector … program_counter'')
    855851    assumption
    856   |94,97:
     852  |53,55:
    857853    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    858854    lapply(good_program_witness program_counter' reachable_program_counter_witness)
    … …  
    866862      assumption
    867863    ]
    868   |5,10,12,13,16,18,19,22,25,28,31,34,37,40,43,46,49,52,55,58,70,73,
    869    76,79,82,85,88,91:
     864  |54,56:
     865    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
     866    lapply(good_program_witness program_counter' reachable_program_counter_witness)
     867    <FETCH normalize nodelta <instr normalize nodelta
     868    try(<real_instruction_refl <instr normalize nodelta) *
     869    #pc_pc_lt_hyp' #pc_tps_lt_hyp'
     870    @(transitive_le
     871      total_program_size
     872      ((S program_size') + nat_of_bitvector … program_counter')
     873      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
     874    normalize in match (S program_size' + nat_of_bitvector … program_counter');
     875    >plus_n_Sm
     876    @monotonic_le_plus_r
     877    change with (
     878      nat_of_bitvector … program_counter' <
     879        nat_of_bitvector … program_counter'')
     880    assumption
     881  |1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,
     882   55:
    870883    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    871884    lapply(good_program_witness program_counter' reachable_program_counter_witness)
    … …  
    876889    <FETCH normalize nodelta whd in match ltb; normalize nodelta
    877890    >(le_to_leb_true … program_counter_lt') %
    878   |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,
    879    92:
     891  |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,
     892   56:
    880893    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    881894    lapply(good_program_witness program_counter' reachable_program_counter_witness)
    … …  
    894907        nat_of_bitvector … program_counter'')
    895908    assumption
    896   |95,98:
    897     cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    898     lapply(good_program_witness program_counter' reachable_program_counter_witness)
    899     <FETCH normalize nodelta <instr normalize nodelta
    900     try(<real_instruction_refl <instr normalize nodelta) *
    901     #pc_pc_lt_hyp' #pc_tps_lt_hyp'
    902     @(transitive_le
    903       total_program_size
    904       ((S program_size') + nat_of_bitvector … program_counter')
    905       (program_size' + nat_of_bitvector … program_counter'') recursive_case)
    906     normalize in match (S program_size' + nat_of_bitvector … program_counter');
    907     >plus_n_Sm
    908     @monotonic_le_plus_r
    909     change with (
    910       nat_of_bitvector … program_counter' <
    911         nat_of_bitvector … program_counter'')
    912     assumption
     909  |*:
     910    normalize nodelta
     911    cases daemon (* XXX: new goals using jump_target *)
    913912  ]
    914913qed.
    … …  
    934933  λreachable_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter.
    935934  λgood_program_witness: good_program code_memory total_program_size. ?.
    936   cases(block_cost' code_memory program_counter total_program_size total_program_size cost_labels
     935  cases(block_cost' code_memory program_counter [ ] total_program_size total_program_size cost_labels
    937936    reachable_program_counter_witness good_program_witness true ?)
    938937  [1:
Note: See TracChangeset for help on using the changeset viewer.